Recursive Types in Games: Axiomatics and Process Representation

(Extended Abstract)

Marcelo Fiore^{∗}

               <marcelo@cogs.susx.ac.uk>

COGS, University of Sussex

Kohei Honda

                                                      <kohei@dcs.ed.ac.uk>

LFCS, University of Edinburgh

Abstract

This paper presents two basic results on game-based semantics of FPC, a metalanguage with sums, products, exponentials and recursive types. First we give an axiomatic account of the category of games G introduced in [15], offering a fundamental structural analysis of the category as well as a transparent way to prove computational adequacy. As a consequence we obtain an intensional fullabstraction result through a standard definability argument. Next we extend the category G by introducing a category of games G_{i} with optimised strategies; we show that the denotational semantics in G_{i} gives a compilation of FPC terms into core Pict codes (the asynchronous polyadic π-calculus without summation). The process representation follows a pioneering idea of Hyland and Ong [18]. However, we advance their representation by introducing semantically well-founded optimisation techniques; we also extend the setting to encompass the rich type structure of FPC. The resulting code gives basic insight on the relationship between the abstract, categorical, types and their possible implementations.

1 Introduction

Games in semantics. Recently, the notions of games and strategies have been used for constructing mathematical models of programming languages; e.g. [4, 1, 17, 7, 18, 2, 22, 15, 3]. The basic common idea underlying these works is to construct a universe of semantic domains in which a program phrase is modelled as an object with internal structure reflecting its computational behaviour in an abstract way. In particular, semantic points are interacting processes called strategies, where interaction represents the behaviour of a program in all contexts.

We mention some salient features of this approach. First, game semantics offers a very precise abstract characterisation of computational behaviour leading to various full abstraction results. Second, despite its novel way of representing programs, game-theoretic models are equipped with familiar semantic structures offering traditional mathematical tools for reasoning about programs. Third, gametheoretic models are closely related to existing models of interaction; e.g. π-calculus [25] and Linear Logic [12]. We expand on this point next, focussing on the relationship to π-calculus. Process representation of games. Following their full abstraction result for (call-by-name) PCF, Hyland and Ong [18] observed that their strategies could be faithfully represented by terms in the π-calculus. This observation suggests a close connection between the games model and π-calculus representation of programming languages (see e.g. [23, 37]). It also opens the possibility of studying dynamics of programs at a level close to implementation using game semantics.

Central themes of this paper are a further investigation in this direction, and an axiomatisation of a category of games following [9, 10]. Among other things, we aim to advance the work of Hyland and Ong [18] in a couple of points.

• Many programming languages adopt a call-by-value evaluation strategy and have more intricate type structure like sums and recursive types, cf. [26]. Can game semantics handle these features, and allow process representation in this setting?

• A close inspection of the process representation in [18] reveals that the frequent use of the “copy-cat” (or “titfor-tat”) behaviour results in quite redundant interactions. This dissociates the resulting code from any feasible implementation. Can one obtain better code from a game-theoretic model of a programming language?

∗Research supported by EPSRC grant GR/J84205, Frameworks for Programming Language Semantics and Logic at LFCS, University of Edinburgh.

Results. This work addresses the above mentioned issues taking FPC [30] as an example programming language. FPC is essentially the functional core of ML; we have chosen it for its rich type structure and call-by-value operational semantics. Moreover its primitive character is useful to examine the basic features of our approach in a simple, though non-trivial, setting. Our results can be summarised as follows.

First, we present a fully abstract interpretation of FPC in the category of games G introduced in [15]. An important contribution here is an axiomatic approach, which offers a basic categorical analysis of the universe of games and a transparent way to prove computational adequacy.

Second, we introduce a new category of games G_{i} extending G. Objects in G_{i} are as in G, but the hom-sets contain “optimised” versions of the strategies in G. The key idea is to represent the “copy-cat” behaviour by a tree isomorphism. Computational adequacy is again obtained from the axiomatisation referred to above.

Finally, we transform the interpretation of FPC in G_{i} into core Pict (the asynchronous polyadic π-calculus) [29], and show that the translation faithfully represents the original strategies. The resulting code exhibits a close link between the abstract type structures and their implementation, cast in the setting of name-passing processes.

Related work. First we comment on the relationship between the axiomatisation in this paper and that of [9, 10]. Both axiomatisations take the same conceptual standpoint based on the interplay between a category of partial maps and a subcategory of total maps there of. However, in order to accommodate the intensional nature of games, here we have to weaken the categorical structure for modelling product types (from monoidal to binoidal). Consequently, we have axiomatised the information-system approach to solving domain equations rather than the one based on the limit-colimit coincidence. This yields new computationally adequate models of FPC. (See Section 3 ‘§ Basic Axiomatisation’ for details.)

We know of two other full abstraction results for FPC. McCusker obtained a full abstraction result for call-by-name FPC [22], while Riecke and Sandholm obtained full abstraction for (call-by-value) FPC via logical relations [33]. The first one differs from ours in that the target language is call-by-name, while the second one uses quite a different construction and so offers a very different semantic analysis. We also note that Abramsky and McCusker [3] presented a category of call-by-value games closely related to the one in [15]. They independently gave a fully abstract interpretation of recursive types in their universe.

Regarding process representation of strategies, we already discussed how our work builds on previous work of Hyland and Ong [18]. The incorporation of rich type structure as well as the new more viable encoding are the main additional contributions of our work. In particular, our treatment of recursive types offers new insights on the relationship between the abstract notion of recursive type (as free algebras [11]) and their implementation (via pointers). Among the work on π-calculus representation of λ-calculi, cf. [23, 6, 35, 5], a new contribution of our work is the type-theoretic (or category-theoretic) perspective it offers. For example, the difference between “eager sum” and “lazy sum” is articulated at the categorical level and consequently in the operational structure. Thus our work broadens the repertoire of π-calculus representation of functional calculi, with type-theoretic background.

Organisation of the paper. In Section 2 we review the category G of games introduced in [15]. In Section 3 we present new axiomatic models of FPC, and establish their computational soundness and adequacy. We apply this result to G, and obtain intensional full abstraction for FPC. In Section 4 we introduce a new category of games G_{i} with optimised strategies. Computational adequacy for G_{i} is again obtained from the axiomatic method of Section 3. In Section 5 we give a compilation of FPC into Pict through its denotational semantics in G_{i}, and establish the computational adequacy of the compilation.

2 Basic games

We outline the basic notions of games introduced in [15]. The key difference from preceding games lies in that interaction becomes data-driven (starts from the arrival of data from the environment) rather than demand-driven (starts from the inquiry of data), thus successfully modelling callby-value computation. This means that arenas —the notion of type in game-based semantics— start from Answers rather than Questions, as formalised below.

Arena. A forest is a directed graph in which every connected component is a tree. Nodes are denoted S, T, etc. We write S ↦ T if there is a directed edge from S to T. The relation ↦ is sometimes called enabling. So a forest is presented by (Σ, ↦ ⊆ Σ^{2}) where Σ is the set of nodes. In a forest, a node S is said to be initial if for no T we have T ↦ S.

A pre-arena is a forest (Σ, ↦ ⊆ Σ^{2}) together with labelling functions ℓ_{1} : Σ → {P, O} and ℓ_{2} : Σ → {Q, A} such that whenever S ↦ T the following are satisfied:

(1) ℓ_{1}(T) = \overline{ℓ_{1}(S)} where \overline{P} =^{def} O and \overline{O} =^{def} P (Opponent justifies P layer, and vice versa) and (2) if ℓ_{2}(S) = A then ℓ_{2}(T) = Q (a Question justifies both Answers and Questions, while an Answer justifies only Questions). The nodes in a pre-arena are called sorts. We often write ℓ for the pairing ⟨ℓ_{1}, ℓ_{2}⟩ of the labelling functions.

