Lambda Calculus

1. Syntax

-calculus is the simplest programming language:

1.1 Free & Bound Variables

• Free variables are those not bound by an abstraction.
• Bound variables are those bound by an abstraction.

For example, in the following expressions, bound variables are and free variables are :

• (contraction)

Terms which have no free variables are called closed terms. More formally, free variables are:

1.2 Substitution

For -equivalence, we can rename bound variables without changing the meaning of the term. For example, is -equivalent to . So, we check:

• Are the terms of the same structure?
• Do all of the free variables match?
• Can you rename the bound variables such that they match?

Formally, substitution is written as where is replaced by in . For example:

Or, more formally:

2. -Reduction

-reduction is the process of applying a function to an argument. For example, reduces to . More formally , where is the function and is the argument. In this example, is the function, is the argument. The result is obtained by replacing every occurence of the function parameter , with the argument , in the function body . Some rules for -reduction are:

An example of -reduction is shown below.

2.2 Normal Forms

A normal form is a term that cannot be reduced further. Critically, any term that has a normal form will eventually reach it. From the example above, we can see that sometimes, there are many different "pathways", or sequences of -reductions that can take place. However, no matter which pathway is chosen, the term will always reach the same normal form.

We call this pathway a multi-step--reduction, or . This multi-step reduction enforces the reflexive transitive closure of -reduction under -conversion:

• Reflexivity:
• Transitivity:

Confluence states that . Or, visually:

-terms are -normal if they contain no redexes:

Normal forms are unique, i.e. . We can prove this using confluence.

-equivalence is the smallest equivalence relation that contains , or with symmetry. . Any two of the terms below are -equivalent:

2.3 Reduction Strategies

A redex means a reducible expression. For example, is a redex.

Not all -terms have a normal form. For example, has no normal form. The order of reduction also matters - some terms only have a normal form under certain reduction strategies.

Take a redex :

• A redex that is in or is inside the redex .
• The redex is outside any redex in or .
• A redex is outermost if there are no redexes outside it.
• A redex is innermost if there are no redexes inside it.

This provides a way to define many different reduction strategies:

• Normal Order - reduces the leftmost, outermost redex first. This always terminates at a normal form if a normal form exists. Can perform computations in unevaluated function bodies, and is hence not used in programming languages.
• Call by Name - reduces the leftmost, outermost redex first, but does not reduce inside abstractions. Does not always reduce to a normal form. Evaluates arguments only when needed. Used by Haskell, R, and .
• Call by Value - reduces the leftmost, innermost redex first, but does not reduce inside abstractions. Does not always reduce to a normal form. Evaluates arguments before passing into a function body. Used by C, Java, and Python.

3. Definability

A partial function is -definable iff there exists a closed -term with the following properties:

• .
• .

The Church-Turing Thesis states that a function is computable iff it is -definable. If a function is lambda-computable, it is also register-machine computable and Turing-machine computable, and vice versa.

3.1 Church Numerals

Church numerals are defined as .

To encode addition, we need a function . To do this, we must obtain the body of (), put it into the body of (), and then abstract over and : . Hence:

More encodings can be found for multiplication, exponentiation, if zero, and more:

3.2 Recursion

IKSTCVBB'W

Combinators are -terms with no free variables:

It is possible to define any computable function with just S, K, I and application, getting rid of the -abstraction. This is called the SKI combinator calculus.

Recursion can be easily defined with calculus. For example, the fact function:

However, we can also rewrite fact as . This means that fact is a fixpoint of . To help with this, we can define the famous Y-combinator:

This is important because step of -reduction leads to , which is the fixpoint equation. is the fixpoint operator. So: