Short introduction to lambda calculus

The following tries to be a short introduction on lambda calculus, however the focus is mostly on the details which were important to its implementation in the cLC, there is probably better literature available about this topic.

Basic operations of the lambda calculus

We do not provide the entire formal definition of the axioms nor the lambda calculus itself, however the text here should be able to give you a grasp for what is happening in the background of the cLC.

α-conversion

Informally this come down to: the naming doesn't matter.

Formally one writes: (λx.M[x]) = (λy.M[y]) for any variable y which is not bound in M.

For example λx.x is α-equivalent to λy.y.

Inside of the cLC α-conversion is never needed as we use (slightly modified) De Bruijn indexes, which means that a variable is represented as a number, this number is equal to the amount of abstractions between the variable and its binding abstraction. Traditionally De Bruijn indexes start counting at 1 (thus 1 means that the variable is bound by the current abstraction) however inside of the cLC we start counting at 0 to use the full range of unsigned integers.

De Bruijn indexes make α-conversion unnecessary as α-equivalence comes down to syntactic equivalence.

β-reduction

Also known as abstraction application. We substitute the bound variable by the term right after the lambda abstraction (application is left associative).

Formally: ((λx.M) E) -> (M[x := E])

Internally in the cLC application means exactly the same, however we do have to heighten and lower the De Bruijn indexes where needed and keep track of which index has to be replaced (eg. when replacing inside of a contained abstraction we have to replace the index one higher).

η-conversion

This is one extra reduction rule which isn't included inside of β-reduction. When we have an abstraction of the form: λx.M x, where x does not appear as a free variable inside of M, the abstraction is equivalent to M.

Normal forms and reduction order

In this section we're only going to discuss the normal forms and reduction strategies used in the cLC.

Beta-eta normal form

A lambda term is in beta-eta normal form if beta nor eta reduction is possible. When one of the reduction functions in the cLC is successful the result will be a beta-eta normal form.

Weak head normal form

A WHNF is when the entire formula is encapsulated inside of one lambda abstraction.

For a lambda abstraction this means doing nothing. When dealing with a lambda expression one applies the reverse of η-conversion.

Normal order reduction

Normal order reduction is when we try application left to right, when there aren't any more expansions possible, we start to expand inside of lambda abstractions.

This always results in a beta normal form if one exists.

Applicative order reduction

Here we do (mostly) the opposite of normal order reduction, we first expand the expression being applied instead of doing the application to begin with.

This is usually faster than normal order, however, unlike normal order, we do not always reach a beta normal form.

Reduction in the cLC

When you enter a formula in the cLC (and don't use weak or wlet) the formula is concurrently reduced using normal order and applicative order until either of them reach beta normal form or the user interrupts the calculation. After we reach a beta normal form we apply eta reduction to get to a beta-eta normal form.