Application

M N as applying one term to another. Left-associative convention.

8 topics • ~844 words

A composing stick sits on the bench with a tagged blank. A type piece sits beside it. To apply, the compositor places the piece into the stick's slot. No glue, no special tool — just placement.

Lambda calculus has only three kinds of expression: variables, abstractions, and applications. Application is how things happen — it is the act of giving one term to another. Without it, abstractions just sit there.

What Is Application

Application is written by placing two terms next to each other:

M N

This means "apply M to N." M is in function position and N is in argument position.

There is no special symbol for application — no parentheses required, no operator, no keyword. Just juxtaposition: one term followed by another.

For example, f x means "apply f to x."

Function and Argument Positions

In an application M N, the two parts have names:

  • M is in function position (the left term)
  • N is in argument position (the right term)

For example, in (λx.x) a:

  • (λx.x) is the function — an abstraction waiting for input
  • a is the argument — the term being given to the function

The function always comes first (on the left), and the argument always comes second (on the right).

Left Associativity

Three type pieces in a row on the bench: the compositor always starts from the left. Place the first into the second, take the result, place it into the third. Left to right, one pair at a time.

When three or more terms appear in a row, application groups from the left. This is called left associativity.

f a b means (f a) b

Read it as: "first apply f to a, then apply the result to b."

It does not mean f (a b) — that would mean "apply a to b first, then apply f to that result."

Without this convention, every chain of applications would need explicit parentheses. Left associativity keeps expressions compact.

Application Needs Two Terms

An application always has exactly two parts:

  • A term in function position (left)
  • A term in argument position (right)

You cannot apply zero terms or one term — application is a binary operation. Writing f alone is just a variable, not an application. Writing f a b is two applications: (f a) and then the result applied to b.

Every application is one function applied to one argument. Chains like f a b c are built from nested binary applications: ((f a) b) c.

Identify the Function

In any application M N, the term on the left is in function position. Identifying the function in an application is a matter of reading the structure:

  • In f a, the function is f
  • In (λx.x) y, the function is (λx.x)
  • In (f a) b, the function is (f a) — the result of an earlier application

Remember: left associativity means f a b is (f a) b, so the function in the outermost application is (f a), not f.

Anything Can Be Applied

In the workshop, anything made of type metal can go into the composing stick. A single letter, a pre-set block, even another composing stick — the slot does not care what it receives.

In lambda calculus, any term can appear in function position. There is no restriction on what can be applied:

  • A variable: f x — apply f to x
  • An abstraction: (λx.x) a — apply a function to a
  • An application: (f a) b — apply the result of f a to b

This uniformity is a core feature. There is no separate category of "things that can be applied" versus "things that cannot." Everything is a term, and any term can be a function.

Parentheses for Clarity

Since application is left-associative, f a b always means (f a) b. But sometimes you want a different grouping.

Parentheses override the default:

  • f (a b) — first apply a to b, then apply f to that result
  • (f a) b — first apply f to a, then apply the result to b

These are different expressions with different structures. In f (a b), the argument to f is the application a b. In (f a) b, the argument to f is just a.

When parentheses match the default left associativity, they are optional: (f a) b and f a b mean the same thing.

Application Is Not Evaluation

Writing (λx.x) a creates an application — a term where (λx.x) is applied to a. But the expression has not been evaluated. No substitution has occurred. The result is not a until we explicitly perform a reduction step.

Application is syntax — it describes structure. Reduction (which comes later) is the computation that transforms (λx.x) a into a.

Think of it this way: (λx.x) a and a are different terms that happen to be related by reduction. Writing the application does not automatically produce the result.

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 Application →