A Complete NormalForm Bisimilarity for State
Abstract
We present a sound and complete bisimilarity for an untyped \(\lambda \)calculus with higherorder local references. Our relation compares values by applying them to a fresh variable, like normalform bisimilarity, and it uses environments to account for the evolving store. We achieve completeness by a careful treatment of evaluation contexts comprising open stuck terms. This work improves over Støvring and Lassen’s incomplete environmentbased normalform bisimilarity for the \(\lambda \rho \)calculus, and confirms, in relatively elementary terms, Jaber and Tabareau’s result, that the state construct is discriminative enough to be characterized with a bisimilarity without any quantification over testing arguments.
1 Introduction
Two terms are contextually equivalent if replacing one by the other in a bigger program does not change the behavior of the program. The quantification over program contexts makes contextual equivalence hard to use in practice and it is therefore common to look for more effective characterizations of this relation. In a calculus with local state, such a characterization has been achieved either through logical relations [1, 5, 15], which rely on types, denotational models [6, 10, 13], or coinductively defined bisimilarities [9, 12, 17, 18, 19].
Koutavas et al. [8] argue that to be sound w.r.t. contextual equivalence, a bisimilarity for state should accumulate the tested terms in an environment to be able to try them again as the store evolves. Such environmental bisimilarities usually compare terms by applying them to arguments built from the environment [12, 17, 19], and therefore still rely on some universal quantification over testing arguments. An exception is Støvring and Lassen’s bisimilarity [18], which compares terms by applying them to a fresh variable, like one would do with a normalform (or open) bisimilarity [11, 16]. Their bisimilarity characterizes contextual equivalence in a calculus with control and state, but is not complete in a calculus with state only: there exist equivalent terms that are not related by the bisimilarity. Jaber and Tabareau [6] go further and propose a sound and complete Kripke Open Bisimilarity for a calculus with local state, which also compares terms by applying them to a fresh variable, but uses notions from Kripke logical relations, namely transition systems of invariants, to reason about heaps.
In this paper, we propose a sound and complete normalform bisimilarity for a callbyvalue \(\lambda \)calculus with local references which relies on environments to handle heaps. We therefore improve over Støvring and Lassen’s work, since our relation is complete, by following a different, potentially simpler, path than Jaber and Tabareau, since we use environments to represent possible worlds and do not rely on any external structures such as transition systems of invariants. Moreover, we do not need types and define our relation in an untyped calculus.
We obtain completeness by treating carefully normal forms that are not values, i.e., open stuck terms of the form \(E[x\,v]\). First, we distinguish in the environment the terms which should be tested multiple times from the ones that should be run only once, namely the evaluation contexts like \(E\) in the above term. The latter are kept in a separate environment that takes the form of a stack, according to the idea presented by Laird [10] and by Jagadeesan et al. [7]. Second, we relate the socalled deferred diverging terms [5, 6], i.e., open stuck terms which hide a diverging behavior in the evaluation context \(E\), with the regular diverging terms.
It may be worth stressing that our congruence proof is based on the machinery we have developed before [3] and is simpler than Støvring and Lassen’s one, in particular in how it accounts for the extensionality of functions.
We believe that this work makes a contribution to the understanding of how one should adjust the normalform bisimulation proof principle when the calculus under consideration becomes less discriminative, assuming that one wishes to preserve completeness of the theory. In particular, it is quite straightforward to define a complete normalform bisimilarity for the \(\lambda \)calculus with firstclass continuations and global store, with no need to refer to other notions than the ones already present in the reduction semantics. Similarly, in the \(\lambda \mu \rho \)calculus (continuations and local references), one only needs to introduce environments to ensure soundness of the theory, but essentially nothing more is required to obtain completeness [18]. In this article we show which new ingredients are needed when moving from these two highly expressive calculi to the corresponding, less discriminative ones—with global or local references only—that do not offer access to the current continuation.
The rest of this paper is as follows. In Sect. 2, we study a simple calculus with global store to see how to reach completeness in that case. In particular, we show in Sect. 2.2 how we deal with deferred diverging terms. We remind in Sect. 2.3 the notion of diacritical progress [3] and the framework our bisimilarity and its proof of soundness are based upon. We sketch the completeness proof in Sect. 2.4. Section 2 paves the way for the main result of the paper, described in Sect. 3, where we turn to the calculus with local store. We define the bisimilarity in Sect. 3.2, prove its soundness and completeness in Sect. 3.3, and use it in Sect. 3.4 on examples taken from the literature. We conclude in Sect. 4, where we discuss related work and in particular compare our work to Jaber and Tabareau’s. A companion report expands on the proofs [4].
2 Global Store
We first consider a calculus where terms share a global store and present how we deal with deferred diverging terms to get a complete bisimilarity.
2.1 Syntax, Semantics, and Contextual Equivalence
A \(\lambda \)abstraction \(\lambda x.t\) binds \(x\) in \(t\); we write \(\mathsf {fv}(t)\) (respectively \(\mathsf {fv}(E)\)) for the set of free variables of \(t\) (respectively \(E\)). We identify terms up to \(\alpha \)conversion of their bound variables. A variable or reference is fresh if it does not occur in any other entities under consideration, and a store is fresh if it maps references to pairwise distinct fresh variables. A term or context is closed if it has no free variables. We write \(\mathsf {fr}(t)\) for the set of references that occur in t.
A term \(t\) of a configuration \(\langle h \;\; t \rangle \) which cannot reduce further is called a normal form. Normal forms are either values or openstuck terms of the form \(E[x\,v]\); closed normal forms can only be \(\lambda \)abstractions. A configuration terminates, written \(c\Downarrow \) if it reduces to a normalform configuration; otherwise it diverges, written \(c\Uparrow \), like configurations running \(\varOmega \mathrel {{\mathop {=}\limits ^{\mathsf {def}}}}(\lambda x.x\,x)\,(\lambda x.x\,x)\).
Contextual equivalence equates terms behaving the same in all contexts. A substitution Open image in new window closes a term \(t\) if Open image in new window is closed; it closes a configuration \(\langle h \;\; t \rangle \) if it closes \(t\) and the values in \(h\).
Definition 1
\(t\) and \(s\) are contextually equivalent, written \(t\mathrel \equiv s\), if for all contexts \(E\), fresh stores \(h\), and closing substitutions Open image in new window , Open image in new window iff Open image in new window .
Testing only evaluation contexts is not a restriction, as it implies the equivalence w.r.t. all contexts \(\mathrel \equiv _C\): one can show that \(t\mathrel \equiv _C s\) iff \(\lambda x.t\mathrel \equiv _C \lambda x.s\) iff \(\lambda x.t\mathrel \equiv \lambda x.s\).
2.2 NormalForm Bisimulation
Informal Presentation. Two open terms are normalform bisimilar if their normal forms can be decomposed into bisimilar subterms. For example in the plain \(\lambda \)calculus, a stuck term \(E[x\,v]\) is bisimilar to \(t\) if \(t\) reduces to a stuck term \(F[x\,w]\) so that respectively \(E\), \(F\) and \(v\), \(w\) are bisimilar when they are respectively plugged with and applied to a fresh variable.
Such a requirement is too discriminating for many languages, as it distinguishes terms that should be equivalent. For instance in plain \(\lambda \)calculus, given a closed value \(v\), \(t\mathrel {{\mathop {=}\limits ^{\mathsf {def}}}}x\,v\) is not normal form bisimilar to \(s\mathrel {{\mathop {=}\limits ^{\mathsf {def}}}}(\lambda y.x\,v) \,(x\,v)\). Indeed, \(\square \) is not bisimilar to \((\lambda y.x\,v) \,\square \) when plugged with a fresh z: the former produces a value z while the latter reduces to a stuck term \(x\,v\). However, \(t\) and \(s\) are contextually equivalent, as for all closed value \(w\), \(t\{w/x\}\) and \(s\{w/x\}\) behave like \(w\,v\): if \(w\,v\) diverges, then they both diverges, and if \(w\,v\) evaluates to some value \(w'\), then they also evaluates to \(w'\). Similarly, \(x\,v\,\varOmega \) and \(\varOmega \) are not normalform bisimilar (one is a stuck term while the other is diverging), but they are contextually equivalent by the same reasoning.
The terms \(t\) and \(s\) are no longer contextually equivalent in a \(\lambda \)calculus with store, since a function can count how many times it is applied and change its behavior accordingly. More precisely, \(t\) and \(s\) are distinguished by the context Open image in new window . But this counting trick is not enough to discriminate \(x\,v\,\varOmega \) and \(\varOmega \), as they are still equivalent in a \(\lambda \)calculus with store. Although \(x\,v\,\varOmega \) is a normal form, it is in fact always diverging when we replace \(x\) by an arbitrary closed value \(w\), either because \(w\,v\) itself diverges, or it evaluates to some \(w'\) and then \(w' \,\varOmega \) diverges. A stuck term which hides a diverging behavior has been called deferred diverging in the literature [5, 6].
It turns out that being able to relate a diverging term to a deferred diverging term is all we need to change from the plain \(\lambda \)calculus normalform bisimilarity to get a complete equivalence when we add global store. We do so by distinguishing two cases in the clause for openstuck terms: a configuration \(\langle h \;\; E[x\,v] \rangle \) is related to \(c\) either if \(c\) can reduce to a stuck configuration with related subterms, or if \(E\) is a diverging context, and we do not require anything of \(c\). The resulting simulation is not symmetric as it relates a deferred diverging configuration with any configuration \(c\) (even converging one), but the corresponding notion of bisimulation equates such configuration only to either a configuration of the same kind or a diverging configuration such as \(\langle h \;\; \varOmega \rangle \).
Progress. We define simulation using the notion of diacritical progress we developed in a previous work [2, 3], which distinguishes between active and passive clauses. Roughly, passive clauses are between simulation states which should be considered equal, while active clauses are between states where actual progress is taking place. This distinction does not change the notions of bisimulation or bisimilarity, but it simplifies the soundness proof of the bisimilarity. It also allows for the definition of powerful upto techniques, relations that are easier to use than bisimulations but still imply bisimilarity. For normalform bisimilarity, our framework enables upto techniques which respects \(\eta \)expansion [3].
Definition 2
 1.\(c\mathrel {\mathcal R}d\) implies

