Abstraction

Lambda abstraction as template with named slot. Parameter, body, dot.

10 topics • ~1083 words

A composing stick sits on the bench. Along one edge, a tag reads x. Everywhere in the stick where that tag appears, an empty slot waits. Nothing has been placed in those slots yet. The stick is a template -- ready to receive a type piece, but doing nothing until one arrives.

Lambda calculus has exactly three kinds of expression: variables, abstractions, and applications. The previous concept introduced all three. Now we focus on the second form -- the abstraction -- which is the source of all computation in this system.

What Is an Abstraction?

An abstraction has the form λx.M, where:

  • λ marks the start of an abstraction
  • x is the parameter (a variable name)
  • . separates the parameter from the body
  • M is the body (any lambda term)

The abstraction λx.M is a function. It says: "given an argument for x, produce the body M." But it does not execute -- it simply waits.

Examples: λx.x, λy.y z, λa.λb.a

Parameter and Body

Every abstraction λx.M has exactly two components:

  • The parameter: the variable name immediately after λ, before the .
  • The body: everything after the .

In λx.x y, the parameter is x and the body is x y. In λa.a, the parameter is a and the body is a. In λf.λx.f x, the parameter is f and the body is λx.f x.

The body can be any lambda term -- a variable, an application, or even another abstraction.

Identify the Parameter

Every composing stick has a tag along its edge -- the name of the blank it will accept type pieces for. Reading the tag is the first step before any typesetting.

The parameter of an abstraction is the variable name between λ and .. It names the slot that an argument will fill.

  • λx.x -- parameter is x
  • λy.y z -- parameter is y
  • λp.λq.p -- parameter of the outer abstraction is p

The parameter is always a single variable. It cannot be an expression or multiple variables.

Identify the Body

The body of an abstraction is the term that follows the . separator. It extends as far right as possible.

  • λx.x -- body is x
  • λy.y z -- body is y z (not just y)
  • λa.λb.a -- body is λb.a (the entire inner abstraction)

Remember: the dot marks the start of the body, and the body consumes everything to the right.

An Abstraction Is a Term

An abstraction λx.M is a term like any other. This means it can appear:

  • As the body of another abstraction: λf.λx.f x
  • As the left side of an application: (λx.x) y
  • As the right side of an application: f (λx.x)

There is no distinction between "functions" and "data" in lambda calculus. An abstraction can be passed as an argument, returned as a result, or nested inside other terms.

Nested Abstractions

A composing stick tagged x contains, in its body, another stick tagged y. The outer stick has one blank; filling it produces the inner stick -- which still has its own blank. One tag at a time.

When one abstraction appears inside another, we get nesting:

λx.λy.x y

This is an abstraction with parameter x whose body is the abstraction λy.x y. It is not a single function with two parameters -- each λ introduces exactly one parameter.

The outer and inner abstractions are separate. The outer one produces, when given an argument, a new abstraction that still has a blank to fill.

More nesting: λa.λb.λc.a has three layers. The outermost parameter is a, and the body is λb.λc.a.

The Dot Extends Right

The body of λx. extends as far right as possible. This is a fundamental convention of lambda calculus notation.

λx.x y means λx.(x y) -- the body is x y.

It does not mean (λx.x) y, which would be an application of the abstraction λx.x to the argument y.

To limit the body, use explicit parentheses:

  • λx.x y = λx.(x y) -- body is x y
  • (λx.x) y -- body is just x, and y is outside

Without parentheses, the λ greedily takes everything to the right as its body.

Abstraction as Template

A composing stick with tagged blanks sits on the bench. The press operator walks past, glances at it, and keeps going. No type piece has been offered, so no typesetting occurs. The stick simply waits.

An abstraction is inert. It defines a pattern -- "here is a body with a named slot" -- but it performs no computation on its own.

λx.x says: "I have a slot named x. Give me something for x, and I will produce a result." Until an argument is supplied, there is nothing to do.

This is different from most programming languages, where writing a function and calling it are obviously distinct. In lambda calculus, the distinction is equally sharp: λx.x is a template. (λx.x) a is the act of filling the template. They are different terms.

Lambda Is Not a Variable

The symbol λ is syntax -- a marker that announces the start of an abstraction. It is not a variable, not a function name, and not a value.

In λx.x:

  • λ means "here begins an abstraction"
  • x (after λ) is the parameter
  • . separates the parameter from the body
  • x (after .) is the body

You cannot use λ as a variable name, pass it as an argument, or refer to it inside an expression. It is part of the notation, like parentheses or the dot.

Compare: in the expression 2 + 3, the + is syntax -- it tells you what operation to perform. You would not say "+ equals 5." Similarly, λ tells you that an abstraction is being formed.

Any Body

The body of λx.M is M, and M can be any lambda term:

  • Variable: λx.y -- body is the variable y
  • Abstraction: λx.λy.x -- body is the abstraction λy.x
  • Application: λx.x z -- body is the application x z

There are no restrictions on what appears in the body. The parameter may or may not appear in the body, and the body can be as simple or as complex as needed.

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