Let A = (Σ, ↦, ℓ) and A′ = (Σ′, ↦′, ℓ′) be pre-arenas. The dual pre-arena \overline{A} has the same set of sorts and enabling relation as the pre-arena A, with Opponent/P layer reversed: that is \overline{ℓ} =^{def} ⟨\overline{ℓ_{1}}, ℓ_{2}⟩ where \overline{ℓ_{1}}(S) =^{def} \overline{ℓ_{1}(S)}.

The disjoint union pre-arena A⊎A′ has sorts given by the disjoint union Σ ⊎ Σ′, with enabling relation and labelling functions as in A and A′.

The pre-arena A is said to be a sub-pre-arena of the pre-arena A′ if (1) every initial sort in A is initial in A′;

(2) Σ ⊆ Σ′; (3) ↦ ⊆ ↦′; and (4) ℓ = ℓ′ ↾ Σ.

Finally an arena is a pre-arena in which initial sorts are labelled P A. Action sequence. Given arenas A and B, an action sequence from A to B is a finite sequence of sorts S_{0} · . . . · S_{n} in the pre-arena \overline{A}⊎B, where occurrences of sorts are called actions (often referred to as P -action, O-action, Question, and Answer according to the labels), together with a justification relation ↷ ⊆ [0..n−1] × [1..n] (where we read i ↷ j as i justifies j) such that: (1) the sort S_{0} is initial in \overline{A};

(2) there exists at most one j ∈ [1..n] which is not justified and, for such j, S_{j} is initial in B; (3) Opponent and P layer alternate; (4) no two actions justify the same action; (5) if i justifies j then S_{i} precedes and enables S_{j}; and (6) every Question justifies at most one Answer.

An action sequence represents a possible interaction sequence a process may be engaged in. A view [17] is part of such a sequence used by a process to decide its next action. View. The P -view ⌈ s ⌉ of an action sequence s is the sequence with justification relation inherited from s, inductively defined by (P v1) ⌈ ε ⌉ = ε; (P v2) ⌈ S ⌉ = S; (P v3) ⌈ s_{0}S ⌉ = ⌈ s_{0} ⌉ · S whenever S is a P -action; (P v4) ⌈ s_{0} · S_{i} · s_{1} · S_{j} ⌉ = ⌈ s_{0} ⌉ · S_{i} · S_{j} whenever i ↷ j and S_{j} is an O-action. The O-view of an action sequence s is denoted ⌊ s ⌋ and is defined dually (that is, by exchanging the rôles of P and O actions in the previous definition). By the view of an action S in an action sequence s · S we mean the P -view ⌈ s · S ⌉ if S is a P -action, and the O-view ⌊ s · S ⌋ if S is an O-action. Innocent strategy. An action sequence s is said to be legal when: it is well-bracketed, i.e. later asked questions are answered first, and it satisfies the visibility condition, i.e. every action is justified by an action in its view. We are now in a position to define morphisms between arenas. Let A and A′ be arenas. An innocent strategy σ from A to A′ (in symbols, σ : A ⇀ A′) is a non-empty set of prefix-closed legal action sequences from A to A′ satisfying:

(Contingency completeness) If s in σ ends with a P -action and s′ = s · S is legal then s′ is also in σ.

(Determinacy) Whenever s · S and s · S′ are in σ with S and S′ P -actions, s · S = s · S′.

(Innocence) For action sequences s · S and s′ in σ with S a P -action, if ⌈ s ⌉ = ⌈ s′ ⌉ then s′ · S is an action sequence in σ with ⌈ s′ · S ⌉ = ⌈ s · S ⌉.

By a P-view from A to B we mean the P-view of some legal action sequence from A to B. Notice that each innocent strategy σ is precisely characterised by its innocent function; namely, the partial function that extends every oddlength P -view by σ’s reaction to it.

An innocent strategy σ : A ⇀ A′ is total if for each initial O-answer it immediately reacts by an initial P-answer; that is, for every initial sort S in \overline{A} there exists an initial sort S′ in A′ such that the action sequence S · S′ (with empty justification relation) is in σ. To indicate that σ is total we either write σ : A → A′ or σ ↓.

A sub-arena A of an arena A′ induces a substructure total innocent strategy A → A′ given by the strategy that copies every O-action in \overline{A} to a P -action in A′, and copies every O-action in A′ appearing in A to a P -action in \overline{A}. Composition. Given innocent strategies σ : A ⇀ B and τ : B ⇀ C, we define their composition σ; τ as follows. Consider a game board with 4 rows and ω columns whose rows are respectively called \overline{A}, B, \overline{B} and C. Columns are counted from 1. A configuration consists of a game board together with a binary relation, called justification, on squares such that: (1) squares are filled (if ever) by sorts from \overline{A}, B, \overline{B}, C, each placed in a square of the corresponding row; (2) for some n, at each i^{th} column (1 ≤ i ≤ n) either only the square at row \overline{A}, or only the square at row C, or only both squares at rows B and \overline{B} are filled, moreover no squares at later columns are filled; (3) only squares in the same row are related by the justification relation; (4) the projections onto B and \overline{B} coincide (including the justification relation). A configuration is legal if, when projected onto \overline{A}-B (resp. \overline{B}-C), it induces a legal sequence from A to B (resp. from B to C). Finally a composed play of σ and τ is a legal configuration such that the \overline{A}-B (resp. the \overline{B}-C) projection is in σ (resp. in τ). It was shown in [15, pp.31– 40] that the set of \overline{A}-C projections of the composed plays yields an innocent strategy from A to C, which we define to be the composition σ; τ. Category of Games. The category of games G has arenas as objects and innocent strategies as morphisms. Identities are given by the copy-cat strategy: that is the strategy which exactly copies the preceding O-action to the next P -action including the justification relation. We shall study these behaviours in more detail in Section 4.

We write G_{t} for the subcategory of G consisting of the total innocent strategies, and G_{s} for the subcategory of G_{t} consisting of the sub-structure total innocent strategies. G_{s} is actually a (large) cpo with lubs given by unions.

We order innocent strategies by inclusion of innocent functions, then each hom-set G(A, A′) becomes a cpo. With respect to this order, henceforth denoted ⊏ ∼ , the composition operation G(A′, A′′) × G(A, A′) → G(A, A′) becomes continuous [15]. Thus, G equipped with ⊏ ∼ is a Cpo-category (see [9, Chapter 2] for the basic concepts of enriched category theory). The restriction of ⊏ ∼ to total innocent strategies is denoted ⊑; it makes G_{t} a Cpocategory. Type structure. We outline the basic construction of types in G. First 0 is the empty arena (no sorts), while 1 is the arena with a (distinguished) single sort. The sum of arenas + is simply given by their disjoint union. The pretensor arena A ⊗ A′ of the arenas A and A′ has forest consisting of the trees obtained as the coalesced sum of every tree in the forest of A with every tree in the forest of A′; the labelling function is inherited from each component. The higher-order arena A⇀ ⇀A′ of the arenas A and A′ has forest consisting of one new initial sort enabling (every tree in) the forest of A and every initial sort of A enabling a copy of (every tree in) the forest of A′; the labelling function labels the new initial sort with P A, each initial sort in A with OQ, each non-initial sort S in A with its dual \overline{ℓ}(S), and each sort in a copy of A′ with the same label.

3 Denotational semantics of FPC

FPC is a metalanguage with sums, products, exponentials and recursive types, equipped with a call-by-value evaluation. The definition of FPC can be found in [13, 38, 9]. Here we only provide the syntax of types and expressions.

Types

α ::= T | α_{1} + α_{2} | α_{1} × α_{2} | α_{1}⇀ ⇀α_{2} | μT.α,

Expressions

