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 $\lambda$-terms is defined inductively as follows:

• all variables and atomic constants are $\lambda$-terms (called atoms);
• if $M$ and $N$ are $\lambda$-terms, then $(MN)$ is a $\lambda$-term (called application);
• if $M$ is a $\lambda$-term and $x$ is a variable, then $(\lambda x.M)$ is a $\lambda$-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 $\lambda$-term (denoted $lgh$) is equal to the number of atoms in the term:

• $lgh(a)=1$ for all atoms $a$;
• $lgh(MN)=lgh(M)+lgh(N)$;
• $lgh(\lambda x.M)=1+lgh(M)$.

Occurrence

For $\lambda$-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 $(MN)$;
• if $P$ occurs in $M$ or $P$ is $x$, then $P$ occurs in $(\lambda x.M)$.

For a particular occurrence of $\lambda x.M$ in a term $P$, the occurrence of $M$ is called the scope of the occurrence of $\lambda 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 $\lambda x$ in $P$;
• bound and binding iff it is the $x$ in $\lambda x$;
• free otherwise.

$FV(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 $\lambda$-terms $M$, $N$, and variables $x$:

• $[x/x]M\equiv M$
• $x\notin FV(M)\Rightarrow [N/x]M\equiv M$
• $x\in FV(M)\Rightarrow FV([N/x]M)=FV(N)\cup (FV(M)-\{x\})$
• $lgh([y/x]M)=lgh(M)$

Bibliography

• Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.