Lambda-mu calculus

Lambda-mu calculus

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.

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:
#V, a variable, where V is any identifier.
#(λ V. E), an abstraction, where "V" is any identifier and "E" is any lambda expression.
#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:
# [α] E, sometimes called freeze, where α is a variable but of a disjoint set from those in 1.
#(μ α. E), sometimes called unfreeze

External links

* [http://lambda-the-ultimate.org/node/811]


Wikimedia Foundation. 2010.

Игры ⚽ Нужна курсовая?

Look at other dictionaries:

  • Lambda calculus — In mathematical logic and computer science, lambda calculus, also written as λ calculus, is a formal system designed to investigate function definition, function application and recursion. It was introduced by Alonzo Church and Stephen Cole… …   Wikipedia

  • Calculus of variations — is a field of mathematics that deals with extremizing functionals, as opposed to ordinary calculus which deals with functions. A functional is usually a mapping from a set of functions to the real numbers. Functionals are often formed as definite …   Wikipedia

  • Lambda — (uppercase Λ, lowercase λ; el. Λάμβδα or el. Λάμδα, Lamda) is the 11th letter of the Greek alphabet. In the system of Greek numerals it has a value of 30. It was derived from the Phoenician letter Lamed the name of the letter, Λάμδα, is… …   Wikipedia

  • Calculus (disambiguation) — Calculus is Latin for pebble, and has a number of meanings in English: In mathematics and computer science Calculus , in its most general sense, is any method or system of calculation. To modern theoreticians the answer to the question what is a… …   Wikipedia

  • Lambda-Calcul — « La notion de λ définissabilité fut la première de ce qui est accepté maintenant comme l équivalent exact des descriptions mathématiques pour lesquelles des algorithmes existent. »  Stephen Kleene, in Origins of Recursive Function …   Wikipédia en Français

  • Lambda calcul — « La notion de λ définissabilité fut la première de ce qui est accepté maintenant comme l équivalent exact des descriptions mathématiques pour lesquelles des algorithmes existent. »  Stephen Kleene, in Origins of Recursive Function …   Wikipédia en Français

  • Lambda Papers — Lambda the Ultimate Papers were written by Gerald Jay Sussman and Guy Steele Jr. in 1975 1978, questioning the then current practices in programming language implementations. The focus was on showing that programming languages can be implemented… …   Wikipedia

  • Lambda lifting — or closure conversion is the process of eliminating free variables from local function definitions from a computer program. The elimination of free variables allows the compiler to hoist local definitions out of their surrounding contexts into a… …   Wikipedia

  • Calculus of constructions — The calculus of constructions (CoC) is a higher order typed lambda calculus, initially developed by Thierry Coquand, where types are first class values. It is thus possible, within the CoC, to define functions from, say, integers to types, types… …   Wikipedia

  • Lambda cube — In mathematical logic and type theory, the λ cube is a framework for exploring the axes of refinement in Coquand s calculus of constructions, starting from the simply typed lambda calculus as the vertex of a cube placed at the origin, and the… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”