Games and Definability for System F

Dominic J.D. Hughes

Oxford University Computing Laboratory

Wolfson Building

Parks Road Oxford OX1 3QD United Kingdom^{∗}

dhughes@comlab.ox.ac.uk

Abstract

We present a game-theoretic model of the polymorphic λ-calculus, system F, as a fibred category. Every morphism σ of the model defines an η-expanded, β-normal form σ̂ of system F whose interpretation is σ. Thus the model gives a precise, non-syntactic account of the calculus.

1 Introduction

Polymorphism is of fundamental interest to computer scientists. Consider the function map in the setting of a typed functional programming language which takes a function f : X → Y and a list a_{1}a_{2} … a_{n} of elements each of type X and returns the list f(a_{1})f(a_{2}) … f(a_{n}) of elements each of type Y. Since the algorithm is independent of the actual data types X and Y, it would be useful to have the flexibility of taking X and Y as type variables, to be instantiated whenever map is called. For example, we might write map(Nat)(Bool) to mean “the map function as defined above, with X := Nat and Y := Bool”, thus extending the notion of application from the usual form term(term) to the form term(type). The function map is said to be polymorphic, and is assigned the type

T = ΠX. ΠY. ((X → Y) → (listX → listY)).

The notation is designed according to the intuition that this type is a “product” indexed by X and Y ranging over all possible types.

A key tool for the analysis of polymorphism is system F [Gir89], which is the simply-typed λ-calculus extended by quantification over type variables, as above. Models of system F do not come about easily. The impredicative nature of the definition of T, that T itself is in the range of X and Y, raises problems for the semanticist. The two standard classes of models are the P ER models [Cro93], and the domain models [CGW89].

Recent advances in our understanding of the nature of sequential computation were made through the paradigm of modelling term(term) application intensionally, by interaction between function and argument. Interaction occurs by the repeated exchange of basic data “tokens” (for example natural numbers, booleans, and requests for data). Thus higher-order functions do not necessarily have instant access to the full information of the whole graph of an argument function f: information can be obtained only by testing the input-output behaviour of f, as a “black box”. This approach forms the basis of game semantics, and has led to many good results, for example the solution of the long-standing full abstraction problem for PCF [AJM94, HO94, Nic94].

In this paper we present a games model for system F. A games model for polymorphism was presented in [Abr95]. The new concept in our approach is that we model not only term(term) application intensionally, but also term(type) application; interaction occurs not only through the communication of basic data tokens, but also by the direct exchange of types themselves. A type is modelled as a first-order polymorphic arena, the analogue for system F of the computational arena of Hyland and Ong for PCF [HO94]^{1}. A second-order polymorphic arena is an arena which has first-order polymorphic arenas as moves. The HO notion of a justified sequence of moves is enriched to a structure which we call a located sequence. Instead of the whole justified sequence being inside one particular arena, each move is located in a different arena. We use a special control move ⋆, called the initialising move, to open a new first-order thread of play inside one of the previous second-order moves of the sequence.

∗This is a slightly revised version of a paper appearing in IEEE 12th Symposium on Logic in Computer Science, Warsaw, June 1997.

Our main result is that every strategy σ of the games model 𝔽 defines an η-expanded, β-normal form σ̂, whose interpretation is σ. This provides us with a very precise non-syntactic characterisation of system F.

2 Syntax of system F

We fix the notation of system F. Types are generated by

T ::= X | unit | T ×T | T → T | ΠX.T

where X ranges over a countably infinite set of type variables. Raw terms are generated by

\begin{aligned}s & ::= & x | ⟨⟩ | ⟨s, s⟩ | F st(s) | Snd(s) \\ & & | λx^{T} .s | ss | ΛX.s | sT \end{aligned}

where x is any term variable, and T is any type. See [Cro93] for further details of the language.

3 Games

We consider alternating, two-player games between P (think of Player, Program, or System) and O (Opponent, User, or Environment) in which P starts. The following diagram represents a trace or history of events in a game:

[figure: ∘; •; ∘; •; ∘; •; ∘; •; a; c; c; d; b; a; c; d]

The labels a, b, c and d are actions names, just like the actions of a labelled transition system. Each node signifies an occurrence of an action, and time runs from left to right. A hollow node ∘ indicates that an action was performed by P, and a solid node • indicates that an action was performed by O. Arcs pointing backwards in time indicate a causal relationship between actions, for example P’s action c occurring in seventh position was justified by O’s action d occurring in fourth position.

We formalise these concepts in the definitions below. A justified sequence of events s on the set of actions Act is a structure ⟨ E_{s}, <_{s} , just_{s}, pl_{s}, act_{s} ⟩ consisting of:

• Events. A finite set E_{s} = {x, y, z, …} of events, pictured as nodes in the diagram above.

• Temporal relation. A strict linear ordering <_{s} on events. Denote the corresponding successor partial function by succ_{s} : E_{s} ⇀ E_{s}.

• Justification pointer. A partial function just_{s} : E_{s} ⇀ E_{s}. Define the relation y is justified by x, written x↶_{s}y, if and only if just_{s}(y) = x.

• Association with players. A total function pl_{s} : E_{s} → {O, P} associating each event with a particular player.

• Labelling with actions. A total function act_{s} : E_{s} → Act, associating an action to each event.

The structure is required to satisfy the following conditions:

1. J Causality. Justification points backwards in time: x↶_{s}y only if x <_{s} y.

1In future we abbreviate this reference to “HO”.

