Math and science::Theory of Computation::Lambda calculus

β-reduction

Beta reduction is a term that encompasses 3 relations defined over the set of all lambda terms: single-step, multi-step and equality.

β-reduction, single step, $\to_{β}$

Let $M, U$ and $L$ be lambda terms.

The following 2 rules define the true entries of the single step beta reduction relation.

Basis

(λ . M) U \to_{β} M [x := U]

Compatibility

M \to_{β} U

, then:

$M L \to_{β} U L$
[ $? \to_{β} ?$ ]
[ $? \to_{β} ?$ ]

the syntax $[x := U]$ refers to the lambda terms that results from substituting all occurrences of the unbound variable $x$ by the term $U$ . This syntax in some sense requires some "work".

There are names given to parts of the above definition:

[What1?] and [what2?]

If a subterm of a lambda expression matches the left-hand side of the basis rule above, it is called a [ what1? ]. This name comes from from reducible expression. The subterm on the right-hand side, $M [x := U]$ , is called the [ what2? ] of the [what1].

Multi-step reduction extends the single step relation by augmenting it with reflexivity and transitivity. Before we get to multi-step reduction, we describe the following definition:

Reduction sequence (personal definition)

A reduction sequence is a sequence of lambda terms $(W_{n})_{n = 0}^{N}$ such that for every $n \in N, n < N$ , we have $W_{n} \to_{β} W_{n + 1}$ . The sequences starts at $W_{0}$ and ends at $W_{N}$ .

β-reduction, multi-step, $↠_{β}$

Let $M$ and $U$ be lambda terms.

$M$ reduces through multi-step β-reduction to $U$ iff [...].

Note: the possibility of $n = 0$ for multi-step reduction is what introduces the quality of reflexivity to the relation.

For multi-step β-reduction, it is possible for $M \to_{β} U$ to be true while $U \to_{β} M$ is false. Below, we extend the multi-step β-reduction with symmetry and arrive at β-equality, an equivalence relation. First, another assisting definition.

Bi-directional reduction sequence (personal definition)

A bi-directional reduction sequence is a sequence of lambda terms $(W_{n})_{n = 0}^{N}$ such that for every $n \in N, n < N$ either $W_{n} \to_{β} W_{n + 1}$ or $W_{n + 1} \to_{β} W_{n}$ .

β-equality, $=_{β}$

Let $M$ and $U$ be lambda terms.

$M$ and $U$ are said to be β-equal iff [...].

β-convertable is sometimes said instead of β-equal.

23.07.2021