\nu-calculus

The \nu-calculus is a minimal extension of the call-by-value simply-typed \lambda-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 \nu-calculus is closely related to Stoughton's identity calculus.

Syntax

The judgements of \nu-calculus are similar to those of the simply-typed \lambda-calculus, but - in addition to the usual context - they also carry a set of names n:

n \mid \Gamma \vdash M : A

All the usual rules are parametric in n. Names have their own type \nu, and can be returned as values:

\frac{
}{
  s, n \mid \Gamma \vdash n : \nu
}

The new typing rules are:

• the equality comparison, which compares two names and returns a boolean:

  \frac{
    s \mid \Gamma \vdash M : \nu
    \qquad
    s \mid \Gamma \vdash N : \nu
  }{
    s \mid \Gamma \vdash M = N : \textsf{Bool}
  }
  

• the name abstraction, which binds a new name in its continuation:

  \frac{
    s, a \mid \Gamma \vdash M : A
  }{
    s \mid \Gamma \vdash \nu a. M : A
  }
  

The usual provisos about \alpha-conversion and a being fresh for s 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.

Operational semantics

The operational semantics of the \nu-calculus takes the form

n \vdash M \Downarrow (n')V

This judgement means that running M with the names in n having been allocated returns the value V after further allocation of the names in n'.

Comparison to Odersky's \lambda\nu-calculus

The \nu-calculus should not be confused with Odersky's \lambda\nu-calculus.

The main differences seem to be about evaluation order.

• The \nu-calculus is call-by-value, and hence more a programming language. Pitts 2013 says:

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 type unit ref of references to the unit value and taking \nu a. e to be let a = ref() in e. The properties of contextual equivalence for the ν-calculus turn out to be remarkably complex, despite the simplicity of the language.

• The \lambda\nu-calculus is untyped and call-by-name, and hence quite different. Stark 1994 says:

Odersky has developed a theory \lambda\nu that extends the lambda-calculus with a binding construct for local names 20, and proves that the theory of observable equivalence in \lambda\nu is a conservative extension of that for the lambda-calculus. Syntactically this language appears similar to the nu-calculus; differences are that \lambda\nu 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.

References

• The \nu-calculus appears to have been introduced in

@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},
}

• A textbook presentation of the \nu-calculus may be found in Section 9.6 of

@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},
}

• A survey of the literature on the \nu-calculus may be found in

@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}
}

• A categorical semantics for \lambda\nu has been presented in

@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}
}