lambda-mu-calculus
The -calculus is a term assignment system for classical natural deduction.
1. syntax
This syntax is consistent throughout the literature, with one major exception: (Philippe de Groote, 1994) does not distinguish syntactically between terms and commands.
The English terminology we use here is adapted from other developments. Sources on the -calculus itself write “ -variables” instead of “variables”, “ -variables” instead of “covariables”, “unnamed terms” instead of “terms”, and “named terms” instead of “commands”.
2. types
The notation for typing assumptions and judgments varies significantly across the literature; I will endeavor to list them all.
The main factor that distinguishes different notations is how to type covariables. Broadly, there are two
There are two kinds of typing assumptions: one for -variables and one for -variables. In (Michel Parigot, 1992, Zena M. Ariola and Hugo Herbelin, 2003), these are written the same way; e.g., and , even though represents not a value of type , but a continuation that expects a value of type .1
- Typing judgments for
cite:@Abel01 uses a different notation. In their notation, every typing judgment has the form . Typing assumptions for -variables are written and moved into the context . Typing judgments for commands are written . Here, is the cotype of
3. semantics
The original semantics for the -calculus corresponds to call-by-name, but there is another semantics corresponding to call-by-value.
3.1. structural substitution
Both semantics make use of a structural substitution operation, here written which means “in , replace every subterm of the form with the term .”
originally written something like You can read this as “replace every subterm of the form with the term ”.
This notation is rather awful.
- It uses square brackets for both commands and substitution.
- It does not immediately read as a substitution, since the slash is buried in the middle between two complex expressions.
- It binds as a metavariable without any indication that this is happening.
Authors have found various solutions to this problem.
4. Curry-Howard
Strictly speaking, the -calculus corresponds to
5. footnotes
Footnotes:
Actually, their concrete notation is rather non-standard. Typing assumptions are written like rather than , and typing judgments for terms are written like .