Reading Terms

Outermost Form

Every lambda term is exactly one of three forms:

• Variable: a single name like x
• Abstraction: starts with λ — e.g., λx.x y
• Application: one term applied to another — e.g., f x

The outermost form is determined by the topmost constructor. In λx.x y, the outermost form is an abstraction (the λ governs the entire expression). The body x y happens to be an application, but that is internal structure.

Parsing Applications

Application is left-associative. When you see a chain of terms without explicit parentheses, group from the left:

• a b c means (a b) c — apply a to b first, then apply the result to c
• f x y z means ((f x) y) z

This convention avoids parentheses everywhere. Without it, every application would need explicit grouping.

Parsing with Lambda

The body of a lambda abstraction extends as far right as possible. The dot after the parameter is greedy — it claims everything to its right, unless parentheses say otherwise.

• λx.x y means λx.(x y) — the body is x y, not just x
• (λx.x) y means something different — parentheses end the body at x, and y is a separate argument

This convention minimizes parentheses. Without it, you would need to write (λx.(x y)) every time.

Full Parenthesization

Full parenthesization makes all implicit grouping explicit. Apply the two conventions:

1. Application is left-associative: a b c becomes ((a b) c)
2. The body of $\lambda$ extends right: λx.M N becomes (λx.(M N))

Examples:

• f a b $\to$ ((f a) b)
• λx.x y $\to$ (λx.(x y))
• a b $\to$ (a b)

Identify Subterms

A subterm of a lambda expression is any well-formed piece of it, including the expression itself. To count subterms, identify every node in the expression's syntax tree.

For example, (λx.x) y has these subterms:

1. (λx.x) y — the whole expression (an application)
2. λx.x — the function part (an abstraction)
3. x — the body of the abstraction (a variable)
4. y — the argument (a variable)

That is 4 subterms total.

Application vs Abstraction

When an expression contains both λ and application, the outermost form depends on where the λ sits.

• λx.f x — the λ governs the whole expression. Outermost form: abstraction. The body f x is an application, but that is internal.
• (λx.x) f — the λ is inside parentheses. Outermost form: application. The abstraction λx.x is applied to f.

The key question: does the λ at the front govern the entire expression, or is it contained inside a subterm?

Where Does the Body End?

Without parentheses, the body of λ extends to the end of the expression. Parentheses override this — a closing parenthesis ends the body.

Compare:

• λx.x y — body is x y (extends to the end)
• (λx.x) y — body is just x (parenthesis ends it)
• (λx.x) (λy.y) — first body is x, second body is y; the whole expression is an application

Getting this wrong changes the meaning entirely.

Classify Expression

Every lambda term has exactly one outermost form:

• variable — a single name: x, f, y
• abstraction — starts with λ that governs the whole expression: λx.M
• application — one term applied to another: M N

To classify a compound expression, find its outermost constructor. Ignore internal structure — only the top level matters.