Lambda-mu calculus

From Wikipedia, the free encyclopedia

In mathematical logic and computer science, the lambda-mu calculus is an extension of the lambda calculus, and was introduced by M. Parigot in [lambda-mu]calculus: an algorithmic interpretation of classical natural deduction, Springer LNAI no. 624 (1992). 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.

[edit] 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 these, lambda-mu calculus adds:

1. [α]E, sometimes called freeze, where α is a variable but of a disjoint set from those in 1.
2. (μ α. E), sometimes called unfreeze

[edit] External links

• [1]