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

Title: Lamba terms. Definition.
λ-terms are the elementary objects of λ-calculus. Below, they are defined first in the traditional way (as sequences) and then as trees.
λ-terms. Defined as sequences.
First, assume the existence of an infinite sequence of term-variables. Term-variables are denoted using "u", "v", "w", "x", "y", "z", with optional subscripts. The set of λ-terms is then inductively defined as follows:
1. each term-variable is a λ-term, called an atomic term;
2. if \( M \) and \( N \) are λ-terms, then \( (MN) \) is a λ-term, called an application;
3. if \( x \) is a term-variable and \( M \) is a λ-term, then \( (\lambda x.\ M )\) is a λ-term, called a λ-abstract.
A composite λ-term is a λ-term that is not an atomic term.
This definition raises some questions. See the reverse for more details, including an alternative.
The above definition treats λ-terms as sequences (one element following another) in a 1D sense, like a sequence of integers. However, a more natural model for λ-terms is that of a tree. The next definition tries to capture this idea.
λ-terms. Defined as trees.
A lambda term is a tree where:
- Nodes may have 0, 1 or 2 children.
- Every 0-child node has a mapping to an ancestor 1-child node.
0-child nodes are called leaf nodes, 1-child nodes are called abstraction nodes, and 2-child nodes are called application nodes.
The reverse side has visualization for the trees. Can you remember them?
This definition is not exactly formal. For example, what is a tree? What are nodes? However, at least these deficiency's are not hidden, like how the reliance on the meaning of character sequences from an alphabet of variable-symbols seems to be hidden in the first definition.
Free nodes?
This definition doesn't allow non-closed terms. The reverse side has an alternative definition that tries to address this second point. Can you remember how it's done?
BackOnlyText: Remarks on the traditional definition
This definition raises some questions.
- can we just assert the existence of an infinite sequence of "variables"? This is like saying "let there be a function from the natural numbers to the set of "variables". Which avoids actually defining the set of variables, and implicitly assumes the definition of a lot of math, such as natural numbers, sequences and cardinality (what else?). It makes the sequence of variables countable, yet the set of variables either finite, countable or uncountable; however, it seems like countable is what is trying to be implied here.
- The second point blurs the line between objects an notation. Are \( M \) and \( N \) labels for set elements, and is \( (MN) \) another label for a set element? What is equality between set elements? No, this is too troublesome. I think \( M \) is meta-notation (what's the right term?) to act as a placeholder in a sequence, and \( (MN) \) is literally a sequence "(", "M", "N", ")", where M and N are in some sense allowed to vary over the set of variables.
Alternative sequence definition
Below is an alternative definition, which I feel has stronger footing. It exists in context of alphabets, languages, grammars etc.
λ-terms. Defined with grammars.
Let \( V \) be a (in)finite (can it be countably infinite?) alphabet. Then the set of λ-terms are those defined by the grammar:
\[ \Lambda = V|(\Lambda \Lambda)|(\lambda V .\ \Lambda )\]
Alternative tree definition
Below is an alternative definition using trees. It tries to allow for free nodes.
λ-terms. Defined as trees with natural number functions.
A lambda term is a tree where:
- Nodes may have 0, 1 or 2 children.
- Every 0-child node has a mapping to a positive integer.
Leaf, abstraction and application nodes are defined as before.
The natural number mapping (instead of the mapping to parent abstraction nodes) encodes a map to a parent abstraction node by counting up through ancestor nodes. In addition, we are able to set counts that go beyond the root of the tree; this is how we can create the sense of the unbound nodes.
The positive integer represents the count up the 1-child ancestor list. The count can go past the root node, and in this way, it will represent unbound nodes. They are not completely "unbound", in that, while they don't know what node they are bound to, they do know what level they are bound to.
Tree visualizations
An tree representation:
A representation with a free variable:

Title: β-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, \( \rightarrow_{\beta} \)
Let \( M, U \) and \( L \) be lambda terms.
The following 2 rules define the true entries of the single step beta reduction relation.
Basis
\( (\lambda .\, M) U \rightarrow_{\beta} M[x :=U] \)
Compatibility
If \( M \rightarrow_{\beta} U \), then:
- \( ML \betaReduction UL \)
- \( LM \betaReduction LU \)
- \( \lambda x.\,M \rightarrow_{\beta} \lambda x. U \)
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:
Redex and contractum
If a subterm of a lambda expression matches the left-hand side of the basis rule above, it is called a redex. This name comes from from reducible expression. The subterm on the right-hand side, \( M[x:=U] \), is called the contractum of the redex.
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 \mathbb{N}, \, n \lt N \), we have \( W_n \betaReduction W_{n+1} \). The sequences starts at \( W_0 \) and ends at \( W_N \).
β-reduction, multi-step, \( \twoheadrightarrow_{\beta} \)
Let \( M \) and \( U \) be lambda terms.
\( M \) reduces through multi-step β-reduction to \( U \) iff there exists a reduction sequence starting at \( M \) and ending at \( U \).
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 \rightarrow_{\beta} U \) to be true while \( U \rightarrow_{\beta} 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 \mathbb{N}, \, n \lt N \) either \( W_n \betaReduction W_{n+1} \) or \( W_{n+1} \betaReduction W_{n} \).
β-equality, \( =_{\beta} \)
Let \( M \) and \( U \) be lambda terms.
\( M \) and \( U \) are said to be β-equal iff there exists a bi-directional reduction sequence starting at \( M \) and ending at \( U \).
β-convertable is sometimes said instead of β-equal.
BackOnlyText: β-equality extends β-reduction in both directions
If \( M \twoheadrightarrow_{\beta} U \) or \( U \twoheadrightarrow_{\beta} M \) then \( M =_{\beta} U \).
The reverse statement is not true.
Graphs of reduction sequences
The following graph shows a possible reduction sequence that implies that \( W_0 \multiBetaReduction W_3 \) is true. \( W_0 \) multi-step reduces to \( W_0 \), \( W_1 \) and \( W_2 \) also.
The next graph shows a bi-directional reduction sequence that implies that \( W_0 \betaEq W_5 \) is true. In fact, all nodes are β-equal to each other.
The nodes are in a zig-zag pattern simply to condense the diagram and this layout is not intended to convey any other meaning.
Context: β-reduction → β-normal form → confluence

