Lambda-mu calculus

In mathematical logic and computer science, the lambda-mu calculus is an extension of the lambda calculus introduced by Michel Parigot.¹ It introduces two new operators: the μ operator (which is completely different both from the μ operator found in computability theory and from the μ operator of modal μ-calculus) and the bracket operator. Proof-theoretically, it provides a well-behaved formulation of classical natural deduction.

One of the main goals of this extended calculus is to be able to describe expressions corresponding to theorems in classical logic. According to the Curry–Howard isomorphism, lambda calculus on its own can express theorems in intuitionistic logic only, and several classical logical theorems can't be written at all. However with these new operators one is able to write terms that have, for example, the type of Peirce's law.

According to de Groote, the μ operator corresponds to Felleisen's undelimited control operator C and bracket corresponds to calling a captured continuation.²

The three forms of expressions in lambda calculus are as follows:

1. A variable x.
2. An abstraction λx. M, where x is any variable and M is any lambda expression.
3. An application (M N), where M and N are any lambda expressions.

In addition to the traditional λ-variables, the lambda-mu calculus includes a distinct set of μ-variables, which can be understood as continuation variables. The set of terms is divided into unnamed (all traditional lambda expressions are of this kind) and named terms. The terms that are added by the lambda-mu calculus are of the form:

1. [α]M is a named term, where α is a μ-variable and M is an unnamed term.
2. (μ α. t) is an unnamed term, where α is a μ-variable and t is a named term.

The basic reduction rules used in the lambda-mu calculus are the following:

beta reduction

${\displaystyle (\lambda x.M)N\to M[N/x]}$

structural reduction

${\displaystyle (\mu \alpha .t)M\to \mu \alpha .t\left[[\alpha ](NM)/[\alpha ]N\right]}$, where the substitutions are to be made for all subterms of ${\displaystyle t}$ of the form ${\displaystyle [\alpha ]N}$.

renaming

${\displaystyle [\alpha ]\mu \beta .t\to t[\alpha /\beta ]}$

μη-reduction

${\displaystyle \mu \alpha .[\alpha ]M\to M}$, if α does not occur freely in M

These rules cause the calculus to be confluent.

The lambda-mu calculus can be typed. The basic theory of the typed lambda-mu calculus is to classical propositional logic as the simply typed lambda calculus is to intuitionistic propositional logic.³

Typed lambda-mu calculus can be presented in sequent calculus:^{3: Figure 6.2}$${\displaystyle {\begin{aligned}\Gamma ,x\mathbin {:} \tau &\vdash x\mathbin {:} \tau \\\\{\frac {\Gamma ,x\mathbin {:} \sigma \vdash M\mathbin {:} \tau }{\Gamma \vdash (\lambda x\mathbin {:} \sigma .M)\mathbin {:} \sigma \to \tau }}&\quad {\frac {\Gamma ,\vdash M\mathbin {:} \sigma \to \tau \quad \Gamma \vdash N\mathbin {:} \sigma }{\Gamma \vdash (MN)\mathbin {:} \tau }}\\\\{\frac {\Gamma ,\alpha \mathbin {:} \neg \sigma \vdash M\mathbin {:} \bot }{\Gamma \vdash (\mu \alpha \mathbin {:} \neg \sigma .M)\mathbin {:} \sigma }}&\quad {\frac {\Gamma ,\alpha \mathbin {:} \neg \sigma \vdash M\mathbin {:} \sigma }{\Gamma ,\alpha \mathbin {:} \neg \sigma \vdash ([\alpha ]M)\mathbin {:} \bot }}\end{aligned}}}$$The first 3 rules are the same as simply typed lambda calculus. The next 2 are new to the lambda-mu calculus.

Simply typed lambda calculus, by the Curry–Howard correspondence, corresponds to purely functional programs that can only redirect their inputs.

A sequent ${\displaystyle \Gamma \vdash t:\tau }$ states that, within a program context ${\displaystyle \Gamma }$, one can construct an object ${\displaystyle t}$ of type ${\displaystyle \tau }$.

