Lambda-mu calculus

Curry–Howard correspondence

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

Examples

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.

Call-by-value lambda-mu calculus

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

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.

De Groote's unstratified syntax

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.^[2] Another variant in this vein is the Λμ-calculus.^[5]

Symmetric lambda-mu calculus

One can consider a structural reduction rule symmetric to the original one:^[1]

${\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.