The -calculus is a minimal extension of the call-by-value simply-typed -calculus that supports the dynamic creation of names. These names are atomic things, which can only be checked for equality.
It was identified by Andy Pitts as a tiny subset of ML that models only the allocation of new memory cells (that do not hold any data!), so that this feature can be studied carefully. It turns out that this was a good choice, because this is already complicated enough.
The -calculus is closely related to Stoughton's identity calculus.
The judgements of -calculus are similar to those of the simply-typed -calculus, but - in addition to the usual context - they also carry a set of names :
All the usual rules are parametric in . Names have their own type , and can be returned as values:
The new typing rules are:
The usual provisos about -conversion and being fresh for apply (and are hugely important here).
The name abstraction rule coresponds to the ML statement
let n = ref () in M end
which generates a fresh reference of type unit ref
pointing to the trivial value ()
of unit
type.
The operational semantics of the -calculus takes the form
This judgement means that running with the names in having been allocated returns the value after further allocation of the names in .
The -calculus should not be confused with Odersky's -calculus.
The main differences seem to be about evaluation order.
Syntactically, the ν-calculus is the same simply-typed λ-calculus with locally scoped names that we used for Odersky’s λν-calculus (Figure 9.1). Unlike Odersky’s calculus, the ν-calculus is given an operational semantics that makes it a fragment of Standard ML (Milner et al., 1997) by interpreting the type
Name
as the ML typeunit ref
of references to the unit value and taking to belet a = ref() in e
. The properties of contextual equivalence for the ν-calculus turn out to be remarkably complex, despite the simplicity of the language.
Odersky has developed a theory that extends the lambda-calculus with a binding construct for local names [20], and proves that the theory of observable equivalence in is a conservative extension of that for the lambda-calculus. Syntactically this language appears similar to the nu-calculus; differences are that is untyped and has a call-by-name reduction strategy, with the possibility of ‘stuck’ terms. [...] Odersky works around the limited scope of names by using a continuation-passing style of programming.
Pitts, Andrew M., and Ian D. B. Stark. 1993. ‘Observable Properties of Higher Order Functions That Dynamically Create Local Names, or: What’s New?’ In Mathematical Foundations of Computer Science 1993, edited by Andrzej M. Borzyszkowski and Stefan Sokołowski, 711:122–41. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/3-540-57182-5_8. [pdf]
@inproceedings{borzyszkowski_observable_1993,
address = {Berlin, Heidelberg},
series = {Lecture {Notes} in {Computer} {Science}},
title = {Observable properties of higher order functions that dynamically create local names, or: {What}'s new?},
volume = {711},
doi = {10.1007/3-540-57182-5_8},
booktitle = {Mathematical {Foundations} of {Computer} {Science} 1993},
publisher = {Springer Berlin Heidelberg},
author = {Pitts, Andrew M. and Stark, Ian D. B.},
editor = {Borzyszkowski, Andrzej M. and Sokołowski, Stefan},
year = {1993},
pages = {122--141},
}
Pitts, Andrew M. 2013. Nominal Sets: Names and Symmetry in Computer Science. Cambridge University Press. https://doi.org/10.1017/CBO9781139084673. [pdf]
@book{pitts_2013,
title = {Nominal {Sets}: {Names} and {Symmetry} in {Computer} {Science}},
publisher = {Cambridge University Press},
author = {Pitts, Andrew M.},
year = {2013},
doi = {10.1017/CBO9781139084673},
}
Benton, Nick, and Vasileios Koutavas. 2012. ‘A Mechanized Bisimulation for the Nu-Calculus’. https://www.scss.tcd.ie/Vasileios.Koutavas/publications/nu-calc.pdf.
@misc{benton_2012,
title = {A {Mechanized} {Bisimulation} for the {Nu}-{Calculus}},
url = {https://www.scss.tcd.ie/Vasileios.Koutavas/publications/nu-calc.pdf},
author = {Benton, Nick and Koutavas, Vasileios},
year = {2012}
}
Stark, Ian. 1996. ‘Categorical Models for Local Names’. LISP and Symbolic Computation 9 (1): 77–107.
@article{stark_1996,
title = {Categorical {Models} for {Local} {Names}},
volume = {9},
url = {http://www.inf.ed.ac.uk/~stark/catmln.html},
number = {1},
journal = {LISP and Symbolic Computation},
author = {Stark, Ian},
month = feb,
year = {1996},
pages = {77--107}
}