M ::= x | inl_{α_{1},α_{2}}(M) | inr_{α_{1},α_{2}}(M) |

case M ofinl(x_{1}).M_{1} orinr(x_{2}).M_{2} |

⟨M_{1}, M_{2}⟩ | fst(M) | snd(M) | λx : α.M | M_{1}(M_{2}) | intro_{μT.α}(M) | elim(e).

Our aim is to show that the category G allows computationally adequate interpretations of FPC via an axiomatic method (cf. [9]). The axiomatics elucidates the type structure of the category G, providing an algebraic method for reasoning about strategies. It also plays an important rôle in later sections. Basic axiomatisation. We start by axiomatising a notion of basic model giving the data for interpreting FPC. These basic models are computationally sound. The notion of model, will be introduced in “§ Axiomatisation” below, by requiring further axioms on basic models.

The axiomatisation of basic models (see Definition 3.1) can be understood as consisting of two parts: (1) the data (BMa)–(BMb) subject to (BM1)–(BM2), providing the data for interpreting the type constructors +, ×, and ⇀ ⇀; and (2) the datum (BMc) subject to (BM3), allowing the interpretation of the recursive-type constructor μ.

The categorical structure for interpreting the sum type constructor + is standard; that is, given by binary coproducts. It then follows that the interpretation of the product type constructor × cannot be standard, viz. given by products (cf. [20, 16]). However, the category of games G admits a pretensor constructor ⊗ (see Section 2, § Type structure) which is a product in the subcategory, G_{t}, of total innocent strategies [15]. This situation, which is typical in models of FPC [9, 10], is the one that we axiomatise. The structure for interpreting the exponential type constructor ⇀ ⇀ arises as in partial cartesian closed categories [21, 27, 34].

We have already mentioned that the pretensor constructor ⊗ on the category of games G is not a product. However, for every pair of arenas A and B, we have endofunctors A⊗( ) and ( )⊗B on G such that A⊗(B) = (A)⊗B [15]. That is, in the terminology of [31], G equipped with the family of endofunctors A ⊗ and ⊗ B (A, B ∈ G) is a binoidal category.

Now, consider the type judgement A, T ⊢ 1 + T × A × T. It induces a function on arenas mapping a pair of arenas (A, T) to the arena 1 + T ⊗ A ⊗ T, which by the previous considerations does not extend to a functor G^{2} → G. Thus one cannot interpret type judgements T_{1}, …, T_{n} ⊢ α as functors G^{n} → G, and consequently one cannot interpret recursive types as parameterised free algebras [11, 9, 30, 32]. Our approach to solving this problem is to restrict attention to a subcategory of G in which type judgements can be interpreted as functors, and find the recursive types there. This idea is traditional in domain theory. For example, it occurs when solving domain equations of functors of mixed variance when one may restrict a Cpo-category to its subcategory of embeddings [36], and it occurs when solving domain equations with information systems when one restricts from the category of information systems to a pointed cpo of them [19, 38]. There are various ways in which one may restrict G so that the action of ⊗ on arenas extends to a functor. One possibility is to consider the centre of G (see [31] for this concept) which in our case coincides with G_{t}. Here, rather than doing so, we will axiomatise the information-system approach (as has been done in [8, 22]). In our example, this will amount to interpreting type judgements T_{1}, …, T_{n} ⊢ α as continuous functions G_{s}^{n} → G_{s} and finding recursive types with Scott’s least fixed-point operator (or rather with Bekic̆’s parameterised version of it). Thus recursive types will be interpreted up to equality; this slightly simplifies the proof of computational adequacy (cf. [9, Chapters 9 and 10]).

An extra ingredient of basic models is a Cpoenrichment axiomatising the information order. This structure is not needed to obtain computational soundness, but plays a central rôle when proving computational adequacy.

We now introduce basic models; an explanation of the definition in elementary terms will follow. It will be helpful to think of G as G, of T as G_{t}, and of S as G_{s}.

Definition 3.1 (Basic models) A basic model consists of

(BMa) a Cpo-category, G, equipped with a Cpobinoidal structure (X ⊗ ( ), ( ) ⊗ Y),

(BMb) a full on objects Cpo-subcategory of G, T , equipped with finite Cpo-coproducts (0, +) and finite Cpo-products (1, ×),

(BMc) a full on objects subcategory of T , S,

such that

(BM1) the inclusion T → G is strict binoidal,

(BM2) for each X, the Cpo-functor ⊗ X : T → G has a right Cpo-adjoint X⇀ ⇀ : G → T ,

(BM3) S is a pointed cpo, and for ⋆ = +, ⊗, ⇀ ⇀, the function ⋆ : S × S → S : (X, Y) ↦ X ⋆ Y is continuous.

The requirement (BM1) amounts to asking for Cpofunctors X ⊗ ( ) : G → G and ( ) ⊗ Y : G → G for all X, Y ∈ | G | such that (i) X ⊗ (Y) = (X) ⊗ Y = X × Y; (ii) for all f in T , X ⊗ (f) = X × f, (f) ⊗ Y = f × Y; and (iii) every map in T is central [31] in G; that is, every f : A → B in T has the property that, for every u : X → Y in G, (A ⊗ u); (f ⊗ Y) = (f ⊗ X); (B ⊗ u) and (u ⊗ A); (Y ⊗ f) = (X ⊗ f); (u ⊗ B).

As a consequence of (BM2), the functor ⊗X preserves Cpo-colimits. Thus, G has finite Cpo-coproducts given as in T . Moreover, there is a canonical isomorphism

(1) δ_{X,Y,Z} : X ⊗ (Y + Z) ≅ (Y + Z) ⊗ X
≅ (X ⊗ Y) + (X ⊗ Z)
≅ (Y ⊗ X) + (Z ⊗ X)

natural with respect to maps in T . This map together with the canonical map Δ_{X} =^{def} ⟨id, id⟩ : X → X ⊗ X will be useful when interpreting the case statement. Interpretation. We sketch the denotational semantics of FPC in basic models.

Throughout this section we fix a basic model (G, T , S). We interpret well-formed types Θ ⊢ α, where Θ is a list of distinct type variables containing those that are free in α, as continuous functions [[Θ ⊢ α]] : S^{|Θ|} → S. The definition is by induction on types, interpreting the sum type constructor as +, the product type constructor as ⊗, the exponential type constructor as ⇀ ⇀, and the recursive-type constructor as Bekic̆’s parameterised least fixed-point operator ( )^{†} (see Figure 1). The interpretation of well-formed types induces the interpretation of well-formed expression contexts Θ ⊢ Γ as continuous functions [[Θ ⊢ Γ]] : S^{|Θ|} → S in the usual way.

Lemma 3.2 (Substitution lemma) For Θ, T ⊢ α_{1} and Θ ⊢ α_{2}, we have that

[[Θ ⊢ α_{1}[T ↦ α_{2}]]] = ⟨Id, [[Θ ⊢ α_{2}]]⟩; [[Θ, T ⊢ α_{1}]] .

Hence, for Θ ⊢ μT.α, the equality [[Θ ⊢ α[T ↦ μT.α]]] = [[Θ ⊢ μT.α]] holds.

Convention. Maps in G will be indicated with ⇀. For a map u : X ⇀ Y, we write u : X → Y or u ↓ to further indicate that it is in the subcategory T .

The interpretation of a well-formed expression Θ, Γ ⊢ M : α is a family [[Θ, Γ ⊢ M : α]] = {[[Θ, Γ ⊢ M : α]]_{X} | X ∈ S^{|Θ|}} where [[Θ, Γ ⊢ M : α]]_{X} is a map [[Θ ⊢ Γ]](X) ⇀ [[Θ ⊢ α]](X). The definition of the interpretation function is essentially that of [9, 10] and is given in Figure 2.

