Terms and Grammar

The BNF grammar. Recognizing variables, abstractions, applications.

10 topics • ~1242 words

A compositor's workshop has exactly three kinds of material. Tagged blank slugs sit in the type case — placeholders marked with a letter. Composing sticks hold a row of material with at least one tagged blank, ready for a piece to be set. And the act of placing a type piece into a stick's tagged slot — that's the third kind. Slug, stick, placement. Everything in the shop is one of these three.

Lambda calculus is built from just three forms of expression. No numbers, no booleans, no special operators — nothing else exists yet. Everything you'll encounter later (arithmetic, logic, data structures) will be constructed from these three forms alone.

What Is a Term?

A lambda term (also called an expression) takes exactly one of three forms:

  1. Variable — a name like x, y, or f
  2. Abstraction — written λx.M, where x is a parameter and M is the body
  3. Application — written M N, two terms side by side

There is nothing else. These three forms are the entire language.

The BNF Grammar

The workshop's inventory list is three lines long. A tagged blank slug. A composing stick with at least one tagged blank. Or the act of setting one piece into another. That's the complete catalog — three entries, and every possible job in the shop is built from them.

The grammar of lambda calculus is written in BNF (Backus-Naur Form):

M ::= x | λx.M | M M

Reading this: a term M is either:

  • x — a variable (any name)
  • λx.M — an abstraction ($\lambda$, a variable, a dot, then a term)
  • M M — an application (two terms side by side)

The rule is recursive: the M on the right side refers back to the definition itself.

Recognizing Variables

A tagged blank slug is the simplest thing in the shop. No moving parts, no internal structure — just a name on a piece of metal. It doesn't do anything by itself. It marks a position where something will eventually be set.

A variable is the simplest form of lambda term. It's just a name — a single letter or identifier like x, y, f, or z.

A variable has no internal structure. It's not an abstraction (no λ or dot), and it's not an application (there's only one thing, not two side by side). When you see a lone name with nothing else attached, that's a variable.

Recognizing Abstractions

A composing stick always has a tag at the front and material behind it. You recognize a stick by that structure: tag, then content. In notation, the tag is the part between λ and the dot, and everything after the dot is the material loaded in the stick.

An abstraction is written λx.M, where:

  • λ (lambda) marks the start
  • x is the parameter — the name being bound
  • . (dot) separates the parameter from the body
  • M is the body — any lambda term

The signature features are the λ and the . (dot). If you see both, you're looking at an abstraction.

Examples: λx.x, λf.f, λy.x

Recognizing Applications

Setting type piece into a composing stick is the act of combining two things: the stick and the piece. You see it as two materials placed together on the bench. Neither one is marked with λ at the top level — they're just sitting side by side, waiting to be combined.

An application is written M N — two terms placed side by side, separated by a space. The first term M is applied to the second term N.

No special symbol marks an application. There's no operator, no parentheses required, no keyword. Just two terms next to each other:

  • f x — apply f to x
  • (λx.x) y — apply λx.x to y
  • f g — apply f to g

The Dot Rule

In an abstraction λx.M, the dot separates two things:

  • Left of the dot: the parameter (x)
  • Right of the dot: the body (M)

The body extends as far right as possible. So λx.y z means λx.(y z) — the entire expression y z is the body. It does not mean (λx.y) z.

This is called the greedy body convention: the dot "grabs" everything to its right.

Nothing Else Exists

Lambda calculus has no built-in data. There are no numbers, no booleans, no strings, no lists, no if statements, no + operator. The grammar M ::= x | λx.M | M M is complete — it defines every possible term.

This might feel restrictive, but it's the whole point. Lambda calculus is a foundation: everything else will be constructed from these three forms. Numbers, booleans, data structures, and even control flow will emerge from variables, abstractions, and applications alone.

Term Classification

Every lambda term has an outermost form — the top-level structure you see before looking inside any subterms.

  • If the whole term is a single name, it's a variable
  • If the whole term starts with λ, it's an abstraction
  • If the whole term is two things side by side (and doesn't start with λ), it's an application

Examples:

  • x — variable
  • λx.x — abstraction (starts with λ)
  • f x — application (two terms side by side)
  • λy.f y — abstraction (starts with λ, even though the body contains an application)

Nested Terms

A composing stick can hold another composing stick as part of its material. Open one stick and you might find another inside, with its own tagged blanks. The materials are uniform — a stick is made of the same stuff as the pieces set into it.

Because the grammar is recursive, terms can nest inside each other. An abstraction's body can be another abstraction, an application, or a variable. An application's parts can be abstractions, other applications, or variables.

For example, λx.(λy.y) is an abstraction whose body is another abstraction. At the outermost level, the whole thing is a single abstraction. But inside its body, there's a second abstraction λy.y.

This nesting is what gives lambda calculus its expressive power despite having only three forms.

Conventions

Two conventions reduce parentheses in lambda calculus:

  1. Outer parentheses are dropped. We write λx.x instead of (λx.x).

  2. Application is left-associative. When multiple terms appear in sequence, group them from the left:

    • f x y means (f x) y — apply f to x first, then apply the result to y
    • It does not mean f (x y)

These are notational shortcuts only. They don't change what the terms mean — just how we write them.

Ready to test your understanding?

Bitwit uses spaced repetition to help you truly master concepts like this—not just read about them. Each card generates with different values, so you can't just memorize answers.

Practice Terms and Grammar →