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:
- each term-variable is a λ-term, called an atomic term;
- if \( M \) and \( N \) are λ-terms, then [what?] is a λ-term, called an application;
- 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.
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?