Lambda-mu calculus

Quality 0.50 · 3 views · Updated 2 months ago

Extension of lambda calculus

title: "Lambda-mu calculus" type: doc version: 1 created: 2026-02-28 author: "Wikipedia contributors" status: active scope: public tags: ["lambda-calculus", "proof-theory"] description: "Extension of lambda calculus" topic_path: "science/mathematics" source: "https://en.wikipedia.org/wiki/Lambda-mu_calculus" license: "CC BY-SA 4.0" wikipedia_page_id: 0 wikipedia_revision_id: 0

::summary 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. 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 the type of, for example, Peirce's law.

The μ operator corresponds to Felleisen's undelimited control operator and bracket corresponds to calling a captured continuation.{{cite conference | last = de Groote | first = Philippe | editor-last = Pfenning | editor-first = Frank | contribution = On the relation between the λμ-calculus and the syntactic theory of sequential control | doi = 10.1007/3-540-58216-9_27 | pages = 31–43 | publisher = Springer | series = Lecture Notes in Computer Science | title = Logic Programming and Automated Reasoning, 5th International Conference, LPAR'94, Kiev, Ukraine, July 16–22, 1994, Proceedings | volume = 822 | year = 1994| isbn = 978-3-540-58216-8

Formal definition

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

  1. A variable , where x is any identifier.
  2. An abstraction , where x is any identifier and M is any lambda expression.
  3. An application , 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. is a named term, where α is a μ-variable and M is an unnamed term.
  2. 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 : (\lambda x.M)N \to M[N/x] ; structural reduction : (\mu \alpha.t)M \to \mu \alpha. t \left [ [\alpha](N M)/[\alpha] N \right ], where the substitutions are to be made for all subterms of t of the form [\alpha]N. ; renaming : [\alpha] \mu \beta. t \to t [\alpha / \beta] ; μη-reduction : \mu \alpha.[\alpha]M \to M, if α does not occur freely in M

These rules cause the calculus to be 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:

;call-by-value beta reduction : (\lambda x.M) V \to M[V/x], where V is a value ; right structural reduction : V (\mu \alpha.t) \to \mu \alpha. t \left [ [\alpha](V N)/[\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. Another variant in this vein is the Λμ-calculus.{{cite conference | last = Saurin | first = Alexis | contribution = Separation with Streams in the λμ-calculus | doi = 10.1109/LICS.2005.48 | pages = 356–365 | publisher = IEEE Computer Society | title = 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26–29 June 2005, Chicago, IL, USA, Proceedings | year = 2005}}

Symmetric lambda-mu calculus

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

M(\mu \alpha.t) \to \mu \alpha. t \left [ \alpha/[\alpha] N \right ]

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

References

References

  1. Michel Parigot. (1992). "λμ-Calculus: An algorithmic interpretation of classical natural deduction.".
  2. (1997-01-01). "Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '97". Association for Computing Machinery.

::callout[type=info title="Wikipedia Source"] This article was imported from Wikipedia and is available under the Creative Commons Attribution-ShareAlike 4.0 License. Content has been adapted to SurfDoc format. Original contributors can be found on the article history page. ::

lambda-calculusproof-theory