Lambda

The lambda calculus distills the essence of computing. Every function that can be calculated is a \lambda-expression: a variable, an abstraction, or an application.

A variable is just a symbol. An abstraction is (x\Rightarrow E) where x is a variable and E is an expression. Application is (EF) where E and F are expressions. The standard notation for x\Rightarrow E is \lambda x.E.

Expressions can be converted to equivalent expressions by renaming and replacing. The abstraction x\Rightarrow E[x] where E is an expression involving the variable x can be \alpha-converted to y\Rightarrow E[y] renaming all (free) occurences of x in E as y. The application (x\Rightarrow E)F can be \beta-reduced to E[x\Leftarrow F] where all (free) occurences of x in E are replace by F. The standard notation for E[x\Leftarrow F] is E[x:=F].

For example, since the variable x is also an expression, the abstraction x\Rightarrow x is an expression. By \alpha-conversion we can write this as y\Rightarrow y for any variable y. By \beta-reduction (x\Rightarrow x)E is equivalent to E for any expression E, so x\Rightarrow x is the identity function.

Variables in an expression can be either bound or free. For an abstraction x\Rightarrow E we say all free occurences of x in E are bound. A variable is free if it is not bound. In the abstraction x\Rightarrow xy the variable x is bound and y is free. If we apply (x\Rightarrow xy)x we would get xx if we did not require x to be free. We must first \alpha-convert/rename x\Rightarrow xy to, e.g., z\Rightarrow zy to apply (z\Rightarrow zy)x and \beta-reduce/replace to get the correct result xy.

True is the expression t = x\Rightarrow y\Rightarrow x = x\Rightarrow(y\Rightarrow x) and false is f = x\Rightarrow y\Rightarrow y = x\Rightarrow(y\Rightarrow y). We assume abstraction is right-to-left associative to reduce the number of parentheses. Note t E F = E and f E F = F for any expression E and F.

The natural number 0 is x\Rightarrow y\Rightarrow y, which is the same as f. Successive numbers are defined by 1 = x\Rightarrow y\Rightarrow xy, 2 = x\Rightarrow y\Rightarrow xxy, …, n = x\Rightarrow y\Rightarrow x\ldots xy where x\ldots x is n x’s. This is not unlike how cavehumans may have counted by making marks on clay tablets equal to the count. We have advanced to using chips made of sand that can move electrons to do the same.

Let x^n = x\ldots x be n x’s. Clearly x^{n + 1} is xx^n but this is not a lambda expression since the \{}^ is not defined using the lambda calculus. Define s = n\Rightarrow x\Rightarrow y\Rightarrow y n x y to be the successor of n. We have \begin{aligned} s\ 0 &= (n\Rightarrow(x\Rightarrow(y\Rightarrow y n x y)))0 \\ &= (x\Rightarrow(y\Rightarrow(y\Rightarrow y 0 x y))) \\ \end{aligned}