key: cord-0060434-tcooyqjy authors: Jaber, Guilhem; Murawski, Andrzej S. title: Complete trace models of state and control date: 2021-03-23 journal: Programming Languages and Systems DOI: 10.1007/978-3-030-72019-3_13 sha: 40830157c29340913bd75567b45de97992ee0e63 doc_id: 60434 cord_uid: tcooyqjy We consider a hierarchy of four typed call-by-value languages with either higher-order or ground-type references and with either [Formula: see text] or no control operator. Our first result is a fully abstract trace model for the most expressive setting, featuring both higher-order references and [Formula: see text] , constructed in the spirit of operational game semantics. Next we examine the impact of suppressing higher-order references and callcc in contexts and provide an operational explanation for the game-semantic conditions known as visibility and bracketing respectively. This allows us to refine the original model to provide fully abstract trace models of interaction with contexts that need not use higher-order references or [Formula: see text] . Along the way, we discuss the relationship between error- and termination-based contextual testing in each case, and relate the two to trace and complete trace equivalence respectively. Overall, the paper provides a systematic development of operational game semantics for all four cases, which represent the state-based face of the so-called semantic cube. Research into contextual equivalence has a long tradition in programming language theory, due to its fundamental nature and applicability to numerous verification tasks, such as the correctness of compiler optimisations. Capturing contextual equivalence mathematically, i.e. the full abstraction problem [26] , has been an important driving force in denotational semantics, which led, among others, to the development of game semantics [2, 12] . Game semantics models computation through sequences of question-and answer-moves by two players, traditionally called O and P, who play the role of the context and the program respectively. Because of its interactive nature, it has often been referred to as a middle ground between denotational and operational semantics. The full version is available at https://hal.archives-ouvertes.fr/hal-03116698. Over the last three decades the game-semantic approach has led to numerous fully abstract models for a whole spectrum of programming paradigms. Most papers in this strand follow a rather abstract pattern when presenting the models, emphasing structure and compositionality, often developing a correspondence with a categorical framework along the way to facilitate proofs. The operational intuitions behind the games are somewhat obscured in this presentation, and left to be discovered through a deeper exploration of proofs. In contrast, operational game semantics aims to define models in which the interaction between the term and the environment is described through a carefully instrumented labelled transition system (LTS), built using the syntax and operational semantics of the relevant language. Here, the derived trace semantics can be shown to be fully abstract. In this line of work, the dynamics is described more directly and provides operational intuitions about the meaning of moves, while not immediately giving structural insights about the structure of the traces. In this paper, we follow the operational approach and present a whole hierarchy of trace models for higher-order languages with varying access to higherorder state and control. As a vehicle for our study, we use HOSC, a call-by-value higher-order language equipped with general references and continuations. We also consider its sublanguages GOSC, HOS and GOS, obtained respectively by restricting storage to ground values, by removing continuations, and by imposing both restrictions. We study contextual testing of a class of HOSC terms using contexts from each of the languages x ∈ {HOSC, GOSC, HOS, GOS}; we write x to refer to each case. Our working notion of convergence will be error reachability, where an error is represented by a free variable. Accordingly, at the technical level, we will study a family of equivalence relations ∼ = x err , each corresponding to contextual testing with contexts from x, where contexts have the extra power to abort the computation. Our main results are trace models Tr x (Γ M ) for each x ∈ {HOSC, GOSC, HOS, GOS}, which capture ∼ = x err through trace equivalence: Γ M 1 ∼ = x err M 2 if and only if Tr x (Γ M 1 ) = Tr x (Γ M 2 ). It turns out that, for contexts with control (i.e. x ∈ {HOSC, GOSC}), ∼ = x err coincides with the standard notion of contextual equivalence based on termination, written ∼ = x ter . However, in the other two cases, the former is strictly more discriminating than the latter. We explain how to account for this difference in the trace-based setting, using complete traces. A common theme that has emerged in game semantics is the comparative study of the power of contexts, as it turned out possible to identify combinatorial conditions, namely visibility [3] and bracketing [22] , that correspond to contextual testing in the absence of general references and control constructs respectively. In brief, visibility states that not all moves can be played, but only those that are enabled by a "visible part" of the interaction, which could be thought of as functions currently in scope. Bracketing in turn imposes a discipline on answers, requiring that the topmost question be answered first. In the paper, we provide an operational reconstruction of both conditions. Overall, we propose a unifying framework for studying higher-order languages with state and control, which we hope will make the techniques of (operational) game semantics clearer to the wider community. The construction of the fully abstract LTSs is by no means automatic, as there is no general methodology for extracting trace semantics from game models. Some attempts in that direction have been reported in [25] , but the type discipline discussed there is far too weak to be applied to the languages we study. As the most immediate precursor to our work, we see the trace model of contextual interactions between HOS contexts and HOS terms from [23] . In comparison, the models developed in this paper are more general, as they consider the interaction between HOSC terms and contexts drawn from any of the four languages ranged over by x. In the 1990s, Abramsky proposed a research programme, originally called the semantic cube [1] , which concerned investigating extensions of the purely functional programming language PCF along various axes. From this angle, the present paper is an operational study of a semantic diamond of languages with state, with GOS at the bottom, extending towards HOSC at the top, either via GOSC or HOS. The main objects of our study will be the language HOSC along with its fragments GOSC, HOS and GOS. HOSC is a higher-order programming language equipped with general references and continuations. Syntax HOSC syntax is given in Figure 1 . Assuming countably infinite sets Loc (locations) and Var (variables), HOSC typing judgments take the form We also consider another way of testing, based on observing whether a program can reach a breakpoint (error point) inside a context. Technically, the breakpoints are represented as occurrences of a special free error variable err : Unit → Unit. Reaching a breakpoint then corresponds to convergence to a stuck For the languages in question, it will turn out that x err is at least as discriminating as x ter for each x ∈ {HOSC, GOSC, HOS, GOS}, and that they coincide for x ∈ {HOSC, GOSC}. We will write ∼ = x err and ∼ = x ter for the associated equivalence relations. For higher-order languages with state and control, it is well known that contextual testing can be restricted to evaluation contexts after instantiating the free variables of terms to closed values (the so-called closed instances of use, CIU). Let us write Σ, Γ γ : Γ for substitutions γ such that, for any (x, σ x ) ∈ Γ , the term γ(x) is a value satisfying Σ; Γ γ(x) : σ x . Then M {γ} stands for the outcome of applying γ to M . Results stating that "CIU tests suffice" are referred to as CIU lemmas. A general framework for obtaining such results for higher-order languages with effects was developed in [10, 33] . The results stated therein are for termination-based testing, i.e. ⇓ ter , but adapting them to ⇓ err is not problematic. The preorders x err will be the central object of study in the paper. Among others, we shall provide their alternative characterizations using trace semantics.The characterizations will apply to a class of terms that we call cr-free. Definition 6. A HOSC term Γ M : τ is cr-free if it does not contain occurrences of cont σ K and locations, and its boundary types are cont-and ref-free. We stress that the boundary restriction applies to Γ and τ only, and subterms of M may well contain arbitrary HOSC types and occurrences of ref σ , call/cc σ , throw σ for any σ. The majority of HOSC/GOSC/HOS/GOS examples studied in the literature, e.g. [28, 4, 8] , are actually cr-free. We will revisit some of them as Examples 6, 7, 10. The fact that cr-free terms may not contain subterms cont τ K or is not really a restriction, as cont τ K and being more of a run-time construct than a feature meant to be used directly by programmers. Finally, we note that the boundary of a cr-free term is an x boundary for any x ∈ {HOSC, GOSC, HOS, GOS}. Thus, we can consider approximation between cr-terms for any x from the range, i.e. the notions x err , x ter are all applicable. Consequently, cr-free terms provide a common setting in which the discriminating power of HOSC, GOSC, HOS and GOS contexts can be compared. We discuss the scope for extending our results outside of the cr-free fragment, and for richer type systems, in Section 7. Recall that HOSC err concerns testing HOSC terms with HOSC contexts. Accordingly, we call this case HOSC [HOSC] . For cont σ (K)-free terms, we show that HOSC err and HOSC ter coincide, which follows from the lemma below. Let Γ M 1 , M 2 be HOSC terms not containing any occurrences of cont τ (K). In what follows, after introducing several preliminary notions, we shall design a labelled transition system (LTS) whose traces will turn out to capture contextual interactions involved in testing cr-free terms according to HOSC err . This will enable us to capture HOSC err via trace inclusion. Actions of the LTS will refer to functions and continuations in a symbolic way, using typed names. Definition 7. Let FNames = σ,σ FNames σ→σ be the set of function names, partitioned into mutually disjoint countably infinite sets FNames σ→σ . We will use f, g to range over FNames and write f : σ → σ for f ∈ FNames σ→σ . Analogously, let CNames = σ CNames σ be the set of continuation names. We will use c, d to range over CNames, and write c : σ for c ∈ CNames σ . Note that the constants represent continuations, so the "real" type of c is cont σ, but we write c : σ for the sake of brevity. We assume that CNames, FNames are disjoint and let Names = FNames CNames. Elements of Names will be weaved into various constructions in the paper, e.g. terms, heaps, etc. We will then write ν(X) to refer to the set of names used in some entity X. Because of the shape of boundary types in cr-free terms and, in particular, the presence of product types, the values that will be exchanged between the context and the program take the form of tuples consisting of (), integers, booleans and functions. To describe such scenarios, we introduce the notion of abstract values, which are patterns that match such values. Abstract values are generated by the grammar with the proviso that, in any abstract value, a name may occur at most once. As function names are intrinsically typed, we can assign types to abstract values in the obvious way, writing A : τ . Our LTS will be based on four kinds of actions, listed below. Each action will be equipped with a polarity, which is either Player (P) or Opponent (O). P-actions describing interaction steps made by a tested term, while O-actions involve the context. Finally, this action corresponds to receiving an abstract value A and a continuation name c from the environment through a function name f . In what follows, a is used to range over actions. We will say that a name is introduced by an action a if it is sent or received in a. If a is an O-action (resp. P-action), we say that the name was introduced by O (resp. P). An action a is justified by another action a if the name that a uses to communicate, i.e. f in questions (f (A, c), f (A, c)) and c in answers (c(A), c(A)), has been introduced by a . We will work with sequences of actions of a very special shape, specified below. The definition assumes two given sets of names, N P and N O , which represent names that have already been introduced by P and O respectively. the actions alternate between Player and Opponent actions; -no name is introduced twice; -names from N O , N P need no introduction; -if an action a uses a name to communicate then • the name has been introduced by an earlier action a of opposite polarity. Note that, due to the shape of actions, a continuation name can only be introduced/justified by a question. Moreover, because names are never introduced twice, if a justifies a then a is uniquely determined in a given trace. Readers familiar with game semantics will recognize that traces are very similar to alternating justified sequences except that traces need not be started by O. . Then the following sequence is an (N O , N P )-trace: We extend the definition of HOSC presented in Figure 2 to take into account these names. We refine the operational reduction using continuation names to keep track of the toplevel continuation. We list all the changes below. -Function names are added to the syntax as constants. Since they are meant to represent values, they are also considered to be syntactic values in the extended language. f ∈ FNames σ→σ Σ; Γ f : σ → σ -Continuation names are not terms on their own. Instead, they are built into the syntax via a new construct cont σ (K, c), subject to the following typing rule. is a staged continuation that first evaluates terms inside K and, if this produces a value, the value is passed to c. This operational meaning will be implemented through a suitable reduction rule, to be discussed next. cont σ (K, c) is also regarded as a value. Note that we remove the old construct cont σ K from the extended syntax. -The operational semantics → underpinning the LTS is based on triples (M, c, h) such that Σ; Γ M : σ, c ∈ CNames σ and h : Σ. The continuation name c is used to represent the surrounding context, which is left abstract. The previous operational rules → are embedded into the new reduction → using the rule below. The two reduction rules related to continuations, previously used to define →, are not included. Instead we use the following rules, which take advantage of the extended syntax. We write Vals for the extended set of syntactic values, i.e. FNames ⊆ Vals. Let ECtxs stand for the set of extended evaluation contexts, defined as K in Figure 1 taking the extended definition of values into account. Before defining the transition relation of our LTS, we discuss the shape of configurations, providing intuitions behind each component. Passive configurations take the form γ, ξ, φ, h and are meant to represent stages at which the environment is to make a move. γ : (FNames Vals) (CNames ECtxs) is a finite map. It will play the role of an environment that relates function names communicated to the environment (i.e. those introduced by P) to syntactic values, and continuation names introduced by P to evaluation contexts. ξ : (CNames CNames) is a finite map. It complements the role of γ for continuation names and indicates the continuation to which the outcome of applying γ(c) should be passed. φ ⊆ Names. The set φ will be used to collect all the names used in the interaction, regardless of which participant introduced them. Following our description above, those introduced by O will correspond to φ \ dom(γ). The components satisfy healthiness conditions, implied by their role in the system. Let Σ = dom(h). -Finally, names introduced by the environment and communicated to the program may end up in the environments and the heap: Active configurations take the form M, c, γ, ξ, φ, h and represent interaction steps of the term. The γ, ξ, φ, h components have already been described above. For M and c, given Σ = dom(h), we will have Σ; ∅ M : σ, c ∈ CNames σ and ν(M ) ∪ {c} ⊆ φ \ dom(γ). Observe that any closed value V of a cont-and ref-free type σ can be decomposed into an abstract value A (pattern) and the corresponding substitution γ (matching). The set of all such decompositions, written AVal σ (V ), is defined below. Given a value V of a (cr-free) type σ, AVal σ (V ) contains all pairs (A, γ) such that A is an abstract value and γ : ν(A) → Vals is a substitution such that A{γ} = V . More concretely, Note that, by writing ·, we mean to implicitly require that the function domains be disjoint. Similarly, when writing , we stipulate that the argument sets be disjoint. Figure 3 . Example 3. Below we analyse the (PQ) rule in more detail. The use of in φ ν(A) {c } is meant to highlight the requirement that the names introduced inf (A, c ), i.e. ν(A)∪{c }, should be fresh and disjoint from φ. Moreover, note how γ and ξ are updated. In general, γ, ξ, h are updated during P-actions. representing multiple (possibly none) τ -actions. This notation is extended to sequences of actions: given t = a 1 . . . a n , we write C Then elements of Tr HOSC (C) are (φ \ dom(γ), dom(γ))-traces. : Example 4. In Figure 5 , we show that the trace from Example 1 is generated by the configuration C M cwl 1 , c, ∅, ∅, {c}, ∅ , where M cwl 1 is given in Figure 4 . We write inc λf.if ¬(! b ) ( b := tt; f (); x :=! x + 1; b := ff ) (), get λ .! x and c : ((Unit → Unit) → Unit) × (Unit → Int). It is interesting to notice that in this interaction, Opponent uses the continuation N twice, incrementing the counter x by two. The second time, it does it without having to call inc again, but rather by using the continuation name c 2 . Due to the freedom of name choice, note that Tr HOSC (C) is closed under type-preserving renamings that preserve names from C. We define two kinds of special configurations that will play an important role in spelling out correctness results for the HOSC[HOSC] LTS. Let Γ = {x 1 : σ 1 , · · · , x k : σ k }. A map ρ from {x 1 , · · · , x k } to the set of abstract values will be called a Γ -assignment provided, for all 1 ≤ i = j ≤ k, we have ρ(x i ) : σ i and ν(ρ(x i )) ∩ ν(ρ(x j )) = ∅. Having defined active configurations associated with terms, we now define passive configurations associated with contexts. Let us fix ∈ FNames Unit→Unit and, for each σ, a continuation name • σ ∈ CNames σ . Let • = σ {• σ }. Intuitively, the names will correspond to ⇓ err and • σ to ⇓ ter . Recall thatê rr stands for err : Unit → Unit. Given a heap h : Σ;ê rr , an evaluation context Σ;ê rr K : τ → τ and a substitution Σ;ê rr γ : Γ (as in the definition of HOSC(ciu) err ), let us replace every occurrence of cont σ K inside h, K, γ with cont σ (K , • σ ), if K has type σ → σ . Moreover, let us replace every occurrence of the variable err with the function name . This is done to adjust h, K, γ to the extended syntax of the LTS: the upgraded versions are called h • , γ • , K • . Next we define the set AVal Γ (γ) of all disjoint decompositions of values from γ • into abstract values and the corresponding matchings. Recall that Γ = {x 1 : σ 1 , · · · , x k : σ k }. Below A i stands for (A 1 , · · · , A k ), and γ i for (γ 1 , · · · , γ k ). ν(A 1 ), · · · , ν(A k ) mutually disjoint and without } Definition 12 (Context configuration). Given Σ, h : Σ;ê rr , Σ;ê rr K : Intuitively, the names ν(A i ) correspond to calling function values extracted from γ, whereas c corresponds to K. Note that traces in Tr HOSC (C γi,c h,K,γ ) will be In preparation for the next result, we introduce the following shorthands. ) and t ⊥¯ ((), c ) ∈ Tr HOSC (C γi,c h,K,γ ). Intuitively, the lemma above confirms that the potential of a term to converge is determined by its traces. Accordingly, we have: To prove the converse, we need to know that every odd-length trace generated by a term actually participates in a contextual interaction. This will follow from the lemma below. Note that ⇓ err relies on even-length traces from the context (Lemma 4). Proof (Sketch) . The basic idea is to use references in order to record all continuation and function names introduced by the environment. For continuations, the use of call/cc τ is essential. Once stored in the heap, the names can be accessed by terms when needed in P-actions. The availability of throw and references to all O-continuations means that arbitrary answer actions can be scheduled when needed. Theorems 1, 2 (along with Lemmas 1, 2) imply the following full abstraction results. Example 6 (Callback with lock [4] ). Recall the term M cwl 1 : ((Unit → Unit) → Unit) × (Unit → Int) from Example 4, given in Figure 4 . We had t 1 =c( g 1 , g 2 ) g 1 (f 1 , c 1 )f 1 ((), c 2 ) c 2 (())c 1 (()) c 2 (())c 1 (()) g 2 ((), c 3 )c 3 (2) ∈ Tr HOSC (C ∅,c M cwl 1 ). Define t 2 to be t 1 except that its last actionc 3 (2) is replaced withc 3 (1). Observe that t 1 ∈ Tr HOSC (C ∅,c The above Corollary also provides a handle to reason about equivalence via trace equivalence. Sometimes this can be done directly on the LTS, especially when γ can be kept bounded. Example 7 (Counter [28] ). Recall that GOSC is the fragment of HOSC in which general storage is restricted to values of ground type, i.e. arithmetic/boolean constants, the associated reference names, references to those names and so on. In what follows, we are going to provide characterizations of GOSC err via trace inclusion. Recall that, by Lemma 2, GOSC err = GOSC ter . Note that we work in an asymmetric setting with terms belonging to HOSC being more powerful than contexts. We start off by identifying several technical consequences of the restriction to GOSC syntax. First we observe that GOSC internal reductions never contribute extra names. The lemma has interesting consequences for the shape of traces generated by the context configurations C γi,c h,K,γ if they are built from GOSC syntax. Recall that P-actions have the formf (A, c ) orc(A), where f, c are names introduced by O. It turns out that when h, K, γ are restricted to GOSC, more can be said about the origin of the names in traces generated by C γi,c h,K,γ : they will turn out to come from a restricted set of names introduced by O, which we identify below. The definition below is based on following the justification structure of a tracerecall that one action is said to justify another if the former introduces a name that is used for communication in the latter. Note that, in the inductive cases, the definition follows links between names introduced by P and the point of their introduction, names introduced inbetween are ignored. Here readers familiar with game semantics will notice similarity to the notion of P-view [12] . Next we specify a property of traces that will turn out to be satisfied by configurations corresponding to GOSC contexts. for any even-length prefix t f (A, c) of t, we have f ∈ Vis P (t ), -for any even-length prefix t c(A) of t, we have c ∈ Vis P (t ). . Then all traces in Tr HOSC (C) are P-visible. The Lemma above shows that contextual interactions with GOSC contexts rely on restricted traces. We shall now modify the HOSC[HOSC] LTS to capture the restriction. Note that, from the perspective of the term, the above constraint is a constraint on the use of names by O (context), so we need to talk about O-available names instead. This dual notion is defined below. we have c ∈ Vis O (t ). Example 8. Recall the trace from previous examples. Observe that Consequently, the first use of c 2 (()) in t 1 does not violate O-visibility, but the second one does. In Figure 6 , we present a new LTS, called the GOSC[HOSC] LTS, which will turn out to capture GOSC ((ρ, c) , t) | ρ is a Γ -assignment, c : τ, t ∈ Tr GOSC (C ρ,c M,vis )}. By construction, it follows that Lemma 8. t ∈ Tr GOSC (C ρ,c M,vis ) iff t ∈ Tr HOSC (C ρ,c M ) and t is O-visible. Noting that the witness trace t from Lemma 4 is O-visible iff t ⊥¯ ((), c ) is Pvisible, we can conclude that, for GOSC, the traces relevant to ⇓ err are O-visible, which yields: To prove the converse, we need a new definability result. This time we are only allowed to use GOSC syntax, but the target is also more modest: we are only aiming to capture P-visible traces. Proof (Sketch). This time we cannot rely on references to recall on demand all continuation and function names introduced by the environment. However, because t is P-visible, it turns the uses of the names can be captured through variable bindings (λx. · · · for function and call/cc τ (x. . . . ) for continuation names). Using throw, we can then force an arbitrary answer action, as long as it uses a P-available name. To select the right action at each step, we branch on the value of a single global reference of type ref Int that keeps track of the number of steps simulated so far. Completeness now follows because, for a potential O-visible witness t from Lemma 4, one can create a corresponding context by invoking the Definability result for t ⊥¯ ((), c ). It is crucial that the addition of¯ ((), c ) does not break P-visibility ( is P-visible). Altogether, Theorems 3, 4 (along with Lemma 1) imply the following result. of type τ = (Unit → Unit) → Int, let and let t 4 be obtained from t 3 by changing 0 in the last action to 1. One can check that both traces are O-visible: in particular, the action c 3 (()) is not a violation because Recall that HOS is the fragment of HOSC that does not feature continuation types and the associated syntax. In what follows we are going to provide alternative characterisations of HOS err and HOS ter in terms of trace inclusion and complete trace inclusion respectively. We start off by identifying several technical consequences of the restriction to HOS syntax. First we observe that HOS internal reductions never change the associated continuation name. (M, c, h) → (M , c , h ), M is a HOS term and h is a HOS heap then c = c . Proof. The only rule that could change c is the rule for throw, but it is not part of HOS. The lemma has a bearing on the shape of traces generated by the (passive) configurations C γi,c h,K,γ corresponding to HOS contexts. In the presence of throw and storage for continuations, it was possible for P to play answers involving arbitrary continuation names introduced by O. By Lemma 10, in HOS this will be restricted to the continuation name of the current configuration, which will restrict the shape of possible traces. Below we identify the continuation name top P (t) that becomes the relevant name after trace t. If the last move was an O-question then the continuation name introduced by that move will become that name. Otherwise, we track a chain of answers and questions, similarly to the definition of P-visibility. Observe The Lemma above characterizes the restrictive nature of contextual interactions with HOS contexts. Next we shall constrain the HOSC[HOSC] LTS accordingly to capture the restriction. Note that, from the point of view of the term, the above-mentioned constraint concerns the use of continuation names by O (the context), so we need to talk about O-bracketing instead. This dual notion of "a top name for O" is specified below. ((ρ, c) , t) | ρ is a Γ -assignment, c : τ, t ∈ Tr HOS (C ρ,c M,bra )}. By construction, it follows that Operationally, one can see that f M 1 HOS err M 2 due to the following HOS context: let r = ref (λy.y) in (let f = λy.(!r)() in (r := •; (!r)())); err . In our framework, this is confirmed by the trace which is in Tr HOS (C ρ,c M1 ) \ Tr HOS (C ρ,c M2 ). On the other hand, , so the terms are incomparable. Note, however, that both traces break O-visibility: specifically, we have err and x ter coincide. Intuitively, this is because the presence of continuations in the context makes it possible to make an escape at any point. In contrast, for HOS, the context must run to completion in order to terminate. At the technical level, one can appreciate the difference when trying to transfer our results for HOS(ciu) err to HOS(ciu) ter . Recall that, according to Lemma 4, ⇓ ter relies on a witness trace t such that the context configuration generates t ⊥• τ (). In HOS, the latter must satisfy P-bracketing, so we need top P (t ⊥ ) = • τ . Note that this is equivalent to top O (t) = ⊥. Consequently, only such traces are relevant to observing ⇓ ter . We The theorem above generalizes the characterisation of contextual equivalence between HOS terms with respect to HOS contexts [23] , where trace completeness means both O-and P-bracketing and "all questions must be answered". Our definition of completeness is weaker (O-bracketing + "the top question must be answered"), because it also covers HOSC terms. However, in the presence of both O-and P-bracketing, i.e. for HOS terms, they will coincide. Recall that GOS features ground state only and, technically, is the intersection of GOSC and HOS. Consequently, it follows from the previous sections that GOS contexts yield configurations that satisfy both P-visibility and P-bracketing. For such traces, the definability result for GOSC yields a GOS context. Thus, in a similar fashion to the previous sections, we can conclude that O-visible and O-bracketed traces underpin GOS err . To define the GOS LTS we simply combine the restrictions imposed in the previous sections, and define Tr GOS (Γ M ) analogously. The results on GOS Asymmetry Our framework is able to deal with asymmetric scenarios, where programs are taken from HOSC, but are tested with contexts from weaker fragments. For example, we can compare the following two HOSC programs, where f : ((Unit → Unit) → Unit) → Unit is a free identifier. callcc(y. f(λg.b := tt; g(); throw() to y); f(λg.g(); throw() to y); if !b then () else div) div) with div representing divergence. The terms happen to be ∼ = HOS err -equivalent, but not ∼ = HOSC err -equivalent. To see this at the intuitive level, we make the following observations. -Firstly, we observe that, to distinguish the terms, f should use its argument. Otherwise, the value of b will remain equal to ff , and the only subterm that distinguishes the terms ('if !b then () else div') will play the same role as div in the second term. -Secondly, if f does use its argument, then b will be set to tt in the first program, raising the possibility of distinguishing the terms. However, if we allow HOS contexts only then, since the argument to f was used, it will have to run to completion, before 'if !b then () else div' is reached. Consequently, we will encounter 'throw () to y' earlier and never reach 'if !b then () else div'. This is represented by the tracē This trace is O-bracketed, but not P-bracketed since Player uses throw to answer directly to the initial continuation c rather than c 2 . -Finally, if HOSC contexts are allowed, it is possible to reach the subterm 'if !b then () else div' with b set to tt. This is represented by the tracē This trace is not O-bracketed, because c 1 is answered rather than c 3 , like above. Consequently, the trace witnesses termination of the first term, but the second term would diverge during interaction with the same context. We plan to explore the opportunities presented by this setting in the future, especially with respect to fully abstract translations, for example, from HOSC to GOS. Richer Types Recall that our full abstraction results are stated for cr-free terms, terms with cont-and ref-free types at the boundary. Here we first discuss how to extend them to more complicated types. To deal with reference type at the boundary, i.e. location exchange, one needs to generalize the notion of traces, so that they can carry, for each action, a heap representing the values stored in the disclosed part of the heap, as in [23, 27] . The extension to sum, recursive and empty types seems conceptually straightforward, by simply extending the definition of abstract values for these types, following the similar notion of ultimate pattern in [24] . The same idea should apply to allow continuation types at the boundary. Operational game semantics for an extension of HOS with polymorphism has been explored in [15] . Innocence On the other hand, all of the languages we considered were stateful. In the presence of state, all of the actions that are represented by labels (and their order and frequency) can be observed, because they could generate a sideeffect. A natural question to ask whether the techniques could also be used to provide analogous theorems for purely functional computation, i.e. contexts taken from the language PCF. Here, the situation is different. For example, the terms f : Int → Int f (0) and f : Int → Int if f (0) f (0) f (0) should be equivalent, even though the sets of their traces are incomparable. It is known [12] that PCF strategies satisfy a uniformity condition called innocence. Unfortunately, restricting our traces to "O-innocent ones" (like we did with O-visibility and O-bracketing) would not deliver the required characterization. Technically, this is due to the fact that, in our arguments, given a single trace (with suitable properties), we can produce a context that induces the given trace and no other traces (except those implied by the definition of a trace). For innocence, this would not be possible due to the uniformity requirement. It will imply that, although we can find a functional context that generates an innocent trace, it might also generate other traces, which then have to be taken into account when considering contextual testing. This branching property makes it difficult to capture equivalence with respect to functional contexts explicitly, e.g. through traces, which is illustrated by the use of the so-called intrinsic quotient in game models of PCF [2, 12] . We have presented four operational game models for HOSC, which capture term interaction with contexts built from any of the four sublanguages x ∈ {HOSC, GOSC, HOS, GOS} respectively. The most direct precursor to this work is Laird's trace model for HOS[HOS] [23] . Other frameworks in this spirit include models for objects [18] , aspects [16] and system-level code [9] . In [13] , Laird's model has been related formally to the denotational game model from [27] . However, in general, it is not yet clear how one can move systematically between the operational and denotational game-based approaches, despite some promising steps reported in [25] . Below we mention other operational techniques for reasoning about contextual equivalence. In [31] , fully abstract Eager-Normal-Form (enf) Bisimulations are presented for an untyped λ-calculus with store and control, similar to HOSC (but with control represented using the λμ-calculus). The bisimulations are parameterised by worlds to model the evolution of store, and bisimulations on contexts are used to deal with control. Like our approach, they are based on symbolic evaluation of open terms. Typed enf-bisimulations, for a language without store and in controlpassing style, have been introduced in [24] . Fully-abstract enf-bisimulations are presented in [7] for a language with state only, corresponding to an untyped version of HOS. Earlier works in this strand include [17, 29] . Environmental Bisimulations [19, 30, 32] have also been introduced for languages with store. They work on closed terms, computing the arguments that contexts can provide to terms using an environment similar to our component γ. They have also been extended to languages with call/cc [34] and delimited control operators [5, 6] . Kripke Logical Relations [28, 4, 8] have been introduced for languages with state and control. In [8] , a characterization of contextual equivalence for each case x[x] (x ∈ {HOSC, GOSC, HOS, GOS}) is given, using techniques called backtracking and public transitions, which exploit the absence of higher-order store and that of control constructs respectively. Importing these techniques in the setting of Kripke Open Bisimulations [14] should allow one to build a bridge between the game-semantics characterizations and Kripke Logical Relations. Parametric bisimulations [11] have been introduced as an operational technique, merging ideas from Kripke Logical Relations and Environmental Bisimulations. They do not represent functional values coming from the environment using names, but instead use a notion of global and local knowledge to compute these values, reminiscent of the work on environmental bisimulations. The notion of global knowledge depends itself on a notion of evolving world. To our knowledge, no fully abstract Parametric Bisimulations have been presented. A general theory of applicative [21] and normal-form bisimulations [20] has been developed, with the goal of being modular with respect to the effects considered. While the goal is similar to our work, the papers consider monadic and algebraic presentation of effects, trying particularly to design a general theory for proving soundness and completeness of such bisimulations. These works complement ours, and we would like to explore possible connections. Games in the semantics of programming languages Full abstraction for PCF. Information and Computation Call-by-value games State-dependent representation independence Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation Environmental bisimulations for delimited-control operators A complete normal-form bisimilarity for state The impact of higher-order state and control effects on local relational reasoning A system-level game semantics A variable typed logic of effects The marriage of bisimulations and kripke logical relations On Full Abstraction for PCF: I. Models, observables and the full abstraction problem, II. Dialogue games and innocent strategies, III. A fully abstract and universal game model Operational nominal game semantics Kripke open bisimulation -A marriage of game semantics and operational techniques Trace semantics for polymorphic references Open bisimulation for aspects Towards a theory of bisimulation for local names A fully abstract may testing semantics for concurrent objects Small bisimulations for reasoning about higher-order imperative programs Effectful normal form bisimulation Effectful applicative bisimilarity: Monads, relators, and howe's method Full abstraction for functional languages with control A fully abstract trace semantics for general references Typed normal form bisimulation Transition systems over games Fully abstract models of typed lambda-calculi Game semantics for good general references Operational reasoning for functions with local state Expressing mobility in process algebras: First-order and higher-order paradigms Environmental bisimulations for higherorder languages A complete, co-inductive syntactic theory of sequential control and state A complete characterization of observational equivalence in polymorphic lambda-calculus with general references Higher-Order Operational Techniques in Semantics A sound and complete bisimulation for contextual equivalence in λ-calculus with call/cc 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.