We write Θ, Γ ⊢ M ⇝ V : α to indicate that both Θ, Γ ⊢ M : α and Θ, Γ ⊢ V : α are derivable and that M evaluates to V according to call-by-value evaluation rules. We also write Θ, Γ ⊢ M ✓ : α when Θ, Γ ⊢ M ⇝ V : α for some value V.

Lemma 3.3 In every basic model, (1) [[Θ, Γ ⊢ V : α]] ↓ for every value V, and (2) if Θ, Γ ⊢ M ⇝ V : α then [[Θ, Γ ⊢ M : α]] = [[Θ, Γ ⊢ V : α]].

Corollary 3.4 (Computational soundness) In every basic model, if Θ, Γ ⊢ M ✓ : α then [[Θ, Γ ⊢ M : α]] ↓.

Axiomatisation. The Cpo-enrichment on G will be denoted ⊏ ∼ . For maps u ⊏ ∼ v in G, we write u ⊑ v to indicate that u and v are in T . Thus, ⊑ denotes the Cpo-enrichment on T .

Roughly speaking, a model (see Definition 3.5) is a basic model that (1) is not trivial; and in which (2) composition is strict (in accordance with call-by-value evaluation); (3) definedness is an observable (or semi-decidable) property;

(4) the information order on T (X, A_{1} + A_{2}) for maps of the form X → A_{i} ^{⨿_{i}}→ A_{1} + A_{2} is determined by the information order on T (X, A_{i}); (5) the approximation structure provided by S corresponds to standard approximation structure in G (viz. embeddings [36]), and moreover is compositional with respect to the type structure.

Definition 3.5 (Model) A model is a basic model that further satisfies:

(M1) 0 ≅ 1̸.

(M2) For u : X ⇀ Y and v : Y ⇀ Z, if u; v ↓ then u ↓.

(M3) For every X, the hom-set T (1, X) is Scott-open in the hom-cpo G(1, X).

[[Θ ⊢ Θ_{i}]] =^{def} Π_{i}  [[Θ ⊢ α_{1} + α_{2}]] =^{def} ⟨[[Θ ⊢ α_{1}]], [[Θ ⊢ α_{2}]]⟩; +
[[Θ ⊢ α_{1} × α_{2}]] =^{def} ⟨[[Θ ⊢ α_{1}]], [[Θ ⊢ α_{2}]]⟩; ⊗  [[Θ ⊢ α_{1}⇀ ⇀α_{2}]] =^{def} ⟨[[Θ ⊢ α_{1}]], [[Θ ⊢ α_{2}]]⟩; ⇀ ⇀

[[Θ ⊢ μT.α]] =^{def} [[Θ, T ⊢ α]]^{†}

Figure 1. Interpretation of well-formed types

(M4) The coproduct injections ⨿_{i} reflect the order in T . That is, if f; ⨿_{i} ⊑ g; ⨿_{i} : X → A_{1} + A_{2} then f ⊑ g : X → A_{i}.

(M5) Every map in S is an embedding in G (and hence it is in T ), and the inclusion functor S → G preserves the initial object and colimits of ω-chains.

Moreover, writing ι_{X,Y} for the unique arrow X → Y in S whenever it exists and writing ȷ_{Y,X} for its associated projection Y ⇀ X, the following equalities hold: ι_{X+Y,X′+Y′} = ι_{X,X′} + ι_{Y,Y′}, ι_{X⊗Y,X′⊗Y′} = ι_{X,X′} × ι_{Y,Y′}, and ι_{X ⇀ ⇀ Y,X′ ⇀ ⇀ Y′} = ȷ_{X′,X} ⇀ ⇀ι_{Y,Y′}.

As expected, (G, G_{t}, G_{s}) provides a model. For instance, to see that (M5) holds one uses the fact that the inclusion functor S → G preserves colimits of ω-chains if and only if, for every ω-chain ⟨X_{i}⟩ in S with lub X, it happens that ⨆_{i} ȷ_{X,X_{i}}; ι_{X_{i},X} = id_{X} (see [36]). Relation to operational semantics. We have the following main results.

Theorem 3.6 (Computational adequacy) In every model, if [[⊢ P : α]] ↓ then ⊢ P ✓ : α.

The proof follows the structure of the one in [9, Chapter 9] (see also [10]).

Corollary 3.7 In the category of games G, the innocent strategy [[⊢ P : α]] is total iff ⊢ P ✓ : α.

Theorem 3.8 (Full abstraction) The standard quotient of G (cf. [15]) gives an inequationally fully abstract model of FPC.

The proof is along the lines of [15, Theorems 5.9 and 5.10] via a definability result in G for finite canonical forms of finite type (cf. [22]).

4 Games with optimised strategies

Two issues in process representation of strategies. This section and the next exploit the intensional nature of game semantics to obtain a semantically directed compilation of FPC terms into Pict codes [29]. Our aim is to deepen the understanding of the operational content of FPC programs through a process representation of their game-theoretic interpretation. From this viewpoint, we may observe the following two basic issues in the original process representation of PCF strategies by Hyland and Ong [18].

(1) (Problem of Sums) When infinitely branching arenas are involved (as, for example, in lists) we should either use an infinite sequence of names (which is infeasible) or use an index from an infinite set of constants as is done in [18] (which is again infeasible when complex data structures are present, as in FPC).

(2) (Problem of Copy-Cat) While copy-cat-like behaviours are prevalent (e.g. in the interpretation of projections and injections), their process representation in [18] reveals significant redundancy. This makes the resulting code hard to understand and far from any imaginable implementation scheme. For example, if the process representation of a closed term M(N) needs n steps to converge, then that of M(IN) (where I =^{def} λx.x) needs, essentially, 2n steps to converge. This is an omnipresent problem. For example, when a term involves unbounded behaviour (like a fixed-point combinator) it is impossible to statically erase the redundancy.

To obtain feasible and concise code without sacrificing the structure of the interpretation of FPC in G, we address these issues at the categorical level. The first problem is solved by introducing a lazy interpretation of sums, as will be presented in Section 5. A solution to the second problem is given in this section by extending G via a slight change in the operational structure of games. The key idea for the new notion of games is to use certain tree isomorphisms to represent copy-cats. As we shall see in Section 5, this new relation on actions represents the communication of free names in π-calculus. The construction is interesting in its own right, since it gives an analysis on the notion of copy-cat, a fundamental idea in game semantics. V-strategies. We use the same arenas as in Section 2. Fix arenas A and B and consider the pre-arena \overline{A} ⊎ B. We write Ŝ for the tree with root S in this pre-arena, and introduce the notation Ψ : Ŝ_{1} ▷◁ Ŝ_{2} to indicate that Ψ is an isomorphism between the trees Ŝ_{1} and Ŝ_{2} that preserves QA-labels but reverses OP -labels. Further, we write source (Ψ) for S_{1} and target(Ψ) for S_{2}. A V-sequence from A to B is an action sequence in the sense of Section 2 (§ Action Sequence) together with a set of V-pointers on it. A V-pointer on an action sequence S_{0} … S_{n−1} is a triple i ⇒^{Ψ} j, satisfying: (1) 0 ≤ i < j ≤ n − 1; (2) S_{i} is by Opponent and S_{j} is by Player; (3) Ψ : T′ ▷◁ T′′ for T′ and T′′ such that S_{i} ↦ T′ and S_{j} ↦ T′′; (4) for no j < k ≤ n − 1 such that S_{k} = target(Ψ) we have that

