Lambda-Mu Calculus (λμ)
Origin. Michel Parigot, "λμ-calculus: an algorithmic interpretation of classical natural deduction" (LPAR 1992, Springer LNCS 624, pp. 190–201): a term calculus for classical natural deduction with multiple conclusions, extracted from Parigot's free deduction. The prehistory is control operators: Timothy Griffin, "A formulae-as-types notion of control" (POPL 1990), typed Felleisen's C operator with ¬¬A → A and call/cc with Peirce's law, extending Curry–Howard to classical logic through an existing programming construct; Parigot's calculus gave that discovery a proof theory of its own, with μ-abstraction as a primitive binder rather than a constant added to λ.
Models. Curry–Howard for classical natural deduction. A judgment Γ ⊢ t : A ∣ Δ carries one active conclusion and a store of named alternatives; μα.c switches which conclusion is active, and [α]t files the value of t under the name α. Computationally the names are continuations: a λμ-term may capture its evaluation context, resume it later, or resume a different one, so the non-constructive steps of a classical proof execute as jumps. Classical proofs have no naive denotational identity — a cartesian closed category with an involutive negation is a preorder (Joyal; see Polarized Logic) — and λμ is one of the two disciplined responses: keep natural deduction and name the outputs; the sequent-calculus response is Curien–Herbelin's λ̄μμ̃.
Formalism.
Syntax: t ::= x | λx.t | t t | μα.c (terms) c ::= [α]t (commands, or named terms) λ binds term variables x, y; μ binds names α, β.
Typing: Γ ⊢ t : A ∣ Δ — Γ types term variables, Δ types names; a command has no active formula.
Γ ⊢ t : A ∣ α : A, Δ ───────────────────── name Γ ⊢ [α]t ∣ α : A, Δ
Γ ⊢ c ∣ α : A, Δ ───────────────── μ Γ ⊢ μα.c : A ∣ Δ
Naming contracts the right-hand side; μ reactivates a stored conclusion. The multiple-conclusion right side is what makes the logic classical; λ and application are the usual →-rules, unchanged.
Reduction: (λx.t) u ⇝ t[u/x] (β) (μα.c) u ⇝ μα.c[[α](t u) / [α]t] (structural: every subterm named α receives the argument u) [β]μα.c ⇝ c[β/α] (renaming) μα.[α]t ⇝ t, α not free in t (simplification)
Control: call/cc := λf. μα.[α] f (λx. μβ.[α] x) : ((A → B) → A) → A Pure λμ derives Peirce's law and proves exactly minimal classical logic; Felleisen's C and full classical strength need ⊥ with its elimination (Ariola and Herbelin, "Minimal classical logic and control operators", ICALP 2003).
Call-by-name and call-by-value: Parigot's reduction is call-by-name; Ong and Stewart gave the call-by-value variant ("A Curry–Howard foundation for functional computation with control", POPL 1997, pp. 215–227). Curien and Herbelin, "The duality of computation" (ICFP 2000, pp. 233–243), recast both in λ̄μμ̃, a term calculus for the sequent calculus in which a command pairs a term against an evaluation context, μ captures contexts and μ̃ binds terms: the calculus has a single critical pair, its two orientations are exactly call-by-value and call-by-name, and the term/context symmetry exchanges them.
CPS: Philippe de Groote (CAAP 1994, LNCS 787, pp. 85–99) translated λμ into the pure λ-calculus by continuation-passing style, correctly for both equality and evaluation; on types the translation is a Kolmogorov-style double-negation translation, so the CPS transform is the computational content of the classical-to-intuitionistic embedding.
Symbols.
| Symbol | Unicode | Name | Meaning |
|---|---|---|---|
| μ | U+03BC | Greek small mu | Binder turning a command into a term; names its conclusion |
| λ | U+03BB | Greek small lamda | Ordinary abstraction |
| α | U+03B1 | Greek small alpha | A name — a continuation variable |
| β | U+03B2 | Greek small beta | Second name; also labels β-reduction |
| Γ | U+0393 | Greek capital gamma | Hypotheses typing term variables |
| Δ | U+0394 | Greek capital delta | Named conclusions, the classical right-hand side |
| ⊢ | U+22A2 | Turnstile | Typing judgment |
| ∣ | U+2223 | Divides (separator bar) | Separates the active conclusion from Δ |
| [ | U+005B | Left square bracket | Opens a naming [α]t |
| ] | U+005D | Right square bracket | Closes it |
| → | U+2192 | Rightwards arrow | Implication / function type |
| ⇝ | U+21DD | Rightwards squiggle arrow | Reduction |
| ¬ | U+00AC | Not sign | Negation in the types of control operators |
| ⊥ | U+22A5 | Up tack / Falsum | Absurdity; its elimination separates full from minimal classical logic |
| μ̃ | — | Mu-tilde | λ̄μμ̃'s term binder, the let of the sequent calculus |
| λ̄μμ̃ | — | Lambda-bar-mu-mu-tilde | Curien–Herbelin's sequent term calculus |
| Λμ | — | Capital lambda-mu | De Groote's relaxed syntax |
| call/cc | — | Call-with-current-continuation | The control operator typed by Peirce's law |
| C | — | Felleisen's C | The control operator typed by ¬¬A → A |
| [α]t | — | Named term | A command filing t under α |
| ::= | — | Grammar production | Defines the term syntax |
Metatheory. Reduction is confluent for β together with the structural and renaming rules (Parigot, by parallel reduction; the diamond property of his parallel reduction has a gap that Py's 1998 thesis repaired). The simply typed calculus is strongly normalizing, and Parigot, "Proofs of strong normalization for second order classical natural deduction" (Journal of Symbolic Logic 62(4), 1997, pp. 1461–1479), proved strong normalization for the second-order calculus by reducibility candidates, after a LICS 1993 conference version; Matthes (2001) reproved it by a reduction-preserving embedding into System F. Subject reduction holds, so normalizing a λμ-term normalizes a classical proof. Selinger, "Control categories and duality" (Mathematical Structures in Computer Science 11, 2001, pp. 207–260), gave the categorical semantics: call-by-name λμ is the internal language of control categories, call-by-value of their duals, and the structure theorem yields mutually inverse syntactic translations between the two disciplines preserving operational semantics — call-by-value is the de Morgan dual of call-by-name, which Curien and Herbelin's single critical pair exhibits syntactically. David and Py (Journal of Symbolic Logic 66, 2001) proved that Böhm's theorem fails for λμ: there are closed normal terms, distinct in the theory, that no context separates; Saurin (LICS 2005) showed separation holds in de Groote's relaxed syntax Λμ — Herbelin and Saurin call the distinction "a capital difference".
Applies to. The computational content of classical proofs — proofs as programs with control. Typing call/cc and its relatives in ML, Scheme and their descendants. The classical leg of the Curry–Howard Correspondence, which this calculus supplies. Sequent-calculus abstract machines and compiler intermediate languages in the λ̄μμ̃ line. CPS translation and double-negation translation, as one construction seen twice. Classical natural deduction's normalization theory — Natural Deduction's classical case routes through λμ.
Limitations. The equational theory is weaker than observation: Böhm separation fails (David–Py 2001), so λμ's syntax does not determine observational equivalence the way the λ-calculus's does, and the repair — de Groote's Λμ — has only weak normalization where typed λμ has strong. Confluence depends on the restricted syntax and rule set: λ̄μμ̃ with both orientations of its critical pair active is not confluent, which is the syntactic face of the fact that classical proof reduction supports no single canonical strategy — call-by-name and call-by-value λμ are different theories and the choice between them is extrinsic. Pure λμ is minimal classical logic only; ex falso and full classical strength are additions (Ariola–Herbelin 2003). And the calculus does not extend to dependent types: Herbelin ("On the degeneracy of Σ-types in presence of computational classical logic", TLCA 2005) proved that unrestricted classical control collapses strong sums, so classical dependent type theory must restrict where control occurs.
© 2026 Lingenic LLC