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. 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.
Semantically these operators correspond to continuations found in some functional programming languages.
Read more about Lambda-mu Calculus: Formal Definition, Reduction
Famous quotes containing the word calculus:
“I try to make a rough music, a dance of the mind, a calculus of the emotions, a driving beat of praise out of the pain and mystery that surround me and become me. My poems are meant to make your mind get up and shout.”
—Judith Johnson Sherwin (b. 1936)