j ↷ k (“free names do not bind”); and (5) if l ⇒^{Ψ′} j for some l and Ψ′ such that target(Ψ) = target(Ψ′), then l = i and Ψ′ = Ψ (“non-ambiguity in binding”). Prefix, equality, etc. on V-sequences are defined considering both justification and V-pointers. A V-sequence satisfies the visibility condition if it does so as an action sequence and, moreover, if for each V-pointer i ⇒^{Ψ} j, i is in the view of j. A V-sequence is legal if it is both well-bracketed as an action sequence and satisfies the visibility condition. A V-strategy is an innocent strategy defined as in Section 2 by replacing “action sequences” with “V-sequences”. A V-strategy is total when, as before, it immediately reacts at the codomain for each initial O-answer.

Note that all strategies in G are trivially V-strategies. As a non-trivial example, let id′_{A} : A → A be the following V-strategy: letting Ψ be the evident isomorphism mapping \overline{A} to A in \overline{A} ⊎ A, for each initial O-answer S, the strategy answers by Ψ(S), carrying one V-pointer for each S′ such that S ↦ S′, with the associated isomorphism Ψ ↾ Ŝ′. No more actions are possible by (4) above. Composition of V-strategies. An extended V-sequence is an action sequence with V-pointers which satisfies (1), (2), (3), and (5) of the preceding subsection. Legality and other notions for extended V-sequences are inherited from V-sequences.

Let σ : A ⇀ B be a V-strategy and let f_{σ} be its innocent function. We define f_{σ}^{+} to be the smallest partial function on P-views of extended V-sequences from A to B, satisfying:

• f_{σ}^{+} ⊇ f_{σ};

• if s is in the range of f_{σ}^{+} with the underlying sequence S_{0} … S_{2n−1} then, for each V-pointer i ⇒^{Ψ} 2n − 1 and for each P-view s′ = s · S_{2n} such that S_{2n} = target(Ψ) and 2n − 1 ↷ 2n, we have that f_{σ}^{+}(s′) = s′ · S_{2n+1} with S_{2n+1} = source (Ψ) and i ↷ 2n + 1, together

with V-pointers {2n ⇒^{Ψ′_{k}} 2n + 1 | S_{2n} ↦ S′_{k}} where

Ψ′_{k} =^{def} Ψ^{−1} ↾ Ŝ′_{k}.

One can check that f_{σ}^{+} is a well-defined partial function. We write σ^{+} for the V-strategy on extended V-sequences generated by f_{σ}^{+}. Given V-strategies σ : A ⇀ B and τ : B ⇀ C, we define σ; τ by the following procedure. Below x, x_{i}, … denote occurrences of sorts on the game board.

(i) Composed plays are defined as in Section 2 using σ^{+} and τ^{+}, but recording V-pointers.

(ii) Given each composed play, for each maximal sequence

of V-pointers x_{0} ⇒^{Φ_{0}} x_{1}, x_{2} ⇒^{Φ_{1}} x_{3}, …, x_{2n} ⇒^{Φ_{n}} x_{2n+1}

such that x_{2i−1} and x_{2i} are in the same column and target(Φ_{i−1}) = source (Φ_{i}) for all 1 ≤ i ≤ n, we erase all these V-pointers and instead put a V-pointer

x_{0} ⇒^{Φ′} x_{2n+1} with Φ′ =^{def} Φ_{n} ∘ Φ_{n−1} ∘ ⋯ ∘ Φ_{0}.

(iii) We take the projection of the result of (ii) above onto the \overline{A}-C components including V-pointers, and define σ; τ as the set of all (non-extended) V-sequences in them.

For a strategy in G, the above composition and that of Section 2 (§ Composition) coincide.

Proposition 4.1 For V-strategies σ : A ⇀ B and τ : B ⇀ C, σ; τ is a V-strategy from A to C. Moreover, composition is associative and has id′_{A} (as defined above) as an identity.

The proof is as for the category G (see [15]), checking innocence w.r.t. (composed) V-pointers too. New category of games. The Cpo-category G_{i} has arenas as objects and V-strategies as morphisms; identities and composition are as presented above; and the enrichment is given by the inclusion of innocent functions. The categories G_{i} and G have the same type structure. Universal arrows as projections and injections in G_{i} are obtained by turning copy-cats in the corresponding maps in G into V-pointers.

Proposition 4.2 The category G_{i} is a model in the sense of Definition 3.5.

5 Compilation of FPC into Pict via games

Lazy-sum interpretation. Having introduced G_{i} to solve the copy-cat problem, we present a solution to the problem of infinite sums. Our approach is to use an interpretation of FPC in which sums are interpreted lazily.

We consider a lazy-sum type ⊕ encapsulating a computation of sum type +. To this end we introduce the lift functor ( )_{⊥} =^{def} 1⇀ ⇀ : G → T , and define the lazy-sum functor ⊕ as the composite +; ( )_{⊥} : G × G → T . For a simple example consider the type of lazy natural numbers μT.1⊕T. The lift functor comes equipped with an operation for encapsulating a value into a computation, up_{X} =^{def} pλ(X⊗1 ≅ X) : X → X_{⊥}, and a dual operation for evaluating a computation to a value, dn_{X} =^{def} (X_{⊥} ≅ X_{⊥} ⊗ 1 ^{ev}⇀ X). By construction, we have that up_{X}; dn_{X} = id_{X}. These operations together with the coproduct injections ⨿_{i} provide corresponding injections for lazy-sums; viz. ⨿′_{i} =^{def} (X_{i} ^{⨿_{i}}→ X_{1} + X_{2} ^{up_{X_{1}+X_{2}}}→ X_{1} ⊕ X_{2}). There is also a non-standard version of δ (see (1)) which is needed for interpreting the case statement, δ′ =^{def} (X ⊗ (Y ⊕

Z) ^{X⊗dn_{Y +Z}}⇀ X ⊗ (Y + Z) δ ; ≅→ (X ⊗ Y) + (X ⊗ Z)).

The lazy-sum interpretation is denoted by ([ ]) and is as the standard one but replacing + by ⊕, δ by δ′, and ⨿_{i} by ⨿′_{i}, see Figure 3.

This lazy-sum interpretation is also computationally adequate.

Theorem 5.1 In every model (in the sense of Definition 3.5) the lazy-sum interpretation is computationally sound and adequate.

Untyped processes. The denotation of FPC terms via ([·]) in G_{i} can be faithfully represented as concise (core) Pict codes [29], i.e. as terms of asynchronous Polyadic π-calculus. The set of processes of core Pict is given by the following grammar. Below let a, b, … and x, y, … range over a countable set N of names.

P ::= \overline{a}[x_{1}, …, x_{n}] | a(x_{1}, …, x_{n}).P | P |Q |

(νx)P | !a(x_{1}, …, x_{n}).P | 0

The notions of binding, free names, subject names (head of input/output) and object names (names carried in input/output) are standard. We let P; Q stand for (νx̃)(P |Q) where x̃ are common free names in P and Q, while \overline{a}(b) · P denotes (νb)(\overline{a}[b]|P) where b does not occur as a free object of a message in P. The structural congruence ≡ and the reduction relation ⟶ are again standard. We write P ↓ for ∃P′. P ⟶^{∗} P′ with P′ −̸→ and P′ ⟶^{l} for an output l. We use the late transition relation [25] with labels τ, a(x_{1} … x_{n}) and \overline{a}⟨(νA)x_{1}, …, x_{n}⟩ where A ⊆ {x_{1} … x_{n}}. We set sub(a(x_{1} … x_{n})) =

sub(\overline{a}⟨(νA)x_{1} … x_{n}⟩) =^{def} a and ob(a(x_{1} … x_{n}), i) =

ob(\overline{a}⟨(νA)x_{1} … x_{n}⟩, i) =^{def} x_{i}. Using a sequence of input/output labels, say t, for which we assume the usual binding relation and binding convention, the weak transition ⟹^{t} is again standard; and so is the weak bisimilarity ≈ (the late and early versions coincide [14]). We also use the following notion, cf. [23]: a π-term P is strongly determinate when for each P′ such that P ⟶^{∗} P′, we have

