skip to content

Lambda Calculus Roots

6 roadmaps4 questions

The two-rule calculus underneath every functional language: build a function, apply it, reduce. Interviewers rarely test it directly but expect you to know where the paradigm's vocabulary comes from.

on this pageshow

explore

questions

4

What does one beta-reduction step replace when you reduce (λx. λy. x) a b by hand?

level: juniorimportance: should knowfreq 40%

answer

  1. one rewrite rule, nothing else
  2. find the redex first
  3. argument in, binder out
  4. free occurrences only, shadowed ones untouched
  5. stop at a redex-free term

basics

~20 s

A beta-reduction step substitutes the argument for every free occurrence of the parameter in the function body, then removes the binder. Two such steps take (λx. λy. x) a b to a, discarding the second argument.

solid answer

~40 s

Beta reduction is the calculus's only computation rule. A *redex* is an abstraction applied to an argument, `(λx. B) A`, and it rewrites to `B` with every **free** occurrence of `x` replaced by the whole term `A`, with the binder `λx` gone. Reducing `(λx. λy. x) a b`: application groups to the left, so the outer redex fires first and gives `(λy. a) b`. That is a redex too; its body is just `a`, which contains no `y`, so the substitution replaces nothing and `b` is thrown away, leaving `a`. You stop when no redex remains anywhere — that term is in *normal form*. The one piece of care the rule needs is that a free variable of the argument must not end up under a binder in the body.

code

pseudocode · 9 lines
pseudocode
term:   (λx. λy. x) a b          -- groups as ((λx. λy. x) a) b

step 1: fire (λx. λy. x) a
        substitute a for x inside (λy. x)
        result: (λy. a) b

step 2: fire (λy. a) b
        y occurs zero times in the body, so b is discarded
        result: a                -- no redex left: normal form

go deeper

for a junior

Recall the three term shapes and the single rule: an abstraction applied to an argument becomes its body with the parameter replaced. Be able to run two steps on a small term without stalling.

for a middle

Explain that only free occurrences are substituted, that the binder disappears with the step, and that an argument whose parameter occurs zero times is discarded along with all the work it stood for.

for a senior

Show where the vocabulary pays off in review: inlining a call by hand is a beta step, and it is only safe when the argument mentions no name the body already binds. Say what a zero-occurrence parameter means for that inlining.

for a principal

The tradeoff worth naming is how much formal vocabulary a team standardises on. Words like binder, free occurrence and normal form make review arguments short and precise, but only if everyone in the room shares them.