Title: β-normal form
β-normal form
Let \( M \) be a lambda term.
- \( M \) is said to be in β-normal form iff \( M \) does not contain any redex.
- \( M \) is said to have a β-normal form iff \( M \betaEq U \) for some lambda term \( U \) that is in β-normal form.
The definition of redex is recalled on back side.
The notion of β-normal form captures a sense of the result of a lambda term; from a β-normal form, no further lambda computation is possible.
The following definition elaborates the concept by considering how many normal forms a term might have.
Weakly normalizing and strongly normalizing
Let \( M \) be a lambda term.
- \( M \) is said to be weakly normalizing iff it has a β-normal form.
- \( M \) is said to be strongly normalizing iff there are no infinite reduction paths starting from \( M \).
BackOnlyText: The two definitions below are referenced in the above material.
Redex and contractum
A subterm of a lambda expression is called a redex, from reducible expression, if it matches the left-hand side of the basis rule above. The subterm on the right-hand side, \( M[x:=U] \) is called the contractum of the redex.
Reduction path
Let \( M \) be a lambda term. A reduction path from \( M \) is a sequence of lambda terms \( (U_n)_{n=0}^{N} \) such that \( M \equiv U_0 \) and \( U_n \betaReduction U_{n+1} \) for every \( 0 \le n \le N \).
A reduction path with an infinite term sequence is called an infinite reduction path.
β-normal form: why \( M \betaEq U \) rather than \( M \multiBetaReduction U \)
It may seem like the multi-step reduction is more appropriate in the definition of the normal form. I think it is in fact true; however, to show it to be true, one must use the confluence theorem. I find this surprising, which suggests that I don't understand the flexibility of the \( \betaEq \) relation.
Finite computation guarantee
The below lemma follows from the definition of strongly normalizing:
A lambda terms is guaranteed to reduce to a β-normal form in finite steps iff it is strongly normalizing.
An interesting part of this lemma is that lambda terms that are not strongly normalizing might reduce to a β-normal form in finite steps or might get stuck in an infinite reduction loop.
Source: Nederpelt, Type Theory and Formal Proof

