Lambda Calculus

The calculus, invented by Alonzo Church, is, essentially, one of the simplest formal “programming” languages. It has a simple syntax and semantics for how programs are evaluated.

Syntax

Let us first consider the untyped calculus containing variables, atoms¹, abstractions and applications. The syntax of terms e in the the untyped calculus is shown here:

e ::= v      > variables like x, y and z
   |  a      > atoms like 1, 2, True, +, *
   |  λv.e   > function abstraction, such as def f(v): return e
   |  e e'   > function call a.k.a function application such as e(e')

Part of the motivation for this new language is for expressing higher-order functions. For example, if we wanted to define a function like:

def add(x):
    def g(y):
        return x + y
    return g

Doing so mathematically might be a little clumsy. Instead, with the calculus, we can write it like so:

Just like in Python, the scope of a abstraction extends as far to the right as possible, so the function above should be read as:

We show the correspondence between terms in the calculus with lambda expressions in Python:

term	Python Expression
	lambda x: x + 1
	lambda x: lambda y: x(y)
	(lambda x: 2 * x)(y)

Function applications are left-associative, therefore should be read as , and in Python, e1(e2)(e3) should be read as (e1(e2))(e3).

Semantics

To begin describing how calculus executes a program (which is really just a term), we first distinguish between free and bound variables in a term.

Definition 1 (Free Variable).

A variable in a term is

• bound if it is in the scope of a in
• free otherwise

Then, the functions and produce the bound and free variables of a term respectively. For example, .

Now we want to be able to perform substitutions of variables with terms. For example, when we have an application of the form , what we want is for to be substituted with in , just like the following function in Python:

def f(x): return x + 1
f(2) # becomes 2 + 1 which is 3, because we substituted x with 2

However, this is not straightforward because we may introduce name clashes. For example, if we had , performing a function call with naive substitution gives us which is wrong, because now the free variable is substituted with the bound variable , so the meaning is not preserved. As such, we define substitutions on terms keeping this in mind.

Definition 2 (Substitution).

is the substitution of all free occurrences of in with , changing the names of bound variables to avoid name clashes. Substitution is defined by the following rules:

2. where is an atom
4. since is not free
5. if
6. if and
7. if and

Example 3 (Substitution).

We give some example applications of each rule:

7. (rename to before performing substitution)

The last rule of Definition 2 where variables are renamed to avoid name clashes introduces a form of equivalence known as congruence. It captures the idea that renaming parameters in functions does not change its meaning. For example, the two functions below are, in operation, identical:

def f(x):
    return x + 1
def f(y):
    return y + 1

In other words, if two terms differ only in the name of the bound variables, they are said to be congruent.

Finally, we get to the actual semantics of calculus, which is described by reduction. Essentially it is as we have briefly described earlier—a function application (lambda x: e1)(e2), evaluates to e1 where x is substituted with e2:

For example:

This is more-or-less how Python evaluates function calls:

Python interactive session (lambda expressions)

>>> (lambda x: lambda y: x(y))(lambda x: x + 1)(2)
3

Typed Variants

Python has types, which describes the class from which an object was instantiated:

Python interactive session (types)

>>> type(1)
<class 'int'>
>>> type(1.0)
<class 'float'>

We will describe more on types in Chapter 2 (Types). But for now, know that we can also assign types to terms in the calculus, giving us new forms of calculi. The simplest type system we can add to the calculus is, well, simple types, forming the simply-typed calculus.

For now, we shall restrict types to be the base types to only include int, giving us a new language for the calculus:

Terms
e ::= v         > variables like x, y and z
   |  a         > atoms like 1, 2, +, *
   |  λv: t.e   > function abstraction, such as def f(v: t): return e
   |  e e'      > function call a.k.a function application such as e(e')

Types
t ::= int         > base type constants, only including integers
   |  t -> t'     > type of functions; -> is right-associative

The introduction of types to the calculus now adds the notion of well-typedness to the language. Specifically, not all terms in the untyped calculus are well-typed in the simply typed calculus. To formalize this notion of well-typedness, we define typing rules that dictate when a term is well-typed, and what type a term has.

First we have typing environments which are sets (or sometimes lists) of typing assumptions of the form , stating that we are assuming that has type . Then, the typing relation states that in the context , the term has type . The reason we need typing environments is so that the types of in-scope bound variables in terms are captured and can be used in the derivation of the types of terms. Instances of typing relations are known as typing judgements.

The validity of a typing judgement is shown by providing a typing derivation that is constructed using typing rules, which are inference rules:

Which basically states that if all the statements are valid, then the statement is also valid.

Then, the simply-typed calculus uses the following rules.

1. If a variable has type in then in the context , has type

2. If an atom has type then we can also judge the type of accordingly

3. Abstraction: If in a certain context we can assume that has type to conclude has type , then the same context without this assumption shows that has type

4. Application: If in a certain context has type and has type , then has type

These rules can be used to perform type checking (the procedure of checking the well-typedness of a term) or type reconstruction (the procedure of finding the types of terms where their typing information is not present, as is the case in the untyped calculus).

For example, in our calculus we can show that has type and is therefore a well-typed term:

That means the following lambda expression in Python (assuming only int exists as a base type) will have the same type:

Python interactive session (types and lambda expressions)

>>> f = lambda x: lambda y: x(y) # (int -> int) -> int -> int
>>> my_fn = lambda x: x + 1 # int -> int
# f(my_fn): int -> int
# f(my_fn)(3): int
>>> f(my_fn)(3) # int
4
>>> type(f(my_fn)(3))
class <'int'>

---

Footnotes

1. The actual untyped calculus does not have atoms like numbers, booleans etc. However, for simplicity’s sake we shall include them in the language. The version we present is frequently termed the applied calculus, in contrast with usual presentations known as the pure calculus which omits atoms. ↩