View source for Lambda-mu calculus

{{Short description|Extension of lambda calculus}}
In [[mathematical logic]] and [[computer science]], the '''lambda-mu calculus''' is an extension of the [[lambda calculus]] introduced by Michel Parigot.<ref name=":0">{{cite book |title=λμ-Calculus: An algorithmic interpretation of classical natural deduction. |author=Michel Parigot |series=Lecture Notes in Computer Science |volume=624| pages=190–201 |year=1992|doi=10.1007/BFb0013061 |isbn=3-540-55727-X }}</ref> 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 theory|Proof-theoretically]], it provides a well-behaved formulation of [[Natural deduction#Classical and modal logics|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&ndash;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 the type of, for example, [[Peirce's law]].

The μ operator corresponds to [[Matthias Felleisen|Felleisen]]'s undelimited control operator {{Mathcal|C}}  and bracket corresponds to calling a captured [[continuation]].<ref name=":1">{{Cite journal |last=Groote |first=Philippe de |date=1994-07-16 |title=On the Relation between the Lambda-Mu-Calculus and the Syntactic Theory of Sequential Control |url=https://dl.acm.org/doi/10.5555/645708.664169 |journal=Proceedings of the 5th International Conference on Logic Programming and Automated Reasoning |series=LPAR '94 |volume=822 |location=Berlin, Heidelberg |publisher=Springer-Verlag |pages=31–43 |doi=10.1007/3-540-58216-9_27 |isbn=978-3-540-58216-8}}</ref>

==Formal definition==

The three forms of expressions in [[lambda calculus]] are as follows:
#A ''variable'' {{mono|x}}, where ''x'' is any [[identifier]].
#An ''abstraction'' {{mono|λx. M}}, where ''x'' is any identifier and ''M'' is any lambda expression.
#An ''application'' {{mono|(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:
#{{mono|[α]M}} is a named term, where ''α'' is a μ-variable and ''M'' is an unnamed term.
#{{mono|(μ α. t)}} is an unnamed term, where ''α'' is a μ-variable and ''t'' is a named term.

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

; beta reduction
: <math>(\lambda x.M)N \to M[N/x]</math>
; structural reduction
: <math>(\mu \alpha.t)M \to \mu \alpha. t \left [ [\alpha](N M)/[\alpha] N \right ]</math>, where the substitutions are to be made for all subterms of <math>t</math> of the form <math>[\alpha]N</math>.
; renaming
: <math>[\alpha] \mu \beta. t  \to t [\alpha / \beta]</math>
; μη-reduction
: <math>\mu \alpha.[\alpha]M \to M</math>, if ''α'' does not occur freely in ''M''

These rules cause the calculus to be [[Confluence (term rewriting)|confluent]].

== Variations ==

=== 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:<ref>{{Cite book |last1=Ong |first1=C.-H. L. |last2=Stewart |first2=C. A. |chapter=A Curry-Howard foundation for functional computation with control |date=1997-01-01 |title=Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '97 |chapter-url=https://dl.acm.org/doi/10.1145/263699.263722 |location=New York, NY, USA |publisher=Association for Computing Machinery |pages=215–227 |doi=10.1145/263699.263722 |isbn=978-0-89791-853-4}}</ref>

;call-by-value beta reduction
: <math>(\lambda x.M) V \to M[V/x]</math>, where ''V'' is a value
; right structural reduction
: <math>V (\mu \alpha.t) \to \mu \alpha. t \left [ [\alpha](V N)/[\alpha] N \right ]</math>, where ''V'' is a value

This addition corresponds to the addition of an additional [[Operational semantics|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.<ref name=":1" /> Another variant in this vein is the Λμ-calculus.<ref>{{Cite book |last=Saurin |first=Alexis |chapter=Separation with Streams in the ?µ-calculus |date=2005-06-26 |title=20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05) |chapter-url=https://dl.acm.org/doi/10.1109/LICS.2005.48 |series=LICS '05 |location=USA |publisher=IEEE Computer Society |pages=356–365 |doi=10.1109/LICS.2005.48 |isbn=978-0-7695-2266-1}}</ref>

=== Symmetric lambda-mu calculus ===
One can consider a structural reduction rule symmetric to the original one:<ref name=":0" />

<math>M(\mu \alpha.t) \to \mu \alpha. t \left [ [\alpha](MN)/[\alpha] N \right ]</math>

This, however, breaks [[Confluence (abstract rewriting)|confluence]] and the correspondence to control operators.

==See also==
* Classical [[pure type system|pure type systems]] for typed generalizations of lambda calculi with control

==References==
{{reflist|1}}

==External links==
* [http://lambda-the-ultimate.org/node/811 Lambda-mu] relevant discussion on Lambda the Ultimate.

[[Category:Lambda calculus]]
[[Category:Proof theory]]