\( \newcommand{\matr}[1] {\mathbf{#1}} \newcommand{\vertbar} {\rule[-1ex]{0.5pt}{2.5ex}} \newcommand{\horzbar} {\rule[.5ex]{2.5ex}{0.5pt}} \)
deepdream of
          a sidewalk
Show Question
\( \newcommand{\cat}[1] {\mathrm{#1}} \newcommand{\catobj}[1] {\operatorname{Obj}(\mathrm{#1})} \newcommand{\cathom}[1] {\operatorname{Hom}_{\cat{#1}}} \newcommand{\multiBetaReduction}[0] {\twoheadrightarrow_{\beta}} \newcommand{\betaReduction}[0] {\rightarrow_{\beta}} \newcommand{\betaEq}[0] {=_{\beta}} \newcommand{\string}[1] {\texttt{"}\mathtt{#1}\texttt{"}} \newcommand{\symbolq}[1] {\texttt{`}\mathtt{#1}\texttt{'}} \)
Math and science::Theory of Computation::Lambda calculus

β-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 \).

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 N_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