The rule ${\displaystyle \Gamma ,x\mathbin {:} \tau \vdash x\mathbin {:} \tau }$ states that, within a context that includes some ${\displaystyle x:\tau }$, one can construct an object ${\displaystyle x}$ with type ${\displaystyle \tau }$. This is obvious, by simply taking that same ${\displaystyle x:\tau }$.

The lambda-introduction rule ${\displaystyle {\frac {\Gamma ,x\mathbin {:} \sigma \vdash M\mathbin {:} \tau }{\Gamma \vdash (\lambda x\mathbin {:} \sigma .M)\mathbin {:} \sigma \to \tau }}}$ states that, if one can construct ${\displaystyle M:\tau }$ within a context of ${\displaystyle \Gamma ,x\mathbin {:} \tau }$, then one can construct ${\displaystyle (\lambda x:\sigma .M):\sigma \to \tau }$ within a context of ${\displaystyle \Gamma }$. This object ${\displaystyle (\lambda x:\sigma .M)}$ is a function-object defined within the context of ${\displaystyle \Gamma }$. It takes an object ${\displaystyle x:\sigma }$ as input, and internally reproduces the context of ${\displaystyle \Gamma ,x\mathbin {:} \tau }$, in which one then constructs ${\displaystyle M:\tau }$. This is a form of closure.

The lambda-reduction rule ${\displaystyle {\frac {\Gamma ,\vdash M\mathbin {:} \sigma \to \tau \quad \Gamma \vdash N\mathbin {:} \sigma }{\Gamma \vdash (MN)\mathbin {:} \tau }}}$ is a reverse of the previous rule.

The typed lambda-mu calculus is similar to the simply typed lambda calculus, but it allows redirecing both the inputs and the outputs. The redirection of input is by lambda abstraction, or closure. The redirection of output is by mu abstraction, or call/cc, jumps, or control operators.

The negation symbol ${\displaystyle \neg }$ denotes duality. Whereas ${\displaystyle x:\sigma }$ in the program context denotes an input from which an object with type ${\displaystyle \sigma }$ appears, ${\displaystyle \alpha :\neg \sigma }$ denotes an output for an object with type ${\displaystyle \sigma }$ goes to.

${\displaystyle M:\bot }$ denotes a computational process that does not return any value, because its value would be returned to an output in context.

The address abstraction rule ${\displaystyle {\frac {\Gamma ,\alpha \mathbin {:} \neg \sigma \vdash M\mathbin {:} \bot }{\Gamma \vdash (\mu \alpha \mathbin {:} \neg \sigma .M)\mathbin {:} \sigma }}}$ closes an output from context. This corresponds to catch in call/cc.

The address application rule ${\displaystyle {\frac {\Gamma ,\alpha \mathbin {:} \neg \sigma \vdash M\mathbin {:} \sigma }{\Gamma ,\alpha \mathbin {:} \neg \sigma \vdash ([\alpha ]M)\mathbin {:} \bot }}}$ redirects the output of a process ${\displaystyle M:\sigma }$ to the output ${\displaystyle \alpha }$ in context. This corresponds to throw in call/cc.

The ${\displaystyle \mu }$ is a channel device. The address ${\displaystyle \alpha :\neg p}$ is a channel that values of type ${\displaystyle p}$ can be transmitted along, and ${\displaystyle [\alpha ]M}$ represents transmittal of ${\displaystyle M}$ to ${\displaystyle \alpha }$, provided that ${\displaystyle M}$ is of type ${\displaystyle p}$.^3: 134

Peirce's law ${\displaystyle ((p\to q)\to p)\to p}$ is the type of the following term:$${\displaystyle \lambda x^{(p\to q)\to p}.\mu \alpha ^{\neg p}.[\alpha ]x(\lambda y^{p}.\mu \beta ^{\neg q}.[\alpha ]y)}$$where we write ${\displaystyle x^{\tau }}$ for ${\displaystyle x:\tau }$, in order to save space.