2. J P goes first. If x is the first event in s then pl_{s}(x) = P.

3. J Alternating play. The players take turns, and justification has to point to an event associated with the opposite player:

(a) If succ_{s}(x) = y, then pl_{s}(x) ≠ pl_{s}(y).

(b) If x↶_{s}y, then pl_{s}(x) ≠ pl_{s}(y).

Two justified sequences of events s and t are isomorphic if there exists a bijection θ : E_{s} → E_{t} of the underlying sets of events that preserves and reflects structure. We say s is a subsequence of t if there exists an injection i : E_{s} → E_{t} that preserves and reflects structure, and s is a prefix of t if in addition the image of E_{s} is an initial segment of the events of t. The empty justified sequence of events ε is defined by E_{ε} = ∅. A justified sequence is an isomorphism class of justified sequences of events.

A move is the information content of the “difference” between two consecutive justified sequences, i.e. a pair (a, i) where a is an action and i is either an odd natural number indicating how far back to justify, or i = 0 meaning no pointer. In this way any justified sequence can be encoded as a string of moves, (a, i)(b, j)(c, k) … ∈ (Act×ℕ)^{∗}. This alternative representation is convenient for manipulations of justified sequences that are “local”, such as in the definition of strategy below, where we are concerned only with the very end of a justified sequence. The original notation is useful for “global” operations such as the deletion of events from a justified sequence.

Notation We take a, b, … to range over actions, x, y, … to range over events, s, t, … to range over justified sequences, and m, n, … to range over moves. Furthermore we write x^{a} to indicate that the event x is labelled with the action a. We will identify a justified sequence s with its encoding as a string of moves. Concatenation of moves and of strings of moves is represented by juxtaposition. If it is clear from the context that an action a occurs at a particular event x, for example in a string of moves smn where m = (a, i), we will often abuse notation and simply write the action a or the move m to mean the event x.

3.1 Games, strategies, and arenas

A game is a specification of certain allowable strings of moves. For example, the game of chess, with moves such as “Knight f3−g5”, can be specified abstractly as the set of all strings of moves that follow the rules. Formally, a game G is a pair ⟨ Act_{G}, L_{G} ⟩ consisting of a set of actions Act_{G}, together with a non-empty, prefix-closed set L_{G} of justified sequences on Act_{G}, called the legal sequences of G.

A strategy on a game is a rule telling P what to do given any reachable^{2} legal sequence in which it is his turn to play next. It is best thought of as a function that maps a reachable sequence s to a move m_{s}, such that sm_{s} is (the move-encoding of) a legal sequence.

A partial strategy σ on a game G is a nonempty, prefix-closed set of legal sequences σ ⊆ L_{G} satisfying

• P-determinism. Whenever sm, sn ∈ σ with pl_{sm}(m) = pl_{sn}(n) = P, then m = n.

• O-contingent completeness. If sm ∈ L_{G} with pl_{sm}(m) = O and s ∈ σ, then sm ∈ σ.

A winning sequence is a legal sequence which is prefix-maximal in L_{G} and in which P performed the last action, and a winning strategy is a partial strategy that is the prefix-closure of a set of winning sequences.

One way to specify the set of legal sequences of a game is to enforce a particular causal relationship between the actions. An arena is a pair ⟨ Act_{A}, ⊢_{A} ⟩ where Act_{A} is a set of actions and ⊢_{A}, the enabling relation of A, is a binary relation between Act + {⋆} (“+” denotes disjoint union) and Act such that for each a ∈ Act there exists a unique finite path ⋆ ⊢ … ⊢ a.

[figure: ⋆; a; b; c; d; e; f; g; h; i; j]

2The domain of definition need only be sequences reached according to the previous play dictated by the strategy.

The direct descendents of the initialising action ⋆ are called initial actions, which in the graph above are the actions a, b and c. An A-sequence is a justified sequence s on the set of actions Act + {⋆} such that

1. Justification respects enabling: x^{a}↶_{s}y^{b} only if a ⊢_{A} b.

2. Every non-initialising event is justified: for any event y^{b} with b ≠ ⋆ there exists an event x such that x↶_{s}y^{b}.

Any non-empty A-sequence necessarily begins with an unjustified initialising action by P. An A-game is a game ⟨ Act_{A} + {⋆}, L_{G} ⟩ for which L_{G} consists only of A-sequences.

The next section highlights how the structures defined so far relate to previous work on game semantics, and can skipped by a reader steering a direct course for system F.

3.2 Relationship with HO-games

A justified sequence s is a P-view if justification by O is only ever to the immediately preceding P-event. Define the P-view game on an arena A to be the maximal A-game whose set of legal sequences consists only of P-views, and in which there is at most one occurrence of the initialising action ⋆. Define a starting strategy to be a partial strategy in which P successfully performs his first ⋆ action, i.e. which is not equal to the singleton set consisting of the empty sequence.

Proposition 1 (HO-correspondence.) Starting strategies on P-view games correspond to innocent strategies on answer-free HO-arenas.

The proof is trivial: actions correspond to questions, and given a legal sequence on a P-view game, delete the P-action ⋆ from the front in order to obtain an HO-P-view.

4 Second-order structure

A universe of actions is a set U such that U + U ↪ U and U × U ↪ U. Let R^{∗} denote the reflexive, transitive closure of a binary relation R, and let ℕ^{+} = ℕ \ {0}. A polymorphic arena A on the universe U is a quadruple ⟨ Act_{A}, ⊢_{A} , ar_{A}, ref_{A} ⟩ consisting of

