λx.x
denotes the identity function in the sense that ((λx.x) E) = E
for any lambda expression E
.
λn.(add n 1)
denotes the successor function on the integers so that ((λn.(add n 1)) 5) = 6
.
(λf.(λx.(f (f x))))
describes a function with two arguments, a function and a value, that applies the function to the value twice.
If sqr
is the (predefined) integer function that squares its argument, then
( ( ( λf . ( λx . ( f ( f x ) ) ) ) sqr ) 3 ) = ( ( λx . ( sqr ( sqr x ) ) ) 3 ) = ( sqr ( sqr 3 ) ) = ( sqr 9 ) = 81Here
f
is replaced by sqr
and then x
by 3.
E1 E2 E3 means ( ( E1 E2 ) E3 )
λ<variable>
“ in an abstraction extends as far to the right as possible.
λx.E1 E2 E3 means (λx.(E1 E2 E3)) and not ((λx.E1 E2) E3)