 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?