Das Kapitel präsentiert eine abstrakte, zertifizierte Darstellung der operativen Spielsemantik, wobei der Schwerpunkt auf normaler Form-Bisimulation als Technik zum Nachweis der kontextuellen Äquivalenz von Programmen liegt. Es stellt das Konzept der Substitutionsäquivalenz vor, ein abstraktes Analogon der kontextuellen Äquivalenz, und demonstriert, wie es verwendet werden kann, um Soliditätsnachweise für Normalform-Bisimulation zu erbringen. Das Kapitel bietet einen detaillierten Überblick über die technische Entwicklung, einschließlich der Erstellung eines funktionsfähigen Spielsemantikmodells für jede Sprachmaschine und den Nachweis ihrer Solidität. Sie diskutiert auch die Mechanisierung der Ergebnisse in Coq, betont ihre rechnerischen Aspekte und begründet das Modell in einer konstruktiven Meta-Theorie. Das Kapitel schließt mit einem Vergleich bestehender Literatur und einer Diskussion zukünftiger Perspektiven ab, wobei das Potenzial für die Einbeziehung weiterer sprachlicher Merkmale und die Untersuchung der Vollständigkeit in den abstrakten Rahmen hervorgehoben wird.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
Operational game semantics (OGS) is a method for interpreting programs as strategies in suitable games, or more precisely as labelled transition systems over suitable games, in the sense of Levy and Staton. Such an interpretation is called sound when, for any two given programs, weak bisimilarity of associated strategies entails contextual equivalence. OGS has been applied to a variety of languages, with rather tedious soundness proofs.
In this paper, we contribute to the unification and mechanisation of OGS. Indeed, we propose an abstract notion of language with evaluator, for which we construct a generic OGS interpretation, which we prove sound. Our framework covers a variety of simply-typed and untyped lambda-calculi with various evaluation strategies. These calculi notably feature recursive definitions, first-class continuations, and a wide variety of datatypes. All constructions and proofs are entirely mechanised in the Coq proof assistant.
1 Introduction
Normal form bisimulation is a technique for proving contextual equivalence of programs in various
-calculi. Although it is generally finer than contextual equivalence, its practical value resides in the fact that it is often easier to establish on concrete examples than other such techniques, such as applicative or environmental bisimulation.
Let us briefly explain why. All three techniques proceed by defining a notion of label, an interpretation of programs as labelled transition systems (LTSs), and then comparing the interpretations of programs w.r.t. weak bisimilarity. However, the involved labels are very different. Indeed, applicative or environmental labels may contain arbitrary values, while normal form labels are restricted to so-called ultimate patterns. This means that they may be, e.g., tuples or elements of sum types, but cannot contain
-abstractions. In a typed setting, in particular, all terms of functional type contained in any ultimate pattern must be variables. Normal form labels thus contain a very limited class of terms.
Anzeige
In order for it to be useful, normal form bisimulation should be sound, i.e., at least as fine as contextual equivalence. One standard method for proving soundness goes through an intermediate LTS model, with labels similar to the normal form ones, but a different interpretation, called operational game semantics [20, 22] (OGS). This induces a different equivalence, say operational game bisimulation. One then proves that normal form bisimulation is at least as fine as operational game bisimulation, which is in turn at least as fine as contextual equivalence. Although the first step is mostly straightforward, the second one is difficult, notably because it involves
extending the OGS interpretation to suitable contexts, and
soundly reflecting the syntactic operation of context application at the level of LTSs.
Because such soundness proofs are highly non-trivial, it seems useful to design an abstract version, covering as many existing cases as possible, and hopefully also future ones.
A few authors have started to explore this direction. Notably, Levy and Staton [23] offer a high-level categorical framework. More recently, Laird [21] proposes a unifying framework for OGS, in which he proves that operational game bisimilarity is a congruence w.r.t. composition, a standard lemma towards soundness.
Contribution In this work, we go further, and prove a generic soundness result for OGS, mechanised in Coq. We thus contribute to both unification and mechanisation of normal form bisimulation. Our contributions to unification are as follows.
Anzeige
We introduce an abstract notion of language with evaluator, called a language machine, which notably covers several variants of
-calculus [5, 6].
For any language machine, we construct an OGS model.
We prove that this model is sound w.r.t. some abstract analogue of contextual equivalence called substitution equivalence, under suitable hypotheses.
We furthermore provide a complete Coq mechanisation of our results [2], to emphasise their computational aspects and firmly ground our model in a constructive meta-theory. We favour a traditional, code-less exposition along the paper for clarity. For the interested reader, we however systematically use hyperlinks represented by () to link definitions and theorems to their mechanised counterpart. The Coq development is inspired by Levy and Staton’s transition systems over games [23], and includes notably the following main contributions.
We present OGS using the well-scoped approach (), in the sense that everything is indexed by typing contexts, and variables are accessed as de Bruijn indices. This contrasts with previous work, which uses nominal style.
We instantiate our abstract notion of language on several concrete examples: a simply-typed call-by-value
-calculus with recursion (), a pure untyped call-by-value
-calculus (), the
-calculus [5] () and the polarised System D () from Downen and Ariola [6].
We implement () an indexed variant of the interaction trees library [29], which we use to define LTSs coinductively — as opposed to the more traditional, relational definition. However, in this extended abstract, we focus more on the math than on the Coq implementation, so interaction trees do not appear (see Remark 9).
We introduce () a new fixed-point combinator over a system of so-called eventually guarded equations, whose solution is unique w.r.t. strong bisimilarity. We use this combinator to define composition of OGS LTSs, which is a crucial ingredient to the soundness proof.
Plan Before diving into the details, let us provide a high-level overview of the technical development in §2. In §3, we explain substitution equivalence, our abstract approach to contextual equivalence, on a concrete example language. In §4, we then introduce abstract language machines, construct the OGS model of any language machine, and state our soundness result. Finally, we provide a comparison with the existing literature in §5, and conclude and give some perspectives in §6.
2 Overview
2.1 Axiomatising contextual equivalence as substitution equivalence
Soundness proofs for normal form bisimulation can be established by the following chain of inclusions
Compared to contextual equivalence, CIU (Closed Instantiation of Use) equivalence restricts the shape of contexts that are considered. This idea of restricting contexts while keeping the same discriminating power was first explored by Milner [27]. This idea was then systematized by Mason and Talcott, who introduced CIU equivalence and proved that it coincides with contextual equivalence [24].
In this work, we focus on the middle inclusion:
In order to propose an abstract version of it, we start by streamlining the usual concrete presentation of languages and CIU equivalence.
Standard CIU equivalence checks that two programs, say
and
, behave the same under any closed instantiation
of their free variables, in any closed evaluation context
of some fixed, basic type like the booleans1:
for some sensible notion
of observation of closed boolean programs, usually cotermination on the same boolean.
This involves both substitution and context application, which is a bit clumsy. In order to avoid having two distinct operations in the abstract setting, we switch to a presentation that unifies them. This presentation is based on abstract machines: one evaluates configurations rather than programs, where a configuration consists of a pair
of a program
and an evaluation context
. In particular, instead of comparing programs
and
as before, we now compare configurations
and
, where
denotes a fresh context variable. And now CIU equivalence is merely a matter of substitution: combining any substitution
with
, we get
and similarly for
.
This is presented in detail in §3, but, briefly, it involves a change of typing paradigm: evaluation contexts are typed like continuations, with “negated” types. E.g., if
has type
, then
has type
. And in a configuration
,
and
have opposite types, e.g.,
and
. We tend to use
to range over simple types, and
to range over the disjoint union of simple types and formally negated simple types.
In this presentation style, evaluation contexts are written inside-out in a stack-like manner, and reduction rules “push” the evaluation context from
to
, and “pop” it when needed, e.g.,
(1)
(2)
Here,
is the inside-out analogue of the evaluation context
. Thus:
the first rule is “searching” for the next redex in the function part of the application
, storing the argument part in the evaluation context, while
in the second rule, the configuration
represents
, so the rule is like a
-reduction in context
.
In conclusion: in the presentation based on abstract machines, CIU equivalence becomes substitution equivalence, which equates configurations
and
when
for all closed substitutions
, where
denotes some suitable, yet straightforward notion of equivalence on closed configurations.
2.2 Axiomatising evaluation, a.k.a. normal forms as triples
Our next step is to analyse how OGS exploits evaluation, and then abstract over it.
To start with, let us consider a configuration
that gets stuck on a function call
, where
is a variable and
is some value, say of the form
. In the abstract machine presentation, this means
reduces to
(3)
for some evaluation context
. The compound evaluation context
means that, once
is evaluated, it should be applied to
, the result of which should be fed to
.
In such a situation, OGS splits the stuck configuration (3) into
a head variable, here
,
a first-order approximation of the evaluation context, which we will call the observation2, and
a substitution called a filling.
In this case, assuming
has some functional type
, the observation, say
, is
, for fresh variables
and
, and the filling, say
, is the assignment
In particular, the stuck configuration
may be recovered as
, where
denotes the result of filling the hole in
with
, i.e.,
, and
denotes capture-avoiding substitution of
in
.
Terminology 1
For clarity, we will now explicitly distinguish between the two meanings of “substitution”: we continue calling the operation substitution, while we call the sequence of values passed as arguments to the operation assignments.
To fix intuition, here is a table displaying a few examples of normal forms, including the one presented previously. They are given both using standard syntax and in the abstract machine presentation. We also present how they may be split into head variable, observation, and filling:
A particular case of a normal form is indeed any value
. In the abstract machine presentation,
must be fed to some context variable
, which we view as the head variable. The observation, here denoted by
, means that the observed variable
is fed with some value
, while the filling associates
to
.
The second row is the previous example.
In the third row,
is an evaluation context that takes the
th component of the running program and continues with
. The corresponding reduction rule is
.
In the fourth example,
is an evaluation context that executes
or
according to whether the running (boolean) program evaluates to true or false. The reduction rules are
(4)
Since our axiomatisation of evaluation is devoted to OGS, it inlines this splitting process. It goes in two steps:
A language on a given, fixed set of types consists of suitably indexed sets of values, configurations, and observations. Fillings are then defined as suitable assignments from variables to values, and they are assumed to act on values, configurations, and observations – this axiomatises substitution.
An evaluator consists of a suitably indexed family of partial maps from configurations to triples of a (head) variable, an observation, and a filling. Intuitively, any configuration either diverges (which is modelled by partiality), or converges to some triple
. In other words, we model normal forms as triples
.
Conversely, a refolding is a map sending such normal forms back to configurations. Intuitively, this merely maps
to
.
A language machine is a language equipped with an evaluator and a refolding, satisfying a few coherence axioms (Definition 13). Notably, in order to ensure soundness of OGS, we need to require that evaluation respect substitution, which roughly means that evaluating a substituted configuration
amounts to evaluating
, and, if this converges to some normal form
, evaluating the substituted refolding of
.
Remark 1
Of course, this definition is informal, notably w.r.t. substitution. In particular, Definition 13 relies on the well-known machinery of substitution monoids and modules over them [9‐11, 14, 15].
Remark 2
Indexing here refers to the fact that our axiomatisation is intrinsically typed and scoped. Thus, e.g., configurations are indexed over lists of types, values are indexed over sequents, i.e., pairs of a list of types and a type, and so on.
2.3 Substitution equivalence
The notion of language machine lets us define substitution equivalence, abstractly. In the usual presentation of
-calculus, we were observing closed programs of some fixed, basic type like the booleans
. Transposed to the abstract machine presentation, this amounts to observing configurations with a single free variable of type
, which models the final continuation to which the closed context returns. There are only two observations at that type, namely
and
, for true and false, which correspond to the two expected observations.
In the abstract setting, i.e., in any given language machine, we postulate a fixed, “final” typing context
, and think of configurations with free variables in
as closed programs. The obvious way to observe them is to check whether they diverge, and otherwise record which observation they perform on which free variable of
.
Thus, two configurations
and
with free variables in
are substitution equivalent iff, for all assignments
from variables in
to values of the same type over
,
and
coterminate, and, if they do terminate, perform the same observation on the same variable of
.
2.4 Games and strategies
We now would like to construct the OGS of any language machine, but before that we need to define what we mean by games and strategies. For this, we follow Levy and Staton [23], up to slight reformulation.
We first introduce half-games from
to
, for any sets
and
of Player and Opponent positions, respectively. Intuitively, a half-game describes the moves available in each Player position, and the Opponent positions they lead to.
A game over
and
then consists of a Player half-game from
to
, and an Opponent half-game from
to
.
A strategy then consists of
an
-indexed family of active states, where Player is to play,
a
-indexed family of waiting states, where Opponent is to play,
an action partial map, which, to any active state over a position
, either diverges, or picks a move from
and a “next” waiting state, and
a reaction map, which, to any waiting state and Opponent move over a position
, associates a “next” active state.
2.5 Constructing the game
We saw that evaluators are viewed as either diverging, or splitting configurations into a head variable
, an observation
, and a filling
. This splitting is used to interpret the considered configuration
as a strategy in a two-player game, where the program plays as Player and the context plays as Opponent. Let us briefly describe this game, which we call the OGS game.
As a first approximation, the game in question has the same Player and Opponent positions, which consist of pairs
of typing contexts:
(i)
variables in
are thought of as defined by the currently waiting player, say
, hence unknown to the currently active player, say
,
(ii)
conversely, variables in
are defined by
, hence unknown to
.
Accordingly, a move (by
) consists of an observation on some variable in
. Such an observation may introduce some fresh variables, which are modelled as a typing context
that we call the context increment. Intuitively,
holds the definitions of variables in
, and the next position is
the definition of variables in
are held by the now waiting player
, while
those of variables in
are held by the now active player
.
Example 1
If
, then a possible move is
, with context increment
.
Weak bisimilarity
of strategies is then defined straightforwardly: either both diverge, or they both converge, play the same move, and reach weakly bisimilar strategies, coinductively.
2.6 Constructing the OGS
The crux of OGS is then to interpret the language machine as a strategy in the OGS game. This strategy, which we call the machine strategy, is essentially straightforward:
an active state over
consists of a configuration
with free variables in
, and, for each
, a value of type
with free variables in
, which we (continue to) call an assignment
;
waiting states over
are assignments
;
the action of any configuration
and assignment
consists in evaluating
, and diverging if it does; otherwise, it evaluates to some normal form
, for some filling
of the context increment
of
; the machine strategy then
plays the move
, and
picks as its next waiting state the compound assignment
, over the position
;
the reaction of an assignment
to any move
with context increment
is the configuration obtained by refolding
, up to some technicalities that we hide under the rug for the moment. In particular, variables in the context increment
remain fresh for this player.
At this point, we may state the soundness property: any two configurations which give weakly bisimilar strategies are substitution equivalent.
In order to prove it, it remains to work around a few technical glitches, which we briefly describe in the coming subsections. The first amounts to taking the final typing context
into account at the level of games: this is easy. The second is well known to the experts: it is the “infinite chattering” problem. We deal with it in a novel way, by building acyclicity into the model. The final difficulty is new and surprising. It has to do with the fact that, in all sensible languages, repeated, non-trivial instantiation of the head variable eventually leads to some redex. In the abstract setting, we need an additional hypothesis to ensure this is indeed the case.
2.7 Final moves
It might be tempting to treat the “final” typing context
normally, i.e., to make it part of positions
. But it would not work. Indeed, once a player makes a final move, the game must stop, in order to reflect the notion of observation that was fixed for substitution equivalence.
We thus tweak the naive definitions of games and strategies given above to incorporate this idea:
(1)
A game comes with a set of final moves.
(2)
The action map of a strategy may either play a proper move as before, or play a final move.
(3)
The final moves of the OGS game are observations on variables in the final typing context
.
(4)
States of the machine strategy are modified similarly: active states over
comprise a configuration with free variables in
and an assignment
, while waiting states are assignments
.
(5)
The action map of the machine strategy discriminates against the head variable: if it is in
, then a proper move is played; if it is in
, a final move is played.
(6)
Finally, we adjust weak bisimilarity accordingly: if one strategy plays a final move, then the other should play the same, and conversely.
At the cost of some moderate additional verbosity, this builds the protocol of substitution equivalence into weak bisimilarity of OGS strategies.
2.8 Infinite chattering
Let us now deal with the second announced technical glitch: the infinite chattering problem. A symptom of it is already visible in our description of OGS. Indeed, from a pair of an active and a passive states on a given position
, we would like to be able to recover a corresponding configuration with free variables in the final typing context
. Such a pair of states amounts to a configuration with free variables in
, and assignments
so one might hope that substituting
with
and
in turn would converge to some configuration with free variables in
. This in fact holds for pairs of states arising from the game, but not for all pairs.
Example 2
For a silly example, consider a case where some free variable
of
is mapped by
to some variable
in
, which is in turn mapped to
in
by
.
Such cyclic configurations do not arise during the game, though. Crucially, in the above description, when we form the new waiting state
, we know that the other assignment
does not depend on the new variables in
.
This leads us to introduce a refined version of the game, in which positions record the sequence of context increments, and states of the machine strategy take them into account to build acyclicity into the model. Positions are thus sequences
of typing contexts.
The idea is that, if the current position is a sequence
of context increments, then
was introduced by the previously active, now waiting player
. Accordingly:
A (non-final) move consists of a variable introduced by
, i.e., one in
, together with an observation
on it – the first index in the sequence depending on the parity of
. The next position is of course
, where
denotes the context increment of
.
An active state of the machine strategy is a configuration with free variables in
, equipped with assignments
as on the left below.
(5)
A passive state consists of complementary assignments
as on the right above.
This time, it is easy to recover a well-defined configuration with free variables in
from an active-passive pair of states, as
(6)
2.9 Focused redexes and eventual guardedness
Let us now come to the last technical glitch that we had to face. It surprised us, as it is rather theoretical: we know of no concrete, sensible language machine in which it arises. It may be viewed as a form of infinite chattering. Let us briefly explain it. A key lemma in virtually any OGS soundness proof roughly states the following: given any compatible pair of an active state
and a waiting state
, the configuration (6), obtained by iterated substitution, behaves the same as letting the strategies associated to
and
play against one another. This lemma is simply wrong in general, so we need an additional hypothesis.
A bit more formally, one defines a composition operation. The result of composition may either diverge or play a final move in
. And the key lemma states that the refolded configuration (6) diverges iff the composition does, and, if not, both play the same final move in
.
The difficulty lies in the definition of composition. In principle, it should work as follows. An invariant is that one of the two given strategies is active while the other is waiting. The composition, say
, is then computed like so:
If the active strategy diverges or performs a final move, then so does the composition.
If the active strategy performs a non-final move, then the waiting strategy reacts to it, the roles are switched, and we start over.
As a first step towards making this precise, we must give a bit more detail on how we handle partiality. For us, a partial map
is a map
, where
is Capretta’s delay monad [3], which we briefly recall in §4.2. This is a rather intensional description of partiality, in the sense that an element of
consists of a sequence of “silent computation steps”, denoted by
, which is either infinite or followed by some “result” in
.
This suggests interpreting the above description as a Coq cofixpoint definition. However, the second clause does not satisfy Coq’s guardedness criterion! Let us illustrate this:
Example 3
Consider
and
, for some program
and evaluation context
. Since
is a normal form,
plays without any computation step the non-final move
on
, and the second recursive clause above says that the composition
equals the composition
thus making an unguarded corecursive call.
Remark 3
At this point, it is tempting to insert a dummy computation step to make the definition guarded. This does give the expected definition up to weak bisimilarity, but makes the proof break later on, as explained in §4.7.
To justify further, in the above example, semantically, the unguarded call seems right, because it matches the behaviour of
as a whole, our stated goal for composition. Indeed, the second clause models communication between
and
, which is invisible in the behaviour of
.
In order to solve the issue, we need to make sure that no two strategies get stuck in a loop involving only the second clause. This is really subtle: if both players keep on exchanging non-final moves, interleaved with computation steps, then composition is well defined (and diverges); so the only problematic case is when both players exchange non-final moves indefinitely without performing any computation step.
How could this happen? In the machine strategy, when both players exchange a non-final move, the head variable gets instantiated. So the question becomes: in concrete cases, how could repeated instantiation of the head variable not lead to a redex? A first possibility is if the head variable always gets replaced by another variable. But this is ruled out by the refinement introduced in the previous subsection to deal with infinite chattering. Indeed, if some non-final move leads to a head variable
being instantiated by another variable
, then acyclicity tells us that
must have been introduced before
. Since this is a well-founded ordering, we are safe on this front.
However, this does not suffice in all languages!
Example 4
Consider a language involving
-abstraction, with an exotic redex of the form
Then, starting from a situation with
active state given by the configuration
and empty assignment,
and passive state given by
,
the first move consists of the observation
on
, leading to
as active state
and
as passive state
.
We are then stuck in a loop between situations of the following forms
where we ignore the fine layering of assignments for readability.
In order to rule out languages in which this issue arises, we state our main result under the hypothesis that a suitable binary relation
on observations should be well-founded. Explicitly, we have
iff there exist
,
,
, and a non-variable
such that substituting
for
in the refolding
yields some normal form (without evaluating!) of the shape
, i.e.,
When
is well-founded, we say that the considered language machine has focused redexes.
Assuming that the considered language machine has focused redexes, we should be able to define composition. However, Coq does not readily accept the definition sketched above, because it does not know that it is productive. In order to proceed cleanly, we introduce a relaxed fixed point operator which contents with a proof that, even though the given equations are not directly guarded in the usual sense, unfolding the definition of each unknown will reach a guard eventually. This enables us to define composition, and at last prove our main result (Theorem 8), which states that any language machine with focused redexes has a sound OGS.
3 ciu equivalence through substitution equivalence
In this section, we explain the idea of substitution equivalence, and the necessary pre-processing step that comes with it, on a simple example, namely simply-typed, call-by-value
-calculus with a boolean type and recursive functions. Terms are generated by the following grammar
where
binds
and
in
, as usual. The language is typed. Types and typing contexts are generated by the following grammar,
with the following, standard typing rules.
From now on, all terms are implicitly considered as coming with a typing derivation. Capture-avoiding substitution is defined as usual, and evaluation contexts are defined by the following grammar, with straightforward typing rules.
Context application is defined accordingly. Finally, evaluation is defined by the following inference rules.
As explained in the introduction, ciu equivalence of
and
is defined to mean
, for all closing substitutions
and boolean contexts
, for some fixed equivalence relation
between boolean closed programs. More precisely,
Notation 2
We write
for assignments to each variable
of a value of type
in typing context
.
Definition 1
Two programs
of type
are deemed observably equivalent whenever we have
iff
, and similarly with
.
Definition 2
For any context
and type
, two programs
are ciu-equivalent, which we denote by
, iff for all assignments
, and closed evaluation contexts
of type
with a hole of type
,
and
are observably equivalent.
With the main purpose of unifying notions, and hence simplifying the abstract framework, we want to put context application
and substitution
on an equal footing in this definition. The overall idea is to compile our simply-typed, call-by-value
-calculus down to a slightly lower-level language, as explained in §2.1.
Fig. 1.
Typing and evaluation rules for the lower-level variant of call-by-value
-calculus
Let us now introduce the low-level language. Low-level types
are either simple types
, or negated simple types
. Programs have simple types
, while evaluation contexts have negated types
. We have syntactic categories for programs and evaluation contexts, and a configuration is a pair of a program of some type
and of an evaluation context of type
. Values and programs are defined and typed exactly as before. Evaluation contexts and configurations are specified by the following grammar.
The typing rules for values and programs are again exactly as before (except that typing contexts may now comprise evaluation context variables). Furthermore, the variable typing rule now covers the fact that any evaluation context variable
is an evaluation context of type
. Additional typing rules, for evaluation contexts and configurations, are shown in the first part of Figure 1. Capture-avoiding substitution is defined straightforwardly, and evaluation rules are displayed in the second part of Figure 1. We may now introduce substitution equivalence.
Definition 3
For any typing context
, two configurations
are substitution equivalent, which we denote by
, iff for all assignments
,
and
are observably equivalent, in the sense that we have
iff
, and similarly with
.
The main point of this section is:
Proposition 1
For any typing context
and type
of the source language, two programs
are ciu-equivalent iff, in the typing context
(with
fresh w.r.t.
),
and
are substitution equivalent.
Proof
There is a bijection between assignments
in the lower-level language and pairs of an assignment
and an evaluation context
of type
with a hole of type
in the source language. Furthermore, for such assignments and evaluation contexts,
and
are observably equivalent in the obvious sense, hence the result follows.
4 Abstract OGS
In this section, we fill the gaps left by the informal overview of §2.
4.1 An abstract account of substitution
Let us first recall (one presentation of) a standard way of abstracting over capture-avoiding substitution.
Notation 3
We fix a set
of types for the whole section, and let
denote the set of sequences of types.
The ambient setting for axiomatising substitution is that of families:
Definition 4
For any sequence
of sets, we extend the set
to a category, by taking
as hom-set
, for any
. In particular, we call the objects of
and
, unsorted and sorted families, respectively.
Example 5
A sorted family of particular interest is the one of variables (), given by the proof-relevant
predicate:
denotes the set of indices at which
occurs in
.
Let us now explain what it means for sorted and unsorted families to be equipped with substitution. As is standard in the well-scoped approach, we mean substitution in the parallel sense. The basic ingredient for this is the following standard notion, which we call assignment.
Definition 5
(). For any typing contexts
and sorted family
, an
, or assignment when
is clear from context, consists of an element of
, for all
. In other words, we have
In order to axiomatise substitution for both kinds of families, we introduce the following notion of power families:
Definition 6
Fixing a sorted family
, for any sorted family
and unsorted family
, we define the power objects
by
We may now axiomatise substitution, for both kinds of families:
Definition 7
(). A substitution monoid is a sorted family
, equipped with morphisms
subject to associativity and unitality laws.
Definition 8
(). A substitution module over a substitution monoid
, or substitution-module for short, is an unsorted family
, equipped with a morphism
subject to assocativity and unitality laws.
In both cases, the substitution morphism takes elements over any context
(and type
, if relevant) and assignments
, to elements over
: this is indeed the expected type for substitution.
4.2 Modelling divergence: the delay monad
Now that we have recalled the standard axiomatisation of substitution, let us explain more precisely how we handle divergence in Coq, which is very simple and standard: we use Capretta’s delay monad [3].
Definition 9
(). The delay endomap on
is defined coinductively by the following inference rules.
We also denote by
the pointwise liftings of delay to categories of families
, e.g.,
and
.
Remark 4
The notation
is meant to suggest a silent computation step. Such
s should not be confused with types, which hopefully will be easy from context.
Elements of
are thought of as potentially diverging computations of type
: divergence is modelled by the infinite chain of
s; converging computations have the shape
.
Depending on context, we will consider elements of
equivalent up to strong or weak bisimilarity, which we now recall.
Definition 10
For any relation
between sets (or families)
and
, we let
be such that
iff
and
either both diverge, or evaluate to some
and
with
. We write
for weak bisimilarity (), which we define as
.
We write
for strong bisimilarity (), the canonical lifting of
to the delay coinductive type: either both sides loop or both converge to the same element in the same number of
steps.
Notation 4
We write interchangeably
and
for the bind () operator of
—evaluate
, and if it returns some
, then evaluate
.
4.3 Language machines and substitution equivalence
Let us now introduce our axiomatisation of evaluation and observation more formally than in the overview. We will then wrap this all up into the definition of language machines, and define substitution equivalence.
Definition 11
(). An evaluation structure on any unsorted families
consists of maps:
and
such that
.
Remark 5
By Definition 10, the equation says that evaluating the embedding
of some normal form
yields
in zero computation steps.
Definition 12
(). An observation structure
is a type-indexed set
together with a map
.
For any observation structure
, we define the unsorted family
of pointed observations by
We extend the map
to
, defining
by
Thus, a pointed observation over
consists of a variable, together with an observation at its type.
Remark 6
In the literature, observations are sometimes called ultimate patterns [22], continuation patterns [30], atomic values [20], or abstract values [18].
Definition 13
A language machine consists of
a substitution monoid
of values,
a substitution
-module
of configurations,
an observation structure
,
an evaluation structure on
and
,
where
.
Evaluation and refolding are furthermore required to respect substitution (), in the sense that, for all
,
,
, with
and
, the following hold
where we denote
both substitution maps and pointwise substitution by
, and
the refolding
of any normal form
by
.
Remark 7
By pointwise substitution, we mean that
.
Notation 5
In the sequel, we often treat refolding
as an implicit coercion. We also extend the notation
to arbitrary values, writing
for
, for fresh
.
Example 6
The lower-level language of §3 forms a language machine. We take
to consist of types
and negated types
(i.e., it is the disjoint union of two copies of simple types);
consists of configurations
;
consists of values
, and
consists of all contexts
. Before defining
, we introduce the family
of ultimate values, which is the subfamily
defined inductively by the following linear type system,
where we write
for
. In words, at each
(a simple or negated simple type),
is an ultimate value; we have
, and so on. We then define
with similar notation:
Let us now define substitution equivalence, for any language machine
.
Definition 14
(). We define
at any
to be the composite
Definition 15
(). For any fixed final typing context
, two configurations
are substitution equivalent at
, written
, iff:
4.4 Games and strategies
We now turn to making precise the contents of §2.4. Levy and Staton’s notion of game is parameterised by sets
and
of client and server positions, respectively. The definition then proceeds to postulate families of client moves from
to
, and server moves from
to
. As this is symmetric, we start by introducing a notion of “half-game”, and then define games as pairs thereof.
Definition 16
A half-game () over sets
and
consists of an
-indexed family of moves
, and a next map in
. We denote by
the set of half-games over
and
.
A game () over sets
and
consists of a client half-game in
, a server half-game in
, and a set of final moves. We denote by
the set of games over
and
.
Notation 6
We denote by
and
the components of any half-game
, and by
,
, and
the components of any game
.
We will need the following notion of dual game.
Definition 17
The dual
of a game
is defined by swapping the client and server:
,
and
.
Now that games are defined, we turn to defining strategies in a game. We proceed coalgebraically, for which we need the following “derived” functors.
Definition 18
(). Given any half-game
, we define two functors
, the action functor
and the reaction functor
:
We may now define strategies.
Definition 19
Given a game
, a strategy for
consists of families
and
of active and waiting states, respectively, together with
which we respectively call the action and reaction morphisms.
We denote by
the set of strategies for
.
Notation 7
We denote by
and
the action and reaction morphisms of any strategy
.
Remark 8
The occurrence of the (family lifting of the) delay monad in the action morphism means that we allow Proponent to “think forever” and never actually play. This is crucial for interpreting languages with general recursion.
Remark 9
In the code, this is where indexed interaction trees come in. We define strategies () not as coalgebras, as here, but as interaction trees, i.e., elements of the final coalgebra
The main point of OGS consists in interpreting configurations as strategies in some game, in the hope that weak bisimilarity between induced strategies entails substitution equivalence. Let us define weak bisimilarity.
Definition 20
Given two strategies
, a weak bisimulation
is a pair of an
-indexed relation
between active states and a
-indexed relation
between waiting states, such that
where
is shorthand for
, and we lift functors to relations in the straightforward way. Let weak bisimilarity, denoted by
, be the largest weak bisimulation.
4.5 The OGS game
Let us now define the OGS game corresponding to any language machine. For §4.5–4.7, we fix a set
of types, a language machine
, and a typing context
.
Definition 21
(). An interleaved context is a list of contexts. We denote by
the set of interleaved contexts.
Of course, we may extract from any interleaved context the variables introduced by the currently active, resp. waiting player:
Definition 22
(). We define two collapsing functions
as follows:
Remark 10
Intuitively,
retains from an interleaved context the variables that are unknown to the currently active player, starting with the last introduced context. Symmetrically,
retains those that are unknown to the waiting player, which does not include the last introduced context.
Let us now define the OGS game, as expected. This only depends on the fixed context
and the observation structure of the considered language machine.
Definition 23
(). We define the OGS half-game
by:
Furthermore, the OGS game
is defined by
4.6 The machine strategy
Let us now define the machine strategy for the given language machine
and final typing context
, fixed at the beginning of §4.5.
Definition 24
(). Let
and
denote the
-indexed families of active, resp. waiting, interleaved assignments defined inductively as follows.
Remark 11
This is merely a formal version of (5). Beware, though, that the active player in an even interleaved context is Proponent, while the active player in an odd interleaved context is Opponent.
Like the interleaved contexts by which they are indexed, interleaved assignments can be collapsed into basic assignments.
Definition 25
(). The collapsing functions for interleaved assignments are defined by mutual induction as follows, for all
,
where
denotes the obvious weakening: we have
for some
and
, and the result is
We now have everything in place to define the machine strategy.
Definition 26
(). The machine strategy
is defined as follows:
the family of active states is
the family of waiting states is
the action morphism is defined by
the reaction morphism is defined by
where
denotes the obvious assignment
.
To finish up, we define two functions injecting configurations (resp. assignments) into active (resp. waiting) machine strategy states (),
where
is the obvious weakening
, and
is the singleton sequence.
4.7 Soundness
We may now state the main result, recalling Notation 5. We introduce the following technical, yet mild conditions on the considered language machine:
Definition 27
A substitution monoid
is clear-cut iff its unit
is injective (where
denotes the variables family of Example 5), and has decidable image whose complement is furthermore stable under renaming. For a clear-cut
, we let
denote the subfamily of non-variable elements.
Definition 28
Assuming
is clear-cut, we define the binary relation
on
by
A language machine has focused redexes iff
is well-founded.
Theorem 8
(). For any language machine with focused redexes and clear-cut values, weak bisimilarity of induced OGS strategies is sound w.r.t. substitution equivalence, i.e., for any pair of configurations
and
, weak bisimilarity of induced strategies entails substitution equivalence:
Remark 12
Let us unfold notations a bit:
denotes the positive component of weak bisimilarity between strategies (Definition 20) in the OGS game (Definition 23), and
denotes substitution equivalence (Definition 15).
The rest of this section is devoted to sketching the proof. We first describe the overall structure, and then focus on the main difficulty.
We start by defining a composition operation
We expect this operation to satisfy the following properties.
Definition 29
1.
Composition is adequate () iff, for all
and
, we have
.
2.
Weak bisimilarity is a congruence () for composition iff, for any
and
, we have
.
Remark 13
The adequacy equation lives in
(recalling Definition 14).
Let us readily show that soundness follows from congruence and adequacy.
Proposition 2
If any adequate composition for which weak bisimilarity is a congruence exists, then OGS is sound.
Proof
For any configurations
with weakly bisimilar interpretations
and
, and any assignment
, we have
hence
, as desired.
It thus remains to define a congruent and adequate composition. The plan for this is to take the fixed point of an equation, in the following sense.
Definition 30
(). An equation consists of a set
of variables, a set
of constants, and a definition function
.
Since we are interested in weak bisimilarity, it seems easier to try and construct weak fixed points of equations
, that is, maps
such that
for all
. This may be done by safely guarding all occurrences of “variables” in
by a
:
Definition 31
(). Given an equation
, the iteration of
is a map
given coinductively by:
Proposition 3
The iteration of any equation is a weak fixed point.
Using this technique, we may define a composition operation for which weak bisimilarity is a congruence. We will see that adequacy is more problematic.
Definition 32
(). The composition equation is:
Let naive composition be the iteration of
.
Proposition 4
Weak bisimilarity is a congruence for naive composition.
Proof
By coinduction: the binary relation on
given by all pairs
such that
and
, is a weak bisimulation.
In order to prove adequacy, we have to give a weak bisimulation between
and
. When facing such an equational proof, where one of the members is defined as a fixed point (here composition), the prime reasoning scheme is uniqueness of fixed points. Indeed, assuming the composition equation has a unique fixed point, and that substituting-then-evaluating-then-observing is one, then both must agree. However, general equations do not have unique weak fixed points, so we have to apply uniqueness of strong fixed points, i.e., fixed points w.r.t. strong bisimilarity. But there is a further complication: while all equations admit weak fixed points, given by iteration as we saw, this is not the case for strong fixed points. Coq’s basic cofixpoint feature enables the construction of strong fixed points for guarded equations, in the following sense.
Definition 33
(). An element
is guarded if it is not of the form
. An equation
is guarded if for all
,
is guarded.
However,
is not guarded in general, as explained in Example 3, which may lead the definition to be ill-founded in some languages, as sketched in Example 4. This is where the focused redexes hypothesis comes in: it allows us to show that
is eventually guarded, in the following sense.
Definition 34
An equation
is eventually guarded if for all
, there exists an
such that
is guarded, where by definition
Proposition 5
(,). All eventually guarded equations admit a unique strong fixed point, which is pointwise weakly bisimilar to any weak fixed point.
Proof
(sketch). Since, for all
, an eventually guarded equation
can be pointwise unrolled a finite number
of times into a guarded element,
, we construct the fixed point of
as the guarded fixed point of
.
Proposition 6
(). If
has focused redexes and clear-cut values, then
is eventually guarded, and thus admits a strong fixed point, say
.
We may now conclude our soundness proof.
Proposition 7
(). If the language machine
has focused redexes, then composition is adequate.
Proof
(sketch). The idea is to show that the map
is something like a strong fixed point of
. This does not quite type check, however, so we need to generalize the two arguments
to pairs of active and passive machine strategy states. Following (6), we define
by:
We have
, and, as desired,
is a strong fixed point of
(). At last, we have, for any
and
:
5 Related work
Beyond the already discussed, closely related work [21, 23, 29], let us mention recent work on the structure needed to collapse the composition of an active and a waiting state into a language machine configuration [19, 21]. Unlike in our work is that acyclicity is not built into the OGS game, but proved after the fact.
The issue of infinite chattering was also studied in game semantics [1, 4, 17] for showing that total strategies are closed under composition. This notion of infinite chattering thus differs from the one studied here, which allows programs to have infinite reduction paths. In our setting, an infinite chattering would be an artifact of the composition looping without even creating a reduction step.
Finally, there is a lot of work on unique solutions of (co)recursive equations. Deducing bisimilarity of two LTSs from the fact that they satisfy the same recursive equation, and that this equation admits a unique solution (up-to bisimilarity), is a standard technique in process calculi, introduced by Hoare [16] and Milner [28], which is still explored today [7]. Let us also mention the category-theoretic work on monads with iteration operators [8, 12, 25, 26], which recently culminated in a widely unifying approach [13], that features an abstract notion of guardedness. Links with the interaction trees library [29] have been established, showing that the itree datatype, considered up to weak bisimilarity, forms a coinductive resumption monad, i.e., it computes cofree coalgebras for a functor of the form
. The resulting monad is furthermore complete Elgot (i.e., it admits potentially non-unique solutions of all equations), and iterative (i.e., it admits unique solutions of “guarded” equations).
6 Conclusion and perspectives
We have proposed an abstract notion of language with evaluator, for which we have constructed a generic OGS interpretation, which we have proved sound, in Coq [2]. We have demonstrated the expressiveness of our framework by instantiating it on a variety of simply-typed
-calculi with control effects – although only one is treated here for lack of space.
An important direction for future work is to incorporate more language features into the framework. Notably, we plan to cover effectful evaluators by generalising from the delay monad to richer, well-behaved monads. It would also be useful to handle more sophisticated type systems, including, e.g., polymorphism or subtyping.
Another direction consists in investigating completeness in the abstract framework, be it by restricting attention to sufficiently effectful languages, or by refining the OGS model to make it fully abstract, i.e., by enforcing conditions like well-bracketing or visibility.
Finally, it might be fruitful to investigate the link between OGS and other models in the abstract framework, including denotational game semantics and Lassen’s normal form bisimilarity.
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.
It is a bit unfortunate that substitution
and context application
have the same notation. It is, however, so common, that we stick to the usual notation.
-calculi. Although it is generally finer than contextual equivalence, its practical value resides in the fact that it is often easier to establish on concrete examples than other such techniques, such as applicative or environmental bisimulation.
-abstractions. In a typed setting, in particular, all terms of functional type contained in any ultimate pattern must be variables. Normal form labels thus contain a very limited class of terms.
-calculus [
) to link definitions and theorems to their mechanised counterpart. The Coq development is inspired by Levy and Staton’s transition systems over games [23], and includes notably the following main contributions.
), in the sense that everything is indexed by typing contexts, and variables are accessed as de Bruijn indices. This contrasts with previous work, which uses nominal style.
) an indexed variant of the interaction trees library [29], which we use to define LTSs coinductively — as opposed to the more traditional, relational definition. However, in this extended abstract, we focus more on the math than on the Coq implementation, so interaction trees do not appear (see Remark 9).
) a new fixed-point combinator over a system of so-called eventually guarded equations, whose solution is unique w.r.t. strong bisimilarity. We use this combinator to define composition of OGS LTSs, which is a crucial ingredient to the soundness proof.
-calculus with recursion (
-calculus (
-calculus [
and
, behave the same under any closed instantiation
of their free variables, in any closed evaluation context
of some fixed, basic type like the booleans1: 
of observation of closed boolean programs, usually cotermination on the same boolean.
of a program
and an evaluation context
. In particular, instead of comparing programs
and
as before, we now compare configurations
and
, where
denotes a fresh context variable. And now CIU equivalence is merely a matter of substitution: combining any substitution
with
, we get 
.
has type
, then
has type
. And in a configuration
,
and
have opposite types, e.g.,
and
. We tend to use
to range over simple types, and
to range over the disjoint union of simple types and formally negated simple types.
to
, and “pop” it when needed, e.g.,
is the inside-out analogue of the evaluation context
. Thus:
, storing the argument part in the evaluation context, while
represents
, so the rule is like a
-reduction in context
.
and
when
for all closed substitutions
, where
denotes some suitable, yet straightforward notion of equivalence on closed configurations.
that gets stuck on a function call
, where
is a variable and
is some value, say of the form
. In the abstract machine presentation, this means
reduces to
for some evaluation context
. The compound evaluation context
means that, once
is evaluated, it should be applied to
, the result of which should be fed to
.
,
has some functional type
, the observation, say
, is
, for fresh variables
and
, and the filling, say
, is the assignment 
may be recovered as
, where
denotes the result of filling the hole in
with
, i.e.,
, and
denotes capture-avoiding substitution of
in
.
. In the abstract machine presentation,
must be fed to some context variable
, which we view as the head variable. The observation, here denoted by
, means that the observed variable
is fed with some value
, while the filling associates
to
.
is an evaluation context that takes the
th component of the running program and continues with
. The corresponding reduction rule is
.
is an evaluation context that executes
or
according to whether the running (boolean) program evaluates to true or false. The reduction rules are 
(4)
. In other words, we model normal forms as triples
.
to
.
amounts to evaluating
, and, if this converges to some normal form
, evaluating the substituted refolding of
.
-calculus, we were observing closed programs of some fixed, basic type like the booleans
. Transposed to the abstract machine presentation, this amounts to observing configurations with a single free variable of type
, which models the final continuation to which the closed context returns. There are only two observations at that type, namely
and
, for true and false, which correspond to the two expected observations.
, and think of configurations with free variables in
as closed programs. The obvious way to observe them is to check whether they diverge, and otherwise record which observation they perform on which free variable of
.
and
with free variables in
are substitution equivalent iff, for all assignments
from variables in
to values of the same type over
,
and
coterminate, and, if they do terminate, perform the same observation on the same variable of
.
to
, for any sets
and
of Player and Opponent positions, respectively. Intuitively, a half-game describes the moves available in each Player position, and the Opponent positions they lead to.
and
then consists of a Player half-game from
to
, and an Opponent half-game from
to
.
-indexed family of active states, where Player is to play,
-indexed family of waiting states, where Opponent is to play,
, either diverges, or picks a move from
and a “next” waiting state, and
, associates a “next” active state.
, an observation
, and a filling
. This splitting is used to interpret the considered configuration
as a strategy in a two-player game, where the program plays as Player and the context plays as Opponent. Let us briefly describe this game, which we call the OGS game.
of typing contexts:
Accordingly, a move (by
) consists of an observation on some variable in
. Such an observation may introduce some fresh variables, which are modelled as a typing context
that we call the context increment. Intuitively,
holds the definitions of variables in
, and the next position is 
are thought of as defined by the currently waiting player, say
, hence unknown to the currently active player, say
,
are defined by
, hence unknown to
.
are held by the now waiting player
, while
are held by the now active player
.
, then a possible move is
, with context increment
.
of strategies is then defined straightforwardly: either both diverge, or they both converge, play the same move, and reach weakly bisimilar strategies, coinductively.
consists of a configuration
with free variables in
, and, for each
, a value of type
with free variables in
, which we (continue to) call an assignment
;
are assignments
;
and assignment
consists in evaluating
, and diverging if it does; otherwise, it evaluates to some normal form
, for some filling
of the context increment
of
; the machine strategy then
, and
, over the position
;
to any move
with context increment
is the configuration obtained by refolding
, up to some technicalities that we hide under the rug for the moment. In particular, variables in the context increment
remain fresh for this player.
into account at the level of games: this is easy. The second is well known to the experts: it is the “infinite chattering” problem. We deal with it in a novel way, by building acyclicity into the model. The final difficulty is new and surprising. It has to do with the fact that, in all sensible languages, repeated, non-trivial instantiation of the head variable eventually leads to some redex. In the abstract setting, we need an additional hypothesis to ensure this is indeed the case.
normally, i.e., to make it part of positions
. But it would not work. Indeed, once a player makes a final move, the game must stop, in order to reflect the notion of observation that was fixed for substitution equivalence.
.
comprise a configuration with free variables in
and an assignment
, while waiting states are assignments
.
, then a proper move is played; if it is in
, a final move is played.
, we would like to be able to recover a corresponding configuration with free variables in the final typing context
. Such a pair of states amounts to a configuration with free variables in
, and assignments 
with
and
in turn would converge to some configuration with free variables in
. This in fact holds for pairs of states arising from the game, but not for all pairs.
of
is mapped by
to some variable
in
, which is in turn mapped to
in
by
.
, we know that the other assignment
does not depend on the new variables in
.
of typing contexts.
of context increments, then
was introduced by the previously active, now waiting player
. Accordingly:
, i.e., one in
, together with an observation
on it – the first index in the sequence depending on the parity of
. The next position is of course
, where
denotes the context increment of
.
, equipped with assignments
as on the left below. 
(5)
as on the right above.
from an active-passive pair of states, as
and a waiting state
, the configuration (6), obtained by iterated substitution, behaves the same as letting the strategies associated to
and
play against one another. This lemma is simply wrong in general, so we need an additional hypothesis.
. And the key lemma states that the refolded configuration (6) diverges iff the composition does, and, if not, both play the same final move in
.
, is then computed like so:
is a map
, where
is Capretta’s delay monad [3], which we briefly recall in §4.2. This is a rather intensional description of partiality, in the sense that an element of
consists of a sequence of “silent computation steps”, denoted by
, which is either infinite or followed by some “result” in
.
and
, for some program
and evaluation context
. Since
is a normal form,
plays without any computation step the non-final move
on
, and the second recursive clause above says that the composition
equals the composition 
as a whole, our stated goal for composition. Indeed, the second clause models communication between
and
, which is invisible in the behaviour of
.
being instantiated by another variable
, then acyclicity tells us that
must have been introduced before
. Since this is a well-founded ordering, we are safe on this front.
-abstraction, with an exotic redex of the form 
on
, leading to
and empty assignment,
,
and
.
on observations should be well-founded. Explicitly, we have
iff there exist
,
,
, and a non-variable
such that substituting
for
in the refolding
yields some normal form (without evaluating!) of the shape
, i.e., 
is well-founded, we say that the considered language machine has focused redexes.
-calculus with a boolean type and recursive functions. Terms are generated by the following grammar 
binds
and
in
, as usual. The language is typed. Types and typing contexts are generated by the following grammar, 
and
is defined to mean
, for all closing substitutions
and boolean contexts
, for some fixed equivalence relation
between boolean closed programs. More precisely,
for assignments to each variable
of a value of type
in typing context
.
of type
are deemed observably equivalent whenever we have
iff
, and similarly with
.
and type
, two programs
are ciu-equivalent, which we denote by
, iff for all assignments
, and closed evaluation contexts
of type
with a hole of type
,
and
are observably equivalent.
and substitution
on an equal footing in this definition. The overall idea is to compile our simply-typed, call-by-value
-calculus down to a slightly lower-level language, as explained in §2.1.
-calculus
are either simple types
, or negated simple types
. Programs have simple types
, while evaluation contexts have negated types
. We have syntactic categories for programs and evaluation contexts, and a configuration is a pair of a program of some type
and of an evaluation context of type
. Values and programs are defined and typed exactly as before. Evaluation contexts and configurations are specified by the following grammar. 
is an evaluation context of type
. Additional typing rules, for evaluation contexts and configurations, are shown in the first part of Figure 1. Capture-avoiding substitution is defined straightforwardly, and evaluation rules are displayed in the second part of Figure 1. We may now introduce substitution equivalence.
, two configurations
are substitution equivalent, which we denote by
, iff for all assignments
,
and
are observably equivalent, in the sense that we have
iff
, and similarly with
.
and type
of the source language, two programs
are ciu-equivalent iff, in the typing context
(with
fresh w.r.t.
),
and
are substitution equivalent.
in the lower-level language and pairs of an assignment
and an evaluation context
of type
with a hole of type
in the source language. Furthermore, for such assignments and evaluation contexts,
and
are observably equivalent in the obvious sense, hence the result follows.
of types for the whole section, and let
denote the set of sequences of types.
of sets, we extend the set 
, for any
. In particular, we call the objects of
and
, unsorted and sorted families, respectively.
), given by the proof-relevant
predicate:
denotes the set of indices at which
occurs in
.
). For any typing contexts
and sorted family
, an
, or assignment when
is clear from context, consists of an element of
, for all
. In other words, we have 
, for any sorted family
and unsorted family
, we define the power objects 
). A substitution monoid is a sorted family
, equipped with morphisms 
). A substitution module over a substitution monoid
, or substitution
-module for short, is an unsorted family
, equipped with a morphism 
(and type
, if relevant) and assignments
, to elements over
: this is indeed the expected type for substitution.
). The delay endomap on
is defined coinductively by the following inference rules. 
the pointwise liftings of delay to categories of families
, e.g.,
and
.
is meant to suggest a silent computation step. Such
s should not be confused with types, which hopefully will be easy from context.
are thought of as potentially diverging computations of type
: divergence is modelled by the infinite chain of
s; converging computations have the shape
.
equivalent up to strong or weak bisimilarity, which we now recall.
between sets (or families)
and
, we let
be such that
iff
and
either both diverge, or evaluate to some
and
with
. We write
for weak bisimilarity (
), which we define as
.
for strong bisimilarity (
), the canonical lifting of
to the delay coinductive type: either both sides loop or both converge to the same element in the same number of
steps.
and
for the bind (
) operator of
—evaluate
, and if it returns some
, then evaluate
.
). An evaluation structure on any unsorted families
consists of maps:
and
such that
.
of some normal form
yields
in zero computation steps.
). An observation structure
is a type-indexed set
together with a map
.
, we define the unsorted family
of pointed observations by
We extend the map
to
, defining
by
consists of a variable, together with an observation at its type.
.
of values,
-module
of configurations,
,
and
,
), in the sense that, for all
,
,
, with
and
, the following hold 
, and
of any normal form
by
.
.
as an implicit coercion. We also extend the notation
to arbitrary values, writing
for
, for fresh
.
to consist of types
and negated types
(i.e., it is the disjoint union of two copies of simple types);
consists of configurations
;
consists of values
, and
consists of all contexts
. Before defining
, we introduce the family
of ultimate values, which is the subfamily
defined inductively by the following linear type system, 
for
. In words, at each
(a simple or negated simple type),
is an ultimate value; we have
, and so on. We then define
with similar notation: 
.
). We define
at any
to be the composite 
). For any fixed final typing context
, two configurations
are substitution equivalent at
, written
, iff: 
and
of client and server positions, respectively. The definition then proceeds to postulate families of client moves from
to
, and server moves from
to
. As this is symmetric, we start by introducing a notion of “half-game”, and then define games as pairs thereof.
) over sets
and
consists of an
-indexed family of moves
, and a next map in
. We denote by
the set of half-games over
and
.
) over sets
and
consists of a client half-game in
, a server half-game in
, and a set of final moves. We denote by
the set of games over
and
.
and
the components of any half-game
, and by
,
, and
the components of any game
.
of a game
is defined by swapping the client and server:
,
and
.
). Given any half-game
, we define two functors
, the action functor
and the reaction functor
: 
, a strategy for
consists of families
and
of active and waiting states, respectively, together with 
the set of strategies for
.
and
the action and reaction morphisms of any strategy
.
) not as coalgebras, as here, but as interaction trees, i.e., elements of the final coalgebra
, a weak bisimulation
is a pair of an
-indexed relation
between active states and a
-indexed relation
between waiting states, such that 
is shorthand for
, and we lift functors to relations in the straightforward way. Let weak bisimilarity, denoted by
, be the largest weak bisimulation.
of types, a language machine
, and a typing context
.
). An interleaved context is a list of contexts. We denote by
the set of interleaved contexts.
). We define two collapsing functions
as follows:
retains from an interleaved context the variables that are unknown to the currently active player, starting with the last introduced context. Symmetrically,
retains those that are unknown to the waiting player, which does not include the last introduced context.
and the observation structure of the considered language machine.
). We define the OGS half-game
by: 
is defined by 
and final typing context
, fixed at the beginning of §4.5.
). Let
and
denote the
-indexed families of active, resp. waiting, interleaved assignments defined inductively as follows. 
). The collapsing functions for interleaved assignments are defined by mutual induction as follows, for all
, 
denotes the obvious weakening: we have
for some
and
, and the result is
). The machine strategy
is defined as follows:where
denotes the obvious assignment
.
), 
is the obvious weakening
, and
is the singleton sequence.
is clear-cut iff its unit
is injective (where
denotes the variables family of Example 5), and has decidable image whose complement is furthermore stable under renaming. For a clear-cut
, we let
denote the subfamily of non-variable elements.
is clear-cut, we define the binary relation
on
by 
is well-founded.
). For any language machine with focused redexes and clear-cut values, weak bisimilarity of induced OGS strategies is sound w.r.t. substitution equivalence, i.e., for any pair of configurations
and
, weak bisimilarity of induced strategies entails substitution equivalence: 
denotes the positive component of weak bisimilarity between strategies (Definition 
denotes substitution equivalence (Definition 
) iff, for all
and
, we have
.
) for composition iff, for any
and
, we have
.
(recalling Definition 14).
with weakly bisimilar interpretations
and
, and any assignment
, we have 
, as desired.
). An equation consists of a set
of variables, a set
of constants, and a definition function
.
, that is, maps
such that
for all
. This may be done by safely guarding all occurrences of “variables” in
by a
:
). Given an equation
, the iteration of
is a map
given coinductively by: 
). The composition equation is: 
.
given by all pairs
such that
and
, is a weak bisimulation.
and
. When facing such an equational proof, where one of the members is defined as a fixed point (here composition), the prime reasoning scheme is uniqueness of fixed points. Indeed, assuming the composition equation has a unique fixed point, and that substituting-then-evaluating-then-observing is one, then both must agree. However, general equations do not have unique weak fixed points, so we have to apply uniqueness of strong fixed points, i.e., fixed points w.r.t. strong bisimilarity. But there is a further complication: while all equations admit weak fixed points, given by iteration as we saw, this is not the case for strong fixed points. Coq’s basic cofixpoint feature enables the construction of strong fixed points for guarded equations, in the following sense.
). An element
is guarded if it is not of the form
. An equation
is guarded if for all
,
is guarded.
is not guarded in general, as explained in Example 3, which may lead the definition to be ill-founded in some languages, as sketched in Example 4. This is where the focused redexes hypothesis comes in: it allows us to show that
is eventually guarded, in the following sense.
is eventually guarded if for all
, there exists an
such that
is guarded, where by definition 
,
). All eventually guarded equations admit a unique strong fixed point, which is pointwise weakly bisimilar to any weak fixed point.
, an eventually guarded equation
can be pointwise unrolled a finite number
of times into a guarded element,
, we construct the fixed point of
as the guarded fixed point of
.
). If
has focused redexes and clear-cut values, then
is eventually guarded, and thus admits a strong fixed point, say
.
). If the language machine
has focused redexes, then composition is adequate.
is something like a strong fixed point of
. This does not quite type check, however, so we need to generalize the two arguments
to pairs of active and passive machine strategy states. Following (6), we define
by: 
, and, as desired,
is a strong fixed point of
(
). At last, we have, for any
and
: 
. The resulting monad is furthermore complete Elgot (i.e., it admits potentially non-unique solutions of all equations), and iterative (i.e., it admits unique solutions of “guarded” equations).
-calculi with control effects – although only one is treated here for lack of space.
and context application
have the same notation. It is, however, so common, that we stick to the usual notation.
