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 LamCalc, there is probably better literature available about this topic.

This page is however not meant as a guide on how to use LamCalc, for that see the LamCalc interface.

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 LamCalc.

α-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 LamCalc α-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 LamCalc 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. In LamCalc this becomes (Term).AlphaEquivalent(other Term) bool

β-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 LamCalc 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).

One can apply this rule in LamCalc using (Abst).BetaReduce(sub Term) Term.

η-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.

This rule is also implemented inside of LamCalc as (Term).EtaReduce() Term.

Normal forms and reduction order

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

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 LamCalc 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.

In LamCalc this becomes (Term).WHNF() Abst

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.

When you enter a formula in the cLC (and don't use weak or wlet) the formula is reduced using normal order until there are no reductions possible or the maximum amount of reductions has been reached. This always results in a beta normal form if one exists.

This is implemented in LamCalc as (Term).NorReduce() (Term, error), after the beta normal form is reached we also apply eta reduction to get a beta-eta normal form.

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.

This is implemented in LamCalc as (Term).AorReduce() (Term, error), after the beta normal form is reached we also apply eta reduction to get a beta-eta normal form.