This post is my note for What is seminar on Lambda Calculus.

Lambda calculus was created by Alonzo Church in the 1930s, and was used by him to solve Entscheidungsproblem in 1936, which is related to Hilbert's tenth problem. In the same year, Alan Turing independently solved Entscheidungsproblem using his invention Turing machine. Shortly after, Turing realized that these two models are actually equivalent as models of computation.

In this note, I will first give the formal definition of lambda expressions. Then with the help of Python, I am going to show how to do Boolean algebra and basic arithmetic using lambda calculus, which to some extend gives an illustration that Turing machine and lambda calculus are equivalent.

Definition

Lambda calculus consists of lambda expressions and operations on them. There are three basic elements in Lambda expression:

  1. variables: x, y, z, ...
  2. symbols in abstraction: λ and .
  3. parentheses for association: ()
Definition. Lambda expression is defined inductively using the following three rules:
1. variables are lambda expressions
2. [Abstraction] if x is a variable and M is a lambda expression, then (λx.M) is also a lambda expression
3. [Application] if M, N are lambda expression, then (M N) is also a lambda expression If no confusion arises, parentheses are usually omitted. For example, (M N) is the same as MN.

The 2nd rule should be thought of definitions of functions, while the 3rd rule should be regraded as evaluations of functions. Let's look at some examples.

Example 1. λx.x

By 1st rule, x is a lambda expression, then by 2nd rule, λx.x is also a lambda expression. This expression is equivalent to the identity function: id(x)=x, which means the function that takes x as an input then gives x as an output. From this example, we should notice that 2nd rule is just a way to define a function anonymously.

Example 2. (λx.xx)y

λx.xx is a function that takes x as an input then output xx. What xx means here is ambiguous, because we have not defined what it means to put two variables together. Let's put this aside for now. A similar argument as in Example 1 can show that λx.xx is a lambda expression. Applying 3rd rule, we know (λx.xx)y is a lambda expression. But the 3rd rule is evaluations of functions, we have that (λx.xx)y is the same as yy.

In Example 2, the idea of evaluation is actually one of two important operations on lambda expression, which is called β-reduction.

Operations. There are two operations on lambda expressions. Let x, y be two variables and M be N be two lambda expressions.
1. [α-conversion] λx.M[x] → λy.M[y]: replacing all x in M by y.
2. [β-reduction] (λx.M N) → M[x:=N]: substituting x in M by N.

Example 3. Lambda expressions in Python.

(lambda x: x+x)(3)
(lambda x: x+x)('hello')

Python has a very good implementation of lambda expression. From now on, I am going to write lambda expressions in Python language. In Example 2, we do not specify what xx means. Here, we define xx to be x+x in Python. Now β-reduction allows us to deduce that 

(lambda x: x+x)(3) = 6
(lambda x: x+x)('hello') = 'hellohello'

Boolean Algebra

Boolean algebra requires Boolean values "True" and "False". In Turing machine, they are represented by 0 and 1. But we can define them to be anything, as long as they respect all Boolean operations.

T = lambda x, y: x
F = lambda x, y: y

AND = lambda x, y: x(y, F)
OR  = lambda x, y: x(T, y)
NOT = lambda x: x(F, T)

In lambda calculus, "True" is define to be a lambda expression that takes two arguments and return the first argument. On the other hand, "False" is similarly defined, but return the second argument. There are three basic operations: and, or and not in Boolean algebra. All these are defined in the above Python code.

Let's examine and operator.

  • AND(T, T) = T(T, F) = T
  • AND(T, F) = T(F, F) = F
  • AND(F, T) = F(T, F) = F
  • AND(F, F) = F(F, F) = F

This is the correct and operator! One can easily check that the above OR and NOT are the correct or and not operators.

Basic Arithmetic

What is more interesting is that we can do arithmetic using lambda calculus. First of all, let's define all natural numbers. In lambda calculus, we do this via the number of iterations: 

ZERO  = lambda f, x: x
ONE   = lambda f, x: f(x)
TWO   = lambda f, x: f(f(x))
THREE = lambda f, x: f(f(f(x)))
...

All natural numbers are lambda expressions taking two arguments, f and x, where f is some lambda expression which has one argument. The number is then encoded in the number of iterations of f on x. This number system is called Church numerals. Let's see how to define some basic arithmetic operators.

SUCC = lambda n: lambda f, x: f(n(f, x))
PLUS = lambda n, m: n(SUCC, m)
MULT = lambda n, m: lambda f, x: n(lambda x: m(f, x), x)

SUCC is a lambda expression to find the successor of a number n. According to our definition of numbers, we just need to do one more iteration of f. PLUS is addition of two numbers, which is achieved by applying SUCC n times to m. Lastly, MULT is multiplication of two numbers. Since m is a lambda expression with f iterating m times, the idea is to repeat m n times. Then f is iterated nm times.

To test these arithmetic operators, we need to convert Church numerals to standard integers. In Python, we can set f to be f(x)=x+1 with x=0, then Church numerals will be converted to integers. Putting all together, we can play with the following codes.

ZERO  = lambda f, x: x
ONE   = lambda f, x: f(x)
TWO   = lambda f, x: f(f(x))
THREE = lambda f, x: f(f(f(x)))

SUCC = lambda n: lambda f, x: f(n(f, x))
PLUS = lambda n, m: n(SUCC, m)
MULT = lambda n, m: lambda f, x: n(lambda x: m(f, x), x)
INT  = lambda n: n(lambda x: x+1, 0)

FOUR = SUCC(THREE)
FIVE = PLUS(ONE, FOUR)
SIX  = MULT(TWO, THREE)

numbers = [ZERO, ONE, TWO, THREE, FOUR, FIVE, SIX]
print map(INT, numbers)

To see more arithmetic operators implemented in lambda calculus, check out a Wikipedia article Church encoding.

what is note