(1) P′ ⟶^{l} P_{1} and P′ ⟶^{l} P_{2} imply P_{1} ≡ P_{2}; (2) P′ ⟶^{l}

(l an output) implies P′ −̸→. FPC sorting. In the lifted-sum interpretation, all types are interpreted in G_{i} as trees (i.e. arenas with at most one initial sort), as can be easily verified. This extends to environments. Henceforth, we restrict attention to finitely branching arenas induced by closed FPC types. These we call FPC arenas. (We believe that all FPC types lie in this class — note that, for closed α, [[μT.T × α]] = 0.) Let A be an FPC arena. Since each branch of A as a tree is constructed according to the structure of a given FPC type, we can assign an ordering on the children nodes of each node of A, respecting the lexicographic ordering of tensor/sum composition (e.g. in A_{1} ⊕ A_{2}, the initial sort of A_{1} is smaller). Given this ordering, the enabling relation can now be written S ↦ S_{1}, …, S_{n}, where the sequence S_{1} … S_{n} gives all sorts enabled by S ordered as mentioned above. An FPC sorting is given by: (1) a family of pairwise disjoint countable sets of names F = {F_{(A,S)}} indexed by pairs (A, S) consisting of an FPC arena A and a sort S in A, and (2) a partial function F ⇀ F^{∗} following the just introduced enabling relation between sorts and their sequences. We write a :_{A} S, omitting the subindex when its clear from the context, to indicate that a is a name in F_{(A,S)}. Under an FPC sorting, we now have the set of well-sorted processes following the standard definition [24]. Note that, in a sorted process, if S ↦ S_{1}, …, S_{n} and a : S then the name a carries (if ever) a sequence of names of length n of sorts S_{1}, …, S_{n}.

Compilation. We fix an FPC sorting for the rest of the section. The compilation of FPC terms into Pict codes is given in Figure 4. For a given FPC term Γ ⊢ M : α, the compilation of M is parameterised by a sequence of pairwise distinct names, say w_{1} … w_{n}u, such that w_{i} : S_{i} for each i and u : S′, where S ↦ S_{1}, …, S_{n} for the initial sort S of [[Γ]] and S′ is the initial sort of [[α]]. In the figure, we assume that all mentioned names (including those in each vector) are pairwise distinct unless textually identical, and that, their usage follows the given FPC sorting, including the length of each vector of names. Note that Γ ≡ x_{1} : β_{1}, …, x_{k} : β_{k} does not imply n = k, since each β_{i} can itself be a nontrivial tensor. In this case, we may write ṽ_{1}ṽ_{2} … ṽ_{k} etc. for w̃, where each ṽ_{i} corresponds to β_{i} above. It is easy to check that the resulting processes are indeed well-sorted. Intuitively, the compilation can be considered as representing the behaviour of a strategy deprived of the initial Opponent signal. For example, when parameterised by w and v, the term x : α⇀ ⇀α ⊢ x : α⇀ ⇀α is mapped to \overline{v}[w]; which, in “strategy form”, becomes u(w).\overline{v}[w].

Correctness of compilation. Our aim in the rest of the section is to show that [[M]]w̃ ; v captures the interactive behaviour of ([M]), and, as a result, that the compilation is computationally adequate with respect to the operational semantics of FPC. For this purpose, we first introduce the notion of representation. Let σ : A ⇀ B be a V-strategy between non-zero finite non-lazy sums of FPC arenas, satisfying: all involved V-pointers use isomorphisms which respect the natural ordering underlying the FPC sorting. Note that all V-pointers involved in strategies resulting from our denotational semantics satisfy this condition. Now let s = S_{0} … S_{n−1} ∈ σ. Assume pairwise distinct names u_{k} : T_{k} (0 ≤ k ≤ m_{1}) and v_{k} : R_{k} (0 ≤ k ≤ m_{2})

[[Θ, Γ ⊢ Γ_{i}]] =^{def} π_{i}

[[Θ, Γ ⊢ inl(M) : α_{1} + α_{2}]] =^{def} [[Θ, Γ ⊢ M : α_{1}]]; ⨿_{1} [[Θ, Γ ⊢ inr(M) : α_{1} + α_{2}]] =^{def} [[Θ, Γ ⊢ M : α_{2}]]; ⨿_{2} [[Θ, Γ ⊢ case M ofinl(x_{1}).M_{1} orinr(x_{2}).M_{2} : α]]

=^{def} Δ; ([[Θ ⊢ Γ]] ⊗ [[Θ, Γ ⊢ M : α_{1} + α_{2}]]); δ;[[[Θ, ⟨Γ, x_{1} : α_{1}⟩ ⊢ M_{1} : α]], [[Θ, ⟨Γ, x_{2} : α_{2}⟩ ⊢ M_{2} : α]]] [[Θ, Γ ⊢ ⟨M_{1}, M_{2}⟩ : α_{1} × α_{2}]] =^{def} Δ; ([[Θ, Γ ⊢ M_{1} : α_{1}]] ⊗ [[Θ ⊢ Γ]]); ([[Θ ⊢ α_{1}]] ⊗ [[Θ, Γ ⊢ M_{2} : α_{2}]]) [[Θ, Γ ⊢ fst(M) : α_{1}]] =^{def} [[Θ, Γ ⊢ M : α_{1} × α_{2}]]; π_{1} [[Θ, Γ ⊢ snd(M) : α_{2}]] =^{def} [[Θ, Γ ⊢ M : α_{1} × α_{2}]]; π_{2}

[[Θ, Γ ⊢ λx.M : α_{1}⇀ ⇀α_{2}]] =^{def} pλ([[Θ, ⟨Γ, x : α_{1}⟩ ⊢ M : α_{2}]])

[[Θ, Γ ⊢ M(M_{1}) : α_{2}]] =^{def} Δ; ([[Θ, Γ ⊢ M : α_{1}⇀ ⇀α_{2}]] ⊗ [[Θ ⊢ Γ]]); ([[Θ ⊢ α_{1}⇀ ⇀α_{2}]] ⊗ [[Θ, Γ ⊢ M_{1} : α_{1}]]); ev [[Θ, Γ ⊢ intro(M) : μT.α]] =^{def} [[Θ, Γ ⊢ M : α[T ↦ μT.α]]] [[Θ, Γ ⊢ elim(M) : α[T ↦ μT.α]]] =^{def} [[Θ, Γ ⊢ M : μT.α]]

Figure 2. Interpretation of well-formed expressions

([Θ ⊢ τ_{1} + τ_{2}]) =^{def} ⟨([Θ ⊢ τ_{1}]), ([Θ ⊢ τ_{2}])⟩; ⊕

([Θ, Γ ⊢ inl(M) : τ_{1} + τ_{2}]) =^{def} ([Θ, Γ ⊢ M : τ_{1}]); ⨿′_{1} ([Θ, Γ ⊢ inr(M) : τ_{1} + τ_{2}]) =^{def} ([Θ, Γ ⊢ M : τ_{2}]); ⨿′_{2} ([Θ, Γ ⊢ case M ofinl(x_{1}).M_{1} orinr(x_{2}).M_{2} : τ])

=^{def} Δ; (([Θ ⊢ Γ]) ⊗ [[Θ, Γ ⊢ M : τ_{1} + τ_{2}]]); δ′; [([Θ, ⟨Γ, x_{1} : τ_{1}⟩ ⊢ M_{1} : τ]), ([Θ, ⟨Γ, x_{2} : τ_{2}⟩ ⊢ M_{2} : τ])] Figure 3. Lazy-sum interpretation

[[Γ ⊢ x_{i} : α_{i}]]_{v}^{x̃_{1}..x̃_{n}} =^{def} \overline{v}[x̃_{i}]

