Lambda-mu calculus

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.

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

logical reduction

${\displaystyle (\lambda x.u)v\;\triangleright _{c}\;u[v/x]}$

structural reduction

${\displaystyle (\mu \beta .u)v\;\triangleright _{c}\;\mu \beta .u\left[[\beta ](wv)/[\beta ]w\right]}$

renaming

${\displaystyle [\alpha ]\mu \beta .u\;\triangleright _{c}\;u[\alpha /\beta ]}$

the equivalent of η-reduction

${\displaystyle \mu \alpha .[\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.

• Classical pure type systems for typed generalizations of lambda calculi with control

• Lambda-mu relevant discussion on Lambda the Ultimate.