λ-Calculus

Overview

Assume that there is given an infinite sequence of expressions called variables and a finite or infinite sequence of expressions called atomic constants, different from the variables. The set of expressions called $λ$ -terms is defined inductively as follows:

all variables and atomic constants are $λ$ -terms (called atoms);
if $M$ and $N$ are $λ$ -terms, then $(M N)$ is a $λ$ -term (called application);
if $M$ is a $λ$ -term and $x$ is a variable, then $(λ x . M)$ is a $λ$ -term (called abstraction).

If the sequence of atomic constants is empty, the system is called pure. Otherwise it is called applied.

Syntactic Identity

Syntactic identity of terms is denoted by " $\equiv$ ".

Length

The length of a $λ$ -term (denoted $l g h$ ) is equal to the number of atoms in the term:

$l g h (a) = 1$ for all atoms $a$ ;
$l g h (M N) = l g h (M) + l g h (N)$ ;
$l g h (λ x . M) = 1 + l g h (M)$ .

Occurrence

For $λ$ -terms $P$ and $Q$ , the relation $P$ occurs in $Q$ is defined by induction on $Q$ as:

$P$ occurs in $P$ ;
if $P$ occurs in $M$ or in $N$ , then $P$ occurs in $(M N)$ ;
if $P$ occurs in $M$ or $P$ is $x$ , then $P$ occurs in $(λ x . M)$ .

For a particular occurrence of $λ x . M$ in a term $P$ , the occurrence of $M$ is called the scope of the occurrence of $λ x$ .

Free and Bound Variables

An occurrence of a variable $x$ in a term $P$ is called

bound if it is in the scope of a $λ x$ in $P$ ;
bound and binding iff it is the $x$ in $λ x$ ;
free otherwise.

$F V (P)$ denotes the set of all free variables of $P$ . A closed term is a term without any free variables.

Substitution

For any $M$ , $N$ , and $x$ , define $[N / x] M$ to be the result of substituting $N$ for every free occurrence of $x$ in $M$ , and changing bound variables to avoid clashes.

For all $λ$ -terms $M$ , $N$ , and variables $x$ :

$[x / x] M \equiv M$
$x \notin F V (M) ⟹ [N / x] M \equiv M$
$x \in F V (M) ⟹ F V ([N / x] M) = F V (N) \cup (F V (M) - {x})$
$l g h ([y / x] M) = l g h (M)$