1 The OGS Library from the Perspective of a User
Our library is intended to be reusable. In this section, we describe to the interested user how to understand our result, and how to instantiate it.
Soundness
Anzeige
The main result, Theorem 8, is proven in
OGS/Soundness.v. It quantifies over any suitable language machine, that is, an axiomatisation of substitution and evaluation in the style of abstract machines. Slightly unfolding the definitions, it is typed as follows.In plain words, for any final scope \(\varOmega \) and language machine configurations x and y, whenever the two OGS strategies obtained by embedding x and y into initial strategy states are weakly bisimilar, then, for any assignment \(\gamma \), substituting x and y by \(\gamma \) and evaluating them to a final observation yields two weakly bisimilar computations. In other words, either both substituted configurations diverge or both return the same final result.
Language Machine Instantiation
Several example language machines satisfying the OGS soundness hypotheses are provided in the
Examples/ folder. Instantiating our generic semantics and proof with one’s favorite language always follows the same blueprint. First, define the standard syntax and substitution. Then, because the language evaluator must be presented as an abstract machine, define a family of configurations for this machine. Note that this abstract machine must reduce open configurations and these must also support substitution. For some languages such as \(\mu \tilde{\mu }\)-calculus [4], or say, Jump-With-Argument [10], configurations are already a standard notion, but for others such as \(\lambda \)-calculi, they are generally obtained by pairing a term with an evaluation context. Further, define the observation structure. This amounts to deciding which part of normal form configurations should be considered observable for the purpose of observational equivalence testing, and which part should be considered as a set of opaque values. Finally, when all these choices are made and the evaluator written, it suffices to check the theorem hypotheses. In our experience, they are always proven quite directly, without any surprising lemma required.Anzeige
2 Inside the Beast: Implementation Details of Interest
We detail two salient aspects of our development. First, we have implemented strategies as shallow monadic computations, which led us to develop an indexed variant of the Interaction Tree (ITree) structure. Second, we have followed a well-scoped approach, relying on the
library and the
universe.
library and the
universe.This section is intended for expert readers familiar with the companion paper.
2.1 Strategies as Indexed Interaction Trees
Indexed Interaction Trees Library
Rather than specifying labelled transition systems relationally in
, we have chosen a shallow Coq embedding for implementing strategies, understood as possibly non-terminating computations featuring uninterpreted actions (move exchanges). This suggests reusing the ITrees [18] library, which is designed for this purpose. It is also in line with Hancock and Hyvernat’s similar construction of interaction structures [9], which represent agents in client-server protocols as coinductive trees.
, we have chosen a shallow Coq embedding for implementing strategies, understood as possibly non-terminating computations featuring uninterpreted actions (move exchanges). This suggests reusing the ITrees [18] library, which is designed for this purpose. It is also in line with Hancock and Hyvernat’s similar construction of interaction structures [9], which represent agents in client-server protocols as coinductive trees.However, the ITree format for specifying possible actions is not expressive enough for our purposes. In essence, it only captures games where the set of allowed client moves is constant throughout. To fix this, instead of describing possible actions by a polynomial functor on \(\textbf{Set}\), we describe them by an indexed polynomial functor on \(\textbf{Set}^I\), for some set I representing active game positions. The
ITree/ folder thus contains a succinct port of the ITree library to this new indexed setting. This part of the artifact could certainly be useful independently of the OGS construction. We hope to extract it into a self-contained library.This small library contains the coinductive definition of ITrees, their monadic structure, and the standard iteration operator. We provide definitions for weak and strong bisimilarity, together with the main reasoning principles: strong bisimulation up-to equivalence, and weak and strong bisimulation up-to monadic bind. Both bisimilarity relations are defined using the 
universe.
Coinduction [14] library, which provides enhanced coinduction principles based on a lattice-theoretic fixed point construction.1 This relies on the impredicativity of the
universe.Eventually Guarded Iteration
Apart from indexing, the main novelty is a pair of new iteration operators, respectively for guarded and eventually guarded iteration (Prop. 5). They have been crucial in our OGS soundness proof and could certainly be backported to the unindexed ITree library.
The standard unguarded operator can iterate any “loop body”, but it must insert a silent step after each iteration to be well-defined. Hence, it only produces a fixed point of the loop body w.r.t. weak bisimilarity, and it is in general not unique. By contrast, our two new operators do not insert any silent step after iteration, and produce unique fixed points w.r.t. strong bisimilarity. For this to work, they respectively require the loop body to feature a guard (a computation step) at each iteration or infinitely often, i.e., after a finite number of iterations.
Theoretically, unguarded iteration can be axiomatised as a complete Elgot monad structure [7] on ITrees quotiented by weak bisimilarity, while our new guarded iteration operators yield two completely iterative monad structures with different notions of guardedness on ITrees quotiented by strong bisimilarity [8].
Relationship with Transition Systems over Games
Following Levy and Staton [11], in the paper (Def. 19), we define strategies over some game \(\mathcal {G}:\texttt{Game}\,I J\) as a pair of active and waiting state families \(S^+ :\textbf{Set}^I\) and \(S^- :\textbf{Set}^J\), together with action and reaction morphisms. This data is dubbed by Levy and Staton a big-step system over G and can be more succinctly expressed as a coalgebra for the following endofunctor on \(\textbf{Set}^I\times \textbf{Set}^J\).Instead of working with arbitrary coalgebras, we can equivalently see strategies as their image in the final coalgebra, whose states consist of coinductive trees. We do not construct this final coalgebra directly, but instead express it using our indexed interaction tree datatype. Given a polynomial endofunctor \(\varSigma \) on \(\textbf{Set}^I\) and an output family X, indexed interaction trees are given by the following final coalgebra:2 \(\texttt{itree}_\varSigma (X) :=\nu S.~X + S + \varSigma (S).\)
$$\begin{aligned} (S^+, S^-) \mapsto (\mathcal {D}(\texttt{final}_\mathcal {G}+ \llbracket \texttt{client}_\mathcal {G} \rrbracket ^+S^-),~ \llbracket \texttt{server}_\mathcal {G} \rrbracket ^-S^+) \end{aligned}$$
The trick is to focus on strategies in some active position, by considering the sequence of choosing a client move and waiting for the next server move as one unit. Indeed, the composition \(\llbracket \texttt{client}_\mathcal {G} \rrbracket ^+ \circ \llbracket \texttt{server}_\mathcal {G} \rrbracket ^-\) is a polynomial functor, and states of the final coalgebra of strategies over \(\mathcal {G}\) may be computed as:3
Our implementation choices are then straightforward. We encode polynomial endofunctors on \(\textbf{Set}^I\) as indexed containers [2], which we dub events.
$$\begin{aligned} & \texttt{strat}^+_\mathcal {G}:=\texttt{itree}_{(\llbracket \texttt{client}_\mathcal {G} \rrbracket ^+ \circ \llbracket \texttt{server}_\mathcal {G} \rrbracket ^-)} \texttt{final}_\mathcal {G}\\ & \texttt{strat}^-_\mathcal {G}:=\llbracket \texttt{server}_\mathcal {G} \rrbracket ^-\texttt{strat}^+_\mathcal {G}. \end{aligned}$$
For some indexed container
and output family
, the interaction tree endofunctor and its final coalgebra are respectively:
and output family
, the interaction tree endofunctor and its final coalgebra are respectively:2.2 Scope Structures
Our development of intrinsically-typed-and-scoped syntax largely follows standard practice [1, 6]. As this mechanisation style is heavy on dependent pattern matching, we make great use of the
Equations plugin [16]. A notable novelty is that we abstract over the concrete representation of scopes and variables, which are usually fixed to lists of object language types and well-typed de Bruijn indices. Our motivation was pragmatic: using tailor-made variable representations drastically reduced the amount of boilerplate in complex \(\mu \tilde{\mu }\)-calculi instances.The root cause is that most standard OGS examples involve separating object language types into so-called positive and negative classes, with only variables of negative types being shared and observed between OGS players. Given a strict predicate
, negative types can be constructed as the strict subset
. The prime benefit is that definitional equality of negative types is exactly definitional equality of the underlying “vanilla” types. For scopes containing only negative types, we lose this nice property if we represent them naively as
. It is vastly more convenient to work with the subset
, where
denotes the strict universal quantifier on lists.
, negative types can be constructed as the strict subset
. The prime benefit is that definitional equality of negative types is exactly definitional equality of the underlying “vanilla” types. For scopes containing only negative types, we lose this nice property if we represent them naively as
. It is vastly more convenient to work with the subset
, where
denotes the strict universal quantifier on lists.To allow for such “non-standard” scope representations and their custom notion of well-typed variable, we devise a notion of scope structure, close in spirit to the Nameless, Painless approach [13]. A scope structure on \(S :\textbf{Set}\) for object language types T consists of an element \(\varnothing :S\), a binary operation \(\oplus :S \rightarrow S \rightarrow S\) and a family of variables \(\ni :S \rightarrow \textbf{Set}^T\), equipped with two isomorphisms \(\varnothing \ni t \approx \bot \) and \((\varGamma \oplus \varDelta ) \ni t \approx (\varGamma \ni t) \uplus (\varDelta \ni t)\). The category of contexts is then taken to be the full image of \(\ni \). In other words, objects are elements of S and renamings \(\varGamma \rightarrow \varDelta \) are given by functions \(\forall t, \varGamma \ni t \rightarrow \varDelta \ni t\). This interface can then be instantiated both by lists and de Bruijn indices as well as by our “subset scopes”. The substitution metatheory is left mostly unchanged.
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.
