Type Theory – The Untyped Lambda Calculus

The Untyped Lambda Calculus or the pure lambda calculus forms the computational substrate for most of the type systems.

Peter Landin observed that complex programming languages can be understood as having a tiny core with all the complex features implemented in the tiny core.

Lambda Calculus can be viewed as a simple programming language or as a mathematical object about which statements can be proved.

Everything is a function.

Definition 1 Lambda Term: It refers to any term in the lambda calculus.

Definition 2 Lambda Abstraction: Lambda terms beginning with a ${\lambda}$ are called lambda abstractions.

There are three kind of terms in the lambda calculus.

A variable {x} itself is a term.
The abstraction of a variable from a term written as ${\lambda{x.t}}$ is a term called a lambda abstraction.
The application of a term to another term is written as {t t}.

The grammar can be summarized as:

Syntax:

$\displaystyle {t} := \text{terms} \\ := {x} \thickspace \text{variable} \\ := \lambda {x.t} \thickspace \text{lambda abstraction} \\ := {t \thickspace t} \thickspace \text{application} \ \ \ \ \ (1)$

To save writing too many parenthesis the convention is that the

application associates to the left, that is, is {s t u} is {(s t) u}.
abstraction extend as far to the right as possible. For example, ${\lambda{x.} \lambda{y.x \thickspace y \thickspace x}}$ is ${\lambda{x.(} \lambda{y.(x \thickspace y) \thickspace x)}}$ .

1. Scope

A variable is said to be bound when it occurs in the body {t} of an abstraction ${\lambda{x.t}}$ .

A variable is said to be free if it is not bound by enclosing abstraction on {x}

An abstraction with no free variables is said to be closed or a combinator.

2. Operational Semantics

In its pure form, lambda calculus has no mechanism for computation except function application, functions are applied to arguments which are themselves functions. Each step in computation is rewriting an application by replacing the value of the bound variable of the lambda abstraction with the argument given on the right side of the application.

$\displaystyle (\lambda x.{t}_{12}){t}_2 \rightarrow [{x} \thickspace \rightarrow \thickspace {t}_2] {t}_{12} \ \ \ \ \ (2)$

There can be many different evaluation strategies.

Full-beta Reduction: Any redex may be reduced at any time.

$\displaystyle (\lambda x.x)((\lambda x.x)(\lambda z.(\lambda x.x) \thickspace z)) \ \ \ \ \ (3)$

Normal Order Strategy: The outermost redex is reduced first. It is a partial function and each evaluation gives a unique term.

Call by Name: In addition to the outermost redex being reduced first, no evaluation is allowed inside abstractions.

Call by Need: A reduction relation on abstract syntax graph, instead of abstract syntax trees.

Call by Value:

3. Multiple Arguments

$\displaystyle \lambda (x \thickspace y).s = \lambda x. \thickspace \lambda y. \thickspace s \ \ \ \ \ (4)$

4. Church Booleans

$\displaystyle {tru} \thickspace = \lambda {t.} \thickspace \lambda {f.} {t} \\ {fls} = \lambda {t.} \lambda {f.} {f} \\ {test} = \lambda {l.} \lambda {m.} \lambda {n.} {l m n} \\ {test \thickspace b \thickspace v \thickspace u} = {b \thickspace v \thickspace u} \\ {and} = \lambda {b.} \lambda {c.} {b \thickspace c \thickspace fls} \ \ \ \ \ (5)$

5. Pairs

$\displaystyle {pair} = \lambda {f.} \lambda {s.} \lambda {b.} {b \thickspace f \thickspace s} \\ {fst} = \lambda {p.} {p \thickspace tru} \\ {snd} = \lambda {p.} {p \thickspace fls} \\ {fst \thickspace (pair \thickspace v \thickspace w)} = (\lambda {p.} {p \thickspace tru})((\lambda {f.} \lambda {s.} \lambda {b.} {b \thickspace f \thickspace s}) { v \thickspace w}) \\ = (\lambda {p.} {p \thickspace tru})((\lambda {s.} \lambda {b.} {b \thickspace v \thickspace s}) { w}) \\ = (\lambda {p.} {p \thickspace tru})(\lambda {b.} {b \thickspace v \thickspace w}) \\ = (\lambda {b.} {b v w}) { tru} \\ = ({tru \thickspace v \thickspace w}) \\ = {v} \ \ \ \ \ (6)$