• An arena ⟨ Act_{A}, ⊢_{A} ⟩ such that Act_{A} ⊆ U.

• A function ar_{A} : Act_{A} → ℕ assigning an arity to each action a. By convention ar_{A}(⋆) = ∞.

• A function ref_{A} : Act_{A} → (Act_{A} + {⋆})×ℕ^{+} assigning a reference further up the ⊢_{A} -tree: if ref_{A}(a) = (b, i) then i ≤ ar_{A}(b) and b ⊢_{A}^{∗}a. We write b_{i} for (b, i).

A selection of polymorphic arenas are shown in Figure 1. If non-zero, the arity of an action is placed to its left; the reference is placed in brackets to the right. We take A, B, C, … to range over polymorphic arenas, and the set of polymorphic arenas on U is denoted ℙ𝔸(U). Take the judgement n ⊢ A to mean that i ≤ n for each reference ⋆_{i} of A, in which case we say A is in context n. (The overloading of the symbol ⊢ should not cause any confusion.)

A second-order polymorphic arena A over the universe U is a polymorphic arena on the universe ℙ𝔸(U). We take A, B, C … to range over second-order polymorphic arenas, and the set ℙ𝔸(ℙ𝔸(U)) of second-order polymorphic arenas over U will be abbreviated to ℙ𝔸^{⊭}(U).

[figure: A; ⋆; A; B; C; D; E; F; G; H; I; J]

A polymorphic arena A ∈ ℙ𝔸(U) will be called a 1-arena, and its actions a ∈ U called 1-actions. A second-order polymorphic arena A ∈ ℙ𝔸^{⊭}(U) will be called a 2-arena, and its actions A ∈ ℙ𝔸(U) called 2-actions. Thus 2-actions are 1arenas. By convention ⋆ is both a 1-action and a 2-action.

4.1 Located sequences

A (second-order) located sequence s in a universe U of actions is a structure ⟨ E_{s}, <_{s} , just_{s}, pl_{s}, act_{s}, loc_{s} ⟩ consisting of

• A justified sequence on the set of actions U + ℙ𝔸(U) + {⋆}. In other words act_{s} assigns either a 1-action or a 2-action to each event.

• A function loc_{s} : E_{s} → ℙ𝔸(U) + ℙ𝔸^{⊭}(U) setting the location of each event.

The structure is required to satisfy the following conditions:

1. L Events are well-located: for all events x^{α} of s, we have α ∈ Act_{loc_{s}(x^{α})} + {⋆}.

2. L Justification respects location: if x↶_{s}y then loc_{s}(x) = loc_{s}(y).

3. L Justification respects enabling locally: if x↶_{s}y then x ⊢_{loc_{s}(x)} y.

4. L Demands for the other player to play an initial move on a new arena are satisfied uniquely and immediately: if act_{s}(x) = ⋆ then x↶_{s}y if and only if succ_{s}(x) = y.

Define x ∈ E_{s} to be a 1-event or a 2-event according as the location of x is a 1-arena or a 2-arena.

A typical located sequence is depicted below.

[figure: ∘; •; ∘; •; ∘; •; ∘; •; ∘; •; ⋆; A; E; ⋆; a; I; ⋆; a; ⋆; I; A; A; A; A; A; A; E; E; B; B]

The first action is by P, initialising the 2-arena A which was pictured above. This forces O to play an initial action in A, and she chooses the 2-action A, a 1-arena. P continues inside A by responding to A with the 1-arena E. Now O initialises the 1-arena A, which occurred earlier as a 2-action in the sequence (the restriction to a previous 2-action is not a consequence of the conditions above, but will be required later). P obliges with an initial 1-action a inside A. Justifying back to the original thread of play inside the 2-arena A, O continues with the 2-action I. Now P forces O to play an initial 1-action in E by locating the initialising move ⋆ in E, a previous 2-action in the sequence. And so on. Note that the 1-action a occurs both as a P-action and as an O-action, and located inside two different arenas.

We end this section with a relationship between the enabling structure of a 1-arena and the justification structure of a located sequence.

Lemma 1 Let s be a located sequence. Suppose x^{a} is a 1-event of s located in the 1-arena A, and that c ⊢_{A}^{∗}a. Then there exists a unique 1-event z^{c} of s such that z^{c}↶_{s}^{∗}x^{a}.

[figure: z; …; •; …; ∘; …; •; …; x; c; ⊢_{A}; a′′′; ⊢_{A}; a′′; ⊢_{A}; a′; ⊢_{A}; a; A; A; A; A; A]

Proof: The existence and uniqueness of z^{c} comes from conditions L1-3 and the fact that the enabling relation forms a tree. □

5 Games for system F

We shall require only one particular 2-arena, a “flat” 2-arena with actions the set of all polymorphic arenas. We denote this 2-arena by K, for “Kind”, as its elements are “types”:

[figure: ⋆; …; A_{1}; A_{2}; A_{3}; …]

Whenever a player performs a 1-event x^{a} with arity n (i.e. the arity of a is n inside the location 1-arena of x) it will be followed by 2n actions located in K. Because of condition L4 and the fact that K is flat, this means we are forced to “import” n new 1-arenas which may become initialised in the future:

[figure: …; x; ∘; •; ∘; •; …; ∘; •; y; …; a; ⋆; A_{1}; ⋆; A_{2}; …; ⋆; A_{n}; b; A; K; K; K; K; …; K; K; B]

