Snapback

The term snapback is used to refer to models of languages with both blocks and variables. Such a language has a snapback semantics when changes to memory are reverted when a block closes. This kind of behaviour is not common in a programming language, but it is a pernicious problem in semantics.

The term snapback appears to have been introduced by O'Hearn and Tennent 1995.

Example

In a language with snapback semantics, the program

x = 0;
{
  x = x + 1;
  print(x);
}
print(x);

first prints 1 and then 0. There are multiple ways to think of this:

• Any changes to global memory that happen within the block { ... } are backtracked/reverted/rolled-back when the block is over.
• The block { ... } creates a local copy of x, which it then uses. The local copy is discarded as soon as the block is over.

One thing is certain: this is not the way imperative languages work! Quoth Strachey from 1972:

The state transformation produced by obeying a command is essentially irreversible and it is, by the nature of the computers we use, impossible to have more than one version of \sigma the state at any one time.

Through the state-passing translation

This perspective comes from Staton and Møgelberg 2014. In any language that has a form of state, a function f : A \to B may be modelled as a pure mathematical function

  f : A \times \mathbb{S} \to B \times \mathbb{S}

where \mathbb{S} is a set of states. We can call this the state-passing translation. It is a way of modelling any impure programming language with functions in a mathematical fashion. It is evident that only a very restricted set of these functions f : A \times \mathbb{S} \to B \times \mathbb{S} arise from actual programs.

However, should we wish to break things, given any such f we could define its snapback $\textsf(f) : A \times \mathbb \to B \times \mathbb

\textsf{snapback}(f)(a, s) \triangleq (out, s) \text{ where } (out, s') = f(a, s)

This is a version of f that has been 'booby-trapped': it returns the same value of B as output, but reverts the state to the original one (instead of returning the new state s'. Of course, this version would never arise as the actual denotation of a program!

References

• The term snapback appears to be due to

@article{ohearn_parametricity_1995,
	title = {Parametricity and local variables},
	volume = {42},
	doi = {10.1145/210346.210425},
	number = {3},
	journal = {Journal of the ACM},
	author = {O'Hearn, P. W. and Tennent, R. D.},
	year = {1995},
	pages = {658--709}
}

@article{mogelberg_linear_2014,
	title = {Linear usage of state},
	volume = {10},
	doi = {10.2168/LMCS-10(1:17)2014},
	number = {1},
	journal = {Logical Methods in Computer Science},
	author = {Møgelberg, Rasmus and Staton, Sam},
	year = {2014},
	pages = {17},
}