Intuitively, one can understand this construction as follows. The program opens an input context ${\displaystyle x:(p\to q)\to p}$, and an output context ${\displaystyle \alpha :\neg p}$. One way to satisfy the output requirement of ${\displaystyle \alpha :\neg p}$ is to construct something of type ${\displaystyle p\to q}$, and give it to ${\displaystyle x}$. That something is ${\displaystyle \lambda y^{p}.\mu \beta ^{\neg q}.[\alpha ]y:p\to q}$. If ${\displaystyle x}$ takes this object without trying to use it, then it will return an object of type ${\displaystyle p}$, which can then be given to ${\displaystyle \alpha }$. Alternatively, ${\displaystyle x}$ might attempt to use it by providing it with an object ${\displaystyle y:p}$, which can then be given to ${\displaystyle \alpha }$ without ever replying an object of type ${\displaystyle q}$ to ${\displaystyle x}$.

The Łukasiewicz axiom is the type of the following term:$${\displaystyle \lambda x^{(p\to q)\to r}\lambda y^{r\to p}.\lambda z^{s}.\mu \alpha ^{\neg p}.[\alpha ]y(\mu \beta ^{\neg r}.[\beta ]x(\lambda u^{p}.\mu \gamma ^{\neg q}.[\alpha ]u))}$$The double-negation translation corresponds to continuation-passing style. That is, the double-negation translation turns every formula provable in classical propositional logic into a provable formula in intuitionistic propositional logic. This corresponds to converting a program with catch/throw into a purely functional program that uses continuation-passing.^{3: Sec. 6.4}

For example, the double-negation translation of Peirce's law ${\displaystyle ((\neg \neg p\to \neg \neg q)\to \neg \neg p)\to \neg \neg p}$ is the type of the following term:$${\displaystyle \lambda x^{(\neg \neg p\to \neg \neg q)\to \neg \neg p}.\lambda \alpha ^{\neg p}x(\lambda y^{\neg \neg p}.\lambda \beta ^{\neg q}.y\alpha )\alpha }$$Compare these two, in parallel:$${\displaystyle {\begin{aligned}&\lambda x^{(p\to q)\to p}.&\mu \alpha ^{\neg p}.[\alpha ]&x(\lambda y^{p}.&\mu \beta ^{\neg q}.[\alpha ]&y)\\&\lambda x^{(\neg \neg p\to \neg \neg q)\to \neg \neg p}.&\lambda \alpha ^{\neg p}.\quad \;&x(\lambda y^{\neg \neg p}.&\lambda \beta ^{\neg q}.y\alpha )\alpha \end{aligned}}}$$The "jump to a different output" control behavior, as defined by ${\displaystyle \mu \alpha \cdots [\alpha ]}$, is translated into a pure lambda expression ${\displaystyle \lambda \alpha \cdots \alpha }$. Instead of allowing a jump to the address ${\displaystyle \alpha :\neg p}$, one encodes the entire "the rest of the computation after the jumping to ${\displaystyle \alpha :\neg p}$" as a single object, called the continuation object. This continuation object can then be called for as many times as one wants, as long as that continuation object remains in context.

To obtain call-by-value semantics, one must refine the beta reduction rule and add another form of structural reduction:⁴

call-by-value beta reduction

${\displaystyle (\lambda x.M)V\to M[V/x]}$, where V is a value

right structural reduction

${\displaystyle V(\mu \alpha .t)\to \mu \alpha .t\left[[\alpha ](VN)/[\alpha ]N\right]}$, where V is a value

This addition corresponds to the addition of an additional evaluation context former when moving from call-by-name to call-by-value evaluation.

For a closer correspondence with conventional formalizations of control operators, the distinction between named and unnamed terms can be abolished, meaning that [α]M is of the same sort as other lambda-expressions and the body of μ-abstraction can also be any expression.² Another variant in this vein is the Λμ-calculus.⁵

One can consider a structural reduction rule symmetric to the original one:¹

${\displaystyle M(\mu \alpha .t)\to \mu \alpha .t\left[[\alpha ](MN)/[\alpha ]N\right]}$

This, however, breaks confluence and the correspondence to control operators.