if \(c\mathrel \rightarrow c'\), then \(d\mathrel {\mathrel \rightarrow ^*}d'\) and \(c' \mathrel {\mathcal T}d'\);

if \(c= \langle h \;\; v \rangle \), then \(d\mathrel {\mathrel \rightarrow ^*}\langle g \;\; w \rangle \), Open image in new window , and Open image in new window ;
 if \(c= \langle h \;\; E[x\,v] \rangle \), then either

\(d\mathrel {\mathrel \rightarrow ^*}\langle g \;\; F[x\,w] \rangle \), Open image in new window , Open image in new window , and Open image in new window , or

\(E\mathop {\in }{\mathrel {\mathcal T} \uparrow ^{\mathsf c}}\).


 2.\(c\mathop {\in }{\mathrel {\mathcal R} \uparrow }\) implies \(c\ne \langle h \;\; v \rangle \) for all \(h\) and \(v\) and

if \(c\mathrel \rightarrow c'\), then \(c' \mathop {\in }{\mathrel {\mathcal T} \uparrow }\);

if \(c= \langle h \;\; E[x\,v] \rangle \), then \(E\mathop {\in }{\mathrel {\mathcal T} \uparrow ^{\mathsf c}}\).

A normalform simulation is a candidate relation \(\mathrel {\mathcal R}\) such that \(\mathrel {\mathcal R}\mathop \rightarrowtail \mathrel {\mathcal R}, \mathrel {\mathcal R}\), and a bisimulation is a candidate relation \(\mathrel {\mathcal R}\) such that \(\mathrel {\mathcal R}\) and \(\mathrel {\mathcal R}^{1}\) are simulations. Normalform bisimilarity \(\mathrel \approx \) is the union of all normalform bisimulations.
We test values and contexts by applying or plugging them with a fresh variable \(x\), and running them in a fresh store; with a global memory, the value represented by \(x\) may access any reference and assign it an arbitrary value, hence the need for a fresh store. The stores of two bisimilar value configurations must have the same domain, as it would be easy to distinguish them otherwise by testing the content of the references that would be in one store but not in the other.
The main novelty compared to usual definitions of normalform bisimilarity [3, 11] is the set of (deferred) diverging configurations used in the stuck terms clause. We detect that \(E\) in a configuration \(\langle h \;\; E[x\,v] \rangle \) is (deferred) diverging by running \(\langle h' \;\; E[y] \rangle \) where \(y\) and \(h'\) are fresh; this configuration may then diverge or evaluate to an other deferred diverging configuration \(\langle h \;\; E'[x\,v] \rangle \).
Like in the plain \(\lambda \)calculus [3], \(\mathrel {\mathcal R}\) progresses towards \(\mathrel {\mathcal S}\) in the value clause and \(\mathrel {\mathcal T}\) in the others; the former is passive while the others are active. Our framework prevents some upto techniques from being applied after a passive transition. In particular, we want to forbid the application of bisimulation up to context as it would be unsound: we could deduce that \(v\,x\) and \(w\,x\) are equivalent for all \(v\) and \(w\) just by building a candidate relation containing \(v\) and \(w\).
Example 1
To prove that \(\langle h \;\; x\,v\,\varOmega \rangle \mathrel \approx \langle h \;\; \varOmega \rangle \) holds for all \(v\) and \(h\), we prove that Open image in new window is a bisimulation. Indeed, \(\langle h \;\; x\,v\,\varOmega \rangle \) is stuck with \(\langle g \;\; y\,\varOmega \rangle \mathop {\in }{\mathrel {\mathcal R} \uparrow }\) for fresh \(y\) and \(g\), and we have \(\langle g \;\; y\,\varOmega \rangle \mathrel \rightarrow \langle g \;\; y\,\varOmega \rangle \). Conversely, the transition \(\langle h \;\; \varOmega \rangle \mathrel \rightarrow \langle h \;\; \varOmega \rangle \) is matched by \(\langle h \;\; x\,v\,\varOmega \rangle \mathrel {\mathrel \rightarrow ^*}\langle h \;\; x\,v\,\varOmega \rangle \) and the resulting terms are in \(\mathrel {\mathcal R}\).
2.3 Soundness
In this framework, proving that \(\mathrel \approx \) is sound is a consequence that a form of bisimulation up to context is valid, a result which itself may require to prove that other upto techniques are valid. We distinguish the techniques which can be used in passive clauses (called strong upto techniques), from the ones which cannot. An upto technique (resp. strong upto technique) is a function f such that \(\mathrel {\mathcal R}\mathop \rightarrowtail \mathrel {\mathcal R}, f(\mathrel {\mathcal R})\) (resp. \(\mathrel {\mathcal R}\mathop \rightarrowtail f(\mathrel {\mathcal R}), f(\mathrel {\mathcal R})\)) implies \(\mathrel {\mathcal R}\mathop \subseteq \mathrel \approx \). To show that a given f is an upto technique, we rely on a notion of respectfulness, which is simpler to prove and gives sufficient conditions for f to be an upto technique.
We briefly recall the notions we need from our previous work [2]. We extend \(\subseteq \) and \(\cup \) to functions argumentwise (e.g., \((f \cup g)(\mathrel {\mathcal R})=f(\mathrel {\mathcal R}) \cup g(\mathrel {\mathcal R})\)), and given a set \(\mathfrak {F}\) of functions, we also write \(\mathfrak {F}\) for the function defined as \(\bigcup _{f \in \mathfrak {F}} f\). We define \(f^\omega \) as \(\bigcup _{n \in \mathbb N} f^n\). We write \(\mathsf {id}\) for the identity function on relations, and \(\widehat{f}\) for \(f \mathop \cup \mathsf {id}\). A function f is monotone if \(\mathrel {\mathcal R}\mathop \subseteq \mathrel {\mathcal S}\) implies \(f(\mathrel {\mathcal R}) \mathop \subseteq f(\mathrel {\mathcal S})\). We write \(\mathcal {P}_{ fin }(\mathrel {\mathcal R})\) for the set of finite subsets of \(\mathrel {\mathcal R}\), and we say f is continuous if it can be defined by its image on these finite subsets, i.e., if \(f(\mathrel {\mathcal R}) \mathop \subseteq \bigcup _{\mathrel {\mathcal S}\in \mathcal {P}_{ fin }(\mathrel {\mathcal R})}f(\mathrel {\mathcal S})\). The upto techniques we use are defined by inference rules with a finite number of premises, so they are trivially continuous.
Definition 3
A function f evolves to g, h, written Open image in new window , if for all \(\mathrel {\mathcal R}\) and \(\mathrel {\mathcal T}\), \(\mathrel {\mathcal R}\mathop \rightarrowtail \mathrel {\mathcal R}, \mathrel {\mathcal T}\) implies \(f(\mathrel {\mathcal R}) \mathop \rightarrowtail g(\mathrel {\mathcal R}), h(\mathrel {\mathcal T})\). A function f strongly evolves to g, h, written Open image in new window , if for all \(\mathrel {\mathcal R}\), \(\mathrel {\mathcal S}\), and \(\mathrel {\mathcal T}\), \(\mathrel {\mathcal R}\mathop \rightarrowtail \mathrel {\mathcal S}, \mathrel {\mathcal T}\) implies \(f(\mathrel {\mathcal R}) \mathop \rightarrowtail g(\mathrel {\mathcal S}), h(\mathrel {\mathcal T})\).
Evolution can be seen as progress for functions on relations. Evolution is more restrictive than strong evolution, as it requires \(\mathrel {\mathcal R}\) such that \(\mathrel {\mathcal R}\mathop \rightarrowtail \mathrel {\mathcal R}, \mathrel {\mathcal T}\).
Definition 4

for all \(f \in \mathfrak {S}\), we have Open image in new window ;

for all \(f \in \mathfrak {F}\), we have Open image in new window .
In words, a function is in a respectful set \(\mathfrak {F}\) if it evolves towards a combination of functions in \(\mathfrak {F}\) after active clauses, and in \(\mathfrak {S}\) after passive ones. When checking that f is regular (second case), we can use a regular function at most once after a passive clause. The (possibly empty) subset \(\mathfrak {S}\) intuitively represents the strong upto techniques of \(\mathfrak {F}\). If \(\mathfrak {S}_1\) and \(\mathfrak {S}_2\) are subsets of \(\mathfrak {F}\) which verify the conditions of the definition, then \(\mathfrak {S}_1 \cup \mathfrak {S}_2\) also does, so there exists the largest subset of \(\mathfrak {F}\) which satisfies the conditions, written \({\mathsf {strong}(\mathfrak {F})}\).
Lemma 1
Let \(\mathfrak {F}\) be a respectful set.

If \(f \in \mathfrak {F}\), then f is an upto technique. If \(f \in {\mathsf {strong}(\mathfrak {F})}\), then f is a strong upto technique.

For all \(f \in \mathfrak {F}\), we have \(f(\mathrel \approx ) \mathop \subseteq \mathrel \approx \).
The upto techniques for the calculus with global store are given in Fig. 1. The techniques \(\mathsf {subst}_{}\) and \(\mathsf {plug}_{}\) allow to prove that \(\mathrel \approx \) is preserved by substitution and by evaluation contexts. The remaining ones are auxiliary techniques which are used in the respectfulness proof: \(\mathsf {red}\) relies on the fact that the calculus is deterministic to relate terms up to reduction steps. The technique \(\mathsf {div}\) allows to relate a diverging configuration to any other configuration, while \(\mathsf {plugdiv}\) states that if \(E\) is a diverging context, then \(\langle h \;\; E[t] \rangle \) is a diverging configuration for all \(h\) and \(t\). We distinguish the technique \(\mathsf {plug}_{\mathsf {c}}\) from \(\mathsf {plug}_{\uparrow }\) to get a more finegrained classification, as \(\mathsf {plug}_{\mathsf {c}}\) is the only one which is not strong.
Lemma 2
The set \(\mathfrak {F}\mathrel {{\mathop {=}\limits ^{\mathsf {def}}}}\{ \mathsf {subst}_{}, \mathsf {plug}_{m}, \mathsf {red}, \mathsf {div}, \mathsf {plugdiv}\ \ m \in \{ \mathsf {c}, \uparrow \} \}\) is respectful, with \({\mathsf {strong}(\mathfrak {F})}= \mathfrak {F}\setminus \{ \mathsf {plug}_{\mathsf {c}}\}\).
We omit the proof, as it is similar but much simpler than for the calculus with local store of Sect. 3. We deduce that \(\mathrel \approx \) is sound using Lemma 1.
Theorem 1
For all \(t\), \(s\), and fresh store \(h\), if \(\langle h \;\; t \rangle \mathrel \approx \langle h \;\; s \rangle \), then \(t\mathrel \equiv s\).
2.4 Completeness
We prove the reverse implication by building a bisimulation which contains \(\mathrel \equiv \).
Theorem 2
For all \(t\), \(s\), if \(t\mathrel \equiv s\), then for all fresh stores \(h\), \(\langle h \;\; t \rangle \mathrel \approx \langle h \;\; s \rangle \).
Proof
A first step is to show that \(\langle g \;\; s \rangle \) also evaluates to an openstuck configuration with \(x\) in function position. To do so, we consider a fresh \(l\) and we define Open image in new window such that Open image in new window sets \(l\) at 1 when it is first applied if \(y= x\), and at 2 if \(y\ne x\). Then Open image in new window sets \(l\) at 1, which should also be the case of Open image in new window , and it is possible only if \(\langle g \;\; s \rangle \mathrel {\mathrel \rightarrow ^*}\langle g' \;\; F[x\,w] \rangle \) for some \(g'\), \(F\), and \(w\).
We then have to show that Open image in new window , Open image in new window , and Open image in new window . We sketch the proof for the contexts, as the proofs for the values and the stores are similar. Given \(h_f\) a fresh store, \(y\) a fresh variable, \(E'\) a context, \(h_{E'}\) a store, Open image in new window a closing substitution, we want Open image in new window iff Open image in new window .
3 Local Store
We adapt the ideas of the previous section to a calculus where terms create their own local store. To be able to deal with local resources, the relation we define mixes principles from normalform and environmental bisimilarities.
3.1 Syntax, Semantics, and Contextual Equivalence
We define contextual equivalence on referenceclosed terms as we expect programs to allocate their own store.
Definition 5
Two referenceclosed terms \(t\) and \(s\) are contextually equivalent, written \(t\mathrel \equiv s\), if for all referenceclosed evaluation contexts \(E\) and closing substitutions Open image in new window , Open image in new window iff Open image in new window .
3.2 Bisimilarity
With local stores, an external observer no longer has direct access to the stored values. In presence of such information hiding, a sound bisimilarity relies on an environment to accumulate terms which should be tested in different stores [8].
Example 2
Let Open image in new window and \(f_2 \mathrel {{\mathop {=}\limits ^{\mathsf {def}}}}\lambda x.\textsf {true}\). If we compare \(\mathsf {new~} l := \textsf {true} \mathsf {~in~} f_1\) and \(f_2\) only once in the empty store, they would be seen as equivalent as they both return \(\textsf {true}\), however \(f_1\) modify its store, so running \(f_1\) and \(f_2\) a second time distinguishes them.
Environments generally contain only values [17], except in \(\lambda \mu \rho \) [18], where plugged evaluation contexts are kept in the environment when comparing openstuck configurations. In contrast with \(\lambda \mu \rho \), our environment collects values, and we use a stack for registering contexts [7, 10]. Unlike values, contexts are therefore tested only once, following a lastin firstout ordering. The next example shows that considering contexts repeatedly would lead to an overlydiscriminating bisimilarity. For the stack discipline of testing contexts in action see Example 8 in Sect. 3.4.
Example 3
With the same \(f_1\) and \(f_2\) as in Example 2, the terms \(t\mathrel {{\mathop {=}\limits ^{\mathsf {def}}}}\mathsf {new~} l := \textsf {true} \mathsf {~in~} f_1 \,(x\,\lambda y.y)\) and \(s\mathrel {{\mathop {=}\limits ^{\mathsf {def}}}}f_2 \,(x\,\lambda y.y)\) are contextually equivalent. Roughly, for all closing substitution Open image in new window , \(t\) and \(s\) either both diverge (if Open image in new window diverges), or evaluate to \(\textsf {true}\), since Open image in new window cannot modify the value in \(l\). Testing \(f_1 \,\square \) and \(f_2 \,\square \) twice would discriminate them and wrongfully distinguish \(t\) and \(s\).
Remark 1
The bisimilarity for \(\lambda \mu \rho \) runs evaluation contexts several times and is still complete because of the \(\mu \) operator, which, like call/cc, captures evaluation contexts, and may then execute them several times.

