In
mathematical logic
Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of for ...
and
computer science
Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to Applied science, practical discipli ...
, the lambda-mu calculus is an extension of the
lambda calculus
Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation ...
introduced by M. Parigot.
It introduces two new operators: the μ operator (which is completely different both from the
μ operator
In computability theory, the μ-operator, minimization operator, or unbounded search operator searches for the least natural number with a given property. Adding the μ-operator to the five primitive recursive operators makes it possible to define ...
found in
computability theory
Computability theory, also known as recursion theory, is a branch of mathematical logic, computer science, and the theory of computation that originated in the 1930s with the study of computable functions and Turing degrees. The field has since e ...
and from the μ operator of
modal μ-calculus In theoretical computer science, the modal μ-calculus (Lμ, Lμ, sometimes just μ-calculus, although this can have a more general meaning) is an extension of propositional modal logic (with many modalities) by adding the least fixed point opera ...
) 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
Classical logic (or standard logic or Frege-Russell logic) is the intensively studied and most widely used class of deductive logic. Classical logic has had much influence on analytic philosophy.
Characteristics
Each logical system in this class ...
. According to the
Curry–Howard isomorphism, lambda calculus on its own can express theorems in
intuitionistic logic
Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems ...
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
In logic, Peirce's law is named after the philosopher and logician Charles Sanders Peirce. It was taken as an axiom in his first axiomatisation of propositional logic. It can be thought of as the law of excluded middle written in a form that i ...
.
Semantically these operators correspond to
continuations
In computer science, a continuation is an abstract representation of the control state of a computer program. A continuation implements ( reifies) the program control state, i.e. the continuation is a data structure that represents the computati ...
, found in some
functional programming languages
In computer science, functional programming is a programming paradigm where programs are constructed by applying and composing functions. It is a declarative programming paradigm in which function definitions are trees of expressions that m ...
.
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:
#, a ''variable'', where ''V'' is any
identifier
An identifier is a name that identifies (that is, labels the identity of) either a unique object or a unique ''class'' of objects, where the "object" or class may be an idea, physical countable object (or class thereof), or physical noncountable ...
.
#, an ''abstraction'', where ''V'' is any identifier and ''E'' is any lambda expression.
#, 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:
# is a named term, where ''α'' is a μ-variable and ''t'' is an unnamed term.
# 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
: