Misplaced Pages

Lambda-mu calculus: Difference between revisions

Article snapshot taken from Wikipedia with creative commons attribution-sharealike license. Give it a read and then ask your questions in the chat. We can research this topic together.
Browse history interactively← Previous editNext edit →Content deleted Content addedVisualWikitext
Revision as of 14:30, 18 May 2009 editRadjenef (talk | contribs)394 editsm →External links: stylistic changes← Previous edit Revision as of 15:22, 18 May 2009 edit undoRadjenef (talk | contribs)394 edits →Reduction: section createdNext edit →
Line 17: Line 17:
#<tt>t</tt> is a named term, where <tt>α</tt> is a μ-variable and <tt>t</tt> is an unnamed term. #<tt>t</tt> is a named term, where <tt>α</tt> is a μ-variable and <tt>t</tt> is an unnamed term.
#<tt>(μ α. E)</tt> is an unnamed term, where <tt>α</tt> is a μ-variable and <tt>E</tt> is a named term. #<tt>(μ α. E)</tt> is an unnamed term, where <tt>α</tt> is a μ-variable and <tt>E</tt> is a named term.

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

{| class="wikitable" border="1" width="500"
|-
| logical reduction
| <math>(\lambda x.u)v \; \triangleright_c \; u</math>
|-
| structural reduction
| <math>(\mu \beta.u)v \; \triangleright_c \; \mu \beta.u \left (w v)/ w \right ]</math>
|-
| renaming
| <math> \mu \beta.u \; \triangleright_c \; u </math>
|-
| the equivalent of η-reduction
| <math>\mu \alpha.u \; \triangleright_c \; u</math>, for α not freely occurring in u
|}

These rules cause the calculus to be ]. Further reduction rules could be added to provide us with a stronger notion of normal form, though this would be at the expense of confluence.


==See Also== ==See Also==

Revision as of 15:22, 18 May 2009

In mathematical logic and computer science, the lambda-mu calculus is an extension of the lambda calculus, and was introduced by M. Parigot. It introduces two new operators: the mu operator (which is completely different both from the mu operator found in computability theory and from the μ operator of modal μ-calculus) and the bracket operator.

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 the law of noncontradiction, or Peirce's law.

Semantically these operators correspond to continuations found in some functional programming languages.

Formal definition

We can augment the definition of a lambda expression to gain one in the context of lambda-mu calculus. The three main expressions found in lambda calculus are as follows:

  1. V, a variable, where V is any identifier.
  2. λV.E, an abstraction, where V is any identifier and E is any lambda expression.
  3. (E E′), an application, where E and E′ are any lambda expressions.

For details, see the corresponding article.

In addition to the traditional λ-variables, the lambda-mu calculus includes a distinct set of μ-variables. These μ-variables can be used to name or freeze arbitrary subterms, allowing us to later abstract on those names. The set of terms contains 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. t is a named term, where α is a μ-variable and t is an unnamed term.
  2. (μ α. E) is an unnamed term, where α is a μ-variable and E is a named term.

Reduction

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

logical reduction ( λ x . u ) v ▹ c u [ v / x ] {\displaystyle (\lambda x.u)v\;\triangleright _{c}\;u}
structural reduction ( μ β . u ) v ▹ c μ β . u [ [ β ] ( w v ) / [ β ] w ] {\displaystyle (\mu \beta .u)v\;\triangleright _{c}\;\mu \beta .u\left(wv)/w\right]}
renaming [ α ] μ β . u ▹ c u [ α / β ] {\displaystyle \mu \beta .u\;\triangleright _{c}\;u}
the equivalent of η-reduction μ α . [ α ] u ▹ c u {\displaystyle \mu \alpha .u\;\triangleright _{c}\;u} , for α not freely occurring in u

These rules cause the calculus to be confluent. Further reduction rules could be added to provide us with a stronger notion of normal form, though this would be at the expense of confluence.

See Also

References

  1. Michel Parigot. λμ-Calculus: An algorithmic interpretation of classical natural deduction. Lecture Notes in Computer Science, Volume 624, pages 190-201, 1992.

External links

  • Lambda-mu relevant discussion on Lambda the Ultimate.
Stub icon

This mathematics-related article is a stub. You can help Misplaced Pages by expanding it.

Categories: