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].
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:
{ ... } are backtracked/reverted/rolled-back when the block is over.{ ... } 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 [the state] at any one time.
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
where 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 arise from actual programs.
However, should we wish to break things, given any such we could define its snapback $\textsf{snapback}(f) : A \times \mathbb{S} \to B \times \mathbb
This is a version of that has been 'booby-trapped': it returns the same value of as output, but reverts the state to the original one (instead of returning the new state . Of course, this version would never arise as the actual denotation of a program!
O’Hearn, P. W., and R. D. Tennent. 1995. ‘Parametricity and Local Variables’. Journal of the ACM 42 (3): 658–709. https://doi.org/10.1145/210346.210425.
@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}
}
Møgelberg, Rasmus, and Sam Staton. 2014. ‘Linear Usage of State’. Logical Methods in Computer Science 10 (1): 17. https://doi.org/10.2168/LMCS-10(1:17)2014.
@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},
}