#The Lambda Calculus

###Factoid:

###Length 1:

###Length 3:

###Length 4:

###Length 4:

###Length 5:

###Length 7:

###Length 7:

###Length 7:

###Length 8:

###Length 9:

###Length 14:

###Length 12:

###Length 12:

###Length 18:

###Length 30

The Lambda Calculus

Factoid:

Length 1:

Length 3:

Length 4:

Length 4:

Length 5:

Length 7:

Length 7:

Length 7:

Length 8:

Length 9:

Length 14:

Length 12:

Length 12:

Length 18:

Length 30

###Factiod:

###Factoid:

Ooh, something exciting! This looks like the Church numeral for zero, but with f x in place of x. Here, the function f is applied once to x, and this result is returned. We'll call this the Church numeral for one. Noticing a pattern? Yep, the Church numeral for n returns a function of x that returns f applied to x n times.

Here's an example: let's call this function on 1's Church numeral, λf.λx.f x. This gives us (λn.λf.λx.f (n f x))(λf.λx.f x), which is by α-conversion equivalent to (λn.λf.λx.f (n f x))(λg.λy.g y) (this is done to avoid name collisions). β-reduction turns this into λf.λx.f ((λg.λy.g y) f x).

Another look at the successor function reveals that it is quite intuitive: it takes a Church numeral n and returns another Church numeral, one that returns a function f applied to n applications of f to x—that is, n+1 applications of f to x.

Ooh, something exciting! This looks like the Church numeral for zero, but with f x in place of x. Here, the function f is applied once to x, and this result is returned. We'll call this the Church numeral for one. Noticing a pattern? Yep, the Church numeral for n returns a function of x that returns f applied to xn times.

Here's an example: let's call this function on 1's Church numeral, λf.λx.f x. This gives us (λn.λf.λx.f (n f x))(λf.λx.f x), which is by α-conversion equivalent to (λn.λf.λx.f (n f x))(λg.λy.g y) (this is done to avoid name collisions). β-reduction turns this into λf.λx.f ((λg.λy.g y) f x).

Another look at the successor function reveals that it is quite intuitive: it takes a Church numeral n and returns another Church numeral, one that returns a function f applied to n applications of f to x—that is, n+1 applications of f to x.

###Length 30

λa.λb.a (λn.λf.λx.f (n f x)) b

Spamming successor functions gets tedious. Let's skip all that and define addition! This snippet takes two Church numerals a and b and returns their sum, as a Church numeral.

Of course, we must test this. Note that the outer parentheses contain the successor function exactly; since we already understand that one, let's just call it SUCC now. Our expression becomes λa.λb.a SUCC b.

Let's add two and three (defining TWO as λf.λx.f (f x) and THREE as SUCC TWO). (λa.λb.a SUCC b) TWO THREE is β-reduced to (λb.TWO SUCC b) THREE and again to TWO SUCC THREE. This does PRECISELY what we'd hoped—it applies succession to three two times, yielding two plus three!