## Three shapes and one rule The lambda calculus is the smallest thing that is still a programming language. Every term is exactly one of three shapes: - a **variable** — `x`, a name standing for something; - an **abstraction** — `λx. B`, read "build a function whose parameter is `x` and whose body is the term `B`"; - an **application** — `F A`, read "apply the term `F` to the term `A`". There are no numbers, no booleans, no records, no loops, no assignment and no declarations. The vocabulary a functional programmer uses daily — *lambda*, *parameter*, *argument*, *binding*, *free variable*, *normal form* — was given to these shapes here, which is the honest reason the subject still comes up. Computation is a single rewrite rule. A subterm of the form `(λx. B) A` is called a **redex** (a reducible expression), and **beta reduction** rewrites it to `B[x := A]`: the body `B` with every *free* occurrence of `x` replaced by the entire argument term `A`, and the binder `λx` removed. That is the whole operational semantics. The rule itself does not inspect `A`, does not require `A` to be reduced first, and does not care how big `A` is. ## Reducing one term by hand Take `(λx. λy. x) a b`. Application groups to the left, so it parses as `((λx. λy. x) a) b`. An abstraction has exactly one parameter, so what looks like a two-parameter function is an abstraction whose body is another abstraction, and it consumes its arguments one at a time. | Step | Redex fired | Substitution | Result | |---|---|---|---| | 1 | `(λx. λy. x) a` | `x := a` inside `λy. x` | `(λy. a) b` | | 2 | `(λy. a) b` | `y := b` inside `a` | `a` | Step 2 is the instructive one. The body is just `a`; `y` occurs in it zero times, so the substitution replaces nothing and the argument `b` is discarded outright. That is not a special case bolted on to the rule — it falls straight out of "replace every free occurrence" when the number of occurrences happens to be zero. Two steps, and the term is `a`. ## What a single step may touch 1. **Free occurrences only.** If the body contains a nested binder that reuses the parameter's name, occurrences under that nested binder belong to it, and the step leaves them exactly as they are. 2. **The argument goes in whole and unexamined.** If the parameter occurs twice, the argument term is duplicated; if it occurs zero times, the argument vanishes along with the work it represented. 3. **The binder disappears** in the same step. A term does not accumulate spent binders. 4. **Capture must be avoided.** If a free variable of the argument would land under a binder inside the body, that binder is renamed to a fresh name first; substitution is simply not defined otherwise. ## Knowing when you are finished You stop when the term contains no redex anywhere — including inside the body of an abstraction, which is a place casual reduction often forgets to look. Such a term is in **normal form**, and it is the calculus's notion of an answer. Two facts here are routinely conflated, and keeping them apart is most of what a good answer demonstrates: - **A normal form is unique.** If a term can be reduced along two different paths, those paths can always be continued until they meet at a common term. That confluence property is the content of the **Church-Rosser theorem**, and it is why the order in which you pick redexes cannot change the answer you get — only how much work you do getting there. - **A normal form need not exist, and a reduction order can miss one that does.** The term `(λx. x x) (λx. x x)` reduces to itself, forever. Write `Ω` for it; then `(λy. a) Ω` reduces to `a` in one step if you fire the outer redex, but never terminates if you insist on working inside the argument first. Uniqueness of the answer says nothing about reaching it. Which order a working language commits to is a separate subject from this one. ## Why the vocabulary outlived the calculus Every language with function values inherited these words and, with them, the hazards. Inlining a call by hand during code review is a beta step performed by a human: you substitute the argument expression into the body. The same two questions apply — does the parameter occur zero times, so the argument's work disappears, and does the argument mention a name that the body already binds, so substituting it silently changes what that name means. Being able to run two steps on a small term is not academic trivia; it is the ability to say precisely what an inlining did.

  • Does the order in which you pick redexes change the term you end up with?
    Not the answer, but possibly whether you get one. Confluence guarantees that two different reduction paths from the same term can always be continued to a common term, so a normal form is unique up to the names of bound variables. It guarantees nothing about termination: an order that works inside an argument the function is about to discard can run forever on a term that another order finishes in one step.
  • What does eta conversion add on top of beta reduction?
    Eta says that an abstraction doing nothing but passing its parameter straight on, `λx. f x`, is interchangeable with `f` itself, provided `x` does not occur free in `f`. Beta tells you how to run an application; eta tells you when a wrapper around a function carries no information at all. It is the formal version of deleting a one-line lambda that only forwards its argument.

saying these in an interview costs you the question

  • Says a step cannot fire until the argument is fully reduced
  • Substitutes into occurrences that a nested binder has rebound
  • Treats beta reduction as evaluating arithmetic rather than rewriting terms
  • Claims every term eventually reaches a normal form
  • Stops reducing when the term looks simple rather than redex-free
open as a page

With only abstraction and application available, how can a term encode a pair and recover each component?

level: middleimportance: should knowfreq 26%

basics

~20 s

A pair becomes a function that carries both components and hands them to a selector the caller supplies. Apply it to a selector returning its first argument to get one component, and to a selector returning its second for the other.

open as a page

Reducing (λx. λy. x) y, why does naive substitution produce the identity function instead of the correct term?

level: middleimportance: should knowfreq 34%

basics

~20 s

The argument is the free variable y, and substituting it blindly drops it under an inner binder that already uses that name, so it is captured. Renaming the bound name first gives λz. y, a constant function.

open as a page

Nothing in the pure lambda calculus can refer to itself by name, so how does recursion arise?

level: seniorimportance: nice to knowfreq 18%

basics

~20 s

Through a fixed-point combinator. You write the body as a function whose first parameter stands for the recursive call, then apply a combinator that keeps handing that body another copy of itself, so the call site is supplied rather than named.

open as a page