Parigot's \lambda\mu-calculus

Parigot 1992 introduced the \lambda\mu-calculus as a system for classical logic.

In terms of programming, the \lambda\mu-calculus is a \lambda-calculus equipped with continuation variables, to which one can throw values, or capture them using binding.

Type system

The \lambda\mu-calculus has two sorts of typing judgments:

• \Gamma \vdash M : A; \Delta, which classifies values M.
• c : (\Gamma \vdash \bot; \Delta), which classifies commands c.

In either case, \Gamma is the usual context of variables x : A, while \Delta is a context of continuation variables \alpha : A.

The idea is that the first sequent is the usual intuitionistic one, stating that M is a term that computes a value of type A using continuation variables in \Delta. Meanwhile, the second sequent corresponds to a command, which does some "internal" computation.

The type system is given by the following rules, which are slightly adapted from the original system by Ariola and Herbelin 2003:

\frac{}{\Gamma, x : A \vdash x : A; \Delta}
\quad
\frac{
  \Gamma, x : A \vdash M : B ; \Delta
}{
  \Gamma \vdash \lambda x .\ M : A \to B ; \Delta
}
\quad
\frac{
  \Gamma \vdash M : A \to B; \Delta \quad
  \Gamma \vdash N : A; \Delta \quad
}{
  \Gamma \vdash MN : B; \Delta
}

\frac{
  \Gamma \vdash M : A; \Delta, \alpha : A
}{
  [\alpha]M : (\Gamma \vdash \bot; \Delta, \alpha : A)
}
\quad
\frac{
  c : (\Gamma \vdash \bot; \Delta, \alpha : A)
}{
  \Gamma \vdash \mu \alpha.\ c : A; \Delta
}

The first three rules are the usual rules of the simply-typed \lambda-calculus. They have an extra context \Delta added to them parametrically.

The last two rules are the classical rules. The first one is sometimes called the passivate rule, and the second one the activate rule.

Read logically, assumptions \alpha : A in \Delta can be understood as proofs of \lnot A. Then the rules capture the following intuitions:

• The passivate rule says: to prove a contradiction assuming \lnot A, it suffices to construct a proof of A.
• The activate rule says: if you can prove a contradiction assuming \lnot A, then you can prove A.

Seen more operationally:

• The passivate rule reads as follows: given a term producing a value of type A, throw it to a continuation variable \alpha waiting for something of type A.
• The activate rule reads as follows: given a command with a free continuation variable \alpha : A, capture that variable to obtain the value passed to it.

Example

It is an instructive exercise to show that Peirce's law is typable as the term

\vdash \lambda f. \mu \alpha. [\alpha](f(\lambda y. \mu \beta. [\alpha] y) : ((A \to B) \to A) \to A

Very roughly, the operational behaviour of this can be described as follows: in trying to produce an A:

• Take f : (A \to B) \to A as input
• Listen for the output on a continuation variable \alpha : A
• Call f with the 'trojan horse' function g := \lambda y. \mu \beta. [\alpha] y : A \to B.
  • If f g ever returns an A, just throw it to the continuation variable \alpha.
  • If f starts poking its argument g to obtain a B, then f can be compelled to provide some y : A to get that B. Listen for that y : A, hijack it, and throw it to the continuation variable \alpha when you see it.

Notice that the fact that \alpha persists even after one throws something at it in the passivate rule is crucial for typing this example.

Dynamics

There are two dynamics for the \lambda\mu calculus.

• The original dynamics presented by Parigot 1992, is call-by-name.
• An alternative dynamics, which is call-by-value, is essentially due to Ong and Stewart 1997.

In either case, the substitution operator

[[\alpha](wM)/[\alpha]w]

replaces every subterm of the form [\alpha]w with the subterm [\alpha](wM). Similarly for [[\alpha](Vw)/[\alpha]w].

The presentation here has been adapted from Ariola and Herbelin 2003.

Call-by-name

• \beta reduction: (\lambda x.\ M)N \to M[N/x]
• Structural reduction: (\mu \alpha.\ c)N \to \mu \alpha.\ c[[\alpha](wN)/[\alpha]w]
• Renaming: \mu \alpha. [\beta](\mu \gamma.\ c) \to \mu \alpha. c[\beta/\gamma]
• Simplification: \mu \alpha. [\alpha]c \to c whenever \alpha \not\in \text{fv}(M).

Call-by-value

Let V be a value, i.e. a variable or a \lambda-abstraction.

• \beta reduction: (\lambda x.\ M)V \to M[V/x]
• Left structural reduction: (\mu \alpha.\ c)N \to \mu \alpha.\ c[[\alpha](wN)/[\alpha]w]
• Right structural reduction: V(\mu \alpha.\ c) \to \mu \alpha.\ c[[\alpha](Vw)/[\alpha]w]
• Renaming: \mu \alpha. [\beta](\mu \gamma.\ c) \to \mu \alpha. c[\beta/\gamma]
• Simplification: \mu \alpha. [\alpha]c \to c whenever \alpha \not\in \text{fv}(M).

References

• There is a Wikipedia page on the \lambda\mu-calculus.

• The \lambda\mu-calculus was introduced in the paper

@inproceedings{parigot_1992,
	address = {Berlin/Heidelberg},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {$\lambda\mu$-{Calculus}: {An} algorithmic interpretation of classical natural deduction},
	volume = {624},
	doi = {10.1007/BFb0013061},
	booktitle = {Logic {Programming} and {Automated} {Reasoning}},
	publisher = {Springer-Verlag},
	author = {Parigot, Michel},
	editor = {Voronkov, Andrei},
	year = {1992},
	pages = {190--201}
}

• A second-order version of the \lambda\mu-calculus (i.e. extended with parametric polymorphism) is presented in

@article{parigot_1997,
	title = {Proofs of strong normalisation for second order classical natural deduction},
	volume = {62},
	doi = {10.2307/2275652},
	number = {4},
	journal = {Journal of Symbolic Logic},
	author = {Parigot, Michel},
	year = {1997},
	pages = {1461--1479}
}

• A call-by-value version of \lambda\mu, along with an extension with recursion, is given in

@inproceedings{ong__1997,
	title = {A {Curry}-{Howard} foundation for functional computation with control},
	doi = {10.1145/263699.263722},
	booktitle = {Proceedings of the 24th {ACM} {SIGPLAN}-{SIGACT} {Symposium} on {Principles} of {Programming} {Languages}  - {POPL} '97},
	publisher = {ACM Press},
	author = {Ong, C.-H. L. and Stewart, C. A.},
	year = {1997},
	pages = {215--227}
}

• The following paper works out the minimal classical logic that corresponds to the original presentation of \lambda\mu-calculus by Parigot:
• Fine distinctions between classical axioms in a minimal/implicational setting are made in

@inproceedings{ariola_2003,
	address = {Berlin, Heidelberg},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Minimal {Classical} {Logic} and {Control} {Operators}},
	volume = {2719},
	doi = {10.1007/3-540-45061-0_68},
	booktitle = {Automata, {Languages} and {Programming}},
	publisher = {Springer Berlin Heidelberg},
	author = {Ariola, Zena M. and Herbelin, Hugo},
	editor = {Baeten, Jos C. M. and Lenstra, Jan Karel and Parrow, Joachim and Woeginger, Gerhard J.},
	year = {2003},
	pages = {871--885}
}