[[Γ ⊢ ⟨M_{1}, M_{2}⟩ : β_{1} × β_{2}]]w̃ ; v =^{def} ([[Γ ⊢ M_{1}]]w̃ ; c_{1} ; c_{1}(x̃_{1}).([[Γ ⊢ M_{2}]]w̃ ; c_{2} ; c_{2}(x̃_{2}).\overline{v}[x̃_{1}x̃_{2}])

[[Γ ⊢ inl(M) : α + β]]w̃ ; v =^{def} ([[Γ ⊢ M]]w̃ ; c ; c(x̃).\overline{v}(y)·!y(z_{1}z_{2}).\overline{z_{1}}[x̃])

[[Γ ⊢ inr(M) : α + β]]w̃ ; v =^{def} ([[Γ ⊢ M]]w̃ ; c ; c(x̃).\overline{v}(y)·!y(z_{1}z_{2}).\overline{z_{2}}[x̃])

[[Γ ⊢ case M of inl (x_{1}).M_{1} or inr (x_{2}).M_{2} : β]]w̃ ; v

=^{def} [[Γ ⊢ M]]w̃ ; c ; c(y).\overline{y}(z_{1}z_{2}) · (z_{1}(x̃_{1}).[[⟨Γ, x_{1} : β_{1}⟩ ⊢ M_{1}]]_{v}^{w̃x̃_{1}} | z_{2}(x̃_{2}).[[⟨Γ, x_{2} : β_{2}⟩ ⊢ M_{2}]]_{v}^{w̃x̃_{2}})

[[Γ ⊢ λx : α.M : α⇀ ⇀β]]w̃ ; v =^{def} \overline{v}(z)·!z(ỹc).[[⟨Γ, x : α⟩ ⊢ M]]_{c}^{w̃ỹ}

[[Γ ⊢ M_{1}(M_{2}) : β]]w̃ ; v =^{def} ([[Γ ⊢ M_{1}]]w̃ ; c_{1} ; c_{1}(y).([[Γ ⊢ M_{2}]]w̃ ; c_{2} ; c_{2}(z̃).\overline{y}[z̃v]))

[[Γ ⊢ intro(M) : μT.α]]w̃ ; v =^{def} [[Γ ⊢ M : α[T ↦ μT.α]]]w̃ ; v

[[Γ ⊢ elim(M) : α[T ↦ μT.α]]]w̃ ; v =^{def} [[Γ ⊢ M : μT.α]]w̃ ; v Figure 4. Direct Compilation

π_{i}_{v}^{u} =^{def} u(x̃_{1}..x̃_{n}).\overline{v}[x̃_{i}]  ⨿′_{i}_{v}^{u} =^{def} u(x̃).\overline{v}(y)·!y(z_{1}z_{2}).\overline{z}_{i}[x̃]
δ′_{v_{1}v_{2}}^{u} =^{def} u(w̃e).\overline{e}(c_{1}c_{2}).(c_{1}(x̃_{1}).\overline{v_{1}}[w̃x̃_{1}] | (c_{2}(x̃_{2}).\overline{v_{2}}[w̃x̃_{2}]))  ev_{v}^{u} =^{def} u(wx̃).\overline{w}[x̃v]

C[[Γ ⊢ x_{i} : α_{i}]]_{v}^{u} =^{def} π_{i}_{v}^{u}

C[[Γ ⊢ ⟨M_{1}, M_{2}⟩ : β_{1} × β_{2}]]_{v}^{u}

=^{def} u(w̃).((C[[Γ ⊢ M_{1}]]_{c_{1}}^{e_{1}}; \overline{e_{1}}[w̃]) ; c_{1}(x̃_{1}).((C[[Γ ⊢ M_{2}]]_{c_{2}}^{e_{2}}; \overline{e_{2}}[w̃]) ; c_{2}(x̃_{2}).\overline{v}[x̃_{1}x̃_{2}])

C[[Γ ⊢ inl(M) : α + β]]_{v}^{u} =^{def} C[[Γ ⊢ M]]_{c}^{u}; ⨿′_{1}_{v}^{c} C[[Γ ⊢ inr(M) : α + β]]_{v}^{u} =^{def} C[[Γ ⊢ M]]_{c}^{u}; ⨿′_{2}_{v}^{c} C[[Γ ⊢ case M of inl (x_{1}).M_{1} or inr (x_{2}).M_{2} : β]]_{v}^{u}

=^{def} C[[Γ ⊢ ⟨Γ|M⟩]]_{c}^{u}; δ′_{c_{1}c_{2}}^{c}; (C[[⟨Γ, x_{1} : β_{1}⟩ ⊢ M_{1}]]_{v}^{c_{1}}|C[[⟨Γ, x_{2} : β_{2}⟩ ⊢ M_{2}]]_{v}^{c_{2}})

C[[Γ ⊢ λx : α.M : α⇀ ⇀β]]_{v}^{u} =^{def} u(w̃).\overline{v}(z)·!z(ỹc).(C[[⟨Γ, x : α⟩ ⊢ M]]_{c}^{e}; \overline{e}[w̃ỹ])

C[[Γ ⊢ M_{1}(M_{2}) : β]]_{v}^{u} =^{def} C[[Γ ⊢ ⟨M_{1}, M_{2}⟩]]_{c}^{u}; ev_{v}^{c}

C[[Γ ⊢ intro(M) : μT.α]]_{v}^{u} =^{def} C[[Γ ⊢ M : α[T ↦ μT.α]]]_{v}^{u} C[[Γ ⊢ elim(M) : α[T ↦ μT.α]]]_{v}^{u} =^{def} C[[Γ ⊢ M : μT.α]]_{v}^{u}

Figure 5. Categorical Compilation where T_{0}, .., T_{m_{1}} and R_{0}, .., R_{m_{2}} are initial sorts of A and B, respectively. Then an instantiation of s w.r.t. ũ, ṽ is a sequence of non-τ labels of length n, say l_{0}l_{1} … l_{n−1}, such that: (1) sub(l_{i}) : S_{i} for 0 ≤ i ≤ n − 1; (2) If S_{i} = T_{k} (resp. S_{i} = R_{k}), sub(l_{i}) = u_{k} (resp. sub(l_{i}) = v_{k});

(3) If S_{i} is by Opponent (resp. Player) then l_{i} is input (resp. output); (4) If i ↷ j and S_{i} ↦ U_{1}, …, U_{m} such that S_{j} = U_{k}, then sub(l_{j}) = ob(l_{i}, k); (5) If i ⇒^{Ψ} j is a V-pointer in s and S_{i} ↦ U_{1}, …, U_{k}, …, U_{m} as well as S_{j} ↦ U′_{1}, …, U′_{k′}, …, U′_{m′} where U_{k} = source (Ψ) and U′_{k′} = target(Ψ), then ob(l_{i}, k) = ob(l_{j}, k′) and ob(l_{j}, j) occurs free in l_{j}; and (6) object names in the output labels occur free only in the case of (5). Instantiations are considered modulo α-equality. If s ∈ σ and t is an instantiation of s w.r.t. ũ and ṽ, then we say t is a play of σ instantiated at ũ and ṽ. The definition of representation follows.

Definition 5.2 (Representation) For σ : A ⇀ B as above, a process P represents σ : A ⇀ B w.r.t. ũ and ṽ, or simply represents σ, when there is a relation ≻ between the set of FPC-sorted strongly determinate processes and the set of plays of σ instantiated at ũ and ṽ such that:

(i) P ≻ ε, (ii) If P′ ≻ t, then (1) for an output l, tl is a play of σ

instantiated at ũ and ṽ iff P′ ⟹^{l}; and, for such l, P′ ⟹^{l} P′′ implies P′′ ≻ tl, and (2) for an input l, if tl is a play of σ instantiated at ũ and ṽ then P′ ⟹^{l}; and, for such l, P′ ⟹^{l} P′′ implies P′′ ≻ tl.

The key property of representation follows.

Lemma 5.3 If P (resp. Q) represents σ : A ⇀ B w.r.t. ã and b̃ (resp. τ : B ⇀ C w.r.t. b̃ and c̃), then P; Q represents σ; τ : A ⇀ C w.r.t. ã and c̃.

The proof uses an alternative, equivalent presentation of composition of V-strategies which precisely corresponds to interaction between representing processes.

We now wish to show that, for every closed FPC term M, the Pict code u(ε).[[M]]_{v}^{ε} and the term M have the same terminating behaviour. For that purpose we introduce an intermediate compilation whose construction is closer to the inductive definition of our denotational semantics while being bisimilar to the compilation in Figure 4. We list this intermediate compilation in Figure 5. This compilation is parameterised by two names, which belong to the respective initial sorts of the domain and codomain. In the case statement, the term ⟨Γ|M⟩ has the following inductive def-

inition: ⟨⟨⟩|M⟩ =^{def} M, and ⟨⟨Γ, x : α⟩|M⟩ =^{def} ⟨Γ|⟨x, M⟩⟩

where ⟨x, M⟩ denotes the standard pairing.

Proposition 5.4 For all FPC terms Γ ⊢ M : α,

(i) [[M]]x̃ ; v is strongly determinate.

(ii) u(x̃).[[M]]x̃ ; v ≈ C[[M]]_{v}^{u}.

(iii) C[[M]]_{v}^{u} represents ([M]) in G_{i}.

For (i), the case of application requires an analysis of IOmodes [28]. For (ii), we use simple algebraic transformations. For (iii) we proceed by induction using Lemma 5.3. Let M be a closed FPC term. Then, M ✓ iff ([M]) ↓,

by Theorem 5.1; that is, by (iii) above, iff C[[M]]_{v}^{u} ⟶^{u(ε)}⟹^{l} where l is an output with sub(l) = v. But this in turn is equivalent to [[M]]_{v}^{ε} ↓, by (i) and (ii). Thus we have the following result.

Theorem 5.5 (Computational adequacy) For all closed FPC terms M, we have that M ✓ iff [[M]]_{u}^{ε} ↓.

References

[1] S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for PCF. To appear, 1994.

[2] S. Abramsky and G. McCusker. Linearity, sharing and state: a fully abstract game semantics for idealized algol with active expressions. Electronic Notes in Theoretical Computer Science, 3, 1996.

[3] S. Abramsky and G. McCusker. Call-by-value games. In Proc. of CSL ’97, LNCS. Springer-Verlag, 1998. To appear.

[4] G. Berry and P.-L. Curien. Sequential algorithms on concrete data structures. Theoretical Computer Science, 20:265–322, 1982.

[5] G. Boudol. The π-calculus in direct style. In POPL ’97 Conf., pages 228–241, 1997.

[6] S. Brock and G. Ostheimer. Process semantics of graph reduction. In CONCUR ’95 Conf., volume 962 of LNCS, pages 471–485. Springer-Verlag, 1995.

[7] R. Cartwright, P.-L. Curien, and M. Felleisen. Fully abstract semantics for observably sequential languages. Information and Computation, 111(2):297– 401, 1994.

[8] A. Edalat and M. Smyth. I-categories as a framework for solving domain equations. Theoretical Computer Science, 115:77–106, 1993.

[9] M. Fiore. Axiomatic Domain Theory in Categories of Partial Maps. Distinguished Dissertations in Computer Science. Cambridge University Press, 1996.

[10] M. Fiore and G. Plotkin. An axiomatisation of computationally adequate domain-theoretic models of FPC. In 9^{th} LICS Conf., pages 92–102. Computer Society Press, 1994.

[11] P. Freyd. Algebraically complete categories. In Category Theory, volume 1488 of LNM, pages 131–156. Springer-Verlag, 1991.

[12] J.-Y. Girard. Geometry of interaction I: Interpretation of system F. In Logic Colloquium ’88. North Holland, 1989.

[13] C. Gunter. Semantics of Programming Languages: Structures and Techniques. The MIT Press, 1992.

[14] K. Honda. Two bisimilarities in ν-calculus. Technical Report 92-002, Department of Computer Science, Keio University, 1992.

[15] K. Honda and N. Yoshida. Game-theoretic analysis of call-by-value computation (full version). Available by ftp from ftp.dcs.ed.ac.uk/export/kohei/cbvfull.ps.gz (An extended abstract appeared in Proc. of ICALP ’97, volume 1256 of lncs, pages 225–236. Springer-Verlag, 1997.).

[16] H. Huwig and A. Poigné. A note on inconsistencies caused by fixpoints in a cartesian closed category. Theoretical Computer Science, 73:101–112, 1990.

[17] M. Hyland and L. Ong. On full abstraction for PCF: I, II and III. To appear, 1994.

[18] M. Hyland and L. Ong. Pi-calculus, dialogue games and PCF. In FPCA ’95 Conf., pages 96–107, 1995.

[19] K. Larsen and G. Winskel. Using information systems to solve recursive domain equations. Information and Computation, 91(2):232–258, 1991.

[20] F. Lawvere. Diagonal arguments and cartesian closed categories. In Category Theory, Homology Theory and their Applications II, volume 92 of LNM. Springer-Verlag, 1969.

[21] G. Longo and E. Moggi. Cartesian closed categories of enumerations for effective type-structures. In Symposium on Semantics of Data Types, volume 173 of LNCS. Springer-Verlag, 1984.

[22] G. McCusker. Games and Full Abstraction for a Functional Metalanguage with Recursive Types. PhD thesis, University of London, 1996.

[23] R. Milner. Functions as processes. Mathematical Structures in Computer Science, 2(2):119–146, 1992.

[24] R. Milner. Polyadic π-calculus: A tutorial. In Proceedings of the International Summer School in Marktoberdorf, 1992.

[25] R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, (Parts I and II). Information and Computation, 100:1–77, 1992.

[26] R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. MIT Press, 1990.

[27] E. Moggi. Categories of partial morphisms and the partial lambda-calculus. In Proceedings of the Workshop on Category Theory and Computer Programming, volume 240 of LNCS, pages 242–251. Springer-Verlag, 1986.

[28] B. Pierce and D. Sangiorgi. Typing and subtyping for mobile processes. In 8^{th} LICS Conf., pages 187–215. Computer Society Press, 1993.

[29] B. C. Pierce and D. N. Turner. Pict: A programming language based on the pi-calculus. To appear in Proof, Language and Interaction: Essays in Honour of Robin Milner, The MIT Press, 1998.

[30] G. Plotkin. Denotational semantics with partial functions. Lecture at C.S.L.I. Summer School, 1985.

[31] J. Power and E. Robinson. Premonoidal categories and notions of computation. Mathematical Structures in Computer Science, 7(5):453–468, 1997.

[32] J. Power and G. Rosolini. Fixpoint operators for domain equations. To appear, 1996.

[33] J. Riecke and A. Sandholm. Relational account of call-by-value sequentiality. In 12^{th} LICS Conf., pages 258–267. Computer Society Press, 1997.

[34] E. Robinson and G. Rosolini. Categories of partial maps. Information and Computation, 79:95–130, 1988.

[35] D. Sangiorgi. π-calculus, internal mobility, and agent-passing calculi. Theoretical Computer Science, 167(2):235–271, 1996.

[36] M. Smyth and G. Plotkin. The category-theoretic solution of recursive domain equations. SIAM Journal of Computing, 11(4):761–783, 1982.

[37] D. Walker. Objects in the pi-calculus. Information and Computation, 116(2):253–271, 1995.

[38] G. Winskel. The Formal Semantics of Programming Languages: An Introduction. The MIT Press, 1993.