\( \newcommand{\matr}[1] {\mathbf{#1}} \newcommand{\vertbar} {\rule[-1ex]{0.5pt}{2.5ex}} \newcommand{\horzbar} {\rule[.5ex]{2.5ex}{0.5pt}} \newcommand{\E} {\mathrm{E}} \)
deepdream of a sidewalk
Show Answer
\( \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{'}} \newcommand{\groupMul}[1] { \cdot_{\small{#1}}} \newcommand{\groupAdd}[1] { +_{\small{#1}}} \newcommand{\inv}[1] {#1^{-1} } \newcommand{\bm}[1] { \boldsymbol{#1} } \require{physics} \require{ams} \require{mathtools} \)
Math and science::Theory of Computation::Lambda calculus

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 [what?] is a λ-term, called an application;
  3. if \( x \) is a term-variable and \( M \) is a λ-term, then [what?] is a λ-term, called a λ-abstract.

A [something] λ-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 [something node?] has a mapping to [what?].

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?