Lambda Calculus, Lambda Abstraction

Lambda Abstraction is the way we define an anonymous function in λ calculus. Suppose we have a function like f(x) = 2x which in fact is a function that maps any x to 2x, now from the previous posts we already knew that in λ calculus the expression 2x (which is a term) can be shown as * 2 x, but the way we show this as an anonymous function is like:

λx. * 2 x

See there is no equality sign, here λx is something anonymously like f(x) and the dot after it shows the start of the evaluation formula. So a familiar C or Java-like function like the following:

int doubleIt(int x) {
  return 2 * x
}

Will be something like the following in Lisp-like language for example (which you can use it inline of course):



(lambda (x) (∗ 2 x))

The above is nothing but what we already talked about it: λx. * 2 x

Just one parameter
Any lambda abstraction can contain only one input parameter, so in general, an abstraction is something like:

λx. t

In which t is any valid lambda expression or simply a term. Here are some more examples:

1. λx. + x 5
2. λx. * 2 * x x
3. λx. + x y

Bound and free variables
Note in the third example y is just an unknown variable for the function, this variable is called free variable while the x is called bound variable. The function gets x and adds y to it. Since we can have abstractions in some part of an anonymous function itself so the third example can be written in the following form to have the meaning we usually like to give it to:

λy.t , t = + x y => λy.λx. + x y 

Or simply as nested abstraction like:

λyx. + x y

In Lisp we write it like:

(lambda (x y) (+ x y))