6. Church Numerals

$\displaystyle {c}_0 = \lambda {s.} \lambda {z.} {z} \\ {c}_1 = \lambda {s.} \lambda {z.} {s \thickspace z} \\ {c}_2 = \lambda {s.} \lambda {z.} {s \thickspace (s \thickspace z)} \\ {c}_3 = \lambda {s.} \lambda {z.} {s \thickspace (s \thickspace (s \thickspace z))} \\ {scc} = \lambda {n.} \lambda {s.} \lambda {z.} {s \thickspace (n \thickspace s \thickspace z)}. \ \ \ \ \ (7)$

A number n is encoded by the action of applying a function s to z n times.

7. Recursion

$\displaystyle {omega} = (\lambda {x.} {x \thickspace x})(\lambda {x.} {x \thickspace x}) \\ {fix} = \lambda {f.} ( \lambda {x.} {f} ( \lambda {y.} {x \thickspace x \thickspace y} ) ) ( \lambda {x.} {f} ( \lambda {y.} {x \thickspace x \thickspace y} ) ) \ \ \ \ \ (8)$

$\displaystyle {factorial} = {body \thickspace containing \thickspace factorial} \\ {g} = \lambda {fct.body \thickspace containing \thickspace fct} \\ {g} = \lambda {fct.(}\lambda {n.if \thickspace (cnd) \thickspace then \thickspace (c1) \thickspace else \thickspace (times \thickspace n \thickspace (fct \thickspace (prd \thickspace n))))} \\ {factorial} = {fix \thickspace g} \\ {h1} = \lambda {x.g(}\lambda {y.x \thickspace x \thickspace y)} \\ {fct} = \lambda {y.h1 \thickspace h1 \thickspace y} \\ {factorial c_3} = {fix \thickspace g \thickspace c}_3 \\ = {h1 \thickspace h1 \thickspace g \thickspace c_3 } \ \ \ \ \ (9)$

factorial = fix (lambda fct. body containing fct)

8. Formalities

Definition 3 The set of terms is the smallest set such that

If ${x \in \mathcal{V}}$ , then ${x \in \mathcal{T}}$ .
If elements ${x, t \in \mathcal{T}}$ , then ${\lambda {x.t} \in \mathcal{T}}$ .
If ${{u, v} \in \mathcal{T}}$ , then ${{u v} \in \mathcal{T}}$ .

Definition 4 The set of free variables of a term {t}, written as ${FV(t)}$ is defined as the set

${FV(x) = x}$
${FV(\lambda x.t) = FV(t) \textbackslash x}$
${FV(t_1 t_2) = FV(t_1) \cup FV(t_2)}$ .

Definition 5 Substituiton:

$\displaystyle (x \mapsto s)x = x \ \ \ \ \ (10)$

$\displaystyle (x \mapsto s)y = y y \neq x \ \ \ \ \ (11)$

$\displaystyle (x \mapsto s)(\lambda y.t) = (\lambda y.(x \mapsto s)t) y \neq x, y \notin FV(s) \ \ \ \ \ (12)$

$\displaystyle (x \mapsto s)(t_1 \thinspace t_2) = ((x \mapsto s)t_1 \thinspace (x \mapsto s)t_2) \ \ \ \ \ (13)$

Syntax:

$\displaystyle {t} := \thickspace \text{terms} \\ := {x} \thickspace \text{variable} \\ := \lambda {x.t} \thickspace \text{lambda abstraction} \\ := {t \thickspace t} \thickspace \text{application} \\ {v} := \thickspace \text{values} \\ := \lambda{x.t} \thickspace \text{variable} \\ \ \ \ \ \ (14)$

Evaluation:

$\displaystyle \frac{ t_1 \thickspace \rightarrow \thickspace t'_1 }{ t_1\thinspace t_2 \rightarrow t'_1\thinspace t_2 } \text{E-App1} \\ \frac{ t_2 \rightarrow t'_2 }{ v_1\thinspace t_2 \rightarrow v_1\thinspace t'_2 } \text{E-App2} \\ (\lambda x.t_1)\thinspace v_2 \rightarrow [x \mapsto v_2]t_1 \text{E-AppAbs} \ \ \ \ \ (15)$