quadruples \((\mathcal E, \varSigma , c, d)\), written \(\mathcal E, \varSigma \vdash c \mathrel {\mathcal R} d\), meaning that \(c\) and \(d\) are related under \(\mathcal E\) and \(\varSigma \);

quadruples \((\mathcal E, \varSigma , h, g)\), written \(\mathcal E, \varSigma \vdash h \mathrel {\mathcal R} g\), meaning that the elements of \(\mathcal E\) and the top of \(\varSigma \) should be related when run with the stores \(h\) and \(g\);

triples \((\epsilon , \sigma , c)\), written \(\epsilon , \sigma \vdash c \mathop {\in }{\mathrel {\mathcal R} \uparrow }\), meaning that either \(c\) is (deferred) diverging, or \(\sigma \) is nonempty and contains a (deferred) diverging context;

triples \((\epsilon , \sigma , h)\), written \(\epsilon , \sigma \vdash h \mathop {\in }{\mathrel {\mathcal R} \uparrow }\), meaning that \(\sigma \) is nonempty and contains a (deferred) diverging context.
Definition 6
 1.\(\mathcal E, \varSigma \vdash c \mathrel {\mathcal R} d\) implies

if \(c\mathrel \rightarrow c'\), then \(d\mathrel {\mathrel \rightarrow ^*}d'\) and \(\mathcal E, \varSigma \vdash c' \mathrel {\mathcal T} d'\);
 if \(c= \langle h \;\; v \rangle \), then either