We will be considering only P-views as the projection used later for interaction is quite complex. Furthermore it is easier to extract definability from a standard notion of strategy on a P-view rather than the corresponding notion of a “second-order” innocent strategy on the total view (compare with Proposition 1). The component additional to HO-projection is that the collapse to a P-view involves the uniformity or typeindependence associated with polymorphism: P has to proceed without the knowledge of which particular 1-arenas A were imported by O as 2-events located in K. In going to the P-view we package all 2-actions A, B, C, … by O into a special symbol ?, indicating a parcel whose contents shall remain forever unknown to P. For example in the P-view the actions of the sequence displayed above would become a ⋆? ⋆? … ⋆? b. Secondly the fact that in the full view of the history of interaction these 2-actions may become initialised is also not visible in the P-view. Intuitively this is uniformity again: if we cannot see the 1-arena A hidden inside the parcel ?, we certainly cannot observe play inside A.

In system F there is a dependency of first-order entities (terms) on second-order entities (types). In a located sequence the dependency is achieved via a pointer from 1-events to previous 2-events, regulating the way in which new locations become initialised during the game.

Finally, P is constrained by a “copy-cat” condition, related to the notion of a copy-cat strategy, which is a standard concept in game semantics. The intuition is that during the composition (interaction) of strategies, moves will be played by P (unknowingly) inside the parcels of O. Since P is unaware of the contents of the ?-parcels, the only safe way of achieving this is by playing uniformly, copying moves between different threads of play in the same parcel. As soon as a parcel is “instantiated” to an arena B (corresponding to the substitution of a type B̂ for a type variable — see section 6), the copy-cat condition becomes “instantiated” to a copy-cat strategy between occurences of B.

5.1 Conditions on located sequences

We specify eight conditions on a located sequence s that will be required in order to model system F. First adjoin the symbol ? to the set of 1-arenas ℙ𝔸(U). Let K = ⟨ Act_{A}, ⊢_{A} , ar_{A}, ref_{A} ⟩ be the 2-arena given by Act_{K} = ℙ𝔸(U), A ⊢_{K} B if and only if A = ⋆ and B ∈ ℙ𝔸(U), ar_{K}(A) = 1, and ref_{K}(A) = (A, 1). (Arity and reference are in fact arbitrary as this structure on K is never used.)

1. F The only 2-arena is K. Whenever loc_{s}(x) ∈ ℙ𝔸^{⊭}(U), loc_{s}(x) = K.

2. F Importation of new 1-arenas. Every noninitialising 1-event x^{a} is followed immediately by 2n 2-events, where n is the arity of a (ar_{loc_{s}(x^{a})}(a)), and then by a 1-event y^{b}. (Unless s terminates beforehand.) See the diagram above.

3. F First-order P-view. O’s pointers do not skip over any of her own actions apart from initialisations: if x↶_{s}y and pl_{s}(y) = O, then whenever x <_{s} z^{α} <_{s} y with pl_{s}(z^{α}) = O, α = ⋆.

4. F Second-order P-view. For any 2-event x^{A}, A = ? if and only if pl_{s}(x^{A}) = O. For any 1-event x^{a}, loc_{s}(x^{a}) ≠ ?.

5. F Contexts. Let n be the number of occurrences of ? preceding the 2-event x^{A}, where A ≠ ⋆ and A ≠ ?. Then n ⊢ A. Let m be the number of occurrences of ? preceding the first 1-event x^{⋆} of s, and let A be the location of x^{⋆}. Then m ⊢_{s} A.

6. F Locations. Let A be the location of the first 1-event x^{⋆} of s. Then every 1-event of s is located either in A or in the 2-action associated with an earlier 2-event.

The following is the formalisation of the dependency of 1-events on 2-events as motivated in the informal discussion. Let x^{a} be a 1-event of s located inside a 1-arena A, and suppose it is not the last 1-event of s. Let c_{i} = ref_{A}(a), the reference of the action a inside A.

1. If c ≠ ⋆ then let z^{c} be as defined by Lemma 1, and let ẑ^{A_{i}} be the (2i)^{th} 2-event after z^{c} in s. (By condition F 2 and the fact that x^{a} is not the last 1-event, s is of sufficient length for ẑ^{A_{i}} to exist.)

2. If c = ⋆ then let the 2-event w^{?} be the i^{th} occurrence of O’s 2-action ? in s. (By conditions F 5 and F 6, s has at least i occurrences of ?.)

Define the 2-reference of x^{a} in s by

