A Simple Lambda Calculus Evaluator - I

Recently, I wrote a very simple lambda calculus evaluator in C, with scanner and parser generated by Lex and Yacc. This series of posts introduces how to implement such a lambda calculus evaluator. This first post gives a brief introduction of the lambda calculus, including its definition and reductions, which are the essentials to the evaluation algorithms. In the second post, the concrete syntax for the lambda calculus expression and its scanner and parser are presented. The evaluation process is described in the third post. You can checkout the source code from here.

This post gives a brief introduction of lambda calculus. Most part is based on the lambda calculus page on Wikipedia. I am not going to write a formal article about lambda calculus, so only the concepts related to this evaluator are mentioned here. For more detailed information, please refer to it.

Lambda Calculus
Lambda calculus, also written as λ-calculus, is accepted as the foundation for functional programming languages. It is introduced by Alonzo Church in 1930s to model the simple semantics for computation with functions in mathematics.

Function can be considered as a black box, which accepts some inputs and sends back some output. Consider the following examples. Function increase(x) = x + 1 takes a single input, x, and returns the result by adding 1 to x. Function sum(x,y) = x + y takes two inputs, x and y, and returns the sum of them, x+y. Some ideas in lambda calculus can be introduced by make some observations of the functions.

Firstly, the function can be anonymous. That means we do not need to name the function. The function increase(x) = x + 1 can be rewritten as (x) -> x + 1.

Secondly, the name for function's argument is irrelevant. That is, choosing different names for a function makes no difference. So function (x,y) -> x + y is equivalent to (a,b) -> a + b.

Finally, any function that requires two inputs can be redefined into an equivalent function that accepts a single input, and returns another function, that in turn accepts a single input. This can be extended to three or more inputs. So function (x,y) -> x + y can be redefined as (x) -> (y) -> x + y.

The lambda calculus provides a way to model functions. Since functions can be anonymous, lambda calculus doesn't provide a means to name a function. Since the names of arguments are irrelevant, the functions with only different argument names are equivalent. Since all functions expecting more than one arguments can be transformed to equivalent functions expecting one argument, lambda calculus creates functions that accepts one single argument.

Here comes the formal definition of the lambda calculus from Wikipedia:

Lambda expressions are composed of:
    variables v₁, v₂, ..., v_n
    the abstraction symbols λ and .
    parentheses ()
The set of lambda expressions, Λ, can be defined recursively:
    1. If x is a variable, then x ∈ Λ
    2. If x is a variable and M ∈ Λ, then (λx. M) ∈ Λ
    3. If M, N ∈ Λ, then (M N) ∈ Λ
Instances of rule 2 are known as abstractions and rule 3 are known as applications.

With this definition, the before mentioned functions can be defined as (λx. x+1) and (λx. (λy. x+y)).

Reductions
Suppose we have two lambda expressions: (λx. x+1) and a. If we apply the first to the second, we will have (λx. x+1) a. According to the semantic, the result should be a+1. This is called a reduction. Actually, it is a β-reduction. There are three kinds of reduction:

• α-conversion: changing bound variables;
• β-reduction: applying functions to their arguments;
• η-conversion: which captures a notion of extensionality.

Only α-conversion and β-reduction will be covered in this post, with some other necessary terms.

Free and bound variables
Variables that only exist in the scope of a lambda abstraction are said to be bound. All others are called free. For example, y is a bould variable and x is free in expression: (λy. x + y).

The set of free variables of expression M is denoted as FV(M). It is defined by recursion as follows:

1. FV(x)    = {x}, where x is a variable
2. FV(λx.M) = FV(M) - {x}
3. FV(M N)  = FV(M) ∪ FV(N)

α-conversion
Alpha-conversion allows bound variable names to be changed. For example, alpha-conversion of (λx. x) could be (λy. y).

You need to pay attention to the "bound" word, which has extended meanings. First, when alpha-converting an abstraction, only the variables bound to the same abstraction could be changed. For example, alpha-conversion of (λx. (λx. x)) could result in (λy. (λx. x)), but not (λy. (λx. y)). Second, after alpha-conversion, the new argument variable should not be captured by a different abstraction. For example, alpha-conversion of (λx. (λy. x)) could not result in (λy. (λy. y)).

Substitution
Substitution, written as E[V := E'], is the process of replacing all free occurrences of the variable V by expression E'. It is defined by recursion as follows:

    x[x := N]        ≡ N

    y[x := N]        ≡ y, if x ≠ y

    (M1 M2)[x := N]  ≡ (M1[x := N]) (M2[x := N])

    (λy. M)[x := N]  ≡ λy. (M[x := N]), if x ≠ y and y ∉ FV(N)

The y ∉ FV(N) condition in the last rule is important. Without it, the variable y, which is free in expression N, will be bound in the result abstraction after substitution. For example, it is not correct for (λx. y)[y := x] to result in (λx. x). For this case, an alpha-conversion should be applied to the expression (λx. y) before substitution, which results in (λz. y).

β-reduction

Beta-reduction captures the idea of function application. It is defined in terms of substitution: the beta-reduction of ((λV. E) E') is E[V := E'].

All the rules defined in this section is essential to lambda calculus. And they are also the basic elements for evaluation algorithm which will be presented in part III.

Encoding Datatypes
From our mathematics knowledge of middle school, we know that functions are usually applied to numbers. However, lambda calculus doesn't have any numbers? That's true! The pure lambda calculus doesn't define any data types. But we can model some data types using this basic lambda calculus. Two data types, boolean and natural number, will be introduced in this section.

Natural Number
The most common way to define natural numbers is as follows:

    0 := (λf. (λx. x))

    1 := (λf. (λx. f x))

    2 := (λf. (λx. f (f x)))

    3 := (λf. (λx. f (f (f x))))

The natural number n is a function, which takes a function f as an argument, and apply it n times to its argument.

From the definition, we can define a successor function, which takes a number n and apply one more time of function f to it:
    SUCC := (λn. (λf. (λx. f (n f x))))

And the addition of two numbers, m and n, can be defined by apply m+n times of function f:
    PLUS := (λm. (λn. (λf. (λx. m f (n f x)))))

Boolean
The boolean values TRUE and FALSE can be defined as follows:

    TRUE   := (λx. (λy. x))

    FALSE  := (λx. (λy. y))

And some logical operators:

    AND := (λp. (λq. p q p))

    OR  := (λp. (λq. p p q))

    NOT := (λp. (λa. (λb. p b a)))

The Wikipedia page has more details about the data types, so I won't duplicated it here.

Till now, the concepts about lambda calculus that are necessary for the evaluator have been covered. In the next post, I am going to define the concrete syntax of lambda calculus and implement the scanner and parser.