\(d\mathrel {\mathrel \rightarrow ^*}\langle g \;\; w \rangle \), and \(\mathcal E\cup \{ (v, w) \}, \varSigma \vdash h \mathrel {\mathcal S} g\), or

\(\varSigma \ne \odot \) and \(\pi _{1}(\mathcal E)\cup \{ v\}, \pi _{1}(\varSigma ) \vdash h \mathop {\in }{\mathrel {\mathcal S} \uparrow }\);

 if \(c= \langle h \;\; E[x\,v] \rangle \), then either

\(d\mathrel {\mathrel \rightarrow ^*}\langle g \;\; F[x\,w] \rangle \), and \(\mathcal E\cup \{ (v, w)\}, (E, F) \mathop {{:}{:}}\varSigma \vdash h \mathrel {\mathcal S} g\), or

\(\pi _{1}(\mathcal E)\cup \{v\}, E\mathop {{:}{:}}\pi _{1}(\varSigma ) \vdash h \mathop {\in }{\mathrel {\mathcal S} \uparrow }\).


 2.\(\mathcal E, \varSigma \vdash h \mathrel {\mathcal R} g\) implies

if Open image in new window , then \(\mathcal E, \varSigma \vdash \langle h \;\; v\,x \rangle \mathrel {\mathcal S} \langle g \;\; w\,x \rangle \) for a fresh \(x\);

