Transfinite StepIndexing: Decoupling Concrete and Logical Steps
 2 Citations
 7 Mentions
 755 Downloads
Abstract
Stepindexing has proven to be a powerful technique for defining logical relations for languages with advanced type systems and models of expressive program logics. In both cases, the model is stratified using natural numbers to solve a recursive equation that has no naive solutions. As a result of this stratification, current models require that each unfolding of the recursive equation – each logical step – must coincide with a concrete reduction step. This tight coupling is problematic for applications where the number of logical steps cannot be statically bounded.
In this paper we demonstrate that this tight coupling between logical and concrete steps is artificial and show how to loosen it using transfinite stepindexing. We present a logical relation that supports an arbitrary but finite number of logical steps for each concrete step.
Keywords
Program Logic Operational Semantic Logical Relation Logical Step Reference Type1 Introduction
Stepindexing has proven to be a powerful technique for defining models of advanced type systems [2, 5, 6, 10, 11] and expressive higherorder program logics [4, 16, 18, 20]. To support abstraction, such type systems and program logics often feature some notion of impredicative invariants. For instance, a reference type can be seen as an invariant about the type of values stored at a given location; for languages with general references this is an impredicative invariant.
To use this artificially stratified model, current stepindexed models take the steps to be concrete reduction steps in the underlying operational semantics. An expression e is thus an inhabitant of type \(\tau \) with n steps left on the clock, if whenever it reduces to \(e'\) in \(i < n\)concrete reduction steps, then \(e'\) is an inhabitant of \(\tau \) with \(ni\) steps left on the clock. As a consequence, each logical step must be associated with a corresponding reduction step.
This suffices to prove many interesting properties. For instance, to prove type soundness of the typing rule for dereference, we have to prove that !l is an inhabitant of \(\tau \) for n steps, assuming l is an inhabitant of \(\tau ~\mathsf {ref}\,\) for n steps. Since !l uses one concrete reduction step, it suffices to know that location l contains a value that is an inhabitant of \(\tau \) for \(n1\) steps. Conceptually, the logical step of unfolding the invariant always happens together with the concrete step of dereferencing the location and the proof goes through. Unfortunately, this is not always the case. For instance, higherorder abstractions often introduce new logical steps without introducing corresponding concrete steps [18].
Similar problems plague stepindexed program logics, where higherorder abstractions that introduce new logical steps without any corresponding concrete steps are more common. For instance, deriving a new simpler specification for a specific way of using a concurrent data structure from an abstract library specification often introduces a new invariant without introducing any new concrete reduction steps [18, 20]. See [18, Sect. 8] for a concrete example of this problem in the context of stepindexed program logics. Existing stepindexing program logics have dealt with this issue by adding additional skip statements, to allow new logical steps to be related to skip reduction steps [14, 18]. Not only is this solution semantically unsatisfying, it is also insufficient for examples where the number of logical unfoldings cannot be statically bounded.
Conceptually, the problem with earlier models is the artificial link made between unfoldings of the recursive domain equation (logical steps) and concrete reduction steps. In this paper we propose a refinement of stepindexing that relaxes this link, by allowing an arbitrary but finite number of logical steps for each concrete reduction step. To achieve this, we stratify the construction of the semantic domain using \(\omega ^2\), or \(\mathbb {N}\times \mathbb {N}\) ordered lexicographically, instead of \(\omega \). We then take the first step index to be concrete reduction steps in the underlying operational semantics and the second step index to be the number of logical steps possible before the next concrete reduction step. The lexicographic ordering ensures that we can pick an arbitrary but finite number of possible logical steps until the next concrete reduction step, after each concrete reduction step.
Instead of presenting a transfinitely stepindexed model of our latest and greatest program logic, we focus on a logical relation. Such a setting is simpler, thus allowing us to present our solution in greater detail and concentrate on the problem of decoupling logical and concrete steps. We develop a general theory for stratifying the construction of semantic domains using stepindexing over \(\omega ^2\). This theory also applies to semantic domains used in recent stepindexed program logics and we believe our approach to decoupling logical and concrete steps also extends to these program logics.
Our main contribution is conceptual: we demonstrate how transfinite stepindexing allows us to loosen the artificial link between concrete and logical steps in stepindexed models. As a technical contribution, we extend previous results for stratifying recursive definitions using stepindexing over \(\omega \) to the transfinite case of \(\omega ^2\).
We have included proof sketches of the main results in the article. Full proofs can be found in the accompanying technical report, which is available at the following address: http://www.kasv.dk/transfinitetr.pdf.
Outline. First we introduce the syntax and operational semantics of a simple higherorder language in Sect. 2. In Sect. 3 we show how to stratify the construction of semantic domains using stepindexing over \(\omega ^2\) and recall some mathematical concepts for working with these domains. Next, we apply this theory to define a transfinitely stepindexed logical relation in Sect. 4. In Sect. 5 we return to the example mentioned above and prove the troublesome contextual equivalence using our transfinitely stepindexed logical relation. We defer most discussions of related work to Sect. 6. Finally, in Sect. 7 we conclude and discuss future work.
2 Syntax and Operational Semantics
Note that our type system does not include store typings, assigning types to locations. Store typings are typically used to facilitate syntactic progress and preservation proofs. However, they are unnecessary for our semantic approach and we only consider source programs that do not contain location constants.
The operational semantics is defined as a smallstep reduction relation between configurations consisting of an expression e and a heap h: \(\langle e, h \rangle \rightarrow \langle e', h' \rangle \). A heap is a finite map from locations to values. Figure 3 includes an excerpt of the reduction rules; the rest of the rules are standard. Note that dereferencing or assigning to a location that has not already been allocated results in a stuck configuration. It will follow from our logical relation that welltyped programs never get stuck and thus never try to dereference a location that has not been allocated.
Our formal definition of contextual approximation is given in Definition 1 below. We say that \(e_I\) contextually approximates \(e_S\) if for any closing context C of unit type, if \(C[e_I]\) terminates with value \(*\), then \(C[e_S]\) terminates with value \(*\). Since welltyped expressions do not contain any location constants, we can simply reduce \(C[e_I]\) and \(C[e_S]\) with an empty heap. The \(C : (\varDelta ; \varGamma , \tau ) \rightsquigarrow (\varDelta '; \varGamma ', \tau ')\) relation expresses that context C takes a term e such that \(\varDelta ; \varGamma \vdash e : \tau \) to a term C[e] such that \(\varDelta '; \varGamma ' \vdash C[e] : \tau '\). The rules for \(C : (\varDelta ; \varGamma , \tau ) \rightsquigarrow (\varDelta '; \varGamma ', \tau ')\) are standard and have been omitted.
Definition 1
We refer to \(e_I\) in \(\varDelta ; \varGamma \vdash e_I \le e_S : \tau \) as the left expression or implementation and we refer to \(e_S\) as the right expression or specification. Contextual equivalence, \(\varDelta ; \varGamma \vdash e_1 \cong _{ctx} e_2 : \tau \), is then defined as the conjunction of lefttoright contextual approximation and righttoleft contextual approximation.
3 StepIndexing over \(\omega ^2\)
Stepindexing is often used to solve the recursive definitions of semantic domains that arise when modelling impredicative invariants. Due to a contravariant occurrence of the recursive variable, these definitions have no solution in settheory. Instead, stepindexing is used to stratify the construction. In this section we present a general theory for stratifying the construction of semantic domains using stepindexing over \(\omega ^2\).
For stepindexing over \(\omega \) one can apply general existence theorems for fixed points of locally contractive functors on the category of \(\omega \) setindexed sets. Birkedal, Støvring and Thamsborg [12] have generalized the inverselimit construction to show the existence of fixed points of locally contractive functors over categories where the Homsets can be equipped with a suitable metric structure. This existence theorem is directly applicable to the category of \(\omega \) stepindexed sets. Unfortunately, the results do not apply to the category of \(\omega ^2\) stepindexed sets. Intuitively, the inverse limit construction is not iterated far enough for stepindexing over \(\omega ^2\).
In this section we define a category of \(\omega ^2\) stepindexed sets, \(\mathcal {U}\), and give a concrete construction for fixedpoints of locally contractive functors on \(\mathcal {U}\). While the results for stepindexing over \(\omega ^2\) are novel, the structure of the development is not and follows existing work. To simplify the exposition we use Di Gianantonio and Miculan’s complete ordered families of equivalences [13] to present the category of stepindexed sets and avoid the use of abstract category theory.
Another intuition to keep in mind is that two elements are (n, m)equivalent if the elements cannot distinguished with n concrete reduction steps left and m logical steps before the next concrete step. Since fewer observations are possible as the number of steps decreases, we require the equivalence to become coarser as the number of steps is decreased. With no reduction steps left no observations are possible and every element is indistinguishable. We thus require that the equivalence is the total relation at the last step index, (0, 0). Lastly, we require that if two elements are indistinguishable for any number of steps, they are identical.
Definition 2

\(\forall x, y \in X.~x \mathop {=}\limits ^{0,0} y\)

\(\forall x, y \in X.~\forall a, b \in \omega ^2.~a \le b \wedge x \mathop {=}\limits ^{b} y \Rightarrow x \mathop {=}\limits ^{a} y\)

\(\forall x, y \in X.~(\forall a \in \omega ^2.~x \mathop {=}\limits ^{a} y) \Rightarrow x = y\)
The function space between two ordered families of equivalences consists of nonexpansive functions that map aequivalent arguments to aequivalent results. Intuitively, nonexpansiveness of f ensures that it takes at least the same number of steps to distinguish \(f(x_1)\) from \(f(x_2)\) as it takes to distinguish \(x_1\) from \(x_2\). Similarly, a function f is contractive if it is strictly harder to distinguish \(f(x_1)\) from \(f(x_2)\) than it is to distinguish \(x_1\) from \(x_2\), i.e., if to show that the results are aequivalent it suffices that the arguments are equivalent at all strictly smaller indices. Contractive functions are thus necessarily nonexpansive.
Definition 3
Definition 4
(Limits). Let \((X, (\mathop {=}\limits ^{a})_{a \in \omega ^2})\) be an ordered family of equivalences and Y a subset of \(\omega ^2\). A Yindexed family \((x_y)_{y \in Y}\) is coherent iff \(\forall a, b \in Y.~a \le b \Rightarrow x_a \mathop {=}\limits ^{a} x_b\) and x is a limit of \((x_y)_{y \in Y}\) iff \(\forall a \in Y.~x \mathop {=}\limits ^{a} x_a\).
Note that limits of coherent families indexed by proper subsets of \(\omega ^2\) are not necessarily unique. For such coherent families we thus additionally require suitably unique chosen limits.
Definition 5
Definition 6
(Complete ordered families of equivalences). A complete ordered family of equivalences (c.o.f.e) is an o.f.e. \(\mathcal {X}\) such that all \(\omega ^2\)indexed coherent families in \(\mathcal {X}\) have limits and \(\mathcal {X}\) has chosen limits.
Lemma 1
(Banach’s fixed point theorem). Let \(\mathcal {X} = (X, (\mathop {=}\limits ^{a})_{a \in \omega ^2})\) be a complete ordered family of equivalences and \(f : X \rightarrow X\) a contractive function. If \(\mathcal {X}\) is inhabited (i.e., there exists an \(x \in X\)), then f has a unique fixed point.
Complete ordered families of equivalences over \(\omega ^2\) form a category, \(\mathcal {U}\), with nonexpansive functions as morphisms. We will use this category to define our semantic domains. To do so, we first introduce a few basic c.o.f.e. constructions followed by a general existence theorem for solutions of recursive domain equations in \(\mathcal {U}\).
Definition 7
Let \(\mathcal {U}\) denote the category of complete ordered families of equivalences. The objects of \(\mathcal {U}\) are complete ordered families of equivalences and the morphisms are nonexpansive functions.
Basic constructions. The set of nonexpansive functions between two c.o.f.e.s forms a c.o.f.e., by lifting the equivalence on the codomain and computing limits pointwise. Restricting the function space further to finite partial nonexpansive functions also yields a c.o.f.e.
Lemma 2
Likewise, restricting the nonexpansive function space to monotone and nonexpansive functions also yields a c.o.f.e. if the partial order on the codomain respects limits in the codomain.
Lemma 3
Let \(\mathcal {X} = (X, (\mathop {=}\limits ^{a}_X)_{a \in \omega ^2})\) be an ordered family of equivalences, \(\mathcal {Y} = (Y, (\mathop {=}\limits ^{a}_Y)_{a \in \omega ^2})\) be complete ordered families of equivalences and \(\le _X\) and \(\le _Y\) be partial orders on X and Y.
We can model a predicate over a set X as a predicate over \(\omega ^2\,\times \,X\), downwardsclosed in the step index. The intuition is that \((n, m, x) \in p\) if x satisfies the stepindexed predicate p with n, m steps left on the clock. The downwardsclosure captures the intuition that it takes a certain number of steps to show that x does not satisfy a given predicate. These predicates form a c.o.f.e., where we consider two predicates n, m equivalent if they agree for all stepindices strictly below n, m.
Definition 8
Solving Recursive Domain Equations in\(\mathcal {U}\). Banach’s fixed point theorem (Lemma 1) allows us to show existence of recursivelydefined elements of complete ordered families of equivalences. To show existence of recursivelydefined complete ordered families of equivalences, we lift the fixed point theorem from contractive functions on complete ordered families of equivalences to locally contractive functors on the category of complete ordered families of equivalences. The fixed point theorem is stated for mixedvariance functors, \(F : {\mathcal {U}}^{\textit{op}} \times \mathcal {U} \rightarrow \mathcal {U}\), where the negative and positive occurrences of the recursive variable have been separated.
Definition 9
Theorem 1
If \(F : {\mathcal {U}}^{\textit{op}} \times \mathcal {U} \rightarrow \mathcal {U}\) is a locally contractive bifunctor and F(1, 1) is inhabited, then there exists an object \(X \in \mathcal {U}\) such that \(F(X, X) \cong X \in \mathcal {U}\).
Proof
(Sketch). The construction of the fixed point uses an inverselimit construction. However, as for Banach’s fixed point theorem, when stepindexing over \(\omega ^2\) we have to iterate the construction further and repeat the inverselimit construction.
Next, we iterate this construction to obtain increasingly better approximations of the fixed point. The real fixed point is then constructed as an inverse limit of these approximate fixed points. \(\square \)
Given a locally nonexpansive functor it is possible to define a locally contractive functor by shifting all the equivalence relations one step. The functor \(\mathop {\blacktriangleright }\), defined below, takes a complete ordered family of equivalences and shifts all the equivalences one step up, such that (n, m)equivalence becomes \((n,m+1)\)equivalence. At limits \((n+1,0)\) the equivalence is taken to be the limit of all smaller equivalences.
Definition 10
Lemma 4
If \(F : {\mathcal {U}}^{\textit{op}} \times \mathcal {U} \rightarrow \mathcal {U}\) is locally nonexpansive then \(\mathop {\blacktriangleright }\circ F\) is locally contractive.
Using Lemma 4 we can obtain a locally contractive functor from a locally nonexpansive functor, and thus use Theorem 1 to obtain a fixed point. However, as we will see in the following section, due to the shifting by \(\mathop {\blacktriangleright }\), we are forced to “go down a step” if we want our definitions to remain nonexpansive, whenever we unfold the isomorphism.
4 Logical Relation
In this section we define a logical relation stepindexed over \(\omega ^2\) for the language introduced in Sect. 2. By only relating the first stepindex with concrete reduction steps, we obtain a logical relation that allows for an arbitrary finite number of logical steps for each concrete reduction step. We prove that this logical relation is sound with respect to contextual approximation.
Since each invariant asserts exclusive ownership of the parts of each heap that are related by the invariant, we can use \(\mathcal {I}\) to reason locally about satisfaction of individual invariants. This is captured by Lemma 5. We use \(\lfloor W \rfloor \) as shorthand for heap satisfaction in the case where all invariants are active, i.e., \(\lfloor W \rfloor _{{\text {dom}}(W)}\).
Lemma 5
As expected, two heaps satisfy the heap invariant \({\text {inv}}(\nu , l_I, l_S)\) if and only if \(h_I(l_I)\) and \(h_S(l_S)\) contain \(\nu \)related values (Lemma 6). Note that Lemma 6 requires that there is at least one concrete reduction step left, even just to prove that \(l_I\) and \(l_S\) are in the domain of \(h_I\) and \(h_S\).
Lemma 6
To ensure that definitions using heap satisfaction are suitably nonexpansive, we require heap satisfaction to satisfy the following nonexpansiveness property (Lemma 7). Intuitively, this property holds because we “go down” one step index from n to \(n1\) in the definition of heap satisfaction.
Lemma 7
Proof
(Sketch). Assume that two heap parts \(h_{1I}\) and \(h_{1S}\) are \(n1, m'\) related at \(\xi (W_1(\iota ))(W_1)\). By nonexpansiveness of \(\xi \) it follows that \(\xi (W_1(\iota ))\) is n, m equivalent to \(\xi (W_2(\iota ))\) in c.o.f.e. \(\mathop {\blacktriangleright }\mathbf {\widehat{Inv}}\). Since \((n1, m'+1) < (n, m)\) it follows that they are also \(n1,m'+1\) equivalent in c.o.f.e. \(\mathbf {\widehat{Inv}}\). Hence, by the equivalence on uniform predicates, \(\xi (W_1(\iota ))(W_1)\) and \(\xi (W_2(\iota ))(W_2)\) agree on all stepindices strictly below \(n1, m'+1\). It follows that \(h_{1I}\) and \(h_{1S}\) are \(n1, m\) related at \(\xi (W_2(\iota ))(W_2)\). \(\square \)
To ensure that the expressions remain related after more invariants have been allocated, we take initial heaps related in an arbitrary future world \(W'\). Likewise, the terminal heaps and return value is related in some future world \(W''\), to allow the allocation of new invariants.
The expression closure further requires that whenever \(\langle e_I, h_I \rangle \) reduces to some irreducible configuration \(\langle e_I', h_I' \rangle \), then \(e_I'\) is in fact a value. This allows us to prove that welltyped expressions do not get stuck.
Just like for heap satisfaction, we need the expression closure to satisfy the following nonexpansiveness property (Lemma 8), to ensure that definitions using the expression closure are suitably nonexpansive.
Lemma 8
Proof
Interpretation. We now have all the ingredients to define the relational interpretation of types. The relational interpretation of types, \(\mathcal {V}\llbracket {\varDelta \vdash \tau }\rrbracket : \mathbf {Type}^\varDelta \rightarrow \mathbf {Type}\), is defined by induction on the type wellformedness derivation, \(\varDelta \vdash \tau \). It is parametrized by a function \(\rho \in \mathbf {Type}^\varDelta \) that assigns a semantic type to each type variable in context \(\varDelta \). Intuitively, it expresses when two values are related at a given type at a particular world and stepindex. The full definition is given in Fig. 4. The most interesting clauses are the interpretation of function types and reference types.
For function types, we assume that the arguments are related for an arbitrary number of logical steps \(m'\), just as we did for heap satisfaction. We also require the application to be related for one more concrete reduction step than the arguments. This is standard in stepindexed models and reflects the fact that we do at least one concrete reduction step (the betareduction of the application), before using the arguments.
The interpretation of reference types asserts the existence of a general invariant in the current world that is n, m equivalent to the reference invariant \({\text {inv}}(\mathcal {V}\llbracket {\varDelta \vdash \tau }\rrbracket _\rho , l_I, l_S)\). Note that the equivalence is stated at the c.o.f.e., \(\mathop {\blacktriangleright }\mathbf {\widehat{Inv}}\).
In turn, the reference invariant asserts exclusive ownership of locations \(l_I\) and \(l_S\) and that these locations contain \(\mathcal {V}\llbracket {\varDelta \vdash \tau }\rrbracket _\rho \) related values.
For product types, we require that the components are pairwise related and for existential types, we require the existence of a semantic type to interpret the abstract type.
Lemma 9

\({\text {inv}}(\nu , l_I, l_S)\) is nonexpansive and monotone and \({\text {inv}}(\nu , l_I, l_S)(W)\) is downwardsclosed for all \(\nu \in \mathbf {Type}\), \(l_I, l_S \in \mathrm {Loc}\) and \(W \in \mathbf {World}\).

\(\mathcal {V}\llbracket {\varDelta \vdash \tau }\rrbracket _\rho \) is nonexpansive and monotone and \(\mathcal {V}\llbracket {\varDelta \vdash \tau }\rrbracket _\rho (W)\) is downwardsclosed for all \(\rho \in \mathbf {Type}^\varDelta \) and \(W \in \mathbf {World}\).
Proof
(Sketch). We prove the second property by induction on the wellformedness derivation, \(\varDelta \vdash \tau \). Most of the cases are straightforward. For reference types, nonexpansiveness follows from Lemma 8. \(\square \)
Finally, the logical relation relates two expressions \(e_I\) and \(e_S\) at type \(\tau \) if they are related for all stepindices in the expression closure of the \(\tau \)relation, after substituting related values for all free term variables.
Definition 11
The logical relation is compatible with the typing rules of the language. Here we include two of the interesting cases of the compatibility proof, namely dereference and unpack. For illustrative purposes we take a more constrained versions of the lemmas where the arguments of the dereferencing and unpacking operations are values. The accompanying technical report features complete proofs of all the compatibility lemmas in their general form.
Lemma 10
If \(\varDelta ; \varGamma \models v_I \le _{log} v_S : \tau ~\mathsf {ref}\,\) then \(\varDelta ; \varGamma \models {\text {!}}v_I \le _{log} {\text {!}}v_S : \tau \).
Proof
Lemma 11
Proof
The fundamental theorem of logical relations (Lemma 12) and a similar property for contexts (Lemma 13) follow as corollaries of the compatibility lemmas. The proofs follow by induction on the respective typing derivations.
Lemma 12
If \(\varDelta ; \varGamma \vdash e : \tau \) then \(\varDelta ; \varGamma \models e \le _{log} e : \tau \).
Lemma 13
For any context C such that \(C : (\varDelta _i; \varGamma _i, \tau _i) \rightsquigarrow (\varDelta _o; \varGamma _o, \tau _o)\), if \(\varDelta _i; \varGamma _i \vdash e_I \le _{log} e_S : \tau _i\) then \(\varDelta _o; \varGamma _o \vdash C[e_I] \le _{log} C[e_S] : \tau _o\).
Theorem 2
(Soundness). If \(\varDelta ; \varGamma \models e_I \le _{log} e_S : \tau \) then \(\varDelta ; \varGamma \vdash e_I \le _{ctx} e_S : \tau \).
Proof
Let C be an arbitrary context such that \(C : (\varDelta ; \varGamma , \tau ) \rightsquigarrow (; , 1)\) and \(\langle C[e_I], [] \rangle \rightarrow ^* \langle *, h_I \rangle \). Then there exists an i such that \(\langle C[e_I], [] \rangle \rightarrow ^i \langle *, h_I \rangle \). By Lemma 13 it follows that \(;  \models C[e_I] \le _{log} C[e_S] : 1\) and thus \((i+1, C[e_I], C[e_S]) \in \mathcal {E}(\mathcal {V}\llbracket {;  \vdash 1}\rrbracket )([])\). By definition of \(\mathcal {E}\) this gives us \(v_S\), \(h_S\) and W such that \(\langle C[e_S], [] \rangle \rightarrow ^* \langle v_S, h_S \rangle \) and \((1, m, *, v_S) \in \mathcal {V}\llbracket {;  \vdash 1}\rrbracket (W)\) for any \(m\in \mathbb {N}\). From the latter we obtain \(v_S = *\), which ends the proof. \(\square \)
5 Example
The lefttoright approximation, \(; x : \tau \vdash x \le _{ctx} f(x) : \tau \), causes problems for previous stepindexed logical relations, as it requires an additional logical step without introducing a corresponding reduction step on the left. In this Section we prove the lefttoright approximation using our logical relation.
Lemma 14
The higher logical stepindex in the assumption is required since, as we shall see, we need to unfold the recursive domain equation to prove it. Once we have the lemma, if we need to show that \((k, m, v_I, h_S(v_S)) \in \nu (W)\) for an arbitrarym, as the expression closure obliges us to do, and know that \(\forall m.~(k, m, v_I, v_S) \in \nu '(W)\), we can simply instantiate our assumption with \(m+2\) and use it. In this way, the fact that our model allows us to take arbitrary number of logical steps is crucial to allow us to prove this type of abstractions correct. We first prove the preceding lemma, and then turn to formally treating the example.
Proof
Lemma 15
Proof
By Theorem 2 it suffices to prove that x is logically related to f(x): \(; x : \tau \models x \le _{log} f(x) : \tau \).
To show that \(\forall m.~(k1, m, u_I, h_S(u_S)) \in \nu (W'')\), take any \(m \in \mathbb {N}\). Since \(k1\le n''\) and \(W'' \ge W'\) we have \((k1, m+2, u_I, u_S) \in \nu '(W')\), and by Lemma 14 the property holds.
6 Related Work
Stepindexing was invented by Appel and McAllester as a way of proving type safety for a language with recursive types using only simple mathematics suitable for foundational proofcarrying code [5]. Ahmed and coworkers developed the technique to support relational reasoning and more advanced languages featuring general references and impredicative polymorphism [1, 2, 3]. These relational models have subsequently been refined with ever more powerful forms of invariants and applied to reason about local state and control effects [15], compiler correctness [7, 17], typebased program transformations [11] and finegrained concurrent data structures [22], among other things. In another concurrent line of work, stepindexing has been applied to define models of increasingly expressive capability type systems [10] and concurrent program logics [4, 18, 20, 21]. A common thread in both of these lines of work, is increasingly powerful recursivelydefined worlds to capture various forms of invariants. We believe the complexity of invariants and associated recursivelydefined worlds is orthogonal to the problem of the tight coupling between concrete and logical steps. In particular, our fixed point construction for locally contractive functors (Theorem 1) allows us to define recursivelydefined worlds of the same form as prior approaches.
Usually, stepindexed logical relations are indexed over \(\omega \), because the closure ordinal of the inductivelydefined convergence (termination) predicate is \(\omega \). An exception is the logical relation in [8] for reasoning about mustequivalence for a pure functional language without references but with countable nondeterminism. Because of the presence of countable nondeterminism, the closure ordinal of the inductively defined mustconvergence predicate in loc. cit. is not \(\omega \). However, it is bounded by \(\omega _1\), and therefore the logical relation is indexed over \(\omega _1\). Note that this use of transfinite indexing is quite different from our use of transfinite indexing in this paper. Here we use transfinite indexing even though the closure ordinal of the convergence predicate is \(\omega \), because we seek to avoid linking unfoldings of the recursive domain equation to concrete reduction steps in the operational semantics.
Various ways have been proposed for stratifying the construction of semantic domains using stepindexing. These include explicit stepindexing [3, 6], Hobor et al.’s indirection theory [16], Birkedal et al.’s ultrametric approach [12] and Birkedal et al.’s guarded recursion approach [9]. Indirection theory and the ultrametric approach are both currently specific to stepindexing over \(\omega \). Birkedal et al. have shown that sheaves over any complete Heyting algebra with a wellfounded base models guarded dependent type theory [9]. It would be interesting to explore the possibility of using the internal language of sheaves over \(\omega ^2 + 1\) to define and reason about models stepindexed over \(\omega ^2\).
Di Gianantonio and Miculan [13] introduced complete ordered families of equivalences as a unifying theory for mixedvariance recursive definitions that supports transfinite fixed point constructions. They define complete ordered families of equivalences over an arbitrary wellfounded order and prove a generalized fixed point theorem for contractive endofunctions over these complete ordered families of equivalences. This allows for mixedvariance recursive definitions of elements of c.o.f.e.s. We extend their theory with an explicit construction for mixedvariance recursive definitions of c.o.f.e.s, for the specific instance of c.o.f.e.s over \(\omega ^2 \).
7 Conclusion and Future Work
Stepindexing has proven to be a very powerful technique for modelling advanced type systems and expressive program logics. Impredicative invariants are crucial for achieving modular reasoning and they show up in many different forms in recent models of type systems and program logics. Stepindexing allows us to model impredicative invariants by stratifying the model construction using steps. Unfortunately, current stepindexed models relate these steps directly to concrete reduction steps in the underlying operational semantics and require a concrete reduction step for each logical step. This is especially problematic for higherorder abstractions that introduce new logical steps, without any corresponding reduction steps. This is a common occurrence in higherorder program logics when deriving new specifications for specific usecases of libraries from an abstract library specification.
In this paper we have isolated the problem in the setting of logical relations and demonstrated a solution based on transfinite stepindexing. This setting is sufficiently simple that we can present all the necessary details to see how transfinite stepindexing solves the problem. To do so we have developed a general theory for solving recursive domain equations using stepindexing over \(\omega ^2\). Since our theory allows us to solve the equations used in the stepindexed models of cuttingedge program logics, we believe our solution will also scale to these systems, which can hopefully lead to development of more robust reasoning principles.
A natural question to ask is whether stepindexing over \(\omega ^2\) suffices or whether we might wish to index beyond \(\omega ^2\). It is not clear whether indexing beyond \(\omega ^2\) will allow us to prove more equivalences than with our current model. However, it seems plausible that indexing beyond \(\omega ^2\) could simplify reasoning by allowing less precise counting of logical steps and in the particular case of a stepindexed program logic might help with modularity by allowing the logic to abstract over the precise number of logical steps used. We leave these questions open for future work.
Footnotes
 1.
There are stepindexed logical relations, which are complete wrt. contextual approximation [15], which would seem to suggest that they should be flexible enough to prove this example, but completeness is achieved using biorthogonality (a kind of closure under evaluation contexts), which means that while the models are technically complete, they do not offer a practical way of proving this kind of example; cf. the discussion in Section 10 of [15].
 2.
This is caused by the order of quantifiers in the definition: we needed to pick a number of logical steps before we obtained the witnesses from the definition, including \(v_I'\), \(v_S'\) and \(\nu \).
Notes
Acknowledgements
This research was supported in part by the ModuRes Sapere Aude Advanced Grant from The Danish Council for Independent Research for the Natural Sciences (FNU) and Danish Council for Independent Research project DFF – 418100273.
References
 1.Ahmed, A.: Stepindexed syntactic logical relations for recursive and quantified types. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 69–83. Springer, Heidelberg (2006)CrossRefGoogle Scholar
 2.Ahmed, A., Dreyer, D., Rossberg, A.: Statedependent representation independence. In: Proceedings of POPL (2009)Google Scholar
 3.Ahmed, A.J.: Semantics of types for mutable state. Ph.D. thesis, Princeton University (2004)Google Scholar
 4.Appel, A.W., Dockins, R., Hobor, A., Dodds, J., Leroy, X., Blazy, S., Stewart, G., Beringer, L.: Program Logics for Certified Compilers. Cambridge University Press, Cambridge (2014)CrossRefzbMATHGoogle Scholar
 5.Appel, A.W., McAllester, D.: An indexed model of recursive types for foundational proofcarrying code. ACM Trans. Program. Lang. Syst. 23(5), 657–683 (2001)CrossRefGoogle Scholar
 6.Appel, A.W., Melliès, P.A., Richards, C.D., Vouillon, J.: A very modal model of a modern, major, general type system. In: Proceedings of POPL (2007)Google Scholar
 7.Benton, N., Hur, C.K.: Biorthogonality, stepindexing and compiler correctness. In: Proceedings of ICFP (2009)Google Scholar
 8.Birkedal, L., Bizjak, A., Schwinghammer, J.: Stepindexed relational reasoning for countable nondeterminism. Log. Methods Comput. Sci. 9(4), 1–23 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
 9.Birkedal, L., Møgelberg, R.E., Schwinghammer, J., Støvring, K.: First steps in synthetic guarded domain theory: stepindexing in the topos of trees. Log. Methods Comput. Sci. 8(4), (2012) http://www.lmcsonline.org/ojs/viewarticle.php?id=1118&layout=abstract
 10.Birkedal, L., Reus, B., Schwinghammer, J., Støvring, K., Thamsborg, J., Yang, H.: Stepindexed kripke models over recursive worlds. In: Proceedings of POPL (2011)Google Scholar
 11.Birkedal, L., Sieczkowski, F., Thamsborg, J.: A concurrent logical relation. In: Proceedings of CSL (2012)Google Scholar
 12.Birkedal, L., Støvring, K., Thamsborg, J.: The categorytheoretic solution of recursive metricspace equations. Theor. Comput. Sci. 411, 4102–4122 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
 13.Di Gianantonio, P., Miculan, M.: A unifying approach to recursive and corecursive definitions. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 148–161. Springer, Heidelberg (2003)CrossRefGoogle Scholar
 14.Dodds, M., Jagannathan, S., Parkinson, M.J., Svendsen, K., Birkedal, L.: Verifying custom synchronization constructs using higherorder separation logic. ACM Trans. Program. Lang. Syst. 38(2), 1–72 (2016)CrossRefGoogle Scholar
 15.Dreyer, D., Neis, G., Birkedal, L.: The impact of higherorder state and control effects on local relational reasoning. J. Funct. Prog. 22, 477–528 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
 16.Hobor, A., Dockins, R., Appel, A.W.: A theory of indirection via approximation. In: Proceedings of POPL (2010)Google Scholar
 17.Hur, C.K., Dreyer, D.: A kripke logical relation between ML and assembly. In: Proceedings of POPL (2011)Google Scholar
 18.Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L., Dreyer, D.: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In: Proceedings of POPL (2015)Google Scholar
 19.Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: Proceedings of LICS (2002)Google Scholar
 20.Svendsen, K., Birkedal, L.: Impredicative concurrent abstract predicates. In: Shao, Z. (ed.) ESOP 2014 (ETAPS). LNCS, vol. 8410, pp. 149–168. Springer, Heidelberg (2014)CrossRefGoogle Scholar
 21.Turon, A., Dreyer, D., Birkedal, L.: Unifying refinement and hoarestyle reasoning in a logic for higherorder concurrency. In: Proceedings of ICFP (2013)Google Scholar
 22.Turon, A.J., Thamsborg, J., Ahmed, A., Birkedal, L., Dreyer, D.: Logical relations for finegrained concurrency. In: Proceedings of POPL (2013)Google Scholar