ref_{s}^{2}(x^{a}) = \{ \begin{matrix}ẑ^{A_{i}} & if c ≠ ⋆, \\ w^{?} & if c = ⋆. \end{matrix}

To understand case 1, insert the following segment in place of z in the diagram following Lemma 1:

[figure: z; •; ∘; …; ẑ; …; •; ∘; c; ⋆; A_{1}; …; A_{i}; …; ⋆; A_{n}; A; K; K; K; K; K]

Note that A_{i} = ? if the O and P nodes are the other way round.

7. F Initialisation of locations. Let x^{a} be the most recent 1-event before the 1-event y^{b}, and let x̃^{B} = ref_{s}^{2}(x^{a}), the 2-reference of x^{a}. If B ≠ ? then b = ⋆ and loc_{s}(y^{b}) = B. If B = ? then b ≠ ⋆ (consequently y^{b} is a justified event in one of the old locations).

[figure: …; x̃; …; x; ∘; •; …; ∘; •; y; …; B; a; ⋆; A_{1}; …; ⋆; A_{n}; ⋆; K; A; K; K; …; K; K; B]

8. F Copy-cat. Whenever P makes a “hidden” 2-reference it must be the same as the most recent “hidden” 2-reference made by O. Suppose x^{a} is a non-initialising 1-event associated with P, and act_{s}(ref_{s}^{2}(x^{a})) = ?. Let z^{c} be the most recent 1-event before x^{a} such that act_{s}(ref_{s}^{2}(z^{c})) = ?. Then ref_{s}^{2}(x^{a}) = ref_{s}^{2}(z^{a}).

5.2 The game associated with a 1-arena in context

Given a 1-arena in context n ⊢ A, let start(A, n) be the located sequence consisting of 2n actions located in K followed by the initialisation of A:

[figure: ∘; •; ∘; •; …; ∘; •; ∘; ⋆; ?; ⋆; ?; …; ⋆; ?; ⋆; K; K; K; K; …; K; K; A]

Let L_{A,n} be the set of located sequences in U satisfying conditions F 1-8 above that are prefixes of or are prefixed by start(A, n). Define \underline{L}_{A,n} to be the set of justified sequences on U + ℙ𝔸(U) + {⋆} obtained by forgetting location structure (in general a non-injective operation).

Lemma 2 \underline{L}_{A,n} ≅ L_{A,n}

Proof: Whenever a justified move is made the location is determined by L2, and whenever an initialising move is made, the location is determined by F 7. □

Thus by identifying L_{A,n} with \underline{L}_{A,n} we are able to define the game G(A, n) associated with n ⊢ A to be ⟨ U + ℙ𝔸(U) + {⋆}, L_{A,n} ⟩, within the scope of the definition of section 3.1.

5.3 Examples

We examine some play on the 1-arenas depicted in Figure 1 and consider the winning strategies available on each. Below are the system F encodings of the interpreted types:

Emp = ΠX. X,
Sgl = ΠX. X → X,
Bool = ΠX. X → X → X,
Nat = ΠX. X → (X → X) → X.

The game G([[ unit]], 0). The only possible action is the initialisation of the game by P. Thus there is a unique winning strategy.

The game G([[ Emp ]], 0). This time O has the action a to continue with after the initialisation. Since the arity of a is 1, by condition F 2 there must follow two actions inside K. Since P cannot respond after this there are no winning strategies. (F 7 forces him to play a justified move: he cannot justify from a because there is no action below a in the tree).

The game G([[ Sgl ]], 0). The first four moves are as for [[ Emp ]]. This time P can justify back to the original thread of play inside [[ Sgl ]], playing c. The game is over, as there are no more actions beneath c in the tree and F 7 forces O to play a justified move. Thus there is exactly one total strategy for P. The copy-cat condition F 8 is satisfied as the 2-reference of P’s action c is the

[figure: \begin{aligned}& & & ⋆ \\ [[ & unit & ]] \end{aligned}; \begin{aligned}& ⋆ \\ ^{[[ Emp ]]} & 1a(a_{1}) \end{aligned}; ^{[[ Sgl ]]}  ⋆ ; 1a(a_{1}) ; c(a_{1}); ^{[[ Bool ]]}; ⋆; 1b(b_{1}); t(b_{1}); f(b_{1}); ^{[[ Nat ]]}; ⋆; 1n(n_{1}); z(n_{1}); s(n_{1}); m(n_{1}); [[ Bool → Bool ]]; ⋆; 1b′(b′_{1}); t′(b′_{1}); t′(b′_{1}); 1b(b_{1}); t(b_{1}); f(b_{1}); \begin{aligned}& ⋆ \\ [[ X_{1} ]] & a(⋆_{1}) \end{aligned}]

G([[ unit ]], 0) :  \begin{aligned}& ∘ \\ & ⋆ \\ [[ & unit & ]] \end{aligned}

G([[ Emp ]], 0) :  [figure: ∘; •; ∘; •; ⋆; a; ⋆; ?; [[ Emp ]]; [[ Emp ]]; K; K]

G([[ Sgl ]], 0) :  [figure: ∘; •; ∘; •; ∘; ⋆; a; ⋆; ?; c; [[ Sgl ]]; [[ Sgl ]]; K; K; [[ Sgl ]]]

G([[ Bool ]], 0) :  [figure: ∘; •; ∘; •; ∘; ⋆; b; ⋆; ?; χ; ^{[[ Bool ]]}; ^{[[ Bool ]]}; K; K; ^{[[ Bool ]]}]

G([[ Nat ]], 0) :  [figure: ∘; •; ∘; •; ∘; •; ∘; •; ∘; ⋆; n; ⋆; ?; s; m; s; m; z; N; N; K; K; N; N; N; N; N]

Figure 1. A selection of 1-arenas and located sequences.

fourth event, the same 2-reference as O’s (most recent and only) 1-action a.

The game G([[ Bool ]], 0). This game is just like G([[ Sgl ]], 0) but for the fact that P now has the choice of the winning action as either χ = t or χ = f, so there are two total strategies. Think of b as a request for boolean data by O, and t or f as the reply of true or false. These two winning strategies are the interpretation of the terms

tt = ΛX.λt^{X}.λf^{X}.t,
ff = ΛX.λt^{X}.λf^{X}.f,

which are the system F encodings of true and false.

The game G([[ Nat ]], 0). Displayed is the winning position of the strategy interpreting the term ΛX. λz^{X}.λs^{X→X}.ssz, which is the encoding of the natural number 2. We abbreviate N = [[ Nat ]]. Think of the action n as a request for a number by O, z as zero by P, s as demand for output from the successor function by P, and m as a request for input by O to the successor function.

The game G([[ Bool → Bool ]], 0). A type quantifier occurs on the left of an arrow in the type Bool → Bool, and so we finally witness the full second-order machinery of “types as moves”. We consider the interpretation of one particular system F encoding of the not function,

not = λb^{Bool}.bBoolfftt.

Figure 2 shows one of its four winning positions on G([[ Bool → Bool ]], 0). We abbreviate B = [[ Bool ]], B^{B} = [[ Bool → Bool ]], and X = [[ X_{1} ]]. The corresponding sequence of regulatory conditions is: start(B^{B}, 0), L4, F 2, F 2 and L4, P choice of b, F 2, F 2 and L4 and P choice of importing the arena B, F 7, L4, F 2, F 2 and L4 and P choice of importing X, F 7, L4, O choice of t inside B^{B}, F 7, L4, F 2, F 2 and L4, P choice of f inside B.

6 Structure on ℙ𝔸(U)

We define the product A × B, function space A⇒B, universal quantification ∀_{n}(A), and substitution of 1-arenas, and an equivalence of 1-arenas “up to renaming of actions”,

Product. A × B is obtained by laying the ⊢-trees side by side and then identifying the two copies of ⋆:

Act_{A×B} = Act_{A} + Act_{B},
a ⊢_{A×B} b ⟺ a ⊢_{A} b or a ⊢_{B} b,
ar_{A×B} = [ar_{A}, ar_{B}],
ref_{A×B} = [ref_{A}, ref_{B}],

where for functions f : P ⟶ R and g : Q ⟶ R, [f, g] : P +Q ⟶ R is defined on x ∈ P +Q as f(x) or g(x) according as x ∈ P or x ∈ Q respectively. Note that the range of a includes ⋆.

Function space. Morally A ⇒ B is obtained by identifying the initial actions of B with the initialising action of A, in other words allowing B to use A as a resource:

Act_{A⇒B} = Act_{A} + Act_{B},
a ⊢_{A⇒B} b ⟺ (a ≠ ⋆ and a ⊢_{A} b) or a ⊢_{B} b
or (⋆ ⊢_{A} b and ⋆ ⊢_{B} a),
ar_{A⇒B} = [ar_{A}, ar_{B}],
ref_{A⇒B} = [ref_{A}, ref_{B}],

but since this labelled graph is not a tree, we make a separate copy of A underneath each of the initial actions of B. Thus we change Act_{A⇒B} to be Act_{A}×I + Act_{B}, where I is the set of initial actions of B, and duplicate the enabling and labelling structure accordingly. See HO for a similar construction.

Universal quantification. Given n ≥ 0 and n+1 ⊢ A the 1-arena n ⊢ ∀_{n}(A) is obtained by incrementing the arity of each initial vertex of A to “create a new hole”, and then “binding” every occurrence of the reference ⋆_{n+1}. For a ∈ Act_{A} let ã be the unique initial action lying on the path from ⋆ to a, and define m_{a} = ar_{A}(ã) + 1.

Act_{∀_{n}(A)} = Act_{A},
a ⊢_{∀_{n}(A)} b ⟺ a ⊢_{A} b,
ar_{∀_{n}(A)}(a) = \{ \begin{matrix}ar_{A}(a) + 1, & when ⋆ ⊢_{A} a \\ ar_{A}(a), & otherwise \end{matrix}
ref_{∀_{n}(A)}(a) = \{ \begin{matrix}(ã, m_{a}), & if ref_{A}(a) = ⋆_{n+1} \\ ref_{A}(a), & otherwise. \end{matrix}

As an example, [[ Bool ]] = ∀_{0}(A) where A is the 1-arena:

[figure: ∘; •; ∘; •; ∘; •; ∘; •; ∘; •; ∘; •; ∘; •; ∘; •; ∘; •; ∘; ⋆; b′; ⋆; ?; b; ⋆; B; ⋆; b; ⋆; X; ⋆; a; t; ⋆; b; ⋆; ?; f; B^{B}; B^{B}; K; K; B^{B}; K; K; B; B; K; K; X; X; B^{B}; B; B; K; K; B]

Figure 2. One of the four winning positions of [[ not ]] on G([[ Bool → Bool ]], 0).

[figure: ⋆; b(⋆_{1}); t(⋆_{1}); f(⋆_{1})]

Equivalence. Write A ∼ B if there exists a bijection θ : Act_{A} → Act_{B} that preserves and reflects structure, an equivalence relation respected by the previous three constructions.

Substitution. We define substitution of 1-arenas for references ⋆_{i} of 1-arenas. It is easiest just to poach the definition of substitution from the type syntax:

Lemma 3 Every system F type in context [X_{1}, X_{2}, …, X_{n}] ⊢ T has an interpretation as a finite 1-arena in context n ⊢ [[ T ]]. Conversely any finite 1-arena in context n ⊢ A defines a type in context [X_{1}, X_{2}, …, X_{n}] ⊢ Â such that [[ Â]] ∼ A.

Proof: The first half of the lemma is by structural induction on the type. [[ unit]] is ⟨ ∅, ∅, ∅, ∅ ⟩ and [[ X_{i}]] is given by Act_{[[ X_{i}]]} = {a}, ⋆ ⊢_{[[ X_{i}]]} a, ar_{[[ X_{i}]]}(a) = 0 and ref_{[[ X_{i}]]}(a) = ⋆_{i}, for some a ∈ U. Product, function space and Π-types are interpreted by the product, function space and universal quantification of 1-arenas respectively.

The converse is by recursion on the depth of the forest of A. For Act_{A} = ∅ define Â = unit. For A of non-zero depth, first consider the case A has a unique initial token a. Let k be the arity of a and let a^{1}, a^{2}, …, a^{m} be the direct descendents of a. Define A^{i} to be the 1-arena with Act_{A^{i}} = { b | a^{i} ⊢_{A}^{∗}b } and structure inherited from A, but with references a_{j} replaced by ⋆_{n+j}. Being of strictly smaller depth they define types [X_{1}, …, X_{n+k}] ⊢ Â^{i}. Now define

Â := ΠX_{n+1} … X_{n+k}.(Â^{1} → … → Â^{m} → X_{l}), where l = i when ref_{A}(a) = ⋆_{i} and l = n + j when ref_{A}(a) = a_{j}. Since in general any 1-arena A is the product of 1-arenas B^{1}, …, B^{k} each with a unique initial vertex (inspect the definition of product of 1-arenas), we define

Â = B̂^{1}×(…×(B̂^{k−2}×(B̂^{k−1}×B̂^{k})) …). □

Given n ⊢ A and an n-tuple θ = [A^{1}, …, A^{n}] of 1-arenas m ⊢ A^{i}, the substitution of A by θ, A ∘ θ, is the interpretation of the type Â[Â^{1}/X_{1}, …, Â^{n}/X_{n}]. Thus m ⊢ A ∘ θ.

7 The fibred category 𝔽 of games

First define an auxiliary fibration p : 𝔾 → 𝔹 with Ob(𝔹) = ℕ and Ob(𝔾_{n}) the set of finite 1-arenas in context n. A morphism in 𝔹(m, n) is an n-tuple of objects of 𝔾_{m}. Composition^{3} is substitution, product is addition, and the terminal object is 0. Define a starting strategy on G(A, n) to be a strategy that contains start(A, n). A morphism in 𝔾_{n}(A, B) is a starting strategy on G^{fin}(A⇒B, n), the subgame of G(A⇒B, n) obtained by restricting all 2-actions to be finite 1arenas.

Composition of strategies is a “second-order” version of HO-projection from a history of interaction. With condition F 4 and the related concepts outlined in the introduction of section 5 the rest is just a combinatorial grind, and there is only one way to proceed.

The fibre 𝔾_{n} is a CCC with product and function space as given in the previous section. Identities are copy-cat strategies as usual, extended to second order by the fact the i^{th} occurrence of the 2-action ? made by O is copied by P as the singleton arena a(⋆_{i}). The generic object is a(⋆_{1}) ∈ 𝔾_{1}.

3As stated here in the informal outline of the fibration, composition is only associative up to ∼. Further technical details are to be found in the author’s thesis [Hug].

Cartesian maps are based on a form of copy-cat strategy. Indexed products are provided by universal quantification of 1-arenas, and the verification of the adjunction is trivial because the first 2n+3 moves of any sequence on ∀_{n}(A) are a simple permutation of start(A, n + 1).

This structure provides an interpretation of system F as detailed in [Pho]. We now present a lemma which will help us to construct our model 𝔽. The proof is by structural induction on normal forms.

Lemma 4 Every normal form is interpreted in 𝔾 as a winning strategy.

The proof of the theorem below is similar in flavour to the HO definability proof.

Theorem Given any finite 1-arena in context n ⊢ A, every winning strategy σ on G^{fin}(A, n) defines a system F η-expanded, β-normal form s_{σ} of type Â, and the interpretation of s_{σ} in 𝔾 is σ.

Proof: By recursion on the size of σ (our games are finitely branching at O-moves, so winning strategies are finite, by König’s Lemma). If σ = start(A, n) then A is necessarily the empty 1-arena, and we define s_{σ} = ⟨⟩ of type Â = unit. First consider the case A has a unique initial action a, with direct descendents b_{11}b_{12}, …, b_{1p_{1}}. Let α⃗ = ⋆? ⋆ ? … ⋆ ? of length 2m, where m is the arity of a. The initial segment of play is of the form start(A, n) a α⃗ β⃗_{1} ⋆ β⃗_{2} ⋆ … ⋆ β⃗_{d} where β⃗_{i} = b_{iq_{1}} ⋆ A_{i1} ⋆ A_{i2} … ⋆ A_{in_{1}} and, for 2 ≤ i ≤ d, b_{i1}, b_{i2}, …, b_{ip_{i}} are the initial actions of the 1-arena A_{(i−1)e_{i}} for some 1 ≤ e_{i} ≤ n_{i−1}.

We construct an arena A′ such that there is a 1-1 correspondence between possible continuations of the rest of the game on A above, and complete games on A′. Let a_{i1}, …, a_{ir_{i}} be the direct descendents of b_{iq_{i}}. Then define

A′ = ∏_{i,j}(C ⇒F_{ij}),

where the product symbol indexed by 1 ≤ i ≤ d and 1 ≤ j ≤ r_{i} is the product of 1-arenas, and C = C_{1}×C_{2}×…×C_{p_{1}}. C represents the continuations that are available to P in the future by justifying back to O’s initial move a, and F_{ij} represents the possible continuations of A that would result from O playing the token a_{ij} directly descendent from b_{iq_{i}}. The construction of C and of the F_{ij} involves the substitution of 1-arenas for variables, as defined in section 6 (details omitted). By the 1-1 correspondence stated above, σ on the rest of A determines a winning strategy σ′ on A′, which is equivalent to a strategy σ′_{ij} on each of the 1-arenas (C ⇒F_{ij}). Since σ′ is strictly smaller than σ, by the induction hypothesis we have normal forms s_{ij} defined by the σ′_{ij}.

We now define the term s_{σ}. For 2 ≤ i ≤ d define the context

π_{i}[…] = \{ \begin{matrix}Snd … Snd F st[…], & if 1 ≤ q_{i} < p_{i}, \\ Snd … Snd Snd[…], & if q_{i} = p_{i}, \end{matrix}

where the number of consequtive “Snd”s in the first case is q_{i} −1, and in the second case is q_{i}, and the context

E_{i}[…] = (π_{i}[…]) Â_{i1}Â_{i2} … Â_{in_{i}}s_{i1}s_{i2} … s_{ir_{i}}

The normal form s_{σ} is given by

ΛX_{1}X_{2} … X_{m}.λb_{11}^{Ĉ_{1}}.λb_{12}^{Ĉ_{2}} … λb_{1p_{1}}^{Ĉ_{p_{1}}} . v

where

v = E_{d}E_{d−1} … E_{2}[a_{1q_{1}} Â_{11} … Â_{1n_{1}}s_{11}s_{12} … s_{1e_{1}}].

The verification that the interpretation of s_{σ} is σ comes from within the proof of Lemma 2.

Finally, in the case that A has more than one initial action, we take the terms that are generated by restriction of σ to each of the components, and then form the appropriate ⟨ , ⟩-pairings of these terms that correspond to the product type Â as defined in Lemma 3. □

Now we define 𝔽 as the subcategory of 𝔾 obtained by reducing the hom-sets in the fibres to the winning strategies. To show that the composition of winning strategies is winning, we lift them to System F (Theorem), sequentially compose the terms, normalise, and reinterpret back into the model (Lemma 4).

8 Conclusions and future research

Interestingly, the definability theorem does not provide a one-to-one correspondance between winning strategies and η-expanded, β-normal forms, since the interpretation map induces the following equations on types (and terms include types in general):

\begin{aligned}unit×T & = & T, & unit → T & = & T, \\ T → unit & = & unit, & ΠX.unit & = & unit, \end{aligned}

T_{1} → T_{2} → T_{3} = T_{1}×T_{2} → T_{3},
T_{1} → T_{2}×T_{3} = (T_{1} → T_{2})×(T_{1} → T_{3}),
ΠX. T_{1}×T_{2} = (ΠX.T_{1})×(ΠX.T_{2}),
T_{1} → ΠX.T_{2} = ΠX. T_{1} → T_{2},

where in the last axiom X is not free in T_{1}.

Work in progress that has stemmed from this model:

• Adaptation of the games in an attempt to obtain a Reynold’s parametric model of system F [Rey83].

• In order to model system F using our hierarchy we required only the use of one particular 2-arena, the “flat” arena K. Can we obtain applicative structure at second order by allowing arbitrary 2-arenas, so that we can model higher-order polymorphism [Cro95]?

• Can we adapt the games in order to model linear polymorphism [Abr95]?

Future work:

• Give a direct proof of compositionality of winning strategies.

• Can we derive the copy-cat condition from a more general notion of game, rather than enforcing it?

• Investigate the abstract machine that corresponds to composition in the model.

• Can we model dependent types with a dual version of 2-reference which relates 2-arenas back to previous 1-arenas?

A long-term objective is to try and adapt the modelling techniques used in this paper in order to conquer every vertex of the λ-cube [Bar84].

Acknowledgements Many thanks to Luke Ong, who originally suggested polymorphism as a thesis topic in March 1996. Also to Martin Hyland, Ralph Loader and Guy McCusker for helpful discussions and comments. Finally Ben Worrell and Adèle Carney for their help with L^{A}TEX.

References

[Abr95] S. Abramsky. Semantics of Interaction. Notes for CLICS II Summer School, Cambridge. Summer 1995.

[AJM94] S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for P CF (extended abstract). Number 789 in Lecture Notes in Computer Science, 1994.

[Bar84] Henk P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, North-Holland, 1984.

[CGW89] T. Coquand, C. Gunter and G. Winskel. Domain theoretic models of polymorphism. Information and Computation, 81:123-167, 1989.

[Cro93] R. L. Crole. Categories for types. Cambridge University Press, 1993.

[Gir89] J.-Y. Girard. Proofs and Types. Cambridge Tracts in Theoretical Computer Science, 45:159-192, 1989.

[HO94] J. M. E. Hyland and C.-H. L. Ong. On Full Abstraction for PCF: I, II and III. ftp-able at ftp.comlab.ox.ac.uk, 1994.

[Hug] D. J. D. Hughes. Games, polymorphism and parametricity. DPhil thesis, University of Oxford.

[McC96] G. McCusker. Games and Full Abstraction for FPC. LiCS 1996.

[Nic94] H. Nickau. Hereditarily sequential functionals. Proceedings of the Symposium on Logical Foundations of Computer Science: Logic at St. Petersburg. Springer, 1994.

[Pho] W. Phoa. An introduction to fibrations, topos theory, the effective topos and modest sets. Lecture Notes, University of Edinburgh, Scotland, U.K.

[Rey83] J. C. Reynolds. Types, abstraction, and parametric polymorphism. Information Processing 83:513-523. North-Holland, 1983.