if \(\varSigma = (E, F) \mathop {{:}{:}}\varSigma '\), then \(\mathcal E, \varSigma ' \vdash \langle h \;\; E[x] \rangle \mathrel {\mathcal S} \langle g \;\; F[x] \rangle \) for a fresh \(x\).

 3.\(\epsilon , \sigma \vdash c \mathop {\in }{\mathrel {\mathcal R} \uparrow }\) implies

if \(c\mathrel \rightarrow c'\), then \(\epsilon , \sigma \vdash c' \mathop {\in }{\mathrel {\mathcal T} \uparrow }\);

if \(c= \langle h \;\; v \rangle \), then \(\sigma \ne \odot \) and \(\epsilon \cup \{ v\}, \sigma \vdash h \mathop {\in }{\mathrel {\mathcal S} \uparrow }\);

if \(c= \langle h \;\; E[x\,v] \rangle \), then \(\epsilon \cup \{ v\}, E\mathop {{:}{:}}\sigma \vdash h \mathop {\in }{\mathrel {\mathcal S} \uparrow }\).

 4.\(\epsilon , \sigma \vdash h \mathop {\in }{\mathrel {\mathcal R} \uparrow }\) implies that \(\sigma \ne \odot \) and

if \(v\in \epsilon \), then \(\epsilon , \sigma \vdash \langle h \;\; v\,x \rangle \mathop {\in }{\mathrel {\mathcal S} \uparrow }\) for a fresh \(x\);

if \(\sigma = E\mathop {{:}{:}}\sigma '\), then \(\epsilon , \sigma ' \vdash \langle h \;\; E[x] \rangle \mathop {\in }{\mathrel {\mathcal S} \uparrow }\) for a fresh \(x\).