Title: Confluence
Q: Confluence
Let \( M \) be a lambda term. If \( M \multiBetaReduction N_1 \) and \( M \multiBetaReduction N_2 \) for some lambda terms \( N_1 \) and \( N_2 \), then there exists [...] such that [...].
Confluence is also called the Church-Rosser theorem.
There are three corollaries of the confluence theorem listed on the back side. Can you remember them?
A: a lambda term \( N_3 \); both \( N_1 \multiBetaReduction N_3 \) and \( N_2 \multiBetaReduction N_3 \)
BackOnlyText: Confluence is a defining theorem in untyped lambda calculus. It shows that the result of a computation is independent of the path taken during computation—paths differ depending on the choice of redex to reduce first.
The proof of confluence is unexpectedly complicated, and hints at lambda calculus not being the best theory in which to express the theorem.
Corollaries
The following three results are typically proved using confluence. Their simplicity might deceive readers into thinking they can be proved easily without using confluence.
Corollary 1
Let \( M \) and \( U \) be lambda terms.
Suppose that \( M \betaEq U \). Then there exists a lambda term \( L \) such that \( M \multiBetaReduction L \) and \( U \multiBetaReduction L \).
Some intuition. Imagine a bi-directional reduction sequence. Nodes like \( W \leftarrow X \rightarrow Y \) can be replaced with \( W \rightarrow X' \leftarrow Y \) using confluence. Repeating this reduction will eventually create a sequence like:
\[ M \rightarrow W_1 \rightarrow ... W_k \leftarrow W_{k+1} \leftarrow W_{k+2} ... \leftarrow U \]
The actual proof uses recursion.
Proof. Let \( M \) and \( U \) be lambda terms and assume that \( M \betaEq U \). By this assumption, there exists a bi-directional reduction sequence, \( (W_n)_{n=0}^{N} \) from \( M \) to \( U \). Induce on the length of this sequence, \( N \).
Base case, \( N = 0 \). If \( N = 0 \), then \( M \equiv U \). So it is true that \( M \multiBetaReduction M \) and \( U \multiBetaReduction M \), so \( M \) meets the criteria of the lambda term we are seeking (so does \( U \)).
Assume that the statement is true for some sequence length \( k > 0 \). Then consider \( k + 1 \). First note that \( W_{k+1} \equiv U \), by the definition of a bi-direction reduction sequence from \( M \) to \( U \). The sub-sequence \( (W_n)_{n=0}^{k} \) connects \( M \) and \( W_k \), meaning \( M \betaEq W_k \), and so, by the induction assumption, there exists a lambda term \( L \) such that \( M \multiBetaReduction L \) and \( W_k \multiBetaReduction L \). From here we consider two cases: it is the case that either \( W_k \betaReduction U \) or \( U \betaReduction W_k \).
- If \( W_k \betaReduction U \) we can use confluence to assert that there exists another lambda term \( L' \) such that both \( L \multiBetaReduction L' \) and \( U \multiBetaReduction L' \). By transitivity of multi-step beta reduction, \( M \multiBetaReduction L' \). Thus, \( L' \) is the lambda term that fits the induction requirement.
- If \( U \betaReduction W_{k} \), then \( U \multiBetaReduction L \), by associativity of the multi-step beta reduction, and \( L \) is the term that fits the induction requirement.
Corollary 2
Let \( M \) and \( U \) be lambda terms.
If \( M \) has \( U \) as a β-normal form, then \( M \multiBetaReduction U \).
Proof. Let \( M \) and \( U \) be lambda terms and assume that \( M \) has \( U \) as a β-normal form. By the previous lemma, there is a lambda term \( L \) such that \( M \multiBetaReduction L \) and \( U \multiBetaReduction L \). Being in normal form, \( U \multiBetaReduction L \) can only be true if \( U \equiv L \).
Corollary 3
A lambda term has at most one β-normal form.
Proof. Proof by contradiction. Assume \( M \) is a lambda term with two normal forms, \( U_1 \) and \( U_2 \). By confluence, there exists a \( U_3 \) such that \( U_1 \multiBetaReduction U_3 \) and \( U_2 \multiBetaReduction U_3 \). Being normal forms, both \( U_1 \) and \( U_2 \) must be equivalent to \( U_3 \), and thus, they must be equivalent to each other. This contradicts the assumption that there were two different normal forms.
Corollary 1 visualization
The following figure tries to illustrate how an algorithm can move along a bi-directional reduction sequence and calculate the term that can be reached by both ends in a single direction. Confluence is invoked where the grey dashed lines are seen.