β-reduction

Overview

Any term of form $(λ x . M) N$ is called a $β$ -redex. The corresponding term $[N / x] M$ is its contractum. If and only if a term $P$ contains an occurrence of $(λ x . M) N$ and we replace that occurrence by $[N / x] M$ , and the result is $P^{'}$ , we say we have contracted the redex-occurrence in $P$ , and $P$ $β$ -contracts to $P^{'}$ or $P ▹_{1 β} P^{'}$ .

If and only if $P$ can be changed to a term $Q$ by a finite series of $β$ -contractions and changes of bound variables, we say $P$ $β$ -reduces to $Q$ , or $P ▹_{β} Q$ .

Substitution is well-defined with respect to $β$ -reduction. That is, if $M ▹_{β} M^{'}$ and $N ▹_{β} N^{'}$ , then $[N / x] M ▹_{β} [N^{'} / x] M^{'}$

Normal Form

A term $Q$ which contains no $β$ -redexes is called a $β$ -normal form (or a term in $β$ -normal form or just a $β -nf$ ). The class of all $β$ -normal forms is called $β -nf$ or $λ β -nf$ . If a term $P$ $β$ -reduces to a term $Q$ in $β -nf$ , then $Q$ is called a $β$ -normal form of $P$ .

As an alternative characterization, the class $β -nf$ is the smallest class such that

all atoms are in $β -nf$ ;
$M, N \in β -nf \Rightarrow a MN \in β -nf$ for all atoms $a$ ;
$M \in β -nf \Rightarrow λ x . M \in β -nf$

β-equality

We say $P$ is $β$ -equal or $β$ -convertible to $Q$ ( $P =_{β} Q$ ) iff $Q$ can be obtained from $P$ by a finite series of $β$ -contractions, reversed $β$ -contractions, and changes of bound variables. That is, $P =_{β} Q$ iff there exist $P_{0}, \dots, P_{n}$ ( $n \geq 0$ ) such that $P_{0} \equiv P$ , $P_{n} \equiv Q$ , and $\forall i \leq n - 1, (P_{i} ▹_{1 β} P_{i + 1}) \lor (P_{i + 1} ▹_{1 β} P_{i}) \lor (P_{i} \equiv_{α} P_{i + 1}) .$

Church-Rosser Theorem

If $P ▹_{β} M$ and $P ▹_{β} N$ , then there exists a term $T$ such that $M ▹_{β} T$ and $N ▹_{β} T$ . As an immediate corollary, if $P$ has a $β$ -normal form then it it is unique modulo $\equiv_{α}$ .

Likewise, if $P =_{β} Q$ , then there exists a term $T$ such that $P ▹_{β} T$ and $Q ▹_{β} T$ .

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.

My Notebook

Explorer