A normalform simulation is a candidate relation \(\mathrel {\mathcal R}\) such that \(\mathrel {\mathcal R}\mathop \rightarrowtail \mathrel {\mathcal R}, \mathrel {\mathcal R}\), and a bisimulation is a candidate relation \(\mathrel {\mathcal R}\) such that \(\mathrel {\mathcal R}\) and \(\mathrel {\mathcal R}^{1}\) are simulations. Normalform bisimilarity \(\mathrel \approx \) is the union of all normalform bisimulations.
When \(\mathcal E, \varSigma \vdash c \mathrel {\mathcal R} d\), we reduce \(c\) until we get a value \(v\) or a stuck term \(E[x\,v]\). At that point, either \(d\) also reduces to a normal form of the same kind, or we test (the first projection of) the stack \(\varSigma \) for divergence, assuming it is not empty. In the former case, we add the values to \(\mathcal E\) and the evaluation contexts at the top of \(\varSigma \), getting a judgment of the form \(\mathcal E', \varSigma ' \vdash h \mathrel {\mathcal R} g\), which then tests the environment and the stack by running either terms in \(\mathcal E'\) or at the top of \(\varSigma '\).
Example 4
We sketch the bisimulation proof for the terms \(t\) and \(s\) of Example 3. Because \(\langle \emptyset \;\; t \rangle \mathrel {\mathrel \rightarrow ^*}\langle l:=\textsf {true} \;\; f_1 \,{(x\,\lambda y.y)} \rangle \) and \(\langle \emptyset \;\; s \rangle = \langle \emptyset \;\; f_2 \,{(x\,\lambda y.y)} \rangle \), we need to define \(\mathrel {\mathcal R}\) such that \(\{ (\lambda y.y, \lambda y.y) \}, (f_1 \,\square , f_2 \,\square ) \mathop {{:}{:}}\odot \vdash l:=\textsf {true} \mathrel {\mathcal R} \emptyset \). Testing the equal values in the environment is easy with upto techniques. For the contexts on the stack, we need \(\{ (\lambda y.y, \lambda y.y) \}, \odot \vdash \langle l:=\textsf {true} \;\; f_1\,z \rangle \mathrel {\mathcal R} \langle \emptyset \;\; f_2\,z \rangle \) for a fresh z. Since \(\langle l:=\textsf {true} \;\; f_1\,z \rangle \mathrel {\mathrel \rightarrow ^*}\langle l:=\textsf {false} \;\; \textsf {true} \rangle \) and \(\langle \emptyset \;\; f_2\,z \rangle \mathrel {\mathrel \rightarrow ^*}\langle \emptyset \;\; \textsf {true} \rangle \), we need \(\{ (\lambda y.y, \lambda y.y), (\textsf {true}, \textsf {true}) \}, \odot \vdash l:=\textsf {false} \mathrel {\mathcal R} \emptyset \), which is simple to check.
Example 5
In contrast, we show that \(t' \mathrel {{\mathop {=}\limits ^{\mathsf {def}}}}\mathsf {new~} l := \textsf {true} \mathsf {~in~} f_1 \,(x\,\lambda y.l:=y;y)\) and \(s' \mathrel {{\mathop {=}\limits ^{\mathsf {def}}}}f_2 \,(x\,\lambda y.y)\) are not bisimilar. We would need to build \(\mathrel {\mathcal R}\) such that \(\{ (\lambda y.l:=y;y, \lambda y.y) \}, (f_1 \,\square , f_2 \,\square ) \mathop {{:}{:}}\odot \vdash l:=\textsf {true} \mathrel {\mathcal R} \emptyset \). Testing the values in the environment, we want \(\{ (\lambda y.l:=y;y, \lambda y.y), (z, z) \}, (f_1 \,\square , f_2 \,\square ) \mathop {{:}{:}}\odot \vdash l:=z \mathrel {\mathcal R} \emptyset \) for a fresh z. Executing the contexts on the stack, we get a stuck term of the form Open image in new window and a value \(\textsf {true}\), which cannot be related, because the former is not deferred diverging.
The terms \(t'\) and \(s'\) are therefore not bisimilar, and they are indeed not contextually equivalent, since \(t'\) gives access to its private reference by passing \(\lambda y.l:=y;y\) to \(x\). The function represented by \(x\) can then change the value of \(l\) to \(\textsf {false}\) and break the equivalence.
The last two cases of the bisimulation definition aim at detecting a deferred diverging context. The judgment \(\epsilon , \sigma \vdash h \mathop {\in }{\mathrel {\mathcal R} \uparrow }\) roughly means that if \(\sigma = E_n \mathop {{:}{:}}\ldots E_1 \mathop {{:}{:}}\odot \), then the configuration \(\langle h' \;\; E_1[\ldots E_n[x]] \rangle \) diverges for all fresh \(x\) and all \(h'\) obtained by running a term from \(\mathcal E\) with the store \(h\). As a result, when \(\epsilon , \sigma \vdash h \mathop {\in }{\mathrel {\mathcal R} \uparrow }\), we have two possibilities: either we run a term from \(\mathcal E\) in \(h\) to potentially change \(h\), or we run the context at the top of \(\sigma \) (which cannot be empty in that case) to check if it is diverging. In both cases, we get a judgment of the form \(\epsilon , \sigma ' \vdash c \mathop {\in }{\mathrel {\mathcal R} \uparrow }\). In that case, either \(c\) diverges and we are done, or it terminates, meaning that we have to look for divergence in \(\sigma '\).
Example 6
We prove that \(\langle \emptyset \;\; x\,v\,\varOmega \rangle \) and \(\langle \emptyset \;\; \varOmega \rangle \) are bisimilar. We define \(\mathrel {\mathcal R}\) such that \(\emptyset , \odot \vdash \langle \emptyset \;\; x\,v\,\varOmega \rangle \mathrel {\mathcal R} \langle \emptyset \;\; \varOmega \rangle \), for which we need \(\{v\}, \square \,\varOmega \mathop {{:}{:}}\odot \vdash \emptyset \mathop {\in }{\mathrel {\mathcal R} \uparrow }\), which itself holds if \(\{v\}, \odot \vdash \langle \emptyset \;\; y\,\varOmega \rangle \mathop {\in }{\mathrel {\mathcal R} \uparrow }\).
3.3 Soundness and Completeness
We briefly discuss the upto techniques we need to prove soundness. We write \(\mathcal E\{(v, w)/x\}\) for the environment Open image in new window , and we also define \(\varSigma \{(x, w)/x\}\), \(\epsilon \{v/x\}\), and \(\sigma \{v/x\}\) as expected. To save space, Fig. 2 presents the upto techniques for the configuration judgment only; see the report [4] for the other judgments.
As in Sect. 2.3, the techniques \(\mathsf {subst}_{}\) and \(\mathsf {plug}_{}\) allow to reason up to substitution and plugging into an evaluation context, except that the substituted values and plugged contexts must be taken from respectively the environment and the top of the stack. The technique \(\mathsf {div}\) relates a diverging configuration to any configuration, like in the calculus with global store. The technique \(\mathsf {ccomp}\) allows to merge successive contexts in the stack into one. The weakening technique \(\mathsf {weak}\), originally known as bisimulation up to environment [17], is an usual technique for environmental bisimulations. Making the environment smaller creates a weaker judgment, as having less testing terms means a less discriminating candidate relation. Bisimulation up to reduction \(\mathsf {red}\) is also standard and allows for a bigstep reasoning by ignoring reduction steps. Finally, the technique \(\mathsf {refl}\) allows to introduce identical contexts in the stack, but also values in the environment or terms in configurations (see the report [4]).
We denote by \(\mathsf {subst}_{\mathsf {c}}\) the up to substitution technique restricted to the configuration and diverging configuration judgments, and by \(\mathsf {subst}_{\mathsf {s}}\) the restriction to the store and diverging store judgments.
Lemma 3
The set \(\mathfrak {F}\mathrel {{\mathop {=}\limits ^{\mathsf {def}}}}\{ \mathsf {subst}_{m}, \mathsf {plug}_{}, \mathsf {ccomp}, \mathsf {div}, \mathsf {weak}, \mathsf {red}, \mathsf {refl}\ \ m \in \{ \mathsf {c}, \mathsf {s}\} \}\) is respectful, with \({\mathsf {strong}(\mathfrak {F})}= \{ \mathsf {subst}_{\mathsf {s}}, \mathsf {ccomp}, \mathsf {div}, \mathsf {weak}, \mathsf {red}, \mathsf {refl}\}\).
In contrast with Sect. 2.3 and our previous work [3], \(\mathsf {subst}_{\mathsf {c}}\) is not strong, because values are taken from the environment. Indeed, with \(\mathsf {subst}_{\mathsf {c}}\) strong, from \(\{ (v, w) \}, \odot \vdash \emptyset \mathrel {\mathcal R} \emptyset \), we could derive \(\{ (v, w) \}, \odot \vdash \langle \emptyset \;\; x\,y \rangle \mathrel {\mathsf {refl}(\mathrel {\mathcal R})} \langle \emptyset \;\; x\,y \rangle \) and then \(\{ (v, w) \}, \odot \vdash \langle \emptyset \;\; v\,x \rangle \mathrel {\mathsf {subst}_{\mathsf {c}}(\mathrel {\mathsf {refl}(\mathrel {\mathcal R})})} \langle \emptyset \;\; w\,x \rangle \) for any \(v\) and \(w\), which would be unsound.
The respectfulness proofs are in the report [4]. Using \(\mathsf {refl}\), \(\mathsf {plug}_{}\), \(\mathsf {subst}_{\mathsf {c}}\), and Lemma 1 we prove that \(\mathrel \approx \) is preserved by evaluation contexts and substitution, from which we deduce it is sound w.r.t. contextual equivalence.
Theorem 3
For all \(t\) and \(s\), if \(\emptyset , \odot \vdash \langle \emptyset \;\; t \rangle \mathrel \approx \langle \emptyset \;\; s \rangle \), then \(t\mathrel \equiv s\).
To establish completeness, we follow the proof of Theorem 2, i.e., we construct a candidate relation \(\mathrel {\mathcal R}\) that contains \(\mathrel \equiv \) and prove it is a simulation by case analysis on the behavior of the related terms.
Theorem 4
For all \(t\) and \(s\), if \(t\mathrel \equiv s\), then \(\emptyset , \odot \vdash \langle \emptyset \;\; t \rangle \mathrel \approx \langle \emptyset \;\; s \rangle \).
The main difference is that the contexts and closing substitutions are built from the environment using compatible closures [17], to take into account the private resources of the related terms. We discuss the proof in the report [4].
3.4 Examples
Example 7
Running \(v\) and \(w\) with a fresh variable f, we obtain \(\langle l:=0 \;\; E_1[f\,()] \rangle \) and \(\langle \emptyset \;\; E_2[f\,()] \rangle \) with \(E_1 \mathrel {{\mathop {=}\limits ^{\mathsf {def}}}}\square ;l:=1;f\,();!l\) and \(F_1 \mathrel {{\mathop {=}\limits ^{\mathsf {def}}}}\square ;f\,();1\). Ignoring the identical unit arguments (using \(\mathsf {refl}\)), we need \(\{ (v, w) \}, (E_1, F_1) \mathop {{:}{:}}\odot \vdash l:=0 \mathrel {\mathcal R} \emptyset \); from that point, we can either test \(v\) and \(w\) again, resulting into an extra pair \((E_1, F_1)\) on the stack, or run \(\langle l:=0 \;\; E_1[g] \rangle \) and \(\langle \emptyset \;\; F_1[g] \rangle \) for a fresh g instead.

\(\varSigma \) is an arbitrary stack composed only of pairs \((E_1, F_1)\) or \((E_2, F_2)\);

if \(\varSigma = (E_2, F_2) \mathop {{:}{:}}\varSigma '\), then \(n=1\).
We can check that such a candidate is a bisimulation, and it ensures that when \(l\) is read (when \(E_2\) is executed), it contains the value 1.
Example 8
Example 9
4 Related Work and Conclusion
Related Work. As pointed out in Sect. 1, the other bisimilarities defined for state either feature universal quantification over testing arguments [9, 12, 17, 19], or are complete only for a more expressive language [18]. Kripke logical relations [1, 5] also involve quantification over arguments when testing terms of a functional type. Finally, denotational models [10, 13] can also be used to prove program equivalence, by showing that the denotations of two terms are equal. However, computing such denotations is difficult in general, and the automation of this task is so far restricted to a language with firstorder references [14].
The work most closely related to ours is Jaber and Tabareau’s Kripke Open Bisimulation (KOB) [6]. A KOB tests functional terms with fresh variables and not with related values like a regular logical relation would do. To relate two given configurations, one has to provide a World Transition System (WTS) which states the invariants the heaps of the configurations should satisfy and how to go from one invariant to the other during the evaluation. Similarly, the bisimulations for the examples of Sect. 3.4 state properties which could be seen as invariants about the stores at different points of the evaluation.
The difficulty for KOB as well as with our bisimilarity is to come up with the right invariants about the heaps, expressed either as a WTS or as a bisimulation. We believe that choosing a technique over the other is just a matter of preference, depending on whether one is more comfortable with game semantics or with coinduction. It would be interesting to see if there is a formal correspondence between KOB and our bisimilarity; we leave this question as a future work.
Conclusion. We define a sound and complete normalform bisimilarity for higherorder local state, with an environment to be able to run terms in different stores. We distinguish in the environment values which should be tested several times from the contexts which should be executed only once. The other difficulty is to relate deferred and regular diverging terms, which is taken care of by the specific judgments about divergence. The lack of quantification over arguments make the bisimulation proofs quite simple.
A future work would be to make these proofs even simpler by defining appropriate upto techniques. The techniques we use in Sect. 3.3 to prove soundness turn out to be not that useful when establishing the equivalences of Sect. 3.4, except for trivial ones such as up to reduction or reflexivity. The difficulty in defining the candidate relations for the examples of Sect. 3.4 is in finding the right property relating the stack \(\varSigma \) to the store, so maybe an upto technique could make this task easier.
As pointed out in Sect. 1, our results can be seen as an indication of what kind of additional infrastructure in a complete normalform bisimilarity is required when the considered syntactic theory becomes less discriminative—in our case, when control operators vanish from the picture, and mutable state is the only extension of the \(\lambda \)calculus. A question one could then ask is whether we can find a less expressive calculus—maybe the plain \(\lambda \)calculus itself—for which a suitably enhanced normalform bisimilarity is still complete.
Notes
Acknowledgements
We thank Guilhem Jaber and the anonymous reviewers for their comments. This work was supported by the National Science Centre, Poland, grant no. 2014/15/B/ST6/00619 and by COST Action EUTypes CA15123.
References
 1.Ahmed, A., Dreyer, D., Rossberg, A.: Statedependent representation independence. In: Pierce, B.C. (ed.) Proceedings of the ThirtyFifth Annual ACM Symposium on Principles of Programming Languages, pp. 340–353. ACM Press, January 2009Google Scholar
 2.Aristizábal, A., Biernacki, D., Lenglet, S., Polesiuk, P.: Environmental bisimulations for delimitedcontrol operators with dynamic prompt generation. Logical Methods Comput. Sci. 13(3) 2017Google Scholar
 3.Biernacki, D., Lenglet, S., Polesiuk, P.: Proving soundness of extensional normalform bisimilarities. In: Silva, A. (ed.) Proceedings of the 33rd Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXXIII), Ljubljana, Slovenia. Electronic Notes in Theoretical Computer Science, vol. 336, pp. 41–56, June 2017Google Scholar
 4.Biernacki, D., Lenglet, S., Polesiuk, P.: A complete normalform bisimilarity for state. Research report RR9251, Inria, Nancy, France, January 2019Google Scholar
 5.Dreyer, D., Neis, G., Birkedal, L.: The impact of higherorder state and control effects on local relational reasoning. J. Funct. Program. 22(4–5), 477–528 (2012)MathSciNetCrossRefGoogle Scholar
 6.Jaber, G., Tabareau, N.: Kripke open bisimulation – a marriage of game semantics and operational techniques. In: Feng, X., Park, S. (eds.) APLAS 2015. LNCS, vol. 9458, pp. 271–291. Springer, Cham (2015)CrossRefGoogle Scholar
 7.Jagadeesan, R., Pitcher, C., Riely, J.: Open bisimulation for aspects. Trans. AspectOriented Softw. Dev. 5, 72–132 (2009)CrossRefGoogle Scholar
 8.Koutavas, V., Levy, P.B., Sumii, E.: From applicative to environmental bisimulation. In: Mislove, M., Ouaknine, J. (eds.) Proceedings of the 27th Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXVII), Pittsburgh, PA, USA. ENTCS, vol. 276, pp. 215–235, May 2011Google Scholar
 9.Koutavas, V., Wand, M.: Small bisimulations for reasoning about higherorder imperative programs. In: Morrisett, J.G., Jones, S.L.P. (eds.) POPL 2006, Charleston, SC, USA, pp. 141–152. ACM Press (2006)Google Scholar
 10.Laird, J.: A fully abstract trace semantics for general references. In: Arge, L., Cachin, C., Jurdziński, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 667–679. Springer, Heidelberg (2007)CrossRefGoogle Scholar
 11.Lassen, S.B.: Eager normal form bisimulation. In: Panangaden, P. (ed.) LICS 2005, Chicago, IL, pp. 345–354. IEEE Computer Society Press (2005)Google Scholar
 12.Madiot, J.M., Pous, D., Sangiorgi, D.: Bisimulations upto: beyond firstorder transition systems. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 93–108. Springer, Heidelberg (2014)Google Scholar
 13.Murawski, A.S., Tzevelekos, N.: Game semantics for good general references. In: Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, pp. 75–84. IEEE Computer Society, June 2011Google Scholar
 14.Murawski, A.S., Tzevelekos, N.: Algorithmic games for full ground references. Formal Methods Syst. Des. 52(3), 277–314 (2018)CrossRefGoogle Scholar
 15.Pitts, A., Stark, I.: Operational reasoning for functions with local state. In: Gordon, A., Pitts, A. (eds.) Higher Order Operational Techniques in Semantics, pp. 227–273. Publications of the Newton Institute, Cambridge University Press (1998)Google Scholar
 16.Sangiorgi, D.: The lazy lambda calculus in a concurrency scenario. In: Scedrov, A. (ed.) LICS 1992, Santa Cruz, California, pp. 102–109. IEEE Computer Society (1992)Google Scholar
 17.Sangiorgi, D., Kobayashi, N., Sumii, E.: Environmental bisimulations for higherorder languages. ACM Trans. Program. Lang. Syst. 33(1), 1–69 (2011)CrossRefGoogle Scholar
 18.Støvring, K., Lassen, S.B.: A complete, coinductive syntactic theory of sequential control and state. In: Felleisen, M. (ed.) SIGPLAN Notices, POPL 2007, Nice, France, vol. 42, no. 1, pp. 161–172. ACM Press (2007)Google Scholar
 19.Sumii, E.: A complete characterization of observational equivalence in polymorphic \(\lambda \)calculus with general references. In: Grädel, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 455–469. Springer, Heidelberg (2009)CrossRefGoogle Scholar
Copyright information
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.