Game Semantics of Martin-L\"of Type Theory

TL;DR

This paper introduces a new game semantics for Martin-Löf type theory that offers more accurate interpretation, supports Sigma-types directly, and provides novel mathematical structures, including finite limits and subtyping interpretation.

Contribution

It presents a novel game semantics for MLTT with enhanced interpretative accuracy, direct Sigma-type interpretation, and a category with finite limits, advancing the understanding of type-theoretic models.

Findings

More accurate interpretation of MLTT than existing semantics

First game semantics to interpret subtyping on dependent types

Game-semantic proof of Markov's principle independence

Abstract

We present new game semantics of Martin-L\"of type theory (MLTT) equipped with One-, Zero-, N-, Pi-, Sigma- and Id-types. Our game semantics interprets MLTT more accurately than existing ones. Another advantage of our game semantics over existing ones is its interpretation of Sigma-types that is direct and compatible with the game semantics of product types . Besides, its mathematical structure is novel and useful; e.g., the category of our games has all finite limits, which is a key step to an extension of the present work to homotopy type theory, and our games interpret subtyping on dependent types for the first time as game semantics. Finally, we provide a new, game-semantic proof of the independence of Markov's principle from MLTT, which demonstrates an advantage of our game semantics over extensional models of MLTT such as the effective topos.

Equations

$$\sigma \upharpoonright G_i:=\{\begin{array}{ll}{\sigma }_i& \text{if σ=σ0⊗σ1 for (necessarily unique) σ0:G0 and σ1:G1;}\\ \uparrow & \text{otherwise, where ↑ means being undefined.}\end{array}$$

$$\tau \upharpoonright j:=\{\begin{array}{ll}\{\mathbf{s}\upharpoonright j\mid \mathbf{s}\in \tau \}& \text{if {s↾k∣s∈τ}:G for all k∈N;}\\ \uparrow & \text{otherwise.}\end{array}$$

$$({\Delta }^{\Gamma })(\varphi )$$

$$\cup \{\mathbf{t}lr\in |{\Delta }^{\Gamma }{|}^{\mathrm{Even}}\mid \mathbf{t}l\in ({\Delta }^{\Gamma })(\varphi ),\forall \gamma :\Gamma .\mathbf{t}l\in \Delta (\varphi \circ \gamma {)}^{{\overline{\gamma }}_{\Gamma }}\Rightarrow \mathbf{t}lr\in \Delta (\varphi \circ \gamma {)}^{{\overline{\gamma }}_{\Gamma }}\},$$

$${\Pi }_{\ell }(\Gamma ,L)(\varphi )$$

$$\cup \{\mathbf{t}lr\in |{\Pi }_{\ell }(\Gamma ,L){|}^{\mathrm{Even}}\mid \mathbf{t}l\in {\Pi }_{\ell }(\Gamma ,L)(\varphi ),\forall \gamma :\Gamma .\mathbf{t}l\in L^{\star }(\gamma )(\varphi \circ \gamma {)}^{{\overline{\gamma }}_{\Gamma }}\Rightarrow \mathbf{t}lr\in L^{\star }(\gamma )(\varphi \circ \gamma {)}^{{\overline{\gamma }}_{\Gamma }}\},$$

$$\Pi (A,B)\{\varphi \}$$

$$=(\Pi (A\{\varphi \}({\delta }_0^{†}),B\{{\varphi }_A^{+}{\}}_{{\delta }_0^{†}}){)}_{{\delta }_0^{†}\in \mathbb{WPG}(\text{oc}\Delta )}$$

$$=\Pi (A\{\varphi \},B\{{\varphi }_A^{+}\}),$$

$$B\{{\varphi }_A^{+}{\}}_{{\delta }_0^{†}}({\hat{\alpha }}_0^{†})$$

$$=B(⟨\varphi \bullet {\mathrm{p}}_{A\{\varphi \}},{\mathrm{v}}_{A\{\varphi \}}{⟩}^{†}\bullet ⟨{\delta }_0,{\hat{\alpha }}_0⟩)$$

$$=B(⟨\varphi \bullet {\delta }_0,{\hat{\alpha }}_0{⟩}^{†})$$

$$=B_{{\varphi }^{†}\circ {\delta }_0^{†}}({\hat{\alpha }}_0^{†}).$$

$${\mathrm{App}}_{A,B}(\kappa ,\alpha )\{\varphi \}$$

$$={\lambda }_{A,B}^{-1}(\kappa )\{⟨\varphi ,\alpha \{\varphi \}⟩\}$$

$$={\lambda }_{A,B}^{-1}(\kappa )\{⟨\varphi \bullet {\mathrm{p}}_{A\{\varphi \}},{\mathrm{v}}_{A\{\varphi \}}⟩\bullet ⟨{\mathrm{der}}_{|\Delta |},\alpha \{\varphi \}⟩\}$$

$$={\lambda }_{A,B}^{-1}(\kappa )\{{\varphi }_A^{+}\}\{\overline{\alpha \{\varphi \}}\}$$

$$={\lambda }_{A\{\varphi \},B\{{\varphi }_A^{+}\}}^{-1}(\kappa \{\varphi \})\{\overline{\alpha \{\varphi \}}\}\text{(by λ-Subst)}$$

$$={\mathrm{App}}_{A\{\varphi \},B\{{\varphi }_A^{+}\}}(\kappa \{\varphi \},\alpha \{\varphi \}).$$

$${\lambda }_{A,B}({\mathrm{App}}_{A\{{\mathrm{p}}_A\},B\{{\mathrm{p}}_A^{+}\}}(\kappa \{{\mathrm{p}}_A\},{\mathrm{v}}_A))$$

$$={\lambda }_{A,B}({\lambda }_{A,B}^{-1}(\kappa )\{{\mathrm{p}}_A^{+}\}\{\overline{{\mathrm{v}}_A}\})\text{(by λ-Subst)}$$

$$={\lambda }_{A,B}({\lambda }_{A,B}^{-1}(\kappa )\{⟨{\mathrm{p}}_A\bullet {\mathrm{p}}_{A\{{\mathrm{p}}_A\}},{\mathrm{v}}_{A\{{\mathrm{p}}_A\}}⟩\bullet ⟨{\mathrm{der}}_{|\Sigma (\Gamma ,A)|},{\mathrm{v}}_A⟩\})$$

$$={\lambda }_{A,B}({\lambda }_{A,B}^{-1}(\kappa )\bullet ⟨{\mathrm{p}}_A,{\mathrm{v}}_A⟩)$$

$$={\lambda }_{A,B}({\lambda }_{A,B}^{-1}(\kappa )\bullet {\mathrm{der}}_{|\Sigma (\Gamma ,A)|})$$

$$={\lambda }_{A,B}({\lambda }_{A,B}^{-1}(\kappa ))$$

$$=k,$$

$${\mathcal{R}}_{A,B,P}^{\Sigma }(\rho )\{{\mathrm{Pair}}_{A,B}\}$$

$$=\rho \{{\mathrm{Pair}}_{A,B}^{-1}\bullet {\mathrm{Pair}}_{A,B}\}$$

$$=\rho \{{\mathrm{id}}_{\Sigma (\Sigma (\Gamma ,A),B)}\}$$

$$=\rho .$$

$${\varphi }_{\Sigma (A,B)}^{+}\bullet {\mathrm{Pair}}_{A\{\varphi \},B\{{\varphi }_A^{+}\}}$$

$$=⟨\varphi \bullet {\mathrm{p}}_{\Sigma (A\{\varphi \},B\{{\varphi }_A^{+}\})}\bullet {\mathrm{Pair}}_{A\{\varphi \},B\{{\varphi }_A^{+}\}},{\mathrm{v}}_{\Sigma (A,B)\{\varphi \}}\{{\mathrm{Pair}}_{A\{\varphi \},B\{{\varphi }_A^{+}\}}\}⟩$$

$$=⟨\varphi \bullet {\mathrm{p}}_{A\{\varphi \}}\bullet {\mathrm{p}}_{B\{{\varphi }_A^{+}\}},{\mathrm{v}}_{\Sigma (A\{\varphi \},B\{{\varphi }_A^{+}\})}\{{\mathrm{Pair}}_{A\{\varphi \},B\{{\varphi }_A^{+}\}}\}⟩\text{(by the above equation)}$$

$$=⟨\varphi \bullet {\mathrm{p}}_{A\{\varphi \}}\bullet {\mathrm{p}}_{B\{{\varphi }_A^{+}\}},⟨{\mathrm{v}}_{A\{\varphi \}}\{{\mathrm{p}}_{B\{{\varphi }_A^{+}\}}\},{\mathrm{v}}_{B\{{\varphi }_A^{+}\}}⟩⟩$$

$$=⟨{\mathrm{p}}_A\bullet {\mathrm{p}}_B,⟨{\mathrm{v}}_A\{{\mathrm{p}}_B\},{\mathrm{v}}_B⟩⟩\bullet ⟨⟨\varphi \bullet {\mathrm{p}}_{A\{\varphi \}}\bullet {\mathrm{p}}_{B\{{\varphi }_A^{+}\}},{\mathrm{v}}_{A\{\varphi \}}\{{\mathrm{p}}_{B\{{\varphi }_A^{+}\}}\}⟩,{\mathrm{v}}_{B\{{\varphi }_A^{+}\}}⟩$$

$$=⟨{\mathrm{p}}_A\bullet {\mathrm{p}}_B,⟨{\mathrm{v}}_A\{{\mathrm{p}}_B\},{\mathrm{v}}_B⟩⟩\bullet ⟨⟨\varphi \bullet {\mathrm{p}}_{A\{\varphi \}},{\mathrm{v}}_{A\{\varphi \}}⟩\bullet {\mathrm{p}}_{B\{{\varphi }_A^{+}\}},{\mathrm{v}}_{B\{{\varphi }_A^{+}\}}⟩$$

$$={\mathrm{Pair}}_{A,B}\bullet ⟨{\varphi }_A^{+}\bullet {\mathrm{p}}_{B\{{\varphi }_A^{+}\}},{\mathrm{v}}_{B\{{\varphi }_A^{+}\}}⟩$$

$$={\mathrm{Pair}}_{A,B}\bullet {\varphi }_{A,B}^{++}.$$

$${\mathcal{R}}_{A,B,P}^{\Sigma }(\rho )\{{\varphi }_{\Sigma (A,B)}^{+}\}$$

$$=\rho \{⟨⟨{\mathrm{p}}_{\Sigma (A,B)},{\varpi }_1^{A,B}⟩,{\varpi }_2^{A,B}⟩\bullet ⟨\varphi \bullet {\mathrm{p}}_{\Sigma (A,B)\{\varphi \}},{\mathrm{v}}_{\Sigma (A,B)\{\varphi \}}⟩\}$$

$$=\rho \{⟨⟨\varphi \bullet {\mathrm{p}}_{\Sigma (A,B)\{\varphi \}},{\varpi }_1^{A\{\varphi \},B\{{\varphi }_A^{+}\}}⟩,{\varpi }_2^{A\{\varphi \},B\{{\varphi }_A^{+}\}}⟩\}\text{(by the definition of ϖ1 and ϖ2)}$$

$$=\rho \{⟨⟨\varphi \bullet {\mathrm{p}}_{A\{\varphi \}},{\mathrm{v}}_{A\{\varphi \}}⟩\bullet {\mathrm{p}}_{B\{{\varphi }_A^{+}\}},{\mathrm{v}}_{B\{{\varphi }_A^{+}\}}⟩\}\{⟨⟨{\mathrm{p}}_{\Sigma (A,B)\{\varphi \}},{\varpi }_1^{A\{\varphi \},B\{{\varphi }_A^{+}\}}⟩,{\varpi }_2^{A\{\varphi \},B\{{\varphi }_A^{+}\}}⟩\}$$

$$=\rho \{⟨{\varphi }_A^{+}\bullet {\mathrm{p}}_{B\{{\varphi }_A^{+}\}},{\mathrm{v}}_{B\{{\varphi }_A^{+}\}}⟩\}\{{\mathrm{Pair}}_{A\{\varphi \},B\{{\varphi }_A^{+}\}}^{-1}\}$$

$$={\mathcal{R}}_{A\{\varphi \},B\{{\varphi }_A^{+}\},P\{{\varphi }_{\Sigma (A,B)}^{+}\}}^{\Sigma }(\rho \{{\varphi }_{A,B}^{++}\}).$$

$$\check{\rho }=\check{\rho }\{{\mathrm{id}}_{\Sigma (\Gamma ,\Sigma (A,B))}\}=\check{\rho }\{{\mathrm{Pair}}_{A,B}\}\{{\mathrm{Pair}}_{A,B}^{-1}\}=\rho \{{\mathrm{Pair}}_{A,B}^{-1}\}={\mathcal{R}}_{A,B,P}^{\Sigma }(\rho ),$$

$${\mathcal{R}}_P^N(c_{\mathrm{z}},c_{\mathrm{s}})\{\mathrm{zero}\}$$

$${\mathcal{R}}_P^N(c_{\mathrm{z}},c_{\mathrm{s}})\{\mathrm{succ}\}$$

Full text

game semantics,

Martin-Löf type theory,

constructive mathematics,

Corresponds¡—¿ \newarrowTeXto—–¿

\startlocaldefs\endlocaldefs

{fmbox}\dochead

Research

This is a preprint submitted to Research in the Mathematical Sciences (RMS).

{abstractbox}

1. 1 Introduction

2. 1.1 Martin-Löf type theory and the meaning explanation

3. 1.2 Game semantics

4. 1.3 Main results

5. 1.4 Related work and our contributions

6. 1.5 Concluding remarks

7. 1.6 The structure of the present article

8. 2 Games and strategies for simple type theories

9. 2.1 Arenas and legal positions

10. 2.2 Games and strategies

11. 2.3 Constructions on games and strategies

12. 3 Predicate games

13. 3.1 Predicate games

14. 3.2 Cartesian closed categories of predicate games

15. 4 Game semantics of Martin-Löf type theory

16. 4.1 Dependent predicate games

17. 4.2 Pi on dependent predicate games

18. 4.3 Sigma on dependent predicate games

19. 4.4 A game-semantic category with families

20. 4.5 Game-semantic type formers

21. 4.5.1 Game semantics of Pi-types

22. 4.5.2 Game semantics of Sigma-types

23. 4.5.3 Game semantics of N-type

24. 4.5.4 Game semantics of One- and Zero-types

25. 4.5.5 Game semantics of Id-types

26. 4.6 Intensionality

27. 4.7 Independence of Markov’s principle

28. 4.8 Game semantics of subtyping on dependent types

1 Introduction

1.1 Martin-Löf type theory and the meaning explanation

Martin-Löf type theory (MLTT) [1, 2] is one of the best-known formal systems for constructive mathematics [3], which is comparable to set theory [4, 5] for classical mathematics. MLTT is also a programming language [6] that is a generalisation of the simply-typed lambda-calculus (STLC) [7] along the generalisation of (intuitionistic) propositional logic to predicate logic under the Curry-Howard isomorphisms [8]. By this computational nature, MLTT and similar formal systems enable computer formalisations of mathematics and its applications to programming [9, 10].

Like set theory is explained informally by sets, the conceptual foundation of MLTT is computations in an informal sense. That is, the fundamental idea of MLTT is to regard objects and proofs in constructive mathematics uniformly as computations, and MLTT is a syntactic formalisation of this foundational idea [6]. Hence, objects and proofs in MLTT are unified into terms, where formulas are called types. This standard, informal semantics of MLTT is called the meaning explanation [11, §5].

However, MLTT is not always the best formalisation of this conceptual foundation of constructive mathematics since it is an intricate formal system that inevitably contains superficial syntactic details.111A syntactic formalisation is also unsatisfactory from the syntax-first-view, i.e., the view that semantic concepts come first, and syntax merely provides notations. In other words, the intuition behind MLTT is often blurred by the complexity and the syntactic nature of MLTT. In addition, the syntactic complexity makes it difficult to study the meta-theory of MLTT.

Accordingly, mathematical semantics [12] of MLTT that faithfully formalises the meaning explanation is strongly desired since such semantics would accurately and directly (or non-inductively) describe the intuition behind MLTT, abstracting the syntactic details. It would not only deepen our understanding of MLTT in this way but also suggest improvements and extensions of MLTT like coherence spaces by Girard [13] led to linear logic [13], and the groupoid model by Hofmann and Streicher [14] to homotopy type theory (HoTT) [10]. Besides, mathematical semantics has been highly effective for the meta-theoretic study of MLTT; e.g., see [15].

1.2 Game semantics

Game semantics [16, 17] is a particular class of mathematical semantics of logic and computation that models types and terms by games and strategies, respectively.

Its strong point is its conceptual naturality: ‘Logic is the study of reasoning’ [18, p. 1], where one can regard ‘reasoning’ as dialogical arguments between Player (or a mathematician) and Opponent (or an oracle), and game semantics formalises this intuition. This game-semantic view on logic is also in harmony with the meaning explanation since dialogical arguments are a certain kind of computations.

Another strong advantage of game semantics is its precision in modelling syntax as various full completeness/abstraction results [19] in the literature demonstrate. This precision is due to its intensionality: Game semantics captures the processes themselves underlying terms rather than their extensions such as functions.

Finally, the concrete nature of game semantics enables its algorithmic applications to program analysis and verification (i.e., meta-theories of programs) [20].

1.3 Main results

To summarise the points so far, mathematical semantics of MLTT that advances our understanding of MLTT, promotes its improvements and extensions, and/or clarifies its meta-theory is strongly desired, and game semantics seems perfect for this role by its conceptual naturality, harmony with the meaning explanation, precision in modelling syntax and algorithmic applications. Also, game semantics models effects [21] and linear logic [13] in a highly systematic way (see [22] for the details); thus, game semantics of MLTT, if any, may lead to MLTT with effects and linear typing.

However, although game semantics of various logics and computations has been given, it is quite difficult to establish game semantics of MLTT. The main challenge in game semantics of MLTT is to model the extensional type dependency in Sigma-types by intensional processes in games; see the beginning of §3. In fact, this problem had been open for more than twenty years, and even today its definitive solution is yet to emerge though a few candidates have arisen recently [23, 24]; see §1.4.

Hence, we aim to provide another candidate for game semantics of MLTT with the hope that it sheds new light on this problem. Motivated in this way, we prove:

Theorem** (Game semantics of MLTT).**

There is new game semantics of MLTT with One-, Zero-, N-, Pi-, Sigma- and Id-types (§4.4–4.5).

Our key idea for this theorem is to generalise games so that they can model Sigma-types, while we keep strategies unchanged so that we retain the advantages of game semantics such as intensionality (§1.2). See the beginning of §3 for the outline of this idea. Also, see §1.4 for the advantages of this method over existing ones [23, 24].

We also illustrate the utility of our game semantics by giving a new proof of:

Corollary** (Independence of Markov’s principle [25]).**

Markov’s principle [26] is independent from MLTT equipped with the types listed in Theorem Theorem (§4.7).

The method used by Mannaa and Coquand [25] is syntactic, while our semantic approach provides a new, intuitive argument on why the independence holds. This corollary also illustrates an advantage of game semantics over other computational models since, e.g., the effective topos [27] cannot show the independence. Moreover, by the non-inductive nature of game semantics, the present method would be easily applied to the independence of Markov’s principle from various extensions of MLTT.

Finally, the novel mathematical structure of our game semantics enables:

Corollary** (Game semantics of subtyping on dependent types).**

The game semantics given by Theorem Theorem models subtyping [28, §15] on dependent types (§4.8).

1.4 Related work and our contributions

Abramsky et al. have established the first game semantics of MLTT equipped with One-, Pi-, Sigma-, Id- and finite inductive types [23, 29]. Its significance is that it is the first intensional model of MLTT, and thus it stands in sharp contrast with other computational models such as realisability and domain models [15, 30], which are extensional. Their main result is a certain kind of full completeness. However, they only interpret Sigma-types indirectly and inductively by a list construction and the adjunction between Pi- and Sigma-types. Specifically, they interpret a Sigma-type $\mathsf{\vdash\Sigma_{x:C}D(x)\ type}$222For simplicity, here we only consider the empty context. by the list $(C,D)$ of the game $C$ that models the simple type $\mathsf{\vdash C\ type}$ and the family $D=(D(x))_{x:C}$ of games $D(x)$ indexed by strategies $x$ on $C$ that models the dependent type $\mathsf{x:C\vdash D(x)\ type}$, and interpret a term of the form $\mathsf{\vdash\langle c,d\rangle:\Sigma_{x:C}D(x)}$ by the list $(c,d)$ of the strategies $c$ and $d$ that respectively model the terms $\mathsf{\vdash c:C}$ and $\mathsf{\vdash d:D(c)}$, and a term of the form $\mathsf{z:\Sigma_{x:C}D(x)\vdash e(z):E(z)}$ by identifying it with the one $\mathsf{x:C,y:D(x)\vdash e(\langle x,y\rangle):E(\langle x,y\rangle)}$. As a result, they interpret types and terms by the lists of (families of) games and strategies, respectively; this method merely simulates the term model [31, §2.4] and drops the non-inductive nature of game semantics. Another undesirable feature of this approach is that it identifies the types $\mathsf{\Pi_{z:\Sigma_{x:A}B(x)}C(z)}$ and $\mathsf{\Pi_{x:A}\Pi_{y:B}C(\langle x,y\rangle)}$. Finally, for composing winning strategies, they use the O-sat operation [29, Remark 4.5]; however, it generates a significant gap between MLTT and their model. In fact, this method only works for a very specific class of finite inductive types [29, Figure 7]; see §4.3 on this point.

Another related work is the denotational model of MLTT [24] by Blot and Laird based on concrete date structures and sequential algorithms [32]. They interpret Boolean-, Pi- and Sigma-types and a universe though their interpretation of the universe is not by game semantics but by domain theory. Their main results are certain full completeness/abstraction. Notably, they directly interpret Sigma-types without the list construction, overcoming the problem of the preceding work. However, it is possible to play on both sides of their interpretation of a Sigma-type within a single play, which is far from the game semantics [33, 34, 35] (and even the graph game semantics [36]) of product types. Thus, it is arguable if their model properly captures the generalisation of product types to Sigma-types. As a more pragmatic disadvantage, their model admits control operators or classical reasonings, but the logical part of MLTT is intuitionistic; i.e., there is a gap between MLTT and their model. Besides, their model does not achieve the linear decomposition of function types [13] or the characterisation of effects by constraints on strategies, which are both strong advantages of game semantics [22]. Last but not least, their interpretation of Id-types by finite tuples of Boolean-type sketched in [24, §9] does not work in the presence of N-type since the set $\mathbb{N}$ of all natural numbers is unbounded.

Thus, each of the existing approaches to game semantics of MLTT has pros and cons, and we have not reached a consensus on which option should be a definitive solution. In this context, we offer the third method with the novel features listed below, hoping that it would eventually lead to a definitive solution in the future.

First, we achieve the first game semantics of both N- and Id-types. The interpretation of these types enables us to show the independence of Markov’s principle.

Second, our games are a modest generalisation of a standard variant, McCusker’s games [35], and we model types and terms by such games and (ordinary) strategies, not lists of them, respectively. As a result, we retain the syntax-independence and the non-inductive nature of game semantics. Besides, we directly model Sigma-types by our games, where a play occurs only in either side. Hence, we overcome the main shortcomings of the preceding methods. For the basic idea, see the beginning of §3.

Third, our method inherits the linear decomposition of function types and the characterisation of effects by constraints on strategies in McCusker’s one [22].

Fourth, the novel mathematical structure of our games enables us to dispense with the O-sat operation unlike Abramsky et al. so that we can interpret the type dependency of a standard class of Pi- and Sigma-types more accurately; see §4.3.

Finally, the mathematical structure of our games is novel and useful. For instance, the category of our games has all finite limits (Corollary 3.14), while that of existing games does not. This novel structure enables us to internalise a certain notion of $\infty$-groupoids in the category of our games, which is a key step to extend the present work to HoTT [37]. Moreover, we accomplish the first game semantics of subtyping on dependent types (§4.8). On the other hand, in order to focus on the main idea of the present work, we leave it to another article to interpret universes.

1.5 Concluding remarks

Due to the novel mathematical structure of our games, one might misunderstand that our semantics is close to extensional models such as realisability and domain models. However, since our strategies are just the ordinary ones (§1.4), our method inherits the advantages of standard game semantics such as intensionality (§1.2). In fact, the intensional features of the preceding game semantics [23, §1] are mostly valid in ours (§4.6); e.g., both refute function extensionality. Also, our model refutes Markov’s principle by its intensionality (§4.7), while the effective topos does not.

Last but not least, we do not prove full completeness for the following reasons. First, the standard syntax of MLTT, specifically N-type, is not very suited to fully complete game semantics. For instance, the full completeness results [23, 29, 24] are on modifications of MLTT, and they exclude N-type. However, our main topic is MLTT itself (§1.1), and thus we leave full completeness on a modification of MLTT as future work. Second, our priority is more on an interpretation of N-type than full completeness without N-type since our motivation comes from foundations of mathematics (§1.1), for which N-type is crucial. Finally, one of our aims is to provide tools for the study of MLTT (§1.1), but full completeness is not necessarily the most important result for this aim. For example, the fully complete model [24] cannot show the independence of Markov’s principle since it admits classical reasonings. Hence, we instead show the utility of our model by proving the independence (§4.7).

1.6 The structure of the present article

The rest of this article proceeds as follows. We first recall McCusker’s games and strategies in §2 and generalise the games in §3. We then interpret MLTT by the generalised games and strategies in §4, where we analyse the intensionality of our game semantics in §4.6, give a game-semantic proof of the independence of Markov’s principle from MLTT in §4.7, and interpret subtyping on dependent types in §4.8.

2 Games and strategies for simple type theories

We first recall McCusker’s games and strategies for simple type theories [35], which the present work is based on. We select this variant for the following reasons. First, it combines the strong points of the two best-known variants: the linear decomposition of function types [13] achieved by AJM-games [33] and the characterisation of effects by constraints on strategies [22] that utilises pointers in HO-games [34] (originally introduced in [38]). Our games inherit these advantages so that they would shed new light on the problem of combining MLTT and linear logic and/or effects. Second, pointers enable us to refine game semantics into a model of computation [39], which is highly desirable as a mathematical foundation of constructive mathematics (§1.1).

We assume that the reader is familiar with McCusker’s games and strategies, and leave more expositions and examples to the gentle introduction [22]. We henceforth call McCusker’s games and strategies respectively games and strategies.

We first recall two preliminary concepts in §2.1, and then games and strategies in §2.2. We finally recall standard constructions on games and strategies in §2.3.

Notation*.*

We use the following notations throughout the present article:

• •

We use bold small letters $\bm{s},\bm{t},\bm{u},\bm{v}$, etc. for sequences, in particular $\bm{\epsilon}$ for the empty sequence, and small letters $a,b,m,n,x,y$, etc. for elements of sequences;

• •

We define $\overline{n}\colonequals\{\,1,2,\dots,n\,\}$ for each $n\in\mathbb{N}^{+}\colonequals\mathbb{N}\setminus\{0\}$, and $\overline{0}\colonequals\emptyset$;

• •

We write $x_{1}x_{2}\dots x_{|\bm{s}|}$ for $\bm{s}=(x_{1},x_{2},\dots,x_{|\bm{s}|})$, where $|\bm{s}|$ is the length of $\bm{s}$, define $\bm{s}(i)\colonequals x_{i}$ ($i\in\overline{|\bm{s}|}$) and write $a\in\bm{s}$ if $a=\bm{s}(j)$ for some $j\in\overline{|\bm{s}|}$;

• •

A concatenation of sequences $\bm{s}$ and $\bm{t}$ is represented by their juxtaposition $\bm{s}\bm{t}$ (or $\bm{s}.\bm{t}$), but we often write $a\bm{s}$, $\bm{t}b$, $\bm{u}c\bm{v}$ for $(a)\bm{s}$, $\bm{t}(b)$, $\bm{u}(c)\bm{v}$, and so on;

• •

We write $\mathrm{Even}(\bm{s})$ (resp. $\mathrm{Odd}(\bm{s})$) if $\bm{s}$ is of even- (resp. odd-) length, and given a set $S$ of sequences and $\mathsf{P}\in\{\mathrm{Even},\mathrm{Odd}\}$, we define $S^{\mathsf{P}}\colonequals\{\,\bm{s}\in S\mid\mathsf{P}(\bm{s})\,\}$;

• •

We write $\bm{s}\preceq\bm{t}$ if $\bm{s}$ is a prefix of $\bm{t}$, and given a set $S$ of sequences, $\mathrm{Pref}(S)$ for the set of all prefixes of sequences in $S$, i.e., $\mathrm{Pref}(S)\colonequals\{\,\bm{s}\mid\exists\bm{t}\in S.\,\bm{s}\preceq\bm{t}\,\}$;

• •

We use informal ‘tags’ $(\_)_{[i]}$ ($i\in\mathbb{N}$) for clarity (e.g., see Definition 2.14).

2.1 Arenas and legal positions

A game is a certain kind of a rooted directed acyclic graph, whose paths from a root represent possible developments or positions in a ‘game in the ordinary sense’ (e.g., chess). These positions are finite sequences of vertices or moves, and a play in the game proceeds as its participants alternately perform moves along a position. It is conventional to identify each game with the set of all positions in the game. We focus on standard two-person games between Player (P) (or a mathematician) and Opponent (O) (or an oracle), in which O always starts a play.

Technically, games are based on two preliminary concepts: arenas and legal positions. An arena defines the basic components of a game, which in turn induces legal positions of the arena that specify the basic rules of the game in the sense that each position of the game must be legal. Let us first recall these two concepts.

Definition 2.1** (Moves).**

Let us fix, throughout the present work, arbitrary pairwise distinct symbols $\mathsf{O}$, $\mathsf{P}$, $\mathsf{Q}$ and $\mathsf{A}$, and call them labels. A move is any triple $m^{xy}\colonequals(m,x,y)$ such that $x\in\{\mathsf{O},\mathsf{P}\}$ and $y\in\{\mathsf{Q},\mathsf{A}\}$. We usually abbreviate moves $m^{xy}$ as $m$, and instead define $\lambda(m)\colonequals xy$, $\lambda^{\mathsf{OP}}(m)\colonequals x$ and $\lambda^{\mathsf{QA}}(m)\colonequals y$.

We call a move $m$ an O-move if $\lambda^{\mathsf{OP}}(m)=\mathsf{O}$, a P-move if $\lambda^{\mathsf{OP}}(m)=\mathsf{P}$, a question if $\lambda^{\mathsf{QA}}(m)=\mathsf{Q}$, and an answer if $\lambda^{\mathsf{QA}}(m)=\mathsf{A}$.

Definition 2.2** (Arenas [34, 35]).**

An arena is a pair $G=(M_{G},\vdash_{G})$ such that

• •

$M_{G}$ is a set of moves;

• •

$\vdash_{G}$ is a subset of the cartesian product $(\{\star\}\cup M_{G})\times M_{G}$, where $\star$ (or represented more precisely by $\star_{G}$) is an arbitrarily fixed element such that $\star\not\in M_{G}$, called the enabling relation, that satisfies

• –

(E1) If $\star\vdash_{G}m$, then $\lambda(m)=\mathsf{OQ}$;

• –

(E2) If $m\vdash_{G}n$ and $\lambda^{\mathsf{QA}}(n)=\mathsf{A}$, then $\lambda^{\mathsf{QA}}(m)=\mathsf{Q}$;

• –

(E3) If $m\vdash_{G}n$ and $m\neq\star$, then $\lambda^{\mathsf{OP}}(m)\neq\lambda^{\mathsf{OP}}(n)$.

We call moves $m\in M_{G}$ initial if $\star\vdash_{G}m$, and set $M_{G}^{\mathrm{Init}}\colonequals\{\,m\in M_{G}\mid\star\vdash_{G}m\,\}$.

An arena $G$ is well-founded (w.f.) if $\vdash_{G}$ is well-founded, i.e., there is no sequence $(m_{i})_{i\in\mathbb{N}}$ of moves $m_{i}\in M_{G}$ such that $\star\vdash_{G}m_{0}$ and $m_{i}\vdash_{G}m_{i+1}$ for all $i\in\mathbb{N}$.

Remark*.*

In the original article [35], an arena is a triple $G=(M_{G},\lambda_{G},\vdash_{G})$, where labels are assigned to moves by the labelling function $\lambda_{G}:M_{G}\rightarrow\{\mathsf{O},\mathsf{P}\}\times\{\mathsf{Q},\mathsf{A}\}$. Instead, we embed labels into moves (Definition 2.1); this modification is convenient, e.g., when we take unions of games, since it makes labels on moves unambiguous without underlying arenas. Besides, the axiom E1 in [35] further requires $n\vdash_{G}m\Leftrightarrow n=\star$ whenever $\star\vdash_{G}m$. We discard this condition too again for unions of games.

An arena $G$ specifies moves in a game, each of which is O’s/P’s question/answer, and which move $n$ can be performed for each move $m$ during a play in the game by the relation $m\vdash_{G}n$ (cf. Definition 2.3), where $\star\vdash_{G}m$ means that O can initiate a play by $m$ in the game. The axioms E1, E2 and E3 are then to be read as follows:

• •

E1 sets the convention that an initial move must be O’s question;

• •

E2 states that an answer must be performed for a question;

• •

E3 says that an O-move must be performed for a P-move, and vice versa.

We next review legal positions, a certain class of finite sequences of moves equipped with pointers from later to earlier occurrences in the sequences. The idea is that each non-initial occurrence in a legal position must be made for a specific previous occurrence, and pointers specify such pairs of occurrences. Technically, pointers enable us to distinguish similar yet different plays [22, §2.4] and define views (Definition 2.4). Views play crucial roles when we define constraints on strategies (Definition 2.9).

We call a finite sequence of moves together with a pointer a justified (j-) sequence. A legal position is then a particular kind of a j-sequence.

Definition 2.3** (Justified sequences [38, 35]).**

An occurrence in a finite sequence $\bm{s}$ is a pair $(\bm{s}(i),i)$ such that $i\in\overline{|\bm{s}|}$. A justified (j-) sequence is a pair $\bm{s}=(\bm{s},\mathcal{J}_{\bm{s}})$ of a finite sequence $\bm{s}$ of moves and a map $\mathcal{J}_{\bm{s}}:\overline{|\bm{s}|}\rightarrow\{0\}\cup\overline{|\bm{s}|-1}$ such that $0\leqslant\mathcal{J}_{\bm{s}}(i)<i$ for all $i\in\overline{|\bm{s}|}$, called the pointer of the j-sequence. An occurrence $(\bm{s}(i),i)$ is initial in $\bm{s}$ if $\mathcal{J}_{\bm{s}}(i)=0$. We say that the occurrence $(\bm{s}({\mathcal{J}_{\bm{s}}(i)}),\mathcal{J}_{\bm{s}}(i))$ is the justifier of a non-initial one $(\bm{s}(i),i)$ in $\bm{s}$, and $(\bm{s}(i),i)$ is justified by $(\bm{s}({\mathcal{J}_{\bm{s}}(i)}),\mathcal{J}_{\bm{s}}(i))$ in $\bm{s}$.

A j-sequence $\bm{s}$ is in an arena $G$ if its elements are moves in $G$, and its pointer respects the enabling relation $\vdash_{G}$ in $G$, i.e., \forall i\in\overline{|\bm{s}|}.\,\Big{(}\mathcal{J}_{\bm{s}}(i)=0\Rightarrow\star\vdash_{G}\bm{s}(i)\Big{)}\wedge\Big{(}\mathcal{J}_{\bm{s}}(i)\neq 0\Rightarrow\bm{s}({\mathcal{J}_{\bm{s}}(i)})\vdash_{G}\bm{s}(i)\Big{)}. We write $\mathscr{J}_{G}$ for the set of all j-sequences in $G$.

A justified (j-) subsequence of a j-sequence $\bm{s}$ is a j-sequence $\bm{t}$, written $\bm{t}\sqsubseteq\bm{s}$, such that $\bm{t}$ is a subsequence of $\bm{s}$, and $\mathcal{J}_{\bm{t}}(i)=j$ if and only if $\mathcal{J}_{\bm{s}}^{n}(i)=j$ for some $n\in\mathbb{N}^{+}$ with the occurrences $(\bm{s}(\mathcal{J}_{\bm{s}}^{k}(i)),\mathcal{J}_{\bm{s}}^{k}(i))$ for $k=1,2,\dots,n-1$ deleted in $\bm{t}$.

Remark*.*

Unlike the original formulation [35], we define j-sequences in such a way that they make sense without underlying arenas. This reformulation is convenient as it enables us to manipulate j-sequences without calculating underlying arenas.

Convention*.*

Henceforth, we are casual about the distinction between moves and occurrences, and by abuse of notation, we frequently keep the pointer $\mathcal{J}_{\bm{s}}$ of each j-sequence $\bm{s}=(\bm{s},\mathcal{J}_{\bm{s}})$ implicit since it is mostly obvious, and abbreviate occurrences $(\bm{s}(i),i)$ in $\bm{s}$ as $\bm{s}(i)$. Besides, we sometimes write $\mathcal{J}_{\bm{s}}(\bm{s}(i))=\bm{s}(j)$ if $\mathcal{J}_{\bm{s}}(i)=j>0$.

Definition 2.4** (Views [38, 34, 35]).**

The P-view $\lceil\bm{s}\rceil$ and the O-view $\lfloor\bm{s}\rfloor$ of a j-sequence $\bm{s}$ are the j-subsequences of $\bm{s}$ defined by the following induction:

• •

$\lceil\bm{\epsilon}\rceil\colonequals\bm{\epsilon}$;

• •

$\lceil\bm{s}m\rceil\colonequals\lceil\bm{s}\rceil.m$ if $m$ is a P-move;

• •

$\lceil\bm{s}m\rceil\colonequals m$ if $m$ is initial;

• •

$\lceil\bm{s}m\bm{t}n\rceil\colonequals\lceil\bm{s}\rceil.mn$ if $n$ is an O-move such that $m$ justifies $n$;

• •

$\lfloor\bm{\epsilon}\rfloor\colonequals\bm{\epsilon}$;

• •

$\lfloor\bm{s}m\rfloor\colonequals\lfloor\bm{s}\rfloor.m$ if $m$ is an O-move;

• •

$\lfloor\bm{s}m\bm{t}n\rfloor\colonequals\lfloor\bm{s}\rfloor.mn$ if $n$ is a P-move such that $m$ justifies $n$.

The idea on views is as follows. Given a nonempty j-sequence $\bm{s}m$ such that $m$ is a P- (resp. O-) move, the P-view $\lceil\bm{s}\rceil$ (resp. O-view $\lfloor\bm{s}\rfloor$) is the currently ‘relevant part’ of the previous occurrences in $\bm{s}$ for P (resp. O). I.e., P (resp. O) is concerned only with the last occurrence of an O- (resp. P-) move, its justifier and that justifier’s P- (resp. O-) view, which then recursively proceeds. See [38] for an explanation of views in terms of their counterparts in logical calculi, and [40] in lambda-calculi.

Definition 2.5** (Legal positions [22]).**

A legal position is a j-sequence $\bm{s}$ such that

• •

(Alternation) If $\bm{s}=\bm{s_{1}}mn\bm{s_{2}}$, then $\lambda^{\mathsf{OP}}(m)\neq\lambda^{\mathsf{OP}}(n)$;

• •

(Visibility) If $\bm{s}=\bm{t}m\bm{u}$ with $m$ non-initial, then $\mathcal{J}_{\bm{s}}(m)$ occurs in the P-view $\lceil\bm{t}\rceil$ if $m$ is a P-move, and in the O-view $\lfloor\bm{t}\rfloor$ otherwise.

A legal position is in an arena $G$ if it is a j-sequence in $G$ (Definition 2.3). We write $\mathscr{L}_{G}$ for the set of all legal positions in $G$.

As already noted, legal positions in an arena are to specify the basic rules of a game in the sense that positions in the game must be legal (Definition 2.6) so that

• •

During a play in the game, O makes the first move by a question (by E1),333Since the initial element $\bm{s}(1)$ of a legal position $\bm{s}$ in an arena $G$ is subject to the equation $\mathcal{J}_{\bm{s}}(1)=0$, we have $\star\vdash_{G}\bm{s}(1)$. Hence, the axiom E1 on $G$ implies $\lambda(\bm{s}(1))=\mathsf{OQ}$. and then P and O alternately make moves (by alternation), where each non-initial move is made for a specific previous occurrence, viz., its justifier;444Again, since we focus on a legal position $\bm{s}$ in an arena $G$, the justifier of each P-move occurring in $\bm{s}$ is an O-move, and vice versa, by the axiom E3 on $G$. In addition, the justifier of each answer occurring in $\bm{s}$ is a question by the axiom E2 on $G$.

• •

The justifiers of non-initial occurrences are in the ‘relevant part’ (by visibility).

2.2 Games and strategies

We are now ready to recall the central concepts of games and strategies. For technical convenience, we slightly modify the original definition of games in [35, 22]:

Definition 2.6** (Games [35, 22]).**

A game is a set $G$ of legal positions such that

$G$ is nonempty and prefix-closed (i.e., $\bm{s}m\in G\Rightarrow\bm{s}\in G$); 2. 2.

$\mathrm{Arn}(G)\colonequals(M_{G},\vdash_{G})$ is an arena, where $M_{G}\colonequals\{\,\bm{s}(i)\mid\bm{s}\in G,i\in\overline{|\bm{s}|}\,\}$ and $\vdash_{G}\,\colonequals\{\,(\star,\bm{s}(j))\mid\bm{s}\in G,\mathcal{J}_{\bm{s}}(j)=0\,\}\cup\{\,(\bm{s}(i),\bm{s}(j))\mid\bm{s}\in S,\mathcal{J}_{\bm{s}}(j)=i>0\,\}$.

It is well-founded (w.f.) if so is $\mathrm{Arn}(G)$, and well-opened (w.o.) if each of its elements has at most one initial occurrence (i.e., the conjunction of $\bm{s}m\in G$ and $m\in M_{G}^{\mathrm{Init}}$ implies $\bm{s}=\bm{\epsilon}$). We call elements of $G$ (valid) positions in $G$.

A subgame of $G$ is a game $H\subseteq G$, and \mathrm{sub}(G)\colonequals\{\,H\mid\text{H$is a subgame of$G}\,\}.

Remark*.*

The original article [35, p. 27] also imposes thread-closure on each game $G$: The thread $\bm{s}\upharpoonright\mathcal{I}\sqsubseteq\bm{s}$ of a position $\bm{s}\in G$ with respect to a given set $\mathcal{I}$ of initial occurrences in $\bm{s}$, which consists of occurrences hereditarily justified555An occurrence $n$ in a j-sequence $\bm{s}$ is hereditarily justified by another occurrence $m$ in $\bm{s}$ if $\mathcal{J}_{\bm{s}}^{i}(n)=m$ for some $i\in\mathbb{N}^{+}$ [35, p. 22]. by elements in $\mathcal{I}$, must be in $G$. This axiom is to ensure that positions in $G$ are in the exponential $\oc G$ (Definition 2.12), i.e., $G\subseteq\oc G$, which matches the intuition on exponential $\oc$ [13].

However, $\oc G$ is well-defined even if $G$ is not thread-closed. Also, we later focus on w.o. games (for the identities in the categories of games to be well-defined), which are trivially thread-closed. For these reasons, we omit thread-closure in Definition 2.6.

Each game $G$ is nonempty and prefix-closed because conceptually each nonempty position or ‘moment’ in $G$ must have the previous ‘moment.’ Note that positions in $G$ are automatically legal in the arena $\mathrm{Arn}(G)$; i.e., as noted before, the legality is the basic or minimal requirement on positions in games. We later focus on w.o., w.f. games because the identities in the categories of such games behave well (§2.3).

The tuple $\mathcal{M}(G)\colonequals(M_{G},\lambda_{G},\vdash_{G},G)$, where $\lambda_{G}:m\mapsto\lambda(m)$, forms a game in the sense of [35]666Except that the axiom E1 is slightly weakened, and the thread-closure is omitted; see the remarks after Definitions 2.2 and 2.6, respectively. whose labels are embedded into moves, which we call an MC-game. The MC-game $\mathcal{M}(G)$ satisfies: Each move $m\in M_{G}$ occurs in some position in $G$, and each pair $\star\vdash_{G}m$ or $m_{1}\vdash_{G}m_{2}$ is used in some position in $G$. Conversely, given an MC-game $H$ that satisfies these two conditions, for which we call $H$ economical, the set of all positions in $H$ forms a game. Besides, these constructions are inverses to each other. Hence, $\mathcal{M}$ is a bijection between games and economical MC-games.

Since the economical axioms only exclude unused structures, our simplification of MC-games into games is harmless. We may further dispense with arenas by directly axiomatising the effects of arenas on legal positions (Footnotes 3–4), but we do not since arenas are convenient for defining constructions on games (Definition 2.12).

Definition 2.7** (Strategies [35, 22]).**

A strategy on a game $G$ is a subset $\sigma\subseteq G^{\mathrm{Even}}$, written $\sigma:G$, that is nonempty, even-prefix-closed (i.e., $\bm{s}mn\in\sigma\Rightarrow\bm{s}\in\sigma$) and deterministic (i.e., $\bm{s}mn,\bm{s}mn^{\prime}\in\sigma\Rightarrow\bm{s}mn=\bm{s}mn^{\prime}$). Let $\mathrm{st}(G)\colonequals\{\,\sigma\mid\sigma:G\,\}$.

We define the closure of a strategy $\sigma:G$ with respect to another game $H$ to be the subgame $\overline{\sigma}_{H}\colonequals\{\bm{\epsilon}\}\cup\{\,\bm{s}m\in H^{\mathrm{Odd}}\mid\bm{s}\in\overline{\sigma}_{H}\,\}\cup\{\,\bm{t}lr\in\sigma\mid\bm{t}l\in\overline{\sigma}_{H}\,\}\subseteq\sigma\cup H$.

The idea is that a strategy $\sigma:G$ describes for P how to play on the game $G$ by the computation $\bm{s}m\in G^{\mathrm{Odd}}\mapsto\bm{s}mn\in\sigma$, which is deterministic by the determinacy of $\sigma$, and in general partial since there can be no $\bm{s}mn\in\sigma$ for some $\bm{s}m\in G^{\mathrm{Odd}}$.

We use the closure operation in §3. We leave it to the reader to verify by induction that the equation $\overline{\sigma}_{G}=\sigma\cup\{\,\bm{s}m\in G\mid\bm{s}\in\sigma\,\}$ holds for all strategies $\sigma:G$.

Example 2.8**.**

The terminal game $T\colonequals\{\bm{\epsilon}\}$ only has the strategy $\top\colonequals\{\bm{\epsilon}\}$.

The flat game on a set $S$ is the game $\mathrm{flat}(S)\colonequals\mathrm{Pref}(\{\,q^{\mathsf{OQ}}.m^{\mathsf{PA}}\mid m\in S\,\})$, where $q$ is an arbitrarily fixed element such that $q\not\in S$, and $q^{\mathsf{OQ}}$ justifies $m^{\mathsf{PA}}$. It has strategies $\bot\colonequals\{\bm{\epsilon}\}$ and $\underline{m}\colonequals\{\bm{\epsilon},qm\}$ for each $m\in S$. Consider, for instance, the empty game $\bm{0}\colonequals\mathrm{flat}(\emptyset)$ and the natural number game $N\colonequals\mathrm{flat}(\mathbb{N})$.

Next, recall that not every strategy corresponds to a proof. For instance, the empty game $\bm{0}$ models falsity, and thus the strategy $\bot:\bm{0}$ should not be an interpretation of a proof. We therefore carve out strategies for proofs as winning ones:

Definition 2.9** (Constraints on strategies [38, 41, 35, 22]).**

A strategy $\sigma:G$ is

• •

Total if it always responds: $\forall\bm{s}\in\sigma,\bm{s}m\in G.\,\exists\bm{s}mn\in\sigma$;

• •

Innocent if it only depends on P-views: $\forall\bm{s}mn\in\sigma,\bm{t}l\in G.\,\lceil\bm{s}m\rceil=\lceil\bm{t}l\rceil\Rightarrow\exists\bm{t}lr\in\sigma.\,\lceil\bm{s}mn\rceil=\lceil\bm{t}lr\rceil$;

• •

Noetherian if there is no strictly increasing (with respect to the prefix relation $\preceq$) infinite sequence of elements in the set $\lceil\sigma\rceil\colonequals\{\,\lceil\bm{s}\rceil\mid\bm{s}\in\sigma\,\}$;

• •

Winning if it is total, innocent and noetherian;

• •

Well-bracketed (w.b.) if its ‘question-answering’ in P-views is in the ‘last-question-first-answered’ fashion: If $\bm{s}q\bm{t}a\in\sigma$, where $\lambda^{\mathsf{QA}}(q)=\mathsf{Q}$, $\lambda^{\mathsf{QA}}(a)=\mathsf{A}$ and $\mathcal{J}_{\bm{s}q\bm{t}a}(a)=q$, then each question occurring in $\bm{t^{\prime}}$, where the P-view $\lceil\bm{s}q\bm{t}\rceil$ is of the form $\lceil\bm{s}q\bm{t}\rceil=\lceil\bm{s}q\rceil.\bm{t^{\prime}}$ by visibility, justifies an answer occurring in $\bm{t^{\prime}}$.

Example 2.10**.**

The strategies $\top:T$ and $\underline{n}:N$ for all $n\in\mathbb{N}$ are winning and w.b., while the strategies $\bot:\bm{0}$ and $\bot:N$ are not even total, let alone winning.

We think of winning strategies as proofs in classical logic as follows. First, proofs should not get ‘stuck,’ and so strategies for proofs must be total. Next, imposing innocence on strategies corresponds to excluding stateful terms [22, §2.9]. Since logic is concerned with truths, which are independent of ‘passage of time,’ proofs should not depended on ‘states of arguments.’ Hence, we impose innocence on strategies for proofs. In addition, we need noetherianity to handle infinite plays: If a play by an innocent, noetherian strategy keeps growing infinitely, then it cannot be P’s ‘intention,’ and so the play must be win for P. Technically, noetherianity is crucial for the closure of winning strategies under composition (Definition 2.14) [38].

Further, well-bracketing bans classical reasoning or control operators [22, §2.10]. Hence, we regard winning, w.b. strategies as proofs in intuitionistic logic.

2.3 Constructions on games and strategies

In this section, we briefly recall constructions on games and strategies. Since they are standard in the literature, we leave expositions and examples to [22, §3.2].

Convention*.*

We omit ‘tags’ for disjoint union $\uplus$. For instance, we write $x\in A\uplus B$ if $x\in A$ or $x\in B$; given relations $R_{A}\subseteq A\times A$ and $R_{B}\subseteq B\times B$, we write $R_{A}\uplus R_{B}$ for the relation on $A\uplus B$ such that $(x,y)\in R_{A}\uplus R_{B}\stackrel{{\scriptstyle\mathrm{df.}}}{{\Leftrightarrow}}(x,y)\in R_{A}\vee(x,y)\in R_{B}$.

Definition 2.11** (Constructions on arenas [35]).**

Given arenas $A$ and $B$, we define

• •

$A\uplus B\colonequals(M_{A}\uplus M_{B},\vdash_{A}\uplus\vdash_{B})$;

• •

$A\multimap B\colonequals(\{\,a^{(x^{\bot})y}\mid a^{xy}\in M_{A}\,\}\uplus M_{B},\vdash_{A\multimap B})$, $\mathsf{O}^{\bot}\colonequals\mathsf{P}$, $\mathsf{P}^{\bot}\colonequals\mathsf{O}$, $\star\vdash_{A\multimap B}m:\Leftrightarrow\star\vdash_{B}m$ and $m\vdash_{A\multimap B}n:\Leftrightarrow m\vdash_{A}n\vee m\vdash_{B}n\vee(\star\vdash_{B}m\wedge\star\vdash_{A}n)$.

Definition 2.12** (Constructions on games [35]).**

Given games $G$ and $H$, we define

• •

$G\otimes H\colonequals\{\,\bm{s}\in\mathscr{L}_{\mathrm{Arn}(G)\uplus\mathrm{Arn}(H)}\mid\forall X\in\{G,H\}.\,\bm{s}\upharpoonright X\in X\,\}$, called the tensor of $G$ and $H$, where $\bm{s}\upharpoonright X\sqsubseteq\bm{s}$ consists of occurrences of moves in $X$;

• •

$\oc G\colonequals\{\,\bm{s}\in\mathscr{L}_{\mathrm{Arn}(G)}\mid\forall i\in|\bm{s}|.\,\mathcal{J}_{\bm{s}}(i)=0\Rightarrow\bm{s}\upharpoonright\{(\bm{s}(i),i)\}\in G\,\}$, called the exponential of $G$, where $\bm{s}\upharpoonright\{(\bm{s}(i),i)\}\sqsubseteq\bm{s}$ consists of occurrence in $\bm{s}$ hereditarily justified (Footnote 5) by the initial occurrence $(\bm{s}(i),i)$ in $\bm{s}$;

• •

$G\mathbin{\&}H\colonequals\{\,\bm{s}\in\mathscr{L}_{\mathrm{Arn}(G)\mathbin{\uplus}\mathrm{Arn}(H)}\mid(\bm{s}\upharpoonright G\in G\wedge\bm{s}\upharpoonright H=\bm{\epsilon})\vee(\bm{s}\upharpoonright G=\bm{\epsilon}\wedge\bm{s}\upharpoonright H\in H)\,\}$, called the product of $G$ and $H$;

• •

$G\multimap H\colonequals\{\,\bm{s}\in\mathscr{L}_{\mathrm{Arn}(G)\multimap\mathrm{Arn}(H)}\mid\bm{s}\upharpoonright G^{\bot}\in G,\bm{s}\upharpoonright H\in H\,\}$, also written $H^{G}$, where $\bm{s}\upharpoonright G^{\bot}$ is obtained from $\bm{s}\upharpoonright G$ by modifying all the moves $m^{(x^{\bot})y}$ occurring in $\bm{s}\upharpoonright G$ into $m^{xy}$, called the linear implication from $G$ to $H$;

• •

$G\Rightarrow H\colonequals\oc G\multimap H$, called the implication from $G$ to $H$.

Notationally, exponential $\oc$ precedes other constructions on games, while tensor $\otimes$ and product $\mathbin{\&}$ do linear implication $\multimap$ and implication $\Rightarrow$.

Lemma 2.13** (Well-defined constructions on games).**

Games and w.f. games are closed under $\otimes$, $\mathbin{\&}$, $\oc$ and $\multimap$, and w.o. ones under $\&$, $\multimap$ and $\Rightarrow$.

Proof.

See [35] for the closure of MC-games under these constructions. The proof is essentially the same for games. The preservation of w.f. (resp. w.o.) ones is clear. ∎

We leave it to the reader to verify that these constructions on games correspond to those on economical MC-games [35] under the bijection $\mathcal{M}$ (except that we have to exclude unused moves and enabled pairs from an MC-game $G\multimap H$ if $H=T$).

Definition 2.14** (Constructions on strategies [35]).**

Given strategies $\phi:A\multimap B$, $\sigma:C\multimap D$, $\tau:A\multimap C$, $\psi:B\multimap C$ and $\theta:\oc A\multimap B$, we define

• •

$\mathrm{cp}_{A}\colonequals\{\,\bm{s}\in(A_{[0]}\multimap A_{[1]})^{\mathrm{Even}}\mid\forall\bm{t}\preceq\bm{s}.\,\mathrm{Even}(\bm{t})\Rightarrow\bm{t}\upharpoonright A_{[0]}^{\bot}=\bm{t}\upharpoonright A_{[1]}\,\}$, called the copy-cat on $A$;

• •

$\mathrm{der}_{A}\colonequals\{\,\bm{s}\in(\oc A\multimap A)^{\mathrm{Even}}\mid\forall\bm{t}\preceq\bm{s}.\,\mathrm{Even}(\bm{t})\Rightarrow\bm{t}\upharpoonright\oc A^{\bot}=\bm{t}\upharpoonright A\,\}$, called the dereliction on $A$;

• •

$\phi\otimes\sigma\colonequals\{\,\bm{s}\in A\otimes C\multimap B\otimes D\mid\bm{s}\upharpoonright A,B\in\phi,\bm{s}\upharpoonright C,D\in\sigma\,\}$, called the tensor of $\phi$ and $\sigma$, where $\bm{s}\upharpoonright A,B\sqsubseteq\bm{s}$ (resp. $\bm{s}\upharpoonright C,D\sqsubseteq\bm{s}$) consists of occurrences of moves in $A$ or $B$ (resp. $C$ or $D$);

• •

$\langle\phi,\tau\rangle\colonequals\{\,\bm{s}\in A\multimap B\mathbin{\&}C\mid(\bm{s}\upharpoonright A,B\in\phi\wedge\bm{s}\upharpoonright C=\bm{\epsilon})\vee(\bm{s}\upharpoonright A,C\in\tau\wedge\bm{s}\upharpoonright B=\bm{\epsilon})\,\}$, called the pairing of $\phi$ and $\tau$;

• •

$\phi;\psi\colonequals\{\,\bm{s}\upharpoonright A,C\mid\bm{s}\in\phi\parallel\psi\,\}$, called the composition of $\phi$ and $\psi$, where $\phi\parallel\psi\colonequals\{\,\bm{s}\in\mathscr{J}\mid\bm{s}\upharpoonright A,B_{[0]}\in\phi,\bm{s}\upharpoonright B_{[1]},C\in\psi,\bm{s}\upharpoonright B_{[0]}^{\bot},B_{[1]}^{\bot}\in\mathrm{cp}_{B}\,\}$, $\mathscr{J}\colonequals\mathscr{J}_{\mathrm{Arn}(((A\multimap B_{[0]})\multimap B_{[1]})\multimap C)}$, $\bm{s}\upharpoonright B_{[0]}^{\bot},B_{[1]}^{\bot}$ is obtained from $\bm{s}\upharpoonright B_{[0]},B_{[1]}$ by applying the operation $(\_)^{\bot}$ on all the moves, and $\phi;\psi$ is also written $\psi\circ\phi$;

• •

$\theta^{\dagger}\colonequals\{\,\bm{s}\in(\oc A\multimap\oc B)^{\mathrm{Even}}\mid\forall i\in|\bm{s}|.\,\mathcal{J}_{\bm{s}}(i)=0\Rightarrow\bm{s}\upharpoonright\{(\bm{s}(i),i)\}\in\theta\,\}$, called the promotion of $\theta$.

For the dereliction $\mathrm{der}_{A}$ to be well-defined, we have to focus on w.o. games $A$; see [35, pp. 42–43]. Although w.o. games are not closed under exponential $\oc$, it does not matter for us, like [35, p. 43], since we only need cartesian closure, not exponential $\oc$ itself, and w.o. games are closed under implication $\Rightarrow$ and product $\&$ (Lemma 2.13).

Lemma 2.15** (Well-defined constructions on strategies).**

If $\phi:A\multimap B$, $\sigma:C\multimap D$, $\tau:A\multimap C$, $\psi:B\multimap C$ and $\theta:\oc A\multimap B$, then $\mathrm{cp}_{A}:A\multimap A$, $\phi\otimes\sigma:A\otimes C\multimap B\otimes D$, $\langle\phi,\tau\rangle:A\multimap B\mathbin{\&}C$, $\phi;\psi:A\multimap C$ and $\theta^{\dagger}:\oc A\multimap\oc B$; also, $\mathrm{der}_{B}:B\Rightarrow B$ if $B$ is w.o. Moreover, $\mathrm{cp}_{A}$ (resp. $\mathrm{der}_{B}$) is winning and w.b. if $A$ is w.f. (resp. if $B$ is w.o. and w.f.), and $\otimes$, $\langle\_,\_\rangle$, $\circ$ and $(\_)^{\dagger}$ preserve winning and well-bracketing.

Proof.

The only nontrivial point not shown in [35] is that $\mathrm{cp}_{A}$ is noetherian if $A$ is w.f. (the case for $\mathrm{der}_{B}$ is the same). Note that $\mathrm{cp}_{A}$ is total, innocent and w.b. even if $A$ is not w.f. Given $\bm{s}mm\in\mathrm{cp}_{A}$, we see by induction on $|\bm{s}|$ that the P-view $\lceil\bm{s}m\rceil$ is of the form $m_{1}m_{1}m_{2}m_{2}\dots m_{k}m_{k}m$, and therefore there is a sequence $\star\vdash_{A}m_{1}\vdash_{A}m_{2}\dots\vdash_{A}m_{k-1}\vdash_{A}m_{k}\vdash_{A}m$. Hence, $\mathrm{cp}_{A}$ is noetherian if $A$ is w.f. ∎

Definition 2.16** (Categories of games [35, 22]).**

The category $\mathbb{G}$ consists of

• •

W.o. games as objects;

• •

Strategies on the implication $A\Rightarrow B$ as morphisms $A\rightarrow B$;

• •

The composition $\psi\bullet\phi\colonequals\psi\circ\phi^{\dagger}:A\Rightarrow C$ of strategies as the composition of morphisms $\phi:A\rightarrow B$ and $\psi:B\rightarrow C$;

• •

The dereliction $\mathrm{der}_{A}$ as the identity on each object $A$.

The subcategory $\mathbb{LG}$ (resp. $\mathbb{WG}$) of $\mathbb{G}$ consists of w.f., w.o. games as objects, and winning (resp. winning, w.b.) strategies as morphisms.

Games in $\mathbb{G}$ (resp. $\mathbb{LG}$ and $\mathbb{WG}$) are w.o. (resp. w.o. and w.f.) for the identities to be well-defined (Lemma 2.15). Strategies in $\mathbb{G}$ embody unconstrained, general computations. In contrast, strategies in $\mathbb{LG}$ (resp. $\mathbb{WG}$) are winning (resp. winning and w.b.), embodying proofs in classical logic (resp. proofs in intuitionistic logic).

These categories are cartesian closed, where a terminal object, product and exponential objects are the terminal game $T$, product $\mathbin{\&}$ and implication $\Rightarrow$, respectively. Since our morphisms are the same as those in the cartesian closed categories of MC-games [22], they satisfy the equational axioms on cartesian closure in the same way.

Therefore, by Lemmata 2.13 and 2.15, we conclude:

Theorem 2.17** (Well-defined cartesian closed categories of games).**

The structures $\mathbb{G}$, $\mathbb{LG}$ and $\mathbb{WG}$ form cartesian closed categories.

Notation*.*

We employ the following notations:

• •

Given a strategy $\sigma:G$, we write $\sigma^{T}:T\multimap G$ and $\sigma^{\oc T}:T\Rightarrow G$ for the evident strategies that coincide with $\sigma$ up to ‘tags’;

• •

Given strategies $\phi:T\multimap G$ and $\phi^{\prime}:T\Rightarrow G$, we write $\phi_{T},\phi^{\prime}_{\oc T}:G$ for the evident strategies that coincide with $\phi$ and $\phi^{\prime}$ up to ‘tags’ respectively;

• •

Given strategies $\psi:A\multimap B$ and $\alpha:A$, we define $\psi\circ\alpha\colonequals(\psi\circ\alpha^{T})_{T}:B$;

• •

Given strategies $\alpha:A$ and $\beta:B$, we define $\alpha\otimes\beta\colonequals((\alpha^{T}\otimes\beta^{T})\circ\iota)_{T}:A\otimes B$, where $\iota$ is the unique strategy on $T\multimap T\otimes T$, and $\langle\alpha,\beta\rangle\colonequals\langle\alpha^{T},\beta^{T}\rangle_{T}:A\mathbin{\&}B$;

• •

Given a strategy $\alpha:A$, we define $\alpha^{\dagger}\colonequals((\alpha^{\oc T})^{\dagger})_{\oc T}:\oc A$.

3 Predicate games

Having reviewed games and strategies in §2, let us now initiate our contributions. Before going into details, we sketch our idea in the following paragraphs. In short, our main challenge is to interpret Sigma-types without destroying the non-inductive nature of game semantics or the additive nature of product $\&$ (§1.4), and we achieve it by generalising games. On the other hand, we keep strategies unchanged so that our method retains the advantages of game semantics such as intensionality (§1.2).

Naively, we can interpret each dependent type $\mathsf{x:C\vdash D(x)\ type}$ by a family $D=(D(\sigma))_{\sigma:C}$ of games $D(\sigma)$ indexed by strategies $\sigma$ on the game $C$ that models the simple type $\mathsf{C}$. In the presence of Sigma-types, dependent types with only a single variable cover those with more than one variable, and so we focus on the former.

In light of product $\&$ (Definition 2.12), which models a particular kind of Sigma-types, viz., product types, it seems a natural idea to model the Sigma-type $\mathsf{\Sigma_{x:C}D(x)}$ by a subgame $\Sigma(C,D)\subseteq C\mathbin{\&}\bigcup_{\sigma:C}D(\sigma)$ such that strategies on $\Sigma(C,D)$ are the pairings $\langle\sigma,\tau\rangle$ of $\sigma:C$ and $\tau:D(\sigma)$. However, this idea does not work since

Each game $G$, by definition, determines the set $\mathrm{st}(G)$ of all strategies on $G$; 2. 2.

It is impossible for P, when playing on such a game $\Sigma(C,D)$, if any, to fix a strategy $\sigma:C$, let alone a game $D(\sigma)$, at the beginning of a play.

As an example of the first problem, consider a dependent type $\mathsf{x:N\vdash N_{b}(x)\ type}$ such that the canonical terms of the simple type $\mathsf{N_{b}(\underline{k})}$ ($k\in\mathbb{N}$) are numerals $\mathsf{\underline{n}}$ such that $n\leqslant k$, and assume that we model $\mathsf{N_{b}}$ by the family $N_{b}=(N_{b}(\sigma))_{\sigma:N}$ of games $N_{b}(\sigma)$ defined by $N_{b}(\underline{k})\colonequals\mathrm{Pref}(\{\,qn\mid n\leqslant k\,\})$ ($k\in\mathbb{N}$) and $N_{b}(\bot)\colonequals N$. However, there is no subgame $G\subseteq N\mathbin{\&}\bigcup_{\sigma:N}N_{b}(\sigma)=N\mathbin{\&}N$ such that $\langle\underline{k},\underline{n}\rangle:G$ if and only if $\underline{n}:N_{b}(\underline{k})$ for all $k,n\in\mathbb{N}$ since if such a game $G$ existed, then $\langle\underline{0},\underline{0}\rangle,\langle\underline{1},\underline{1}\rangle:G$, which implies $\langle\underline{0},\underline{1}\rangle:G$ by the definition of strategies on a game (Definition 2.7), a contradiction. Hence, no game can properly model the Sigma-type $\mathsf{\Sigma_{x:N}N_{b}(x)}$.

Let us next give an example of the second problem. Let $\mathsf{x:N\vdash List_{N}(x)\ type}$ be a dependent type such that the canonical terms of the simple type $\mathsf{List_{N}(\underline{k})}$ ($k\in\mathbb{N}$) are the $k$-lists of numerals, and assume that we model $\mathsf{List_{N}}$ by the family $\mathrm{List}_{N}=(\mathrm{List}_{N}(\sigma))_{\sigma:N}$ of games $\mathrm{List}_{N}(\sigma)$ such that $\mathrm{List}_{N}(\underline{k})$ ($k\in\mathbb{N}$) is the $k$-ary tensor $\otimes$ on $N$, where $\mathrm{List}_{N}(\underline{0})\colonequals T$, and $\mathrm{List}_{N}(\bot)\colonequals\bigcup_{k\in\mathbb{N}}\mathrm{List}_{N}(\underline{k})$. If there were a subgame $H\subseteq N\mathbin{\&}\bigcup_{\sigma:N}\mathrm{List}_{N}(\sigma)$ that models the Sigma-type $\mathsf{\Sigma_{x:N}List_{N}(x)}$, then the pairings $\langle\underline{k},\underline{n_{1}}\otimes\underline{n_{2}}\otimes\cdots\otimes\underline{n_{k}}\rangle$ for all $k,n_{1},n_{2},\dots,n_{k}\in\mathbb{N}$ would be total on $H$ since strategies for proofs must be winning (§2.2). However, there is no such $H$ since O may select, by his first move, e.g., the $(k+1)$st component of $\mathrm{List}_{N}(\underline{k+1})$.

We have seen the two fundamental limitations of games in modelling Sigma-types. We solve this problem by generalising games to pairs $\Gamma=(|\Gamma|,\|\Gamma\|)$ of a game $|\Gamma|$ and a family $\|\Gamma\|=(\Gamma(\gamma))_{\gamma:|\Gamma|}$ of subgames $\Gamma(\gamma)\subseteq|\Gamma|$, called predicate (p-) games, and define strategies $\gamma$ on $\Gamma$, written $\gamma:\Gamma$, to be those $\gamma:|\Gamma|$ satisfying $\overline{\gamma}_{\Gamma(\gamma)}^{\mathrm{Even}}:\Gamma(\gamma)$. That is, a p-game $\Gamma$ is a game $|\Gamma|$ equipped with the specification $\|\Gamma\|$ for strategies $\gamma:|\Gamma|$ to be on $\Gamma$: The restriction of $\gamma$ to $\Gamma(\gamma)$, i.e., $\overline{\gamma}_{\Gamma(\gamma)}^{\mathrm{Even}}$, is a strategy on $\Gamma(\gamma)$.

A play in a p-game $\Gamma$ then proceeds as follows. First, Judge (J) asks P a question $q_{\Gamma}$ (‘What is your strategy?’) and P answers it by a strategy $\gamma:\Gamma$ (‘It is $\gamma$!’). After this initial protocol between J and P, an ordinary play on the game $\Gamma(\gamma)$ between P and O follows, in which P must employ the declared strategy $\gamma$ restricted to $\Gamma(\gamma)$, i.e., $\overline{\gamma}_{\Gamma(\gamma)}^{\mathrm{Even}}:\Gamma(\gamma)$. Accordingly, $\gamma:\Gamma$ is winning (resp. w.b.) if so is $\overline{\gamma}_{\Gamma(\gamma)}^{\mathrm{Even}}:\Gamma(\gamma)$.

This generalisation of games to p-games solves the first problem as follows. Let us define a p-game $\Sigma(N,N_{b})$ by $|\Sigma(N,N_{b})|\colonequals N\mathbin{\&}N$ and \Sigma(N,N_{b})(\langle\sigma,\tau\rangle)\colonequals\begin{cases}N\mathbin{\&}N_{b}(\underline{k})&\text{if \sigma=\underline{k}$for some$k\in\mathbb{N}}\\ N\mathbin{\&}N&\text{otherwise}\end{cases} for all $\langle\sigma,\tau\rangle:|\Sigma(N,N_{b})|$. Then, observe that strategies on the p-game $\Sigma(N,N_{b})$ are the pairings $\langle\sigma,\tau\rangle:N\mathbin{\&}N$ such that $\tau:N_{b}(\underline{k})$ if $\sigma=\underline{k}$. For instance, typical plays by the strategy $\langle\underline{7},\underline{3}\rangle:\Sigma(N,N_{b})$ are

{mathpar}

$\Sigma(N,$

$N_{b})$

$q_{\Sigma(N,N_{b})}$

$\langle\underline{7},\underline{3}\rangle$

$q$

$7$

and

$\Sigma(N,$

$N_{b})$

$q_{\Sigma(N,N_{b})}$

$\langle\underline{7},\underline{3}\rangle$

$q$

$3$

where J first asks P the question $q_{\Sigma(N,N_{b})}$ (‘What is your strategy?’), and P answers it by $\langle\underline{7},\underline{3}\rangle:\Sigma(N,N_{b})$ (‘It is $\langle\underline{7},\underline{3}\rangle$!’); then, an ordinary play between P and O on the game $\Sigma(N,N_{b})(\langle\underline{7},\underline{3}\rangle)=N\mathbin{\&}N_{b}(\underline{7})$ follows, where P must play by $\overline{\langle\underline{7},\underline{3}\rangle}_{N\mathbin{\&}N_{b}(\underline{7})}^{\mathrm{Even}}=\langle\underline{7},\underline{3}\rangle$. The arrows in the diagram represent pointers in j-sequences (Definition 2.3).

Although the declaration of a strategy is not necessary in this example, it is clear why P cannot play by, e.g., $\langle\underline{0},\underline{1}\rangle$ on $\Sigma(N,N_{b})$: $\overline{\langle\underline{0},\underline{1}\rangle}_{N\mathbin{\&}N_{b}(\underline{0})}^{\mathrm{Even}}\not\subseteq\Sigma(N,N_{b})(\langle\underline{0},\underline{1}\rangle)$. In this way, the specification $\|\Sigma(N,N_{b})\|$ solves the first problem by filtering strategies.

Moreover, the declaration of a strategy solves the second problem: The p-game $\Sigma(N,\mathrm{List}_{N})$ defined by $\Sigma(N,\mathrm{List}_{N})(\underline{k})\colonequals N\mathbin{\&}(\underbrace{N\otimes N\otimes\dots\otimes N}_{k})$ for all $k\in\mathbb{N}$, $\Sigma(N,\mathrm{List}_{N})(\bot)\colonequals\bigcup_{k\in\mathbb{N}}\Sigma(N,\mathrm{List}_{N})(\underline{k})$ and $|\Sigma(N,\mathrm{List}_{N})|\colonequals\Sigma(N,\mathrm{List}_{N})(\bot)$ models the Sigma-type $\mathsf{\Sigma_{x:N}List_{N}(x)}$. Typical plays in $\Sigma(N,\mathrm{List}_{N})$ look like

{mathpar}

$\Sigma(N,$

$\mathrm{List}_{N})$

$q_{\Sigma(N,\mathrm{List}_{N})}$

$\langle\underline{2},\underline{1}\otimes\underline{3}\rangle$

$q$

$2$

and

$\Sigma(N,$

$\mathrm{List}_{N})$

$q_{\Sigma(N,\mathrm{List}_{N})}$

$\langle\underline{2},\underline{1}\otimes\underline{3}\rangle$

$q$

$3$

$q$

$1$

where the declaration of the strategy $\langle\underline{2},\underline{1}\otimes\underline{3}\rangle:\Sigma(N,\mathrm{List}_{N})$ fixes the underlying game $N\mathbin{\&}(N\otimes N)$. Thus, $\overline{\langle\underline{2},\underline{1}\otimes\underline{3}\rangle}_{N\mathbin{\&}(N\otimes N)}^{\mathrm{Even}}=\langle\underline{2},\underline{1}\otimes\underline{3}\rangle$ is total on $\Sigma(N,\mathrm{List}_{N})$.

In this way, we achieve game semantics of Sigma-types directly without the list construction of Abramsky et al. [23, 29] (§1.4). Let us add another important point that their method cannot properly interpret the Sigma-type $\mathsf{\Sigma(N,List_{N})}$ since total strategies on their interpretation of this Sigma-type are the lists $(\underline{k},\underline{n_{1}}\otimes\underline{n_{2}}\otimes\dots)$ of strategies, where the second component is an infinite iteration of tensor $\otimes$, due to the O-sat operation [29, Remark 4.5]; we come back to this point in §4.3.

Besides, our interpretation of Sigma-types retains the additive nature of product $\&$ because a play in the interpretation occurs in either side, not both, which is in contrast with the interpretation of Sigma-types by Blot and Laird [24] (§1.4).

Finally, we justify p-games, in particular the use of J, as a generalisation of games as follows. First, J is also assumed at least implicitly in conventional games as well since there must be someone other than P or O to check if j-sequences played by P and O are valid positions in the underlying game. Hence, the use of J is not a big departure from games. However, this argument is only conceptual, and the following mathematical arguments matter much more. Second, even in the literature of game semantics, P always plays by a fixed strategy as well. Besides, this predetermination of a strategy does not lose generality since each position $\bm{s}$ in a game $G$ is the result of a play by some $\sigma:G$, viz., $\sigma\colonequals\mathrm{Pref}(\{\bm{s}\})^{\mathrm{Even}}$. Third, the initial two elements played in p-games are by J and P, not O and P, so that p-games inherit the intensionality of games: Strategies for P are revealed to O only gradually along the development of a play. I.e., the declaration of a strategy by P is hidden from O, so that O can see the strategy only gradually via his play against the strategy (as in the case of games). Technically, we implement this idea by excluding the initial two elements from ordinary plays (especially from O-views). Dually, O’s strategy on the domain $\Gamma$ of a linear implication $\Gamma\multimap\Delta$ between p-games is revealed only gradually to P via plays. Consequently, the extensions of strategies on $\Gamma\multimap\Delta$ are continuous maps as in the case of games. More generally, since our strategies are just the ordinary ones, our method inherits the intensionality of standard game semantics; see §4.6–4.7.

In summary, since the declarations of strategies by P and O are invisible to each other, plays in p-games proceed just like those in games, and our approach inherits the intensionality of game semantics. We emphasise this intensionality since due to the declarations the reader may mistake our model to be close to extensional ones.

The rest of this section proceeds as follows. We first define p-games in §3.1, and then generalise constructions on games (§2.3) to p-games in §3.2. In these sections, we slightly modify and formalise the aforementioned interpretation of dependent types (Definition 3.3) as well as the examples $\mathrm{List}_{N}$ and $N_{b}$ (Example 4.2).

3.1 Predicate games

We reformulate the idea of p-games $\Gamma=(|\Gamma|,\|\Gamma\|)$ sketched above in a handier way as follows. First, recall that the closure $\overline{\gamma}_{|\Gamma|}$ of a strategy $\gamma:|\Gamma|$ with respect to the ambient game $|\Gamma|$ is characterised by a simple form $\overline{\gamma}_{|\Gamma|}=\gamma\cup\{\,\bm{s}m\in|\Gamma|\mid\bm{s}\in\gamma\,\}$.

Second, the central condition $\overline{\gamma}_{\Gamma(\gamma)}^{\mathrm{Even}}:\Gamma(\gamma)$ is equivalent to another relation $\overline{\gamma}_{|\Gamma|}\preccurlyeq\Gamma(\gamma)$, where the symbol $\preccurlyeq$ denotes Chroboczek’s beautiful liveness ordering:

Definition 3.1** (Liveness ordering [42]).**

The liveness ordering is a partial order $\preccurlyeq$ between games [42, Definition 8 and Theorem 9], which defines $G\preccurlyeq H$ to mean that O (resp. P) is less (resp. more) restricted in $G$ than in $H$, i.e., they satisfy

If $\bm{s}\in(G\cap H)^{\mathrm{Even}}$ and $\bm{s}m\in H^{\mathrm{Odd}}$, then $\bm{s}m\in G^{\mathrm{Odd}}$; 2. 2.

If $\bm{t}l\in(G\cap H)^{\mathrm{Odd}}$ and $\bm{t}lr\in G^{\mathrm{Even}}$, then $\bm{t}lr\in H^{\mathrm{Even}}$.

Proposition 3.2** (Liveness characterisation).**

Assume $\sigma:G$ and $H\in\mathrm{sub}(G)$.

$\overline{\sigma}_{H}^{\mathrm{Even}}:H$* if and only if $\overline{\sigma}_{G}\preccurlyeq H$;* 2. 2.

If $\overline{\sigma}_{G}\preccurlyeq H$, then $\overline{\sigma}_{H}^{\mathrm{Even}}=\sigma\cap H$.

Proof.

We focus on the first clause since it is just a routine to verify the second one.

First, it is straightforward to see that the relation $\overline{\sigma}_{H}^{\mathrm{Even}}:H$ is equivalent to the subset relation $\overline{\sigma}_{H}^{\mathrm{Even}}\subseteq H^{\mathrm{Even}}$. Hence, it suffices to show $\overline{\sigma}_{H}^{\mathrm{Even}}\subseteq H^{\mathrm{Even}}$ if and only if $\overline{\sigma}_{G}\preccurlyeq H$. The sufficiency ($\Leftarrow$) is shown straightforwardly by the induction on the lengths of positions, which we leave to the reader; we focus on the necessity ($\Rightarrow$).

Assume $\overline{\sigma}_{G}\not\preccurlyeq H$; it remains to show $\overline{\sigma}_{H}^{\mathrm{Even}}\not\subseteq H^{\mathrm{Even}}$. By $\overline{\sigma}_{G}\not\preccurlyeq H$, there is some $\bm{s}mn\in\overline{\sigma}_{G}^{\mathrm{Even}}$ such that $\bm{s}m\in\overline{\sigma}_{G}\cap H$ and $\bm{s}mn\not\in H$. Note that $\bm{s}mn\in\overline{\sigma}_{G}^{\mathrm{Even}}$ implies $\bm{s}mn\in\sigma$. We also see by induction on the lengths of positions that $\overline{\sigma}_{G}\cap H\subseteq\overline{\sigma}_{H}$ holds, whence $\bm{s}m\in\overline{\sigma}_{H}$. Then, $\bm{s}mn\in\overline{\sigma}_{H}$ follows from $\bm{s}m\in\overline{\sigma}_{H}$ and $\bm{s}mn\in\sigma$. We have shown $\overline{\sigma}_{H}^{\mathrm{Even}}\not\subseteq H^{\mathrm{Even}}$ since $\bm{s}mn\in\overline{\sigma}_{H}^{\mathrm{Even}}$ and $\bm{s}mn\not\in H^{\mathrm{Even}}$. ∎

Proposition 3.2 reduces the relation $\overline{\gamma}_{\Gamma(\gamma)}^{\mathrm{Even}}:\Gamma(\gamma)$ to another $\overline{\gamma}_{|\Gamma|}\preccurlyeq\Gamma(\gamma)$, where $\overline{\gamma}_{|\Gamma|}$ is often easier to handle than $\overline{\gamma}_{\Gamma(\gamma)}^{\mathrm{Even}}$ by its simple form $\overline{\gamma}_{|\Gamma|}=\gamma\cup\{\,\bm{s}m\in|\Gamma|\mid\bm{s}\in\gamma\,\}$.

Finally, if $\overline{\gamma}_{|\Gamma|}\preccurlyeq\Gamma(\gamma)$, then Proposition 3.2 simplifies $\overline{\gamma}_{\Gamma(\gamma)}^{\mathrm{Even}}$ by $\overline{\gamma}_{\Gamma(\gamma)}^{\mathrm{Even}}=\gamma\cap\Gamma(\gamma)$.

We are now ready to introduce the central concept of the present work:

Definition 3.3** (Predicate games).**

A predicate (p-) game is a pair $\Gamma=(|\Gamma|,\|\Gamma\|)$ of a game $|\Gamma|$ and a family $\|\Gamma\|=(\Gamma(\gamma))_{\gamma:|\Gamma|}$ of subgames $\Gamma(\gamma)\subseteq|\Gamma|$. It is well-founded (w.f.) (resp. well-opened (w.o.)) if so is the game $|\Gamma|$.

A strategy on $\Gamma$, written $\gamma:\Gamma$, is a strategy $\gamma:|\Gamma|$ that satisfies $\overline{\gamma}_{|\Gamma|}\preccurlyeq\Gamma(\gamma)$. It is total (resp. innocent, noetherian, w.b.) if so is the strategy $\gamma\cap\Gamma(\gamma):\Gamma(\gamma)$.

Let $\mathrm{st}(\Gamma)\colonequals\{\,\gamma\mid\gamma:\Gamma\,\}$ and $\overline{\gamma}_{\Gamma}\colonequals\overline{\gamma}_{\Gamma(\gamma)}$ ($\gamma:\Gamma$). A position in $\Gamma$ is a prefix of a sequence $q_{\Gamma}\gamma\bm{s}$ such that $\gamma:\Gamma$ and $\bm{s}\in\overline{\gamma}_{\Gamma}$, where $q_{\Gamma}$ is an arbitrarily fixed element such that $q_{\Gamma}\not\in M_{|\Gamma|}$, $q_{\Gamma}\gamma$ is an initial protocol, and $\bm{s}$ is an actual position.

A play in a p-game $\Gamma$ proceeds as follows. First, Judge (J) asks P a question $q_{\Gamma}$ (‘What is your strategy?’), and P answers it by a strategy $\gamma:\Gamma$ (‘It is $\gamma$!’). After this initial protocol $q_{\Gamma}\gamma$, an ordinary play on the game $\Gamma(\gamma)$ between O and P follows, in which P must play by $\gamma$ restricted to $\Gamma(\gamma)$, i.e., $\gamma\cap\Gamma(\gamma):\Gamma(\gamma)$. The crucial points of p-games are that P can only select a strategy $\gamma:|\Gamma|$ that satisfies $\overline{\gamma}_{|\Gamma|}\preccurlyeq\Gamma(\gamma)$ in the initial protocol, and the declaration of $\gamma:\Gamma$ fixes the underlying game $\Gamma(\gamma)$.

In essence, the game-semantic counterpart of the path from STLC to MLTT (§1.1) is the family $\|\Gamma\|$ added to the game $|\Gamma|$, which brings these strategy filtering and game fixing abilities to $|\Gamma|$. As we have seen, the first and the second abilities address the first and the second problems listed at the beginning of §3, respectively.

If initial protocols were part of ordinary plays or visible to O, then by duality those on the domain of each linear implication would be visible to P, so that the extensions of strategies on linear implication may not be continuous. This extensionality would be undesirable for the intensional nature of game semantics. We address this point by excluding initial protocols from actual positions. In particular, initial protocols are out of the scope of P- and O-views since pointers are only on actual positions.

Example 3.4**.**

Given a game $G$, we define the p-game $\mathscr{P}(G)\colonequals(G,\kappa_{G})$, where $\kappa_{G}$ is the constant family at $G$. Clearly, $\mathrm{st}(\mathscr{P}(G))=\mathrm{st}(G)$. We abbreviate $\mathscr{P}(T)$, $\mathscr{P}(\bm{0})$ and $\mathscr{P}(N)$ as $T$, $\bm{0}$ and $N$, and call them the terminal p-game, the empty p-game and the natural number p-game, respectively (cf. Example 2.8).

3.2 Cartesian closed categories of predicate games

Next, we lift constructions on games (§2.3) to p-games. The cases of product $\mathbin{\&}$, tensor $\otimes$ and exponential $\oc$ are simple since we can construct them pointwisely:

Notation*.*

Let $G$ be a game, $\bm{s}\in\oc G$ and $i\in\mathbb{N}$. We write $\bm{s}\upharpoonright i$ for the j-subsequence of $\bm{s}$ that consists of occurrences hereditarily justified by the $(i+1)$st initial occurrence in $\bm{s}$. For instance, if $\bm{s}=q2q1q0\in\oc N$, then $\bm{s}\upharpoonright 0=q2$, $\bm{s}\upharpoonright 1=q1$ and $\bm{s}\upharpoonright 2=q0$.

Convention*.*

Given a strategy $\sigma$ on the tensor $G_{0}\otimes G_{1}$ of games $G_{i}$ ($i=0,1$), let

[TABLE]

Similarly, given a strategy $\tau$ on the exponential $\oc G$ of a game $G$ and $j\in\mathbb{N}$, let

[TABLE]

Given a p-game $\Gamma$, we define the value $\Gamma(\uparrow)$ to be undefined, and the constructions $\otimes$, $\multimap$, $\&$ and $\oc$ on undefined games to be undefined. Finally, we extend the relation $\overline{\gamma}_{|\Gamma|}\preccurlyeq\Gamma(\gamma)$ by defining that it does not hold if the game $\Gamma(\gamma)$ is undefined.

Definition 3.5** (Product and tensor on predicate games).**

The product of p-games $\Gamma$ and $\Delta$ is the p-game $\Gamma\mathbin{\&}\Delta$ defined by $|\Gamma\mathbin{\&}\Delta|\colonequals|\Gamma|\mathbin{\&}|\Delta|$ and $(\Gamma\mathbin{\&}\Delta)(\langle\gamma,\delta\rangle)\colonequals\Gamma(\gamma)\mathbin{\&}\Delta(\delta)$ for all $\langle\gamma,\delta\rangle:|\Gamma\mathbin{\&}\Delta|$, and their tensor is the p-game $\Gamma\otimes\Delta$ defined by $|\Gamma\otimes\Delta|\colonequals|\Gamma|\otimes|\Delta|$ and $(\Gamma\otimes\Delta)(\sigma)\colonequals\Gamma(\sigma\upharpoonright|\Gamma|)\otimes\Delta(\sigma\upharpoonright|\Delta|)$ for all $\sigma:|\Gamma\otimes\Delta|$.

Definition 3.6** (Countable tensor).**

The countable tensor of a family $(G_{i})_{i\in\mathbb{N}}$ of subgames $G_{i}\subseteq H$ is the subgame $\otimes_{i\in\mathbb{N}}G_{i}\colonequals\{\,\bm{s}\in\oc H\mid\forall j\in\mathbb{N}.\,\bm{s}\upharpoonright j\in G_{j}\,\}\subseteq\oc H$.

Definition 3.7** (Exponential of predicate games).**

The exponential of a p-game $\Gamma$ is the p-game $\oc\Gamma$ defined by $|\oc\Gamma|\colonequals\oc|\Gamma|$ and $(\oc\Gamma)(\sigma)\colonequals\otimes_{i\in\mathbb{N}}\Gamma(\sigma\upharpoonright i)$ for all $\sigma:|\oc\Gamma|$.

Hence, strategies on $\Gamma\mathbin{\&}\Delta$ are the pairings $\langle\gamma,\delta\rangle$ of $\gamma:\Gamma$ and $\delta:\Delta$. Besides, by the above convention, strategies on $\Gamma\otimes\Delta$ are the tensors $\gamma\otimes\delta$ of $\gamma:\Gamma$ and $\delta:\Delta$, and strategies on $\oc\Gamma$ are those $\sigma:\oc|\Gamma|$ such that $\{\,\bm{s}\upharpoonright i\mid\bm{s}\in\sigma\,\}:\Gamma$ for all $i\in\mathbb{N}$.

In contrast, we cannot apply the pointwise method to linear implication $\multimap$: If we define $|\Delta^{\Gamma}|\colonequals|\Delta|^{|\Gamma|}$ for the linear implication $\Delta^{\Gamma}$, then it is unclear how to decompose strategies $\phi:|\Delta|^{\Gamma}$ into those on $|\Gamma|$ and $|\Delta|$. We solve this problem based on the elegant game semantics of universal quantification [43, p. 17]:

Definition 3.8** (Linear implication and implication between predicate games).**

The linear implication between p-games $\Gamma$ and $\Delta$ is the p-game $\Gamma\multimap\Delta$ (also denoted by $\Delta^{\Gamma}$) defined by $|\Delta^{\Gamma}|\colonequals|\Delta|^{|\Gamma|}$ and for all $\phi:|\Delta^{\Gamma}|$

[TABLE]

and the implication between $\Gamma$ and $\Delta$ is the linear implication $\Gamma\Rightarrow\Delta\colonequals\oc\Gamma\multimap\Delta$.

The first clause of the inductive definition of the subgame $(\Delta^{\Gamma})(\phi)\subseteq|\Delta^{\Gamma}|$ is the base case. Then, the second one specifies one of the two inductive steps: At an even-length position $\bm{s}\in(\Delta^{\Gamma})(\phi)^{\mathrm{Even}}$, O can make a move $m$ as in $\Delta(\phi\circ\gamma)^{\overline{\gamma}_{\Gamma}}\subseteq|\Delta^{\Gamma}|$ for any $\gamma:\Gamma$ not yet excluded, i.e., $\bm{s}\in\Delta(\phi\circ\gamma)^{\overline{\gamma}_{\Gamma}}$. Finally, the third one stipulates the other inductive step: At an odd-length position $\bm{t}l\in(\Delta^{\Gamma})(\phi)^{\mathrm{Odd}}$, the next move $r$ by $\phi$ must be as in $\Delta(\phi\circ\gamma)^{\overline{\gamma}_{\Gamma}}\subseteq|\Delta^{\Gamma}|$ for any $\gamma:\Gamma$ not yet excluded, i.e., $\bm{t}l\in\Delta(\phi\circ\gamma)^{\overline{\gamma}_{\Gamma}}$.

The basic idea is that in the subgame $\Delta^{\Gamma}(\phi)\subseteq|\Delta^{\Gamma}|$ O can play as in any subgame $\Delta(\phi\circ\gamma)^{\overline{\gamma}_{\Gamma}}\subseteq|\Delta^{\Gamma}|$ not yet excluded; then, since P or $\phi$ should see what $\gamma:\Gamma$ is only via plays, $\Delta^{\Gamma}(\phi)$ only allows P to play as in $\Delta(\phi\circ\gamma)^{\overline{\gamma}_{\Gamma}}$ for all $\gamma$ not yet excluded.

In particular, O’s strategy $\gamma:\Gamma$ on the domain $|\Gamma|$ at each moment determines its underlying game $\overline{\gamma}_{\Gamma}$, and P’s play by $\phi:\Delta^{\Gamma}$ on the domain must be as in $\overline{\gamma}_{\Gamma}$ for all possible $\gamma$ not yet excluded. This is crucial for composition of strategies between p-games to be well-defined (Lemma 3.11); see Footnote 9. This additional subtlety is the main difference from the game semantics of universal quantification [43].

For instance, a strategy $\phi:|\Sigma(N_{[0]},(\mathrm{List}_{N})_{[1]})|\multimap|N_{[2]}|$ containing $q_{[2]}m_{[1]}$ is not on $\Sigma(N_{[0]},(\mathrm{List}_{N})_{[1]})\multimap N_{[2]}$ whatever $m$ is since at the odd-length position $q_{[2]}$ the strategy $\langle\underline{0},\top\rangle:\Sigma(N,(\mathrm{List}_{N}))$ is not excluded, and $\Sigma(N,\mathrm{List}_{N})(\langle\underline{0},\top\rangle)=N\mathbin{\&}T$.

As emphasised before, strategies $\phi:\Delta^{\Gamma}$ are indeed ordinary ones (Definition 2.7), which just satisfy some additional axiom. In particular, $\phi$ can see O’s strategy $\gamma:\Gamma$ on the domain $\Gamma$ only gradually via plays; i.e., the declaration of $\gamma$ by O is invisible to $\phi$. In this way, our approach retains the intensionality of game semantics.

Lemma 3.9** (Well-defined constructions on predicate games).**

P-games and w.f. p-games are closed under $\&$, $\otimes$, $\oc$ and $\multimap$, and w.o. ones under $\&$, $\multimap$ and $\Rightarrow$.

Proof.

Straightforward and left to the reader. ∎

Lemma 3.10** (Well-defined copy-cats and derelictions between predicate games).**

Suppose that $\Gamma$ is a p-game, and $\Delta$ is a w.o. p-game.

The copy-cat $\mathrm{cp}_{|\Gamma|}$ is a w.b. strategy on $\Gamma\multimap\Gamma$, and winning if $\Gamma$ is w.f.; 2. 2.

The dereliction $\mathrm{der}_{|\Delta|}$ is a w.b. strategy on $\Delta\Rightarrow\Delta$, and winning if $\Delta$ is w.f.

Proof.

We focus on the first clause since the second one is similar, where we require $\Delta$ to be w.o. for the same reason as the case of derelictions between games (§2.3).

We only show $(\overline{\mathrm{cp}_{|\Gamma|}})_{|\Gamma|^{|\Gamma|}}\preccurlyeq\Gamma^{\Gamma}(\mathrm{cp}_{|\Gamma|})$ as it is the only nontrivial point. We do it by induction on the lengths of positions. The base case and the inductive step on odd-length positions are trivial. For the other inductive step, let $\bm{t}lr\in\mathrm{cp}_{|\Gamma|}$ and $\bm{t}l\in(\overline{\mathrm{cp}_{|\Gamma|}})_{|\Gamma|^{|\Gamma|}}\cap\Gamma^{\Gamma}(\mathrm{cp}_{|\Gamma|})$; we have to prove $\bm{t}lr\in\Gamma^{\Gamma}(\mathrm{cp}_{|\Gamma|})$. By $\bm{t}l\in\Gamma^{\Gamma}(\mathrm{cp}_{|\Gamma|})$ and $\bm{t}lr\in\mathrm{cp}_{|\Gamma|}$, it follows that $\bm{t}lr$ satisfies the inductive condition for $\bm{t}lr\in\Gamma^{\Gamma}(\mathrm{cp}_{|\Gamma|})$. ∎

Lemma 3.11** (Well-defined constructions on strategies between predicate games).**

Given strategies $\phi:\Gamma\multimap\Delta$, $\psi:\Delta\multimap\Theta$, $\sigma:\Theta\multimap\Xi$, $\tau:\Gamma\multimap\Theta$ and $\theta:\oc\Gamma\multimap\Delta$ between p-games, by applying Definition 2.14 to them,777Definition 2.14 is valid here since $\phi:|\Delta|^{|\Gamma|}$, $\psi:|\Theta|^{|\Delta|}$, $\sigma:|\Theta|^{|\Xi|}$, $\tau:|\Theta|^{|\Gamma|}$ and $\theta:|\Delta|^{\oc|\Gamma|}$. we obtain strategies $\psi\circ\phi:\Gamma\multimap\Theta$, $\phi\otimes\sigma:\Gamma\otimes\Theta\multimap\Delta\otimes\Xi$, $\langle\phi,\tau\rangle:\Gamma\multimap\Delta\mathbin{\&}\Theta$ and $\theta^{\dagger}:\oc\Gamma\multimap\oc\Delta$ between p-games, and these constructions preserve winning and well-bracketing.888We go into details in the proof since this lemma is foundational for the rest of the present work. After proving the lemma, we are more sketchy on similar arguments.

Proof.

We focus on the tensor $\phi\otimes\sigma$ and the composition $\psi\circ\phi$ because the other constructions are simpler to verify. First, let us show $\phi\otimes\sigma:\Gamma\otimes\Theta\multimap\Delta\otimes\Xi$, for which it suffices to verify $(\overline{\phi\otimes\sigma})_{|\Delta\otimes\Xi|^{|\Gamma\otimes\Theta|}}\preccurlyeq(\Delta\otimes\Xi)^{\Gamma\otimes\Theta}(\phi\otimes\sigma)$. We prove it by induction on the lengths of positions. The base case and the inductive step on odd-length positions are trivial. For the other inductive step, let $\bm{s}mn\in\phi\otimes\sigma$ and $\bm{s}m\in(\overline{\phi\otimes\sigma})_{|\Delta\otimes\Xi|^{|\Gamma\otimes\Theta|}}\cap(\Delta\otimes\Xi)^{\Gamma\otimes\Theta}(\phi\otimes\sigma)$; we have to show $\bm{s}mn\in(\Delta\otimes\Xi)^{\Gamma\otimes\Theta}(\phi\otimes\sigma)$.

By $\bm{s}m\in(\Delta\otimes\Xi)^{\Gamma\otimes\Theta}(\phi\otimes\sigma)$, it suffices to show $\bm{s}mn\in(\Delta\otimes\Xi)((\phi\otimes\sigma)\circ\varphi)^{\overline{\varphi}_{\Gamma\otimes\Theta}}$ for all $\varphi:\Gamma\otimes\Theta$ such that $\bm{s}m\in(\Delta\otimes\Xi)((\phi\otimes\sigma)\circ\varphi)^{\overline{\varphi}_{\Gamma\otimes\Theta}}$. Fix such $\varphi$. Note that $\varphi=\gamma\otimes\vartheta$ for unique $\gamma:\Gamma$ and $\vartheta:\Theta$, and $(\phi\otimes\sigma)\circ\varphi=(\phi\circ\gamma)\otimes(\sigma\circ\vartheta)$. Hence, it suffices to show $\bm{s}mn\upharpoonright|\Delta^{\Gamma}|\in\Delta(\phi\circ\gamma)^{\overline{\gamma}_{\Gamma}}$ and $\bm{s}mn\upharpoonright|\Xi^{\Theta}|\in\Xi(\phi\circ\vartheta)^{\overline{\vartheta}_{\Theta}}$. Assume $n$ in $\phi$; the other case is similar. Then, we have $\bm{s}m\upharpoonright|\Delta^{\Gamma}|\in\Delta(\phi\circ\gamma)^{\overline{\gamma}_{\Gamma}}$ and $\bm{s}mn\upharpoonright|\Xi^{\Theta}|=\bm{s}m\upharpoonright|\Xi^{\Theta}|\in\Xi(\phi\circ\vartheta)^{\overline{\vartheta}_{\Theta}}$ by $\bm{s}m\in(\Delta\otimes\Xi)((\phi\otimes\sigma)\circ\varphi)^{\overline{\varphi}_{\Gamma\otimes\Theta}}$. It remains to show $\bm{s}mn\upharpoonright|\Delta^{\Gamma}|\in\Delta(\phi\circ\gamma)^{\overline{\gamma}_{\Gamma}}$, but it follows from $\phi:\Delta^{\Gamma}$, $(\bm{s}m\upharpoonright|\Delta^{\Gamma}|).n\in\phi$ and $\bm{s}m\upharpoonright|\Delta^{\Gamma}|\in\overline{\phi}_{|\Delta^{\Gamma}|}\cap\Delta^{\Gamma}(\phi)$, where $(\bm{s}m\upharpoonright|\Delta^{\Gamma}|).n\in\phi$ follows from $\bm{s}mn\in\phi\otimes\sigma$, and $\bm{s}m\upharpoonright|\Delta^{\Gamma}|\in\overline{\phi}_{|\Delta^{\Gamma}|}\cap\Delta^{\Gamma}(\phi)$ from $(\bm{s}m\upharpoonright|\Delta^{\Gamma}|).n\in\phi$, $\bm{s}\upharpoonright|\Delta^{\Gamma}|\in\phi\cap\Delta^{\Gamma}(\phi)\subseteq\Delta^{\Gamma}(\phi)$ and $\bm{s}m\upharpoonright|\Delta^{\Gamma}|\in\Delta(\phi\circ\gamma)^{\overline{\gamma}_{\Gamma}}$. We have shown $\phi\otimes\sigma:\Gamma\otimes\Theta\multimap\Delta\otimes\Xi$. The same induction shows that $\phi\otimes\sigma$ is total if so are $\phi$ and $\sigma$, and it trivially follows from Lemma 2.15 that $\phi\otimes\sigma$ is innocent (resp. noetherian and w.b.) if so are $\phi$ and $\sigma$.

Let us proceed to show $\psi\circ\phi:\Gamma\multimap\Theta$, for which it suffices to show $(\overline{\psi\circ\phi})_{|\Theta|^{|\Gamma|}}\preccurlyeq\Theta^{\Gamma}(\psi\circ\phi)$. Again, we prove it by induction on the lengths of positions, and the base case and the inductive step on odd-length positions are trivial. For the remaining inductive step, assume $\bm{t}lr\in\psi\circ\phi$ and $\bm{t}l\in(\overline{\psi\circ\phi})_{|\Theta|^{|\Gamma|}}\cap(\Theta)^{\Gamma}(\psi\circ\phi)$; we have to show $\bm{t}lr\in(\Theta)^{\Gamma}(\psi\circ\phi)$. Similarly to the case of tensor $\otimes$, fix $\gamma:\Gamma$ such that $\bm{t}l\in\Theta(\psi\circ\phi\circ\gamma)^{\overline{\gamma}_{\Gamma}}$; then it suffices to show $\bm{t}lr\in\Theta(\psi\circ\phi\circ\gamma)^{\overline{\gamma}_{\Gamma}}$. Assume $l$ in $\Gamma$; the other case is analogous. Note that $\bm{t}l=(\bm{w}\upharpoonright|\Gamma|,|\Theta|).l$ for some unique $\bm{w}\in\phi\parallel\psi$ (Definition 2.14) by the covering lemma [16, p. 12]. The computation of $\phi\parallel\psi$ on $\bm{w}l$ produces $r$ after playing a finite fragment $\bm{u}$ of a position in the intermediate game $\mathrm{Pref}(\mathrm{cp}_{|\Delta|})$; see [16, p. 11]. Crucially, $\phi:\Delta^{\Gamma}$ and $\psi:\Theta^{\Delta}$ imply by induction that $\bm{u}$ is a suffix of a position in $(\overline{\mathrm{cp}_{|\Delta|}})_{\Delta(\phi\circ\gamma)^{\Delta(\phi\circ\gamma)}}$.999In other words, the contact point $\subseteq|\Delta|$ between $\phi$ and $\psi$ matches at each moment. Hence, $\bm{t}lr\in\Theta(\psi\circ\phi\circ\gamma)^{\overline{\gamma}_{\Gamma}}$.

Finally, the same inductive argument verifies that $\psi\circ\phi$ is winning if so are $\phi$ and $\psi$, and it trivially follows from Lemma 2.15 that $\psi\circ\phi$ is w.b. if so are $\phi$ and $\sigma$. ∎

We are now ready to summarise the present section by:

Definition 3.12** (Categories of predicate games).**

The category $\mathbb{PG}$ consists of

• •

W.o. p-games as objects;

• •

Strategies on the implication $\Gamma\Rightarrow\Delta$ as morphisms $\Gamma\rightarrow\Delta$;

• •

The composition $\psi\bullet\phi\colonequals\psi\circ\phi^{\dagger}:\Gamma\Rightarrow\Theta$ of strategies as the composition of morphisms $\phi:\Gamma\rightarrow\Delta$ and $\psi:\Delta\rightarrow\Theta$;

• •

The dereliction $\mathrm{der}_{|\Gamma|}:\Gamma\Rightarrow\Gamma$ as the identity $\mathrm{id}_{\Gamma}$ on each object $\Gamma$.

The subcategory $\mathbb{LPG}$ (resp. $\mathbb{WPG}$) of $\mathbb{PG}$ consists of w.f., w.o. p-games as objects, and winning (resp. winning, w.b.) strategies as morphisms.

Remark*.*

As in the case of games [35, §3.3], there are the linear counterparts of the categories $\mathbb{PG}$, $\mathbb{LPG}$ and $\mathbb{WPG}$, in which morphisms $\Gamma\rightarrow\Delta$ are strategies on the linear implication $\Gamma\multimap\Delta$. We skip them since they are not central in this article.

Nevertheless, our game semantics of MLTT (§4) together with these six categories implies that some combinations of dependent types and linearity/effects are already there in game semantics. We leave it as future work to study such combinations.

Just like the categories of games (Definition 2.16), p-games in $\mathbb{PG}$ (resp. $\mathbb{LPG}$ and $\mathbb{WPG}$) are w.o. (resp. w.f. and w.o.) for the identities to be well-defined.

Theorem 3.13** (Well-defined cartesian closed categories of predicate games).**

The structures $\mathbb{PG}$, $\mathbb{LPG}$ and $\mathbb{WPG}$ form cartesian closed categories.

Proof.

By Lemma 3.11, it suffices to focus on $\mathbb{PG}$. The composition is well-defined by Lemma 3.11, and so are the identities by Lemma 3.10. Since morphisms in $\mathbb{PG}$ are a certain class of those in $\mathbb{G}$, and the composition and the identities in $\mathbb{PG}$ are those in $\mathbb{G}$, the associativity and the unit law on $\mathbb{PG}$ follow from those on $\mathbb{G}$ (Theorem 2.17). The cartesian closure of $\mathbb{PG}$ is by Example 3.4 on $T$ and Lemmata 3.9 and 3.11, where the required equations on morphisms again follow from those on $\mathbb{G}$. ∎

Convention*.*

We write $\mathbb{PG}(\Gamma)$, $\mathbb{LPG}(\Gamma)$ and $\mathbb{WPG}(\Gamma)$ for the hom-sets $\mathbb{PG}(T,\Gamma)$, $\mathbb{LPG}(T,\Gamma)$ and $\mathbb{WPG}(T,\Gamma)$, respectively, for each object $\Gamma$, and do not distinguish $\Gamma$ and $\mathbb{PG}(\Gamma)$; e.g., we say that $\gamma:\Gamma$ is winning and w.b. if and only if $\gamma\in\mathbb{WPG}(\Gamma)$.

Finally, let us show a categorically pleasing feature of p-games (Corollary 3.14). We focus on $\mathbb{WPG}$ for brevity, but the following argument is valid in $\mathbb{LPG}$ and $\mathbb{PG}$ as well. First, we define an equivalence relation $\simeq$ between morphisms $\phi,\phi^{\prime}:\Gamma\rightarrow\Delta$ by $\phi\simeq\phi^{\prime}\Leftrightarrow/\phi\bullet\gamma=\phi^{\prime}\bullet\gamma:\Delta$ for all $\gamma:\Gamma$; i.e., $\phi\simeq\phi^{\prime}$ means that $\phi$ and $\phi^{\prime}$ are extensionally equal. Next, recall that a morphism $\phi:\Gamma\rightarrow\Delta$ is strict if $m^{xy}n^{zw}\in\phi$ implies $n^{(z^{\bot})w}\in\Gamma$ [44]. We then define a category $\mathbb{WPG}^{\sharp}_{\simeq}$ out of $\mathbb{WPG}$, in which objects are those of $\mathbb{WPG}$, and morphisms $\Gamma\rightarrow\Delta$ are the equivalence classes $[\phi]$ of strict morphisms $\phi:\Gamma\rightarrow\Delta$ in $\mathbb{WPG}$ modulo $\simeq$. The composition of morphisms $[\phi]:\Gamma\rightarrow\Delta$ and $[\psi]:\Delta\rightarrow\Theta$ in $\mathbb{WPG}^{\sharp}_{\simeq}$ is given by $[\psi]\bullet[\phi]\colonequals[\psi\bullet\phi]$, and the identities in $\mathbb{WPG}^{\sharp}_{\simeq}$ by $\mathrm{id}_{\Gamma}\colonequals[\mathrm{der}_{|\Gamma|}]$ for all $\Gamma\in\mathbb{WPG}^{\sharp}_{\simeq}$. We leave it to the reader as an easy exercise to prove that $\mathbb{WPG}^{\sharp}_{\simeq}$ forms a cartesian closed category.

Corollary 3.14** (Game-semantic finite limits).**

$\mathbb{WPG}^{\sharp}_{\simeq}$* has all finite limits.*

Proof.

It suffices to establish the equaliser of given morphisms $[\phi_{1}],[\phi_{2}]:\Gamma\rightrightarrows\Delta$. Let us then show that the required equaliser is given by the pair $(\Theta,[\mathrm{der}_{|\Theta|}])$, where $\Theta$ is the p-game defined by $|\Theta|\colonequals|\Gamma|$ and \Theta(\theta)\colonequals\begin{cases}\Gamma(\theta)&\text{if \phi_{1}\bullet\theta=\phi_{2}\bullet\theta;}\\ T&\text{otherwise,}\end{cases} for all $\theta:|\Theta|$. The p-game $\Theta$ is well-defined since it does not depend on the choice of the representatives $\phi_{i}$ of the morphisms $[\phi_{i}]$ ($i=1,2$). Note that $\gamma:\Theta$ if and only if $\phi_{1}\bullet\gamma=\phi_{2}\bullet\gamma$ or $\gamma=\{\bm{\epsilon}\}$ for all $\gamma:\Gamma$. Besides, we have $\phi_{1}\bullet\{\bm{\epsilon}\}=\phi_{2}\bullet\{\bm{\epsilon}\}$ thanks to the strictness of $\phi_{i}$ ($i=1,2$). Hence, it follows that $[\phi_{1}]\bullet[\mathrm{der}_{|\Theta|}]=[\phi_{2}]\bullet[\mathrm{der}_{|\Theta|}]$.

Next, given an object $\Theta^{\prime}$ and a morphism $[\varphi]:\Theta^{\prime}\rightarrow\Gamma$ with $[\phi_{1}]\bullet[\varphi]=[\phi_{2}]\bullet[\varphi]$, we have $[\varphi]:\Theta^{\prime}\rightarrow\Theta$ and $[\mathrm{der}_{|\Theta|}]\bullet[\varphi]=[\varphi]$, where we leave the details to the reader. Finally, if another morphism $[\varphi^{\prime}]:\Theta^{\prime}\rightarrow\Theta$ satisfies $[\mathrm{der}_{|\Theta|}]\bullet[\varphi^{\prime}]=[\varphi]$, then $[\varphi^{\prime}]=[\mathrm{der}_{|\Theta|}]\bullet[\varphi^{\prime}]=[\varphi]$. We have shown the universal property of $(\Theta,[\mathrm{der}_{|\Theta|}])$. ∎

We focus on strict strategies in $\mathbb{WPG}^{\sharp}_{\simeq}$ for Corollary 3.14 since, e.g., there is no equaliser of the non-strict strategies $\underline{0},\underline{1}:N\rightrightarrows N$. We further take the extensional quotient $[\phi]$ of strict strategies $\phi$ in $\mathbb{WPG}^{\sharp}_{\simeq}$ since it seems that otherwise the category would not be finitely complete (though we have not shown this negative result).

This categorical structure is quite novel. For instance, if we apply the proof of Corollary 3.14 to $[\kappa_{\underline{0}}],[\mathbin{\geqslant}]:N\mathbin{\&}N\rightrightarrows N$ such that $\kappa_{\underline{0}}$ is any strict strategy such that $\kappa_{\underline{0}}\bullet\sigma=\underline{0}$ for all $\sigma:N\mathbin{\&}N$, and $\geqslant$ is any strict strategy such that $\mathbin{\geqslant}\bullet\mathbin{\langle\underline{k},\underline{n}\rangle}=\underline{0}$ if and only if $k\geqslant n$ for all $k,n\in\mathbb{N}$, then their equaliser is the p-game that models the Sigma-type $\mathsf{\Sigma_{x:N}N_{b}(x)}$ (see the beginning of §3). Therefore, this construction is impossible for games (even if we focus on strict strategies and take their quotient).

Corollary 3.14 is also useful: It enables us to internalise a certain notion of $\infty$-groupoids in $\mathbb{WPG}^{\sharp}_{\simeq}$, which is a key step to extend this work to HoTT [37]. Note that we do not focus on strict strategies or take their quotient when we interpret HoTT, and so it is a proper extension of our game semantics of MLTT to HoTT.

4 Game semantics of Martin-Löf type theory

We are now ready to present our game semantics of MLTT. Concretely, we show that the CCC $\mathbb{WPG}$ forms abstract semantics of MLTT: a category with families (CwF) [45]. CwFs are closer to the syntax than other abstract semantics, so that we can directly see the semantic counterparts of MLTT. In fact, we even regard a CwF as another presentation of MLTT as Clairambault and Dybjer [46] do, and so we only show that $\mathbb{WPG}$ forms a CwF, leaving how a CwF models MLTT to [31].

Specifically, we prove that the CCC $\mathbb{WPG}$ gives rise to a CwF equipped with semantic type formers [31] for One-, Zero-, N-, Pi-, Sigma- and Id-types, establishing game semantics of MLTT equipped with these types.

The rest of this section proceeds as follows. We model dependent types in §4.1, Pi-types in §4.2, and Sigma-types in §4.3. We then show that $\mathbb{WPG}$ forms a CwF in §4.4 and equip it with all the semantic type formers in §4.5. Finally, we analyse the intensionality of our game semantics in §4.6, prove the independence of Markov’s principle from MLTT in §4.7, for which we use $\mathbb{WPG}$, not $\mathbb{PG}$ or $\mathbb{LPG}$, and extend the game semantics of MLTT to subtyping on dependent types in §4.8.

4.1 Dependent predicate games

First, we interpret dependent types by w.o., w.f. dependent p-games:

Definition 4.1** (Dependent predicate games).**

A linearly dependent predicate (p-) game over a p-game $\Gamma$ is a pair $L=(|L|,\|L\|)$ of a game $|L|$ and a family $\|L\|=(L(\gamma_{0}))_{\gamma_{0}\in\mathbb{WPG}(\Gamma)}$ of p-games $L(\gamma_{0})$ such that $|L(\gamma_{0})|=|L|$. It is well-opened (w.o.) (resp. well-founded (w.f.)) if so is the game $|L|$.

The extension of the family $\|L\|$ is the family $L^{\star}=(L^{\star}(\gamma))_{\gamma:\Gamma}$ of p-games $L^{\star}(\gamma)$ defined by L^{\star}(\gamma)\colonequals\begin{cases}L(\gamma)&\text{if \gamma\in\mathbb{WPG};}\\ \mathscr{P}(|L|)&\text{otherwise (cf.~{}Example~{}\ref{ExPGames}).}\end{cases}

A dependent predicate (p-) game over $\Gamma$ is a linearly dependent one over $\oc\Gamma$.

Notation*.*

We write $\mathscr{D}_{\ell}(\Gamma)$ (resp. $\mathscr{D}_{\ell}^{\mathrm{w}}(\Gamma)$) for the set of all linearly dependent p-games (resp. w.o., w.f. ones) over $\Gamma$, and $\{\Gamma^{\prime}\}_{\Gamma}$ or $\{\Gamma^{\prime}\}$ for the constant one at $\Gamma^{\prime}$, i.e., $\{\Gamma^{\prime}\}_{\Gamma}\colonequals(\Gamma^{\prime},\gamma:\Gamma\mapsto\Gamma^{\prime})$. We define $\mathscr{D}(\Gamma)\colonequals\mathscr{D}_{\ell}(\oc\Gamma)$ and $\mathscr{D}^{\mathrm{w}}(\Gamma)\colonequals\mathscr{D}^{\mathrm{w}}_{\ell}(\oc\Gamma)$.

We often write $\gamma_{0}^{\dagger}$ for an arbitrary element of $\mathbb{WPG}(\oc\Gamma)$, where $\gamma_{0}\in\mathbb{WPG}(\Gamma)$, since elements of $\mathbb{WPG}(\oc\Gamma)$ are all innocent and so promotions of elements of $\mathbb{WPG}(\Gamma)$.

We explain Definition 4.1 as follows. First, we define p-games $\mathcal{U}$ to model universes and encode w.o., w.f. dependent p-games $A$ over a p-game $\Gamma$ by morphisms $\phi_{A}:\Gamma\rightarrow\mathcal{U}$ in $\mathbb{WPG}$ in a forthcoming article. Thus, naively $\|A\|$ would be the map $\gamma:\oc\Gamma\mapsto\mathrm{El}(\phi_{A}\circ\gamma)$, where $\mathrm{El}(\mu)\in\mathbb{WPG}$ is the p-game encoded by each $\mu\in\mathbb{WPG}(\mathcal{U})$. However, $\phi_{A}\circ\gamma$ can be invalid as an encoding, i.e., $\phi_{A}\circ\gamma\not\in\mathbb{WPG}(\mathcal{U})$, for instance when $\phi_{A}\circ\gamma$ is partial, where the value $A(\gamma)=\mathrm{El}(\phi_{A}\circ\gamma)$ is undefined. This suggests us to restrict $\|A\|$ to $\mathbb{WPG}(\oc\Gamma)$, so that $\mathrm{El}(\phi_{A}\bullet\gamma_{0})\in\mathbb{WPG}$ for all $\gamma_{0}^{\dagger}\in\mathbb{WPG}(\oc\Gamma)$. Accordingly, $\|A\|$ is trivially continuous since elements of $\mathbb{WPG}(\oc\Gamma)$ are all total.101010This point matches the remark by Abramsky et al. [29, Footnote 5] that the continuity of their interpretation of dependent types does not play any roles.

Then, however, we also need the ambient game $|A|$. For instance, if $A=\{N\}_{\oc\bm{0}}$, then the family $\|A\|$ is empty, and so $\|A\|$ cannot retain the natural number p-game $N$. We address this problem by adding the game $|A|$ and extending $\|A\|$ to $A^{\star}$.

Example 4.2**.**

We slightly modify and formalise the examples $\mathrm{List}_{N},N_{b}\in\mathscr{D}^{\mathrm{w}}(N)$ by $\mathrm{List}_{N}(\underline{k}^{\dagger})\colonequals\underbrace{N\otimes N\otimes\dots\otimes N}_{k}$ for all $k\in\mathbb{N}$ and $|\mathrm{List}_{N}|\colonequals\bigcup_{k\in\mathbb{N}}\mathrm{List}_{N}(\underline{k}^{\dagger})$, as well as $|N_{b}|\colonequals N$ and $N_{b}(\underline{k}^{\dagger})\colonequals\mathrm{Pref}(\{\,qn\mid n\leqslant k\,\})$ for all $k\in\mathbb{N}$.

4.2 Pi on dependent predicate games

We next interpret Pi-types. Our idea is best explained by the set-theoretic analogy as follows. Given a dependent type $\mathsf{x:C\vdash D(x)}$, the Pi-type $\mathsf{\Pi_{x:C}D(x)}$ is something like the set of all functions $f$ from $C$ to $\bigcup_{x:C}D(x)$ such that $f(x)\in D(x)$ for all $x\in C$, called dependent maps from $C$ to $D$, where recall that the set-theoretic semantics interprets simple types $\mathsf{C}$ and terms $\mathsf{x:C}$ as sets $C$ and elements $x\in C$, respectively, and dependent types $\mathsf{D}$ over $\mathsf{C}$ as families $D=(D(x))_{x\in C}$ of sets $D(x)$.

Hence, in light of implication $\Rightarrow$ between p-games (Definition 3.8), it is now clear how to model Pi-types. We interpret Pi-types by the following pi $\Pi$:

Definition 4.3** (Linear-pi and pi).**

Let $L$ be a linearly dependent p-game over a p-game $\Gamma$, and $A$ a dependent p-game over $\Gamma$. The linear-pi from $\Gamma$ to $L$ is the p-game $\Pi_{\ell}(\Gamma,L)$ defined by $|\Pi_{\ell}(\Gamma,L)|\colonequals|L|^{|\Gamma|}$ and for all $\phi:|\Pi_{\ell}(\Gamma,L)|$

[TABLE]

and the pi from $\Gamma$ to $A$ is the linear-pi $\Pi(\Gamma,A)\colonequals\Pi_{\ell}(\oc\Gamma,A)$.

The idea of linear-pi is that it is linear implication between p-games except that it also satisfies type dependency. Specifically, the codomain of a linear-pi $\Pi_{\ell}(\Gamma,L)$ is the p-game $L(\gamma)$ if the strategy $\gamma:\Gamma$ on the domain satisfies $\gamma\in\mathbb{WPG}(\Gamma)$, and the constant one $\mathscr{P}(|L|)$ otherwise. We then define pi out of linear-pi and exponential in the same way as we define implication out of linear implication and exponential.

Accordingly, linear-pi (resp. pi) generalises linear implication (resp. implication): Given p-games $\Gamma$ and $\Gamma^{\prime}$, $\Pi_{\ell}(\Gamma,\{\Gamma^{\prime}\}_{\Gamma})=\Gamma\multimap\Gamma^{\prime}$ (resp. $\Pi(\Gamma,\{\Gamma^{\prime}\}_{\oc\Gamma})=\Gamma\Rightarrow\Gamma^{\prime}$).

Essentially the same proof as the one of Lemma 3.9 on linear implication shows:

Theorem 4.4** (Well-defined linear-pi).**

Given a (w.o., w.f.) linearly dependent p-game $L$ over a (w.o., w.f.) p-game $\Gamma$, the linear-pi $\Pi_{\ell}(\Gamma,L)$ is a (w.o., w.f.) p-game.

This theorem also implies that, given a (w.o., w.f.) dependent p-game $A$ over a (w.o., w.f.) p-game $\Gamma$, the pi $\Pi(\Gamma,A)$ is a (w.o., w.f.) p-game. However, we have to handle the case where $\Gamma$ is a dependent p-game. We address this point in §4.5.1.

Example 4.5**.**

A strategy $\zeta:\Pi(N,\mathrm{List}_{N})$ plays as the dependent map $n\in\mathbb{N}\mapsto(0,0,\dots,0)\in\mathbb{N}^{n}$ as follows. If O makes the first move $q_{[k]}$ ($k\in\mathbb{N}^{+}$) on the codomain $|\mathrm{List}_{N}|$, where $(\_)_{[k]}$ is the ‘tag’ for tensor $N_{[1]}\otimes N_{[2]}\otimes\dots$, then $\zeta$ asks a question $q_{[0]}$ on the domain $\oc N_{[0]}$, where $(\_)_{[0]}$ is another ‘tag’ for clarity. Finally, if O plays by $q_{[k]}q_{[0]}\mapsto n_{[0]}$ for any $n\in\mathbb{N}^{+}$, then $\zeta$ plays by $q_{[k]}q_{[0]}n_{[0]}\mapsto 0_{[k]}$. If $k\leqslant n$, then $\underline{n}^{\dagger}\in\mathbb{WPG}(\oc N)$ on the domain is not yet excluded; $\zeta$ is compatible with this possibility since its computation so far is within the subgame $N\Rightarrow\mathrm{List}_{N}(\underline{n}^{\dagger})\subseteq|\Pi(N,\mathrm{List}_{N})|$.

At this point, O can further play on the pi $\Pi(N,\mathrm{List}_{N})$. For instance, O can make another move $q_{[k^{\prime}]}$ on the codomain such that $k\neq k^{\prime}$; then, $\zeta$ again makes the move $q_{[0]}$ on the domain. If O answers it by $n^{\prime}_{[0]}$ for any $n^{\prime}\in\mathbb{N}^{+}$, then $\zeta$ plays $0_{[k^{\prime}]}$ on the codomain. If $n\neq n^{\prime}$, $k>n$ or $k^{\prime}>n$, then $\zeta$ no longer has to play within the subgame $N\Rightarrow\mathrm{List}_{N}(\underline{n}^{\dagger})$. In contrast, if $n=n^{\prime}$, $k\leqslant n$ and $k^{\prime}\leqslant n$, then $\zeta$ still has to play on the subgame $N\Rightarrow\mathrm{List}_{N}(\underline{n}^{\dagger})$, and its computation still satisfies this condition. In this way, a play by $\zeta$ proceeds. Hence, we indeed have $\zeta:\Pi(N,\mathrm{List}_{N})$.

4.3 Sigma on dependent predicate games

We next interpret Sigma-types. Recall that by the set-theoretic analogy the Sigma-type $\mathsf{\Sigma_{x:C}D(x)\ type}$ represents the set of all pairs $(c,d)$ such that $c\in C$ and $d\in D(c)$, called dependent pairs on $C$ and $D$. Hence, we model Sigma-types by:

Definition 4.6** (Sigma).**

The sigma of a p-game $\Gamma$ and a dependent p-game $A$ over $\Gamma$ is the p-game $\Sigma(\Gamma,A)$ defined by $|\Sigma(\Gamma,A)|\colonequals|\Gamma|\mathbin{\&}|A|$ and $\Sigma(\Gamma,A)(\langle\gamma,\alpha\rangle)\colonequals\Gamma(\gamma)\mathbin{\&}A^{\star}(\gamma^{\dagger})(\alpha)$ for all $\langle\gamma,\alpha\rangle:|\Sigma(\Gamma,A)|$.

The basic idea of a sigma $\Sigma(\Gamma,A)$ is that strategies on $\Sigma(\Gamma,A)$ must be the pairings $\langle\gamma,\alpha\rangle:|\Gamma|\mathbin{\&}|A|$ that satisfy $\gamma:\Gamma$ and $\alpha:A(\gamma^{\dagger})$ whenever $\gamma\in\mathbb{WPG}(\Gamma)$. The second condition matches the constraint on the pi $\Pi(\Gamma,A)$ as we shall see shortly.

When $A$ is a constant dependent p-game $\{\Gamma^{\prime}\}_{\oc\Gamma}$, the sigma $\Sigma(\Gamma,\{\Gamma^{\prime}\}_{\oc\Gamma})$ coincides with the product $\Gamma\mathbin{\&}\Gamma^{\prime}$. Thus, sigma $\Sigma$ generalises product $\mathbin{\&}$ on p-games.

Theorem 4.7** (Well-defined sigma).**

Given a (w.o., w.f.) dependent p-game $A$ over a (w.o., w.f.) p-game $\Gamma$, the sigma $\Sigma(\Gamma,A)$ is a (w.o., w.f.) p-game.

Proof.

Straightforward and left to the reader. ∎

Let $\Gamma\in\mathbb{WPG}$ and $A\in\mathscr{D}^{\mathrm{w}}(\Gamma)$. Then, $\Sigma(\Gamma,A)\in\mathbb{WPG}$, and it attains the following nontrivial point. First, the categorical view on semantics of MLTT (Definition 4.9) tells us that there must be a bijection between strategies $\psi\in\mathbb{WPG}(\Delta,\Sigma(\Gamma,A))$ and pairs $(\phi,\check{\alpha})$ of strategies $\phi\in\mathbb{WPG}(\Delta,\Gamma)$ and $\check{\alpha}\in\mathbb{WPG}(\Pi(\Delta,A\{\phi\}))$, where the dependent p-game $A\{\phi\}\in\mathscr{D}^{\mathrm{w}}(\Delta)$ is defined by $|A\{\phi\}|\colonequals|A|$ and $A\{\phi\}(\delta)\colonequals A(\phi^{\dagger}\circ\delta)$ ($\delta\in\mathbb{WPG}(\oc\Delta)$). Next, the constraint on the codomain $A\{\phi\}$ of $\Pi(\Delta,A\{\phi\})$ is gradually revealed along the gradual specification of a strategy $\delta$ on the domain $\oc\Delta$. However, since $\Sigma(\Gamma,A)$ itself cannot refer to $\Delta$, unlike $\Pi(\Delta,A\{\phi\})$, the challenge is to define $\Sigma(\Gamma,A)$ in such a way that strategies $\psi\in\mathbb{WPG}(\Delta,\Sigma(\Gamma,A))$ achieve the bijection.111111This problem is vacant in Abramsky et al. [23, 29] as they define morphisms $\Delta\rightarrow\Sigma(\Gamma,A)$ to be the pairs $(\phi,\check{\alpha})$ at the cost of the non-inductive nature of game semantics. Then, the sigma $\Sigma(\Gamma,A)$ in fact meets this requirement (Theorem 4.11).

Example 4.8**.**

The sigmas $\Sigma(N,\mathrm{List}_{N})$ and $\Sigma(N,N_{b})$ respectively formalise the two examples given at the beginning of §3.

The pairings $\langle\underline{k},\underline{n_{1}}\otimes\underline{n_{2}}\otimes\dots\otimes\underline{n_{k}}\rangle$, where $k,n_{1},n_{2},\dots,n_{k}\in\mathbb{N}$, are all winning on $\Sigma(N,\mathrm{List}_{N})$ since the declaration of a strategy in a p-game can control odd-length positions. Besides, given a morphism $\phi:\Sigma(N,\mathrm{List}_{N})\rightarrow\Delta$ in $\mathbb{WPG}$, the composition $T\stackrel{{\scriptstyle\langle\underline{k},\underline{n_{1}}\otimes\underline{n_{2}}\otimes\dots\otimes\underline{n_{k}}\rangle}}{{\rightarrow}}\Sigma(N,\mathrm{List}_{N})\stackrel{{\scriptstyle\phi}}{{\rightarrow}}\Delta$ is well-defined and winning (Lemma 3.11).

In contrast, the list $(\underline{k},\underline{n_{1}}\otimes\underline{n_{2}}\otimes\dots\otimes\underline{n_{k}})$ is partial on the list $(N,\mathrm{List}_{N})$ in Abramsky et al. [23, 29], where we regard $N$ and the components of $\mathrm{List}_{N}$ as games in the evident way, since there is no way in their method to prevent O from playing arbitrarily on the ambient game $|\mathrm{List}_{N}|$. For instance, $(\underline{0},\top)$ is partial on $(N,\mathrm{List}_{N})$.

Note that the underlying list of (families) games for $(\underline{k},\underline{n_{1}}\otimes\underline{n_{2}}\otimes\dots\otimes\underline{n_{k}})$ cannot be $(N,\{\mathrm{List}_{N}(\underline{k}^{\dagger})\})$ as the composition of their morphisms $(\underline{k},\underline{n_{1}}\otimes\underline{n_{2}}\otimes\dots\otimes\underline{n_{k}}):T\rightarrow(N,\{\mathrm{List}_{N}(\underline{k}^{\dagger})\})$ and $\psi:(N,\mathrm{List}_{N})\rightarrow\Theta$ is ill-defined. Also, we cannot replace the domain of $\psi$ with $(N,\{\mathrm{List}_{N}(\underline{k}^{\dagger})\})$ either since it cannot handle the other values of $k\in\mathbb{N}$. Hence, the codomain of $(\underline{k},\underline{n_{1}}\otimes\underline{n_{2}}\otimes\dots\otimes\underline{n_{k}})$ must be $(N,\mathrm{List}_{N})$.

For this problem, they instead take the lists $(\underline{k},\tau)$ of winning strategies $\underline{k}:N$ and $\tau:|\mathrm{List}_{N}|$. However, $\tau$ is redundant as it is total on $|\mathrm{List}_{N}|$; e.g., $(\underline{0},\top)$ is replaced with any $(\underline{0},\underline{n_{1}}\otimes\underline{n_{2}}\otimes\cdots)$ such that $n_{i}\in\mathbb{N}$ for all $i\in\mathbb{N}$ in their approach, where $\underline{n_{1}}\otimes\underline{n_{2}}\otimes\cdots$ is an infinite iteration of tensor $\otimes$, but neither of them is canonical. Consequently, their approach cannot properly model the Sigma-type $\mathsf{\Sigma(N,List_{N})}$.

Technically, Abramsky et al. employ the O-sat operation [29, Remark 4.5 and Theorem 5.6], which allows O to ignore the type dependency of Pi- and Sigma-types, and impose winning on strategies against such unrestricted plays by O. However, this method generates a significant gap between their model and MLTT since terms $\mathsf{\vdash\langle a,b\rangle:\Sigma(A,B)}$ satisfy $\mathsf{\vdash a:A}$ and $\mathsf{\vdash b:B(a)}$, not $\mathsf{x:A\vdash b:B(x)}$. How does their full completeness hold then? The answer is that they focus on a very specific class of finite inductive types [29, Figure 7] for which the problem just disappears. However, as we have just seen, their method is unsuited for more standard types such as $\mathsf{List_{N}}$, which is generated by the elimination rule of N-type in the presence of universes.

In summary, the novel mathematical structure of p-games enables us to not only dispense with the list construction but also accurately model Pi- and Sigma-types.

Finally, recall that the interpretation of Sigma-types by Blot and Laird [24] does not preserve the additive nature of product $\&$ on games (§1.4). In contrast, sigma $\Sigma$ preserves the additive nature. The challenge we have overcome is that the additive nature requires that a play in $\Sigma(\Gamma,A)$ is either a play in $\Gamma$ or $A$, but then we have to specify the constraint on plays in $A$ for $\Sigma(\Gamma,A)$ even without playing on $\Gamma$.

Again, however, this construction of sigma $\Sigma$ is not general enough for the same reason as the case of pi $\Pi$ (§4.2); we generalise it in §4.5.2.

4.4 A game-semantic category with families

We are now ready to present our game-semantic CwF. Let us first recall the general definition of CwFs introduced by Dybjer [45]:

Definition 4.9** (CwFs [45, 31]).**

A category with families (CwF) is a tuple $\mathcal{C}=(\mathcal{C},\mathrm{Ty},\mathrm{Tm},\_\{\_\},T,\_.\_,\mathrm{p},\mathrm{v},\langle\_,\_\rangle_{\_})$, where

• •

$\mathcal{C}$ is a category with a terminal object $T\in\mathcal{C}$;

• •

$\mathrm{Ty}$ assigns, to each object $\Gamma\in\mathcal{C}$, a set $\mathrm{Ty}(\Gamma)$ of types in the context $\Gamma$;

• •

$\mathrm{Tm}$ assigns, to each pair $(\Gamma,A)$ of an object $\Gamma\in\mathcal{C}$ and a type $A\in\mathrm{Ty}(\Gamma)$, a set $\mathrm{Tm}(\Gamma,A)$ of terms of type $A$ in the context $\Gamma$;

• •

To each $\phi:\Delta\to\Gamma$ in $\mathcal{C}$, $\_\{\_\}$ assigns a map $\_\{\phi\}:\mathrm{Ty}(\Gamma)\to\mathrm{Ty}(\Delta)$, called the substitution on types, and a family $(\_\{\phi\}_{A})_{A\in\mathrm{Ty}(\Gamma)}$ of maps $\_\{\phi\}_{A}:\mathrm{Tm}(\Gamma,A)\to\mathrm{Tm}(\Delta,A\{\phi\})$, called the substitutions on terms;

• •

$\_.\_$ assigns, to each pair $(\Gamma,A)$ of a context $\Gamma\in\mathcal{C}$ and a type $A\in\mathrm{Ty}(\Gamma)$, a context $\Gamma.A\in\mathcal{C}$, called the comprehension of $A$;

• •

$\mathrm{p}$ (resp. $\mathrm{v}$) associates each pair $(\Gamma,A)$ of a context $\Gamma\in\mathcal{C}$ and a type $A\in\mathrm{Ty}(\Gamma)$ with a morphism $\mathrm{p}_{A}:\Gamma.A\to\Gamma$ in $\mathcal{C}$ (resp. a term $\mathrm{v}_{A}\in\mathrm{Tm}(\Gamma.A,A\{\mathrm{p}_{A}\})$), called the first projection on $A$ (resp. the second projection on $A$);

• •

$\langle\_,\_\rangle_{\_}$ assigns, to each triple $(\phi,A,\check{\alpha})$ of a morphism $\phi:\Delta\to\Gamma$ in $\mathcal{C}$, a type $A\in\mathrm{Ty}(\Gamma)$ and a term $\check{\alpha}\in\mathrm{Tm}(\Delta,A\{\phi\})$, a morphism $\langle\phi,\check{\alpha}\rangle_{A}:\Delta\to\Gamma.A$ in $\mathcal{C}$, called the extension of $\phi$ by $\check{\alpha}$,

that satisfies, for any $\Theta\in\mathcal{C}$, $\varphi:\Theta\to\Delta$ and $\alpha\in\mathrm{Tm}(\Gamma,A)$, the equations

• •

(Ty-Id) $A\{\mathrm{id}_{\Gamma}\}=A$;

• •

(Ty-Comp) $A\{\phi\circ\varphi\}=A\{\phi\}\{\varphi\}$;

• •

(Tm-Id) $\alpha\{\mathrm{id}_{\Gamma}\}_{A}=\alpha$;

• •

(Tm-Comp) $\alpha\{\phi\circ\varphi\}_{A}=\alpha\{\phi\}_{A}\{\varphi\}_{A\{\phi\}}$;

• •

(Cons-L) $\mathrm{p}_{A}\circ\langle\phi,\check{\alpha}\rangle_{A}=\phi$;

• •

(Cons-R) $\mathrm{v}_{A}\{\langle\phi,\check{\alpha}\rangle_{A}\}=\check{\alpha}$;

• •

(Cons-Nat) $\langle\phi,\check{\alpha}\rangle_{A}\circ\varphi=\langle\phi\circ\varphi,\check{\alpha}\{\varphi\}_{A\{\phi\}}\rangle_{A}$;

• •

(Cons-Id) $\langle\mathrm{p}_{A},\mathrm{v}_{A}\rangle_{A}=\mathrm{id}_{\Gamma.A}$.

Roughly, judgements of MLTT are interpreted in a CwF $\mathcal{C}$ by

{mathpar} ⊢Γ ctx ↦⟦Γ ⟧∈C and Γ⊢A  type ↦⟦A ⟧∈Ty(⟦Γ ⟧) and Γ⊢a : A ↦⟦a ⟧∈Tm(⟦Γ ⟧, ⟦A ⟧) and ⊢Γ= Δ ctx ⇒⟦Γ ⟧= ⟦Δ ⟧ and Γ⊢A = B  type ⇒⟦A ⟧= ⟦B ⟧ and Γ⊢a = a’ : A ⇒⟦a ⟧= ⟦a’ ⟧,

where $\llbracket\_\rrbracket$ denotes the semantic map or interpretation. See [31] for the details.

Let us now turn to introducing our game-semantic CwF:

Definition 4.10** (A game-semantic CwF).**

We define a CwF $\mathbb{WPG}$ as follows:

• •

The category $\mathbb{WPG}$ is given in Definition 3.12, and $T\in\mathbb{WPG}$ in Example 3.4;

• •

$\mathrm{Ty}(\Gamma)\colonequals\mathscr{D}^{\mathrm{w}}(\Gamma)$ ($\Gamma\in\mathbb{WPG}$) and $\mathrm{Tm}(\Gamma,A)\colonequals\mathbb{WPG}(\Pi(\Gamma,A))$ ($A\in\mathscr{D}^{\mathrm{w}}(\Gamma)$);

• •

Given $\phi:\Delta\rightarrow\Gamma$ in $\mathbb{WPG}$, define $\_\{\phi\}:\mathrm{Ty}(\Gamma)\to\mathrm{Ty}(\Delta)$ by $|A\{\phi\}|\colonequals|A|$ and $A\{\phi\}(\delta_{0}^{\dagger})\colonequals A(\phi^{\dagger}\bullet\delta_{0})$ for all $A\in\mathrm{Ty}(\Gamma)$ and $\delta_{0}^{\dagger}\in\mathbb{WPG}(\oc\Delta)$, and define $\_\{\phi\}_{A}:\mathrm{Tm}(\Gamma,A)\to\mathrm{Tm}(\Delta,A\{\phi\})$ by $\alpha\{\phi\}_{A}\colonequals\alpha\bullet\phi$ for all $\alpha\in\mathrm{Tm}(\Gamma,A)$;

• •

$\Gamma.A\colonequals\Sigma(\Gamma,A)$, $\mathrm{p}_{A}\colonequals\mathrm{der}_{|\Gamma|}:\Sigma(\Gamma,A)\rightarrow\Gamma$, $\mathrm{v}_{A}\colonequals\mathrm{der}_{|A|}:\Pi(\Sigma(\Gamma,A),A\{\mathrm{p}_{A}\})$ and $\langle\phi,\check{\alpha}\rangle_{A}\colonequals\langle\phi,\check{\alpha}\rangle:\Delta\rightarrow\Sigma(\Gamma,A)$ ($\check{\alpha}\in\mathrm{Tm}(\Delta,A\{\phi\})$).

Given $\Gamma\in\mathbb{WPG}$ and $A\in\mathscr{D}^{\mathrm{w}}(\Gamma)$, we write $\mathbb{WPG}(\Gamma,A)$ for $\mathrm{Tm}(\Gamma,A)$. We often omit subscripts on components of $\mathbb{WPG}$ when they are evident.

Theorem 4.11** (A well-defined game-semantic CwF).**

The category $\mathbb{WPG}$ together with the structures defined in Definition 4.10 gives rise to a CwF.

Proof.

We focus on substitution of terms, second projections and extensions since the other structures of $\mathbb{WPG}$ are straightforward to check (e.g., the equational axioms on morphisms and terms in $\mathbb{WPG}$ simply follow from Theorem 3.13). Let $\Gamma,\Delta\in\mathbb{WPG}$, $A\in\mathscr{D}^{\mathrm{w}}(\Gamma)$, $\phi\in\mathbb{WPG}(\Delta,\Gamma)$, $\alpha\in\mathbb{WPG}(\Gamma,A)$ and $\check{\alpha}\in\mathbb{WPG}(\Delta,A\{\phi\})$.

On $\alpha\{\phi\}=\alpha\bullet\phi\in\mathbb{WPG}(|\Delta|,|A|)$,121212The following argument is based on the proof of Lemma 3.11 on composition. we see by induction on the lengths of positions that $(\overline{\alpha\{\phi\}})_{|\Pi(\Delta,A\{\phi\})|}\preccurlyeq\Pi(\Delta,A\{\phi\})(\alpha\{\phi\})$ follows from $\phi\in\mathbb{WPG}(\Delta,\Gamma)$ and $\alpha\in\mathbb{WPG}(\Gamma,A)$. The same induction also shows that $\alpha\{\phi\}\cap\Pi(\Delta,A\{\phi\})(\alpha\{\phi\}):\Pi(\Delta,A\{\phi\})(\alpha\{\phi\})$ is winning and w.b., proving $\alpha\{\phi\}\in\mathbb{WPG}(\Delta,A\{\phi\})$.

The same induction proves $\mathrm{v}_{A}=\mathrm{der}_{|A|}\in\mathbb{WPG}(\Sigma(\Gamma,A),A\{\mathrm{p}_{A}\})$, where the point is that the pi $\Pi(\Gamma,A)$ and the sigma $\Sigma(\Gamma,A)$ are defined by the same family $A^{\star}$.

Finally, on $\langle\phi,\check{\alpha}\rangle\in\mathbb{WPG}(|\Delta|,|\Gamma|\mathbin{\&}|A|)$, the same induction shows that $\langle\phi,\check{\alpha}\rangle\in\mathbb{WPG}(\Delta,\Sigma(\Gamma,A))$ follows from $\phi\in\mathbb{WPG}(\Delta,\Gamma)$ and $\check{\alpha}\in\mathbb{WPG}(\Delta,A\{\phi\})$, where the fixed $\phi$ in $\langle\phi,\check{\alpha}\rangle$ plays a crucial role even if a play in $\Pi(\Delta,\Sigma(\Gamma,A))$ starts in $A$. ∎

It is notable that terms in the CwF $\mathbb{WPG}$ are simply a certain class of strategies, and constructions on terms are those on strategies. This point is quite desirable since it means that the results/techniques on existing game semantics are also available for our game semantics of MLTT. It also implies that our game semantics inherits the advantages of existing game semantics (§1.2) such as intensionality (§4.6).

4.5 Game-semantic type formers

Nevertheless, CwFs only model the fragment of MLTT common to all types. Hence, in this section, we equip the CwF $\mathbb{WPG}$ with semantic type formers [31] that model One-, Zero-, N-, Pi-, Sigma- and Id-types.

4.5.1 Game semantics of Pi-types

We begin with Pi-types. Recall first their semantic type former in an arbitrary CwF:

Definition 4.12** (CwFs with Pi-types [31]).**

A CwF $\mathcal{C}$ supports Pi-types if

• •

($\Pi$-Form) Given $\Gamma\in\mathcal{C}$, $A\in\mathrm{Ty}(\Gamma)$ and $B\in\mathrm{Ty}(\Gamma.A)$, there is a type $\Pi(A,B)\in\mathrm{Ty}(\Gamma)$, where we also write $A\Rightarrow B$ for $\Pi(A,B)$ if $B\{\langle\mathrm{id}_{\Gamma},\alpha\rangle\}=B\{\langle\mathrm{id}_{\Gamma},\alpha^{\prime}\rangle\}\in\mathrm{Ty}(\Gamma)$ for all $\alpha,\alpha^{\prime}\in\mathrm{Tm}(\Gamma,A)$;

• •

($\Pi$-Intro) Given $\beta\in\mathrm{Tm}(\Gamma.A,B)$, there is a term $\lambda_{A,B}(\beta)\in\mathrm{Tm}(\Gamma,\Pi(A,B))$;

• •

($\Pi$-Elim) Given $\kappa\in\mathrm{Tm}(\Gamma,\Pi(A,B))$ and $\alpha\in\mathrm{Tm}(\Gamma,A)$, there is a term $\mathrm{App}_{A,B}(\kappa,\alpha)\in\mathrm{Tm}(\Gamma,B\{\overline{\alpha}\})$, where $\overline{\alpha}\colonequals\langle\mathrm{id}_{\Gamma},\alpha\rangle_{A}:\Gamma\to\Gamma.A$;

• •

($\Pi$-Comp) $\mathrm{App}_{A,B}(\lambda_{A,B}(\beta),\alpha)=\beta\{\overline{\alpha}\}$;

• •

($\Pi$-Subst) Given $\Delta\in\mathcal{C}$ and $\phi:\Delta\to\Gamma$ in $\mathcal{C}$, $\Pi(A,B)\{\phi\}=\Pi(A\{\phi\},B\{\phi_{A}^{+}\})$, where $\phi_{A}^{+}\colonequals\langle\phi\circ\mathrm{p}_{A\{\phi\}},\mathrm{v}_{A\{\phi\}}\rangle_{A}:\Delta.A\{\phi\}\to\Gamma.A$;

• •

($\lambda$-Subst) $\lambda_{A,B}(\beta)\{\phi\}=\lambda_{A\{\phi\},B\{\phi_{A}^{+}\}}(\beta\{\phi_{A}^{+}\})\in\mathrm{Tm}(\Delta,\Pi(A\{\phi\},B\{\phi_{A}^{+}\}))$;

• •

(App-Subst) $\mathrm{App}_{A,B}(\kappa,\alpha)\{\phi\}=\mathrm{App}_{A\{\phi\},B\{\phi_{A}^{+}\}}(\kappa\{\phi\},\alpha\{\phi\})\in\mathrm{Tm}(\Delta,B\{\overline{\alpha}\}\{\phi\})$.

Furthermore, $\mathcal{C}$ strictly supports Pi-types if it additionally satisfies

• •

($\lambda$-Uniq) $\lambda_{A,B}\circ\mathrm{App}_{A\{\mathrm{p}_{A}\},B\{(\mathrm{p}_{A})_{A\{\mathrm{p}_{A}\}}^{+}\}}(\kappa\{\mathrm{p}_{A}\},\mathrm{v}_{A})=\kappa$.

Pi-types (with $\eta$-rule) are modelled in a CwF that (strictly) supports Pi-types [31]. Let us now proceed to show that the CwF $\mathbb{WPG}$ strictly supports Pi-types.

Lemma 4.13** (Currying).**

Given $\Gamma\in\mathbb{WPG}$, $A\in\mathscr{D}^{\mathrm{w}}(\Gamma)$ and $B\in\mathscr{D}^{\mathrm{w}}(\Sigma(\Gamma,A))$, there is a bijection $\lambda_{A,B}:\mathbb{WPG}(\Sigma(\Gamma,A),B)\stackrel{{\scriptstyle\sim}}{{\rightarrow}}\mathbb{WPG}(\Gamma,\Pi(A,B))$, where $\Pi(A,B)\in\mathscr{D}^{\mathrm{w}}(\Gamma)$ is defined by $|\Pi(A,B)|\colonequals|A|\Rightarrow|B|$ and $\Pi(A,B)(\gamma_{0}^{\dagger})\colonequals\Pi(A(\gamma_{0}^{\dagger}),B_{\gamma_{0}^{\dagger}})$ for all $\gamma_{0}^{\dagger}\in\mathbb{WPG}(\oc\Gamma)$, and $B_{\gamma_{0}^{\dagger}}\in\mathscr{D}^{\mathrm{w}}(A(\gamma_{0}^{\dagger}))$ by $|B_{\gamma_{0}^{\dagger}}|\colonequals|B|$ and $B_{\gamma_{0}^{\dagger}}(\alpha_{0}^{\dagger})\colonequals B(\langle\gamma_{0},\alpha_{0}\rangle^{\dagger})$ for all $\alpha_{0}^{\dagger}\in\mathbb{WPG}(\oc A(\gamma_{0}^{\dagger}))$.

Proof.

Let $\phi\in\mathbb{WPG}(\Sigma(\Gamma,A),B)$; we first construct $\phi^{\prime}\in\mathbb{WPG}(\Gamma,\Pi(A,B))$ from $\phi$ as follows. By the isomorphism $|\oc\Sigma(\Gamma,A)|=\oc(|\Gamma|\mathbin{\&}|A|)\cong\oc|\Gamma|\otimes\oc|A|$, we adjust ‘tags’ or curry $\phi$ with respect to the adjunction between tensor $\otimes$ and linear implication $\multimap$ [35], obtaining another strategy $\phi^{\prime}:|\Gamma|\Rightarrow(|A|\Rightarrow|B|)$.

Next, let us verify $\overline{\phi^{\prime}}_{|\Pi(\Gamma,\Pi(A,B))|}\preccurlyeq\Pi(\Gamma,\Pi(A,B))(\phi^{\prime})$ by induction on the length of positions, where again the only nontrivial case is the inductive step on even-length positions. This inductive step goes through by $\phi\in\mathbb{WPG}(\Sigma(\Gamma,A),B)$ thanks to the correspondence between the constraints on $\Pi(\Sigma(\Gamma,A),B)(\phi)$ and $\Pi(\Gamma,\Pi(A,B))(\phi^{\prime})$.

The same argument also shows that $\phi^{\prime}\cap\Pi(\Gamma,\Pi(A,B))(\phi^{\prime}):\Pi(\Gamma,\Pi(A,B))(\phi^{\prime})$ is winning and w.b., and hence we have proven $\lambda_{A,B}(\phi)\colonequals\phi^{\prime}\in\mathbb{WPG}(\Gamma,\Pi(A,B))$.

Finally, the inverse of this construction $\lambda_{A,B}$ is given in the same vein. ∎

Example 4.14**.**

Define $N_{b}^{+}\in\mathscr{D}^{\mathrm{w}}(\Sigma(N,N_{b}))$ by $|N_{b}^{+}|\colonequals N$ and $N_{b}^{+}(\langle\underline{k},\underline{n}\rangle^{\dagger})\colonequals N_{b}(\underline{k+n}^{\dagger})$ for all $k,n\in\mathbb{N}$ such that $k\geqslant n$. Then, Lemma 4.13 allows us to obtain $\lambda_{N_{b},N_{b}^{+}}(\mathrm{der}_{N})\in\mathbb{WPG}(N,\Pi(N_{b},N_{b}^{+}))$ from $\mathrm{der}_{N}=\mathrm{v}_{N_{b}^{+}}\in\mathbb{WPG}(\Sigma(N,N_{b}),N_{b}^{+})$.

Theorem 4.15** (Game semantics of Pi-types).**

$\mathbb{WPG}$* strictly supports Pi-types.*

Proof.

Let $\Gamma\in\mathbb{WPG}$, $A\in\mathscr{D}^{\mathrm{w}}(\Gamma)$, $B\in\mathscr{D}^{\mathrm{w}}(\Sigma(\Gamma,A))$ and $\beta\in\mathbb{WPG}(\Sigma(\Gamma,A),B)$.

• •

($\Pi$-Form) $\Pi(A,B)\in\mathscr{D}^{\mathrm{w}}(\Gamma)$ is defined in Lemma 4.13.

• •

($\Pi$-Intro) By Lemma 4.13, we obtain $\lambda_{A,B}(\beta)\in\mathbb{WPG}(\Gamma,\Pi(A,B))$. We often omit the subscripts $(\_)_{A,B}$ on $\lambda_{A,B}$ and the inverse $\lambda_{A,B}^{-1}$.

• •

($\Pi$-Elim) $\mathrm{App}_{A,B}(\kappa,\alpha)\colonequals\lambda_{A,B}^{-1}(\kappa)\{\overline{\alpha}\}$ for all $\kappa\in\mathbb{WPG}(\Gamma,\Pi(A,B))$ and $\alpha\in\mathbb{WPG}(\Gamma,A)$. We indeed have $\mathrm{App}_{A,B}(\kappa,\alpha)=\lambda_{A,B}^{-1}(\kappa)\{\overline{\alpha}\}\in\mathbb{WPG}(\Gamma,B\{\overline{\alpha}\})$ by Theorem 4.11. We often omit the subscripts $(\_)_{A,B}$ on $\mathrm{App}_{A,B}$.

• •

($\Pi$-Comp) $\mathrm{App}_{A,B}(\lambda_{A,B}(\beta),\alpha)=\lambda_{A,B}^{-1}(\lambda_{A,B}(\beta))\{\overline{\alpha}\}=\beta\{\overline{\alpha}\}$.

• •

($\Pi$-Subst) Let $\Delta\in\mathbb{WPG}$ and $\phi\in\mathbb{WPG}(\Delta,\Gamma)$. For the first components, we have $|\Pi(A,B)\{\phi\}|=|\Pi(A,B)|=|A|\Rightarrow|B|=|A\{\phi\}|\Rightarrow|B\{\phi_{A}^{+}\})|=|\Pi(A\{\phi\},B\{\phi_{A}^{+}\})|$. For the second components, we have

[TABLE]

where the second equation holds since for all $\hat{\alpha}_{0}^{\dagger}\in\mathbb{WPG}(\oc A(\phi^{\dagger}\circ\delta_{0}^{\dagger}))$ we have

[TABLE]

We have shown $\|\Pi(A,B)\{\phi\}\|=\|\Pi(A\{\phi\},B\{\phi_{A}^{+}\})\|$ as well.

• •

($\lambda$-Subst) By the definition of $\lambda$, we have $\lambda_{A,B}(\beta)\{\phi\}=\lambda_{A\{\phi\},B\{\phi_{A}^{+}\}}(\beta\{\phi_{A}^{+}\})$.

• •

(App-Subst) We have

[TABLE]

• •

($\lambda$-Uniq) We have

[TABLE]

which completes the proof. ∎

4.5.2 Game semantics of Sigma-types

Next, we consider Sigma-types. Again, let us first recall their general semantic type former in an arbitrary CwF:

Definition 4.16** (CwFs with Sigma-types [31]).**

A CwF $\mathcal{C}$ supports Sigma-types if

• •

($\Sigma$-Form) Given $\Gamma\in\mathcal{C}$, $A\in\mathrm{Ty}(\Gamma)$ and $B\in\mathrm{Ty}(\Gamma.A)$, there is a type $\Sigma(A,B)\in\mathrm{Ty}(\Gamma)$, where we also write $A\times B$ for $\Sigma(A,B)$ if $B\{\langle\mathrm{id}_{\Gamma},\alpha\rangle\}=B\{\langle\mathrm{id}_{\Gamma},\alpha^{\prime}\rangle\}\in\mathrm{Ty}(\Gamma)$ for all $\alpha,\alpha^{\prime}\in\mathrm{Tm}(\Gamma,A)$;

• •

($\Sigma$-Intro) There is a morphism $\mathrm{Pair}_{A,B}:\Gamma.A.B\to\Gamma.\Sigma(A,B)$ in $\mathcal{C}$;

• •

($\Sigma$-Elim) Given $P\in\mathrm{Ty}(\Gamma.\Sigma(A,B))$ and $\rho\in\mathrm{Tm}(\Gamma.A.B,P\{\mathrm{Pair}_{A,B}\})$, there is a term $\mathcal{R}^{\Sigma}_{A,B,P}(\rho)\in\mathrm{Tm}(\Gamma.\Sigma(A,B),P)$;

• •

($\Sigma$-Comp) $\mathcal{R}^{\Sigma}_{A,B,P}(\rho)\{\mathrm{Pair}_{A,B}\}=\rho$;

• •

($\Sigma$-Subst) Given $\Delta\in\mathcal{C}$ and $\phi:\Delta\to\Gamma$ in $\mathcal{C}$, $\Sigma(A,B)\{\phi\}=\Sigma(A\{\phi\},B\{\phi_{A}^{+}\})$, where $\phi_{A}^{+}\colonequals\langle\phi\circ\mathrm{p}_{A\{\phi\}},\mathrm{v}_{A\{\phi\}}\rangle_{A}:\Delta.A\{\phi\}\to\Gamma.A$;

• •

(Pair-Subst) $\mathrm{p}_{\Sigma(A,B)}\circ\mathrm{Pair}_{A,B}=\mathrm{p}_{A}\circ\mathrm{p}_{B}$ and $\phi_{\Sigma(A,B)}^{+}\circ\mathrm{Pair}_{A\{\phi\},B\{\phi_{A}^{+}\}}=\mathrm{Pair}_{A,B}\circ\phi^{++}_{A,B}$, where $\phi^{++}_{A,B}\colonequals(\phi_{A}^{+})^{+}_{B}:\Delta.A\{\phi\}.B\{\phi_{A}^{+}\}\to\Gamma.A.B$;

• •

($\mathcal{R}^{\Sigma}$-Subst) $\mathcal{R}^{\Sigma}_{A,B,P}(p)\{\phi^{+}_{\Sigma(A,B)}\}=\mathcal{R}^{\Sigma}_{A\{f\},B\{\phi_{A}^{+}\},P\{\phi^{+}_{\Sigma(A,B)}\}}(p\{\phi_{A,B}^{++}\})$.

In addition, $\mathcal{C}$ strictly supports Sigma-types if it also satisfies

• •

($\mathcal{R}^{\Sigma}$-Uniq) $\check{\rho}=\mathcal{R}^{\Sigma}_{A,B,P}(\rho)$ if $\check{\rho}\in\mathrm{Tm}(\Gamma.\Sigma(A,B),P)$ and $\check{\rho}\{\mathrm{Pair}_{A,B}\}=\rho$.

Sigma-types (with $\eta$-rule) are modelled in a CwF that (strictly) supports Sigma-types [31]. Now, we show that our CwF $\mathbb{WPG}$ strictly supports Sigma-types:

Theorem 4.17** (Game semantics of Sigma-types).**

$\mathbb{WPG}$* strictly supports Sigma-types.*

Proof.

Let $\Gamma\in\mathbb{WPG}$, $A\in\mathscr{D}^{\mathrm{w}}(\Gamma)$, $B\in\mathscr{D}^{\mathrm{w}}(\Sigma(\Gamma,A))$ and $P\in\mathscr{D}^{\mathrm{w}}(\Sigma(\Gamma,\Sigma(A,B)))$.

• •

($\Sigma$-Form) Similarly to pi $\Pi$, $\Sigma(A,B)\colonequals(|A|\mathbin{\&}|B|,(\Sigma(A(\gamma_{0}^{\dagger}),B_{\gamma_{0}^{\dagger}}))_{\gamma_{0}^{\dagger}\in\mathbb{WPG}(\oc\Gamma)})$.

• •

($\Sigma$-Intro) By the evident bijection $\Sigma(\Sigma(\Gamma,A),B)\cong\Sigma(\Gamma,\Sigma(A,B))$, define $\mathrm{Pair}_{A,B}:\Sigma(\Sigma(\Gamma,A),B)\rightarrow\Sigma(\Gamma,\Sigma(A,B))$ in $\mathbb{WPG}$ to be the dereliction up to ‘tags,’ i.e., $\mathrm{Pair}_{A,B}\colonequals\langle\mathrm{p}_{A}\bullet\mathrm{p}_{B},\langle\mathrm{v}_{A}\{\mathrm{p}_{B}\},\mathrm{v}_{B}\rangle\rangle$. Note that the inverse $\mathrm{Pair}^{-1}_{A,B}$ is $\langle\langle\mathrm{p}_{\Sigma(A,B)},\varpi^{A,B}_{1}\rangle,\varpi^{A,B}_{2}\rangle$, where $\varpi^{A,B}_{1}:\Sigma(\Gamma,\Sigma(A,B))\rightarrow A\{\mathrm{p}_{\Sigma(A,B)}\}$ and $\varpi^{A,B}_{2}:\Sigma(\Gamma,\Sigma(A,B))\rightarrow B\{\langle\mathrm{p}_{\Sigma(A,B)},\varpi^{A,B}_{1}\rangle\}$ are the derelictions up to ‘tags.’

• •

($\Sigma$-Elim) Given $\rho\in\mathbb{WPG}(\Sigma(\Sigma(\Gamma,A),B),P\{\mathrm{Pair}_{A,B}\})$, define $\mathcal{R}^{\Sigma}_{A,B,P}(\rho)\colonequals\rho\{\mathrm{Pair}_{A,B}^{-1}\}\in\mathbb{WPG}(\Sigma(\Gamma,\Sigma(A,B)),P\{\mathrm{Pair}_{A,B}\}\{\mathrm{Pair}_{A,B}^{-1}\})=\mathbb{WPG}(\Sigma(\Gamma,\Sigma(A,B)),P)$.

• •

($\Sigma$-Comp) We have

[TABLE]

• •

($\Sigma$-Subst) Similar to the case of pi $\Pi$ (Theorem 4.15).

• •

(Pair-Subst) $\mathrm{p}_{\Sigma(A,B)}\bullet\mathrm{Pair}_{A,B}=\mathrm{p}_{\Sigma(A,B)}\bullet\langle\mathrm{p}_{A}\bullet\mathrm{p}_{B},\langle\mathrm{v}_{A}\{\mathrm{p}_{B}\},\mathrm{v}_{B}\rangle\rangle=\mathrm{p}_{A}\bullet\mathrm{p}_{B}$ and

[TABLE]

• •

($\mathcal{R}^{\Sigma}$-Subst) We have

[TABLE]

• •

($\mathcal{R}^{\Sigma}$-Uniq) Given $\check{\rho}\in\mathbb{WPG}(\Sigma(\Gamma,\Sigma(A,B)),P)$ with $\check{\rho}\{\mathrm{Pair}_{A,B}\}=\rho$, we have

[TABLE]

which completes the proof. ∎

4.5.3 Game semantics of N-type

We next present our game semantics of N-type. Again, we first recall the general semantic type former for N-type in an arbitrary CwF:

Definition 4.18** (CwFs with N-type [31]).**

A CwF $\mathcal{C}$ supports N-type if

• •

($N$-Form) Given $\Gamma\in\mathcal{C}$, there is a type $N^{[\Gamma]}\in\mathrm{Ty}(\Gamma)$. We abbreviate it as $N$.

• •

($N$-Intro) There are a term $\underline{0}_{\Gamma}\in\mathrm{Tm}(\Gamma,N)$ and a morphism $\mathrm{succ}_{\Gamma}:\Gamma.N\to\Gamma.N$ in $\mathcal{C}$ that satisfy for any morphisms $\phi:\Delta\to\Gamma$ and $\psi:\Delta.N\to\Gamma$ in $\mathcal{C}$ {mathpar} 0_Γ { ϕ} = 0_Δ∈Tm(Δ, N) and p_N ∘succ_Γ = p_N : Γ. N →Γ and succ_Γ ∘⟨ψ, v_N ⟩_N = ⟨ψ, v_N{succ_Δ} ⟩_N : Δ. N →Γ. N,

where the last equation makes sense since $\mathrm{succ}_{\Gamma}\circ\langle\psi,\mathrm{v}_{N}\rangle_{N},\langle\psi,\mathrm{v}_{N}\{\mathrm{succ}_{\Delta}\}\rangle_{N}:\Delta.N\to\Gamma.N$ by $N$-Subst given below. We henceforth skip the same remark.

Notation*.*

Define $\mathrm{zero}_{\Gamma}\colonequals\langle\mathrm{id}_{\Gamma},\underline{0}_{\Gamma}\rangle_{N}:\Gamma\to\Gamma.N$ for each $\Gamma\in\mathcal{C}$; it satisfies $\mathrm{zero}_{\Gamma}\circ\phi=\langle\phi,\underline{0}_{\Delta}\rangle_{N}=\langle\phi,\mathrm{v}_{N}\{\mathrm{zero}_{\Delta}\}\rangle_{N}:\Delta\to\Gamma.N$ for any $\phi:\Delta\to\Gamma$ in $\mathcal{C}$. We often omit the subscript $(\_)_{\Gamma}$ on $\underline{0}$, $\mathrm{zero}$ and $\mathrm{succ}$. Define $\underline{n}_{\Gamma}\in\mathrm{Tm}(\Gamma,N)$ for each $n\in\mathbb{N}$ by: $\underline{0}_{\Gamma}$ is already given, and $\underline{n+1}_{\Gamma}\colonequals\mathrm{v}_{N}\{\mathrm{succ}_{\Gamma}\circ\langle\mathrm{id}_{\Gamma},\underline{n}_{\Gamma}\rangle_{N}\}$.

• •

($N$-Elim) Given a type $P\in\mathrm{Ty}(\Gamma.N)$, and terms $c_{\mathrm{z}}\in\mathrm{Tm}(\Gamma,P\{\mathrm{zero}\})$ and $c_{\mathrm{s}}\in\mathrm{Tm}(\Gamma.N.P,P\{\mathrm{succ}\circ\mathrm{p}_{P}\})$, there is a term $\mathcal{R}^{N}_{P}(c_{\mathrm{z}},c_{\mathrm{s}})\in\mathrm{Tm}(\Gamma.N,P)$;

• •

($N$-Comp) We have

[TABLE]

• •

($N$-Subst) $N^{[\Gamma]}\{\phi\}=N^{[\Delta]}\in\mathrm{Ty}(\Delta)$;

• •

($\mathcal{R}^{N}$-Subst) $\mathcal{R}^{N}_{P}(c_{\mathrm{z}},c_{\mathrm{s}})\{\phi_{N}^{+}\}=\mathcal{R}^{N}_{P\{\phi_{N}^{+}\}}(c_{\mathrm{z}}\{\phi\},c_{\mathrm{s}}\{\phi_{N,P}^{++}\})\in\mathrm{Tm}(\Delta.N,P\{\phi_{N}^{+}\})$, where $\phi_{N}^{+}\colonequals\langle\phi\circ\mathrm{p}_{N},\mathrm{v}_{N}\rangle_{N}:\Delta.N\to\Gamma.N$ and $\phi_{N,P}^{++}\colonequals(\phi_{N}^{+})^{+}_{P}:\Delta.N.P\{\phi_{N}^{+}\}\to\Gamma.N.P$.

Let us now present our game semantics of N-type, which is based on the standard game semantics of PCF [22]:

Theorem 4.19** (Game semantics of N-type).**

$\mathbb{WPG}$* supports N-type.*

Proof.

Let $\Gamma,\Delta\in\mathbb{WPG}$, $\phi\in\mathbb{WPG}(\Delta,\Gamma)$ and $\psi\in\mathbb{WPG}(\Sigma(\Delta,\{N\}_{\oc\Delta}),\Gamma)$.

• •

($N$-Form) $N^{[\Gamma]}$ is the constant one $\{N\}_{\oc\Gamma}\in\mathscr{D}^{\mathrm{w}}(\Gamma)$ at $N$ (Example 3.4).

• •

($N$-Intro) $\underline{0}_{\Gamma}\in\mathbb{WPG}(\Gamma,\{N\})$ is $\underline{0}:N$ (Examples 2.8 and 3.4) up to ‘tags,’ and $\mathrm{succ}_{\Gamma}\colonequals\langle\mathrm{p},\mathrm{sc}_{\Gamma}\rangle\in\mathbb{WPG}(\Sigma(\Gamma,\{N\}),\Sigma(\Gamma,\{N\}))$, where we define $\mathrm{sc}_{\Gamma}\colonequals\mathrm{Pref}(\{\,q_{[1]}q_{[0]}n_{[0]}(n+1)_{[1]}\mid n\in\mathbb{N}\,\})^{\mathrm{Even}}\in\mathbb{WPG}(\Sigma(\Gamma,\{N_{[0]}\}),\{N_{[1]}\})$.

Clearly, we have $\underline{0}_{\Gamma}\bullet\phi=\underline{0}_{\Delta}$ and $\mathrm{sc}_{\Gamma}\bullet\langle\psi,\mathrm{v}_{\{N\}_{\Delta}}\rangle=\mathrm{sc}_{\Delta}=\mathrm{v}_{\{N\}_{\Delta}}\{\mathrm{succ}_{\Delta}\}$, and therefore the required three equations hold.

• •

($N$-Elim) Given $P\in\mathscr{D}^{\mathrm{w}}(\Sigma(\Gamma,\{N\}))$, $c_{\mathrm{z}}\in\mathbb{WPG}(\Gamma,P\{\mathrm{zero}\})$ and $c_{\mathrm{s}}\in\mathbb{WPG}(\Sigma(\Sigma(\Gamma,\{N\}),P),P\{\mathrm{succ}\bullet\mathrm{p}_{P}\})$, there are two terms

[TABLE]

where note that $\mathrm{v}\in\mathbb{WPG}(\Sigma(\Pi(\Sigma(\Gamma,\{N\}),P),\{\Sigma(\Gamma,\{N\})\}),\{\Sigma(\Gamma,\{N\})\}\{\mathrm{p}\})$ is just $\pi_{2}\in\mathbb{WPG}(\Pi((\Gamma\mathbin{\&}N),P)\mathbin{\&}(\Gamma\mathbin{\&}N),\Gamma\mathbin{\&}N)$, defined respectively by

[TABLE]

where $\mathrm{ev}_{P}\in\mathbb{WPG}(\Sigma(\Pi(\Sigma(\Gamma,\{N\}),P),\{\Sigma(\Gamma,\{N\})\}),P\{\mathrm{v}\})$ is the evaluation [16], i.e., $\mathrm{ev}_{P}\colonequals\lambda^{-1}(\mathrm{der}_{\Pi(\Sigma(\Gamma,\{N\}),P)})$.

Next, we define $\mathrm{pred}_{\Gamma}\colonequals\langle\mathrm{p},\mathrm{pd}_{\Gamma}\rangle\in\mathbb{WPG}(\Sigma(\Gamma,\{N\}),\Sigma(\Gamma,\{N\}))$, where $\mathrm{pd}_{\Gamma}\colonequals\mathrm{Pref}(\{q_{[1]}q_{[0]}0_{[0]}0_{[1]}\}\cup\{\,q_{[1]}q_{[0]}(n+1)_{[0]}n_{[1]}\mid n\in\mathbb{N}\,\})^{\mathrm{Even}}\in\mathbb{WPG}(\Sigma(\Gamma,\{N_{[0]}\}),\{N_{[1]}\})$, and often omit the subscript $(\_)_{\Gamma}$ on $\mathrm{pred}$. Besides, let $\mathrm{cond}_{P}\in\mathbb{WPG}(\Sigma(\Sigma(\Sigma(\Gamma,\{N\}),P\{\mathrm{zero}\bullet\mathrm{p}\}),P\{\mathrm{succ}\bullet\mathrm{pred}\bullet\mathrm{p}\}),P\{\mathrm{p}\bullet\mathrm{p}\})$ be the game semantics of conditionals [33, 34, 22]: Given any initial move, it asks the number $n$ on $N$, and plays as the dereliction between $P\{\mathrm{zero}\bullet\mathrm{p}\}$ and $P\{\mathrm{p}\bullet\mathrm{p}\}$ if $n=0$, and between $P\{\mathrm{succ}\bullet\mathrm{pred}\bullet\mathrm{p}\}$ and $P\{\mathrm{p}\bullet\mathrm{p}\}$ otherwise.

We then define $\mathcal{F}^{N}_{P}(c_{\mathrm{z}},c_{\mathrm{s}})\in\mathbb{WPG}(\Pi(\Sigma(\Gamma,\{N\}),P),\Pi(\Sigma(\Gamma,\{N\}),P))$ by

[TABLE]

which is well-defined thanks to the equation $(\mathrm{succ}\bullet\mathrm{v})\bullet\langle\mathrm{p},\mathrm{pred}\bullet\mathrm{v}\rangle=\mathrm{succ}\bullet\mathrm{pred}\bullet\mathrm{v}=(\mathrm{succ}\bullet\mathrm{pred}\bullet\mathrm{p})\bullet\langle\mathrm{v},\widetilde{c}_{\mathrm{z}}\rangle$.

Finally, let $\mathcal{R}^{N}_{P}(c_{\mathrm{z}},c_{\mathrm{s}})\in\mathbb{WPG}(\Sigma(\Gamma,\{N\}),P)$ be the least upper bound of the chain $(\mathcal{R}^{N}_{P}(c_{\mathrm{z}},c_{\mathrm{s}})_{n}:\Pi(\Sigma(\Gamma,\{N\}),P))_{n\in\mathbb{N}}$ given by {mathpar} R^N_P(c_z, c_s)_0 \colonequals{ ϵ } and R^N_P(c_z, c_s)_n+1 \colonequalsF^N_P(c_z, c_s) ∙R^N_P(c_z, c_s)_n.

The difference from the game semantics of fixed-point combinator [33, 34, 22] is that the strategy $\mathrm{pred}$ occurring in $\mathcal{F}^{N}_{P}(c_{\mathrm{z}},c_{\mathrm{s}})$ (3) decreases the parameter number on $N$ at every recursive call by $\mathcal{F}^{N}_{P}(c_{\mathrm{z}},c_{\mathrm{s}})$, so that $\mathcal{R}^{N}_{P}(c_{\mathrm{z}},c_{\mathrm{s}})$ is total.

• •

($N$-Comp) By the definition of $\mathcal{R}^{N}_{P}(c_{\mathrm{z}},c_{\mathrm{s}})$, we clearly have

[TABLE]

• •

($N$-Subst) It is clear that $\{N\}_{\oc\Gamma}\{\phi\}=\{N\}_{\oc\Delta}$ holds.

• •

($\mathcal{R}^{N}$-Subst) Finally, by the definition of $\mathcal{R}^{N}_{P}(c_{\mathrm{z}},c_{\mathrm{s}})$, we clearly have

[TABLE]

(or alternatively show $\mathcal{R}^{N}_{P}(c_{\mathrm{z}},c_{\mathrm{s}})_{n}\{\phi_{N}^{+}\}=\mathcal{R}^{N}_{P\{\phi_{N}^{+}\}}(c_{\mathrm{z}}\{\phi\},c_{\mathrm{s}}\{\phi_{N,P}^{++}\})_{n}$ for all $n\in\mathbb{N}$ by induction on $n$ so that the above equation holds), which completes the proof. ∎

4.5.4 Game semantics of One- and Zero-types

Next, we interpret One- and Zero-types. Since it is trivial to interpret these types, we only sketch the proof. See [31] for the semantic type formers for these types.

Theorem 4.20** (Game semantics of One- and Zero-types).**

$\mathbb{WPG}$* supports the semantic type formers for One- (in the strict sense) and Zero-types.*

Proof (sketch).

We model One- and Zero-types by the constant dependent p-games at the terminal p-game $T$ and the empty p-game $\bm{0}$, respectively (Example 3.4).

The only point on One-type is that there is only the trivial one $\{\bm{\epsilon}\}\in\mathbb{WPG}(\Gamma,\{T\})$ for any $\Gamma\in\mathbb{WPG}$, so that we can interpret all the rules of One-type.

Finally, given $A\in\mathscr{D}^{\mathrm{w}}(\Sigma(\Gamma,\{\bm{0}\}))$ and $\zeta\in\mathbb{WPG}(\Gamma,\{\bm{0}\})$, the only point on Zero-type is that for the elimination rule we may obtain $\mathcal{R}^{\bm{0}}_{A}(\zeta)\in\mathbb{WPG}(\Gamma,A\{\langle\mathrm{id}_{\Gamma},\zeta\rangle\})$ from $\zeta$ by case distinction: Let $\mathcal{R}^{\bm{0}}_{A}(\zeta)$ be the one obtained from $\zeta$ by replacing the unique first move $q$ of $\bm{0}$ in $\zeta$ with those of $|A|$ if any, and $\mathcal{R}^{\bm{0}}_{A}(\zeta)\colonequals\{\bm{\epsilon}\}$ otherwise. ∎

4.5.5 Game semantics of Id-types

Let us proceed to present our game semantics of Id-types. Again, we first review the general semantic type former for Id-types in an arbitrary CwF:

Definition 4.21** (CwFs with Id-types [31]).**

A CwF $\mathcal{C}$ supports Id-types if

• •

(Id-Form) Given $\Gamma\in\mathcal{C}$ and $A\in\mathrm{Ty}(\Gamma)$, there is a type $\mathrm{Id}_{A}\in\mathrm{Ty}(\Gamma.A.A^{+})$, where $A^{+}\colonequals A\{\mathrm{p}_{A}\}\in\mathrm{Ty}(\Gamma.A)$;

• •

(Id-Intro) There is a morphism $\mathrm{Refl}_{A}:\Gamma.A\rightarrow\Gamma.A.A^{+}.\mathrm{Id}_{A}$ in $\mathcal{C}$ that satisfies $\mathrm{p}_{\mathrm{Id}_{A}}\circ\mathrm{Refl}_{A}=\overline{\mathrm{v}_{A}}:\Gamma.A\rightarrow\Gamma.A.A^{+}$, where $\overline{\mathrm{v}_{A}}\colonequals\langle\mathrm{id}_{\Gamma.A},\mathrm{v}_{A}\rangle$;

• •

(Id-Elim) Given $B\in\mathrm{Ty}(\Gamma.A.A^{+}.\mathrm{Id}_{A})$ and $\beta\in\mathrm{Tm}(\Gamma.A,B\{\mathrm{Refl}_{A}\})$, there is a term $\mathcal{R}^{\mathrm{Id}}_{A,B}(\beta)\in\mathrm{Tm}(\Gamma.A.A^{+}.\mathrm{Id}_{A},B)$;

• •

(Id-Comp) $\mathcal{R}^{\mathrm{Id}}_{A,B}(\beta)\{\mathrm{Refl}_{A}\}=\beta$;

• •

(Id-Subst) $\mathrm{Id}_{A}\{\phi_{A,A^{+}}^{++}\}=\mathrm{Id}_{A\{\phi\}}\in\mathrm{Ty}(\Delta.A\{\phi\}.A\{\phi\}^{+})$ for all $\Delta\in\mathcal{C}$ and $\phi:\Delta\to\Gamma$ in $\mathcal{C}$, where $\phi_{A}^{+}\colonequals\langle\phi\circ\mathrm{p}_{A\{\phi\}},\mathrm{v}_{A\{\phi\}}\rangle_{A}:\Delta.A\{\phi\}\to\Gamma.A$ and $\phi_{A,A^{+}}^{++}\colonequals(\phi_{A}^{+})^{+}_{A^{+}}:\Delta.A\{\phi\}.A^{+}\{\phi_{A}^{+}\}\to\Gamma.A.A^{+}$;

• •

(Refl-Subst) $\mathrm{Refl}_{A}\circ\phi_{A}^{+}=\phi_{A,A^{+},\mathrm{Id}_{A}}^{+++}\circ\mathrm{Refl}_{A\{\phi\}}:\Delta.A\{\phi\}\to\Gamma.A.A^{+}.\mathrm{Id}_{A}$, where $\phi_{A,A^{+},\mathrm{Id}_{A}}^{+++}\colonequals(\phi_{A,A^{+}}^{++})^{+}_{\mathrm{Id}_{A}}:\Delta.A\{\phi\}.A^{+}\{\phi^{+}\}.\mathrm{Id}_{A\{\phi\}}\to\Gamma.A.A^{+}.\mathrm{Id}_{A}$;

• •

($\mathcal{R}^{\mathrm{Id}}$-Subst) $\mathcal{R}^{\mathrm{Id}}_{A,B}(\beta)\{\phi_{A,A^{+},\mathrm{Id}_{A}}^{+++}\}=\mathcal{R}^{\mathrm{Id}}_{A\{\phi\},B\{\phi_{A,A^{+},\mathrm{Id}_{A}}^{+++}\}}(\beta\{\phi_{A}^{+}\})$.

Then, we present our game semantics of Id-types, which is essentially the same as the interpretation of Id-types by Abramsky et al. [23, 29]:

Theorem 4.22** (Game semantics of Id-types).**

$\mathbb{WPG}$* supports Id-types.*

Proof.

Let $\Gamma\in\mathbb{WPG}$, $A\in\mathscr{D}^{\mathrm{w}}(\Gamma)$ and $B\in\mathscr{D}^{\mathrm{w}}(\Sigma(\Sigma(\Sigma(\Gamma,A),A^{+}),\mathrm{Id}_{A}))$.

• •

(Id-Form) Let $\bm{1}$ be the flat game $\mathrm{flat}(\{\mathbin{\surd}\})$ (Example 2.8), where $\{\mathbin{\surd}\}$ is an arbitrarily fixed singleton set. Define $\mathrm{Id}_{A}\in\mathscr{D}^{\mathrm{w}}(\Sigma(\Sigma(\Gamma,A),A^{+}))$ by $|\mathrm{Id}_{A}|\colonequals\bm{1}$ and \mathrm{Id}_{A}(\langle\langle\gamma_{0},\alpha_{0}\rangle,\alpha_{0}^{\prime}\rangle^{\dagger})\colonequals\begin{cases}(\bm{1},\kappa_{\bm{1}})&\text{if \alpha_{0}=\alpha_{0}^{\prime};}\\ (\bm{1},\kappa_{\bm{0}})&\text{otherwise,}\end{cases} for all $\langle\langle\gamma_{0},\alpha_{0}\rangle,\alpha_{0}^{\prime}\rangle^{\dagger}\in\mathbb{WPG}(\oc\Sigma(\Sigma(\Gamma,A),A^{+}))$, where $\kappa_{X}$ is the constant family at $X$ ($X=\bm{1},\bm{0}$);

• •

(Id-Intro) Define $\mathrm{Refl}_{A}\colonequals\langle\overline{\mathrm{v}_{A}},\mathrm{refl}_{A}\rangle\in\mathbb{WPG}(\Sigma(\Gamma,A),\Sigma(\Sigma(\Sigma(\Gamma,A),A^{+}),\mathrm{Id}_{A}))$, where $\mathrm{refl}_{A}\in\mathbb{WPG}(\Sigma(\Gamma,A),\mathrm{Id}_{A}\{\overline{\mathrm{v}_{A}}\})$ is $\underline{\surd}:\bm{1}$ (Example 2.8) up to ‘tags.’ Note that $\mathrm{refl}_{A}$ is well-defined since its codomain is always the game $\bm{1}$.

• •

(Id-Elim) Given $\beta\in\mathbb{WPG}(\Sigma(\Gamma,A),B\{\mathrm{Refl}_{A}\})$, let us construct the strategy $\mathcal{R}^{\mathrm{Id}}_{A,B}(\beta)\in\mathbb{WPG}(\Sigma(\Sigma(\Sigma(\Gamma,A_{[0]}),A_{[1]}^{+}),\mathrm{Id}_{A}),B)$ such that given any initial move in $B$ it makes the move $q$ in $\mathrm{Id}_{A}$, and if O plays there by $\surd$, then it plays as $\beta$ between $\Sigma(\Gamma,A_{[0]})$ and $B$ in the rest of the play. Since there is the evident bijection $\mathbb{WPG}(\Sigma(\Gamma,A))\cong\mathbb{WPG}(\Sigma(\Sigma(\Sigma(\Gamma,A),A^{+}),\mathrm{Id}_{A}))$ thanks to the definition of $\mathrm{Id}_{A}$, $\mathcal{R}^{\mathrm{Id}}_{A,B}(\beta)$ can play as $\beta$ after the initial two moves.

Having gone through the detailed proofs of Theorems 4.15 and 4.17, it is a routine to verify Id-Comp, Id-Subst and Refl-Subst. Also, essentially the same interpretation of Id-types is given by Abramsky et al. [23, 29]. Hence, we leave it to the reader. ∎

4.6 Intensionality

We next show the intensionality of our game semantics. In this section, we focus on the components of $\mathbb{WPG}$ definable by MLTT with One-, Zero-, N-, Pi-, Sigma- and Id-types (see [31] for the interpretation) and formulate type-theoretic principles in $\mathbb{WPG}$. In the following, let us also fix an arbitrary CwF $\mathcal{C}$ that supports One-, Zero-, N-, Pi-, Sigma- and Id-types, and assume $\Gamma\in\mathcal{C}$, $A\in\mathrm{Ty}(\Gamma)$ and $B\in\mathrm{Ty}(\Gamma.A)$.

Equality reflection.

Equality reflection [11] states that propositionally equal terms are judgmentally equal: $\alpha=\alpha^{\prime}\in\mathrm{Tm}(\Gamma,A)$ if $\mathrm{Tm}(\Gamma,\mathrm{Id}_{A}\{\langle\langle\mathrm{id},\alpha\rangle,\alpha^{\prime}\rangle\})$ is inhabited.

Equality reflection fails in our game semantics: $N\mathbin{\&}\bm{0}\stackrel{{\scriptstyle\pi_{1}}}{{\rightarrow}}N$ and $N\mathbin{\&}\bm{0}\stackrel{{\scriptstyle\mathrm{succ}}}{{\rightarrow}}N\mathbin{\&}\bm{0}\stackrel{{\scriptstyle\pi_{1}}}{{\rightarrow}}N$ are different definable terms in $\mathbb{WPG}(\Sigma(N,\{\bm{0}\}),\{N\})$, but the elimination rule on Zero-type gives a definable one $\rho\in\mathbb{WPG}(\Sigma(N,\{\bm{0}\}),\mathrm{Id}_{N}\{\langle\langle\mathrm{id},\pi_{1}\bullet\mathrm{succ}\rangle,\pi_{1}\rangle\})$.

Recall that $\rho$ is the strategy that makes, after the initial move $q$ on the codomain is made by O, the move $q$ in $\bm{0}$ on the domain (see the proof of Theorem 4.20).

Function extensionality.

Function extensionality [10] postulates that if terms of a Pi-type are propositionally equal as a function, then they are propositionally equal, i.e., the inhabitance of the type $\Pi(A,\mathrm{Id}_{B}\{\langle\langle\mathrm{id},\mathrm{App}(\psi\{\mathrm{p}\},\mathrm{v})\rangle,\mathrm{App}(\psi^{\prime}\{\mathrm{p}\},\mathrm{v})\rangle\})\Rightarrow\mathrm{Id}_{\Pi(A,B)}\{\langle\langle\mathrm{id},\psi\rangle,\psi^{\prime}\rangle\}\in\mathrm{Ty}(\Gamma)$ for all terms $\psi,\psi^{\prime}\in\mathrm{Tm}(\Gamma,\Pi(A,B))$.

Our game semantics refutes function extensionality since terms $\psi\in\mathbb{WPG}(\Gamma,A)$ are in general not completely specified by their extensions $\gamma:\oc\Gamma\mapsto\phi\circ\gamma$. To see this point closely, consider, e.g., the terms $\underline{0},\underline{0}^{\prime}\in\mathbb{WPG}(T,\Pi(\{N_{[0]}\},\{N_{[1]}\}))$ defined by $\underline{0}\colonequals\mathrm{Pref}(\{\,q_{[1]}q_{[0]}n_{[0]}0_{[1]}\mid n\in\mathbb{N}\,\})^{\mathrm{Even}}$ and $\underline{0}^{\prime}\colonequals\mathrm{Pref}(\{q_{[1]}0_{[1]}\})^{\mathrm{Even}}$. They are definable in MLTT by the introduction and the elimination rules of N-type. Then, for the reason mentioned above, the function extensionality on these terms fails.

Criteria of intensionality.

There are Streicher’s Criteria of Intensionality [47]:

$\mathrm{v}\{\mathrm{p}\circ\mathrm{p}\}\neq\mathrm{v}\{\mathrm{p}\}\in\mathrm{Tm}(\Gamma.A.A^{+}.\mathrm{Id}_{A},A\{\mathrm{p}\circ\mathrm{p}\circ\mathrm{p}\})$; 2. 2.

$B\{\langle\mathrm{p}\circ\mathrm{p}\circ\mathrm{p},\mathrm{v}\{\mathrm{p}\circ\mathrm{p}\rangle\}\}\neq B\{\langle\mathrm{p}\circ\mathrm{p}\circ\mathrm{p},\mathrm{v}\{\mathrm{p}\}\rangle\}\in\mathrm{Tm}(\Gamma.A.A^{+}.\mathrm{Id}_{A})$; 3. 3.

If $\mathrm{Tm}(T,\mathrm{Id}_{S}\{\langle\langle\mathrm{id}_{T},\sigma\rangle,\sigma^{\prime}\rangle\})$ is inhabited, then $\sigma=\sigma^{\prime}\in\mathrm{Tm}(T,S)$,

for all $\Gamma\in\mathcal{C}$, $A\in\mathrm{Ty}(\Gamma)$, $B\in\mathrm{Ty}(\Gamma.A)$, $S\in\mathrm{Ty}(T)$ and $\sigma,\sigma^{\prime}\in\mathrm{Tm}(T,S)$.

Our game semantics satisfies the first criterion. For example, let $\Gamma\colonequals T$, $A\colonequals\{N\}_{\oc T}$ and $B\colonequals\{N\}_{\oc\Sigma(T,\{N\})}$. Then, $\mathrm{v}\{\mathrm{p}\circ\mathrm{p}\}$ is $T\mathbin{\&}N\mathbin{\&}N\mathbin{\&}\mathrm{Id}_{\{N\}}\stackrel{{\scriptstyle\pi_{1}}}{{\rightarrow}}T\mathbin{\&}N\mathbin{\&}N\stackrel{{\scriptstyle\pi_{1}}}{{\rightarrow}}T\mathbin{\&}N\stackrel{{\scriptstyle\pi_{2}}}{{\rightarrow}}N$, and $\mathrm{v}\{\mathrm{p}\}$ is $T\mathbin{\&}N\mathbin{\&}N\mathbin{\&}\mathrm{Id}_{\{N\}}\stackrel{{\scriptstyle\pi_{1}}}{{\rightarrow}}T\mathbin{\&}N\mathbin{\&}N\stackrel{{\scriptstyle\pi_{2}}}{{\rightarrow}}N$. They are distinct.

In contrast, our game semantics does not satisfy the second criterion as dependent p-games are indexed by winning strategies: Any $\tau\in\mathbb{WPG}(\oc\Sigma(\Sigma(\Sigma(\Gamma,A),A^{+}),\mathrm{Id}_{A}))$ must be of the form $\tau=\langle\langle\langle\gamma_{0},\alpha_{0}\rangle,\alpha_{0}^{\prime}\rangle,\underline{\surd}\rangle^{\dagger}$ such that $\alpha_{0}=\alpha_{0}^{\prime}$. In other words, our game semantics of dependent types is extensional as opposed to that of terms.

Finally, our model satisfies the third criterion: Any $\rho\in\mathbb{WPG}(T,\mathrm{Id}_{S}\{\langle\langle\mathrm{id}_{T},\sigma\rangle,\sigma^{\prime}\rangle\})$ must be the strategy $\underline{\surd}$ (up to ‘tags’) since it is winning, and hence $\sigma=\sigma^{\prime}$.

4.7 Independence of Markov’s principle

Markov’s principle (MP) [26] is a subtle principle in constructive mathematics and computability theory. In fact, it depends on the school of constructive mathematics whether MP should be regarded as constructive. Roughly, MP postulates that if it is impossible that there is no natural number $n\in\mathbb{N}$ such that $f(n)=0$ for a given function $f:\mathbb{N}\rightarrow\mathbb{N}$, then there is a natural number $n^{\prime}\in\mathbb{N}$ such that $f(n^{\prime})=0$.

We can formulate MP in MLTT as the type

[TABLE]

where $\mathsf{\neg A}$ abbreviates $\mathsf{A\Rightarrow\bm{0}}$ for any type $\mathsf{A}$, and $\mathsf{0}$, $\mathsf{N}$, $\mathsf{\Rightarrow}$, $\mathsf{\Pi}$, $\mathsf{\Sigma}$ and $\mathsf{Id_{N}}$ are Zero-, N-, implication, Pi-, Sigma- and Id-types, respectively.

Mannaa and Coquand [25] have shown that MP is independent from MLTT; i.e., there is no term of the type (4) in MLTT. Their proof of this result is syntactic.

However, even representative computational models of MLTT such as the effective topos [27] validate MP. Besides, it is easy to see that the model by Blot and Laird [24] validates MP too (though this is hardly surprising as their model admits classical reasonings [24, §8]). In other words, there is a gap between MLTT and these models.

In this context, we illustrate the precision of our game semantics of MLTT by:

Corollary 4.23** (Game semantics refutes Markov’s principle).**

There is no game-semantic term on the interpretation of (4) in $\mathbb{WPG}$. Hence, the game semantics of MLTT in $\mathbb{WPG}$ (§4.4–4.5) implies that MP is independent from MLTT.

Proof (sketch).

Assume for a contradiction that there is a term on the interpretation of (4) in $\mathbb{WPG}$, which is the p-game

[TABLE]

where we omit the terminal p-game $T$ and the bracket $\{\_\}$ for constant dependent p-games; e.g., we write $N$ for $T.\{N\}$. We call $\Sigma(N_{[6]},\mathrm{Id}_{N}\{\langle\mathrm{App}(\pi_{1},\pi_{2}),\underline{0}\rangle\}_{[7]})$ the codomain, and $N_{[0]}\Rightarrow N_{[1]}$ and \big{(}\Sigma(N_{[2]},\mathrm{Id}_{N}\{\langle\mathrm{App}(\pi_{1},\pi_{2}),\underline{0}\rangle\}_{[3]})\Rightarrow\bm{0}_{[4]}\big{)}\Rightarrow\bm{0}_{[5]} the outer and the inner domains of (5). We write $\langle\phi,\psi\rangle$ for the assumed term.

Assume first that there are total input strategies $\varphi^{\dagger}:\oc(N_{[0]}\Rightarrow N_{[1]})$ and $\langle\underline{n},\underline{\surd}\rangle^{\dagger}:\oc\Sigma(N_{[2]},\mathrm{Id}_{N}\{\langle\mathrm{App}(\pi_{1},\pi_{2}),\underline{0}\rangle\}_{[3]})$ on which $\phi$ eventually makes a P-move $n^{\prime}_{\varphi}$ in $N_{[6]}$ when O begins a play in $N_{[6]}$. If $\varphi\bullet\underline{n^{\prime}_{\varphi}}\neq\underline{0}$ for some of these $\varphi$ and $n$, and O plays by them, then $\mathrm{Id}_{N}\{\langle\mathrm{App}(\pi_{1},\pi_{2}),\underline{0}\rangle\}_{[7]}$ can be the empty p-game $\bm{0}$, and $\psi$ plays on the domains forever, contradicting its noetherianity. If $\varphi\bullet\underline{n^{\prime}_{\varphi}}=\underline{0}$ for all $\varphi$ and $n$, then $\phi$ is strict since otherwise $n^{\prime}_{\varphi}$ is the same even when O slightly changes $\varphi$ so that $\varphi\bullet\underline{n^{\prime}_{\varphi}}\neq\underline{0}$, a contradiction; hence, $\phi$ is strict and answers the question in $N_{[6]}$ yet with no answer to the question in $\bm{0}_{[4]}$, contradicting the well-bracketing of $\phi$.

Thus, given any total inputs $\varphi^{\dagger}$ and $\langle\underline{n},\underline{\surd}\rangle^{\dagger}$, $\phi$ does not make a P-move in $N_{[6]}$. Similarly to the case of $\psi$, however, this contradicts the noetherianity of $\phi$. ∎

4.8 Game semantics of subtyping on dependent types

Finally, we show that p-games enable us to interpret subtyping on dependent types. The subtyping relation between types is something like the subset relation between sets, and it is mainly to ensure that if $\alpha$ is a term of a type $A$, and $A$ is a subtype of a type $B$, then $\mathrm{coe}(\alpha)$ is a term of $B$ that computes in the same way as $\alpha$, where $\mathrm{coe}$ is an operation on terms, called coercion. Therefore, subtyping has a pragmatic importance since it ensures reusability of terms in different types.

Let us first formulate a subtyping relation between dependent types in CwFs:

Definition 4.24** (CwFs with subtyping).**

A CwF $\mathcal{C}$ that supports One-, Pi- and Sigma-types supports subtyping (on One-, Pi- and Sigma-types) if it is equipped with a partial order $\trianglelefteqslant_{\Gamma}$ on $\mathrm{Ty}(\Gamma)$ for each $\Gamma\in\mathcal{C}$ that satisfies

\big{(}A\trianglelefteqslant_{\Gamma}A^{\prime}\wedge\alpha\in\mathrm{Tm}(\Gamma,A)\big{)}\Rightarrow\alpha\in\mathrm{Tm}(\Gamma,A^{\prime}); 2. 2.

\big{(}A\trianglelefteqslant_{\Gamma}A^{\prime}\wedge\phi\in\mathcal{C}(\Delta,\Gamma)\big{)}\Rightarrow A\{\phi\}\trianglelefteqslant_{\Delta}A^{\prime}\{\phi\}; 3. 3.

$\forall\Gamma\in\mathcal{C},A\in\mathrm{Ty}(\Gamma).\,A\trianglelefteqslant_{\Gamma}\bm{1}$; 4. 4.

\big{(}A\trianglelefteqslant_{\Gamma}A^{\prime}\wedge B\trianglelefteqslant_{\Gamma.A^{\prime}}B^{\prime}\big{)}\Rightarrow\big{(}\Pi(A^{\prime},B)\trianglelefteqslant_{\Gamma}\Pi(A,B^{\prime})\wedge\Sigma(A,B)\trianglelefteqslant_{\Gamma}\Sigma(A^{\prime},B^{\prime})\big{)}.

The first axiom requires the reusability of terms. In addition, for the compositional nature of denotational semantics, the other axioms require that constructions on types preserve $\trianglelefteqslant_{\Gamma}$. Note that the last axiom tacitly assumes $B,B^{\prime}\in\mathrm{Ty}(\Gamma.A)$, and the order between $A$ and $A^{\prime}$ is flipped in Pi-types as fewer morphisms can take more inputs [12, p. 419]. We define game semantics of subtyping based on Definition 3.1:

Definition 4.25** (Predicate liveness ordering).**

The predicate (p-) liveness ordering is a partial order $\trianglelefteqslant$ between p-games $\Gamma$ and $\Delta$ defined by $\Gamma\trianglelefteqslant\Delta\Leftrightarrow/|\Gamma|=|\Delta|\wedge\forall\gamma:|\Gamma|.\,\Gamma(\gamma)\preccurlyeq\Delta(\Gamma)$, and lifted to the one $\trianglelefteqslant_{\Gamma}$ between linearly dependent p-games $L$ and $R$ over $\Gamma$ by $L\trianglelefteqslant_{\Gamma}R\Leftrightarrow/|L|=|R|\wedge\forall\gamma:\Gamma.\,L(\gamma)\trianglelefteqslant R(\gamma)$.

It is easy to see that the p-liveness orderings $\trianglelefteqslant$ and $\trianglelefteqslant_{\Gamma}$ are partial orders since so is the liveness ordering $\preccurlyeq$ [42, Theorem 9]. Besides, the p-liveness ordering $\trianglelefteqslant_{\Gamma}$ clearly satisfies the second and the third axioms of Definition 4.24, where $\bm{1}=\{T\}$.

Moreover, if $\gamma:\Gamma$ and $\Gamma\trianglelefteqslant\Delta$, then $\gamma:\Delta$ since $\gamma:|\Gamma|=|\Delta|$ and $\overline{\gamma}_{|\Delta|}=\overline{\gamma}_{|\Gamma|}\preccurlyeq\Gamma(\gamma)\preccurlyeq\Delta(\gamma)$. This observation shows that $\trianglelefteqslant_{\Gamma}$ also satisfies the first axiom:

Lemma 4.26** (Preservation of linear typing under predicate liveness ordering).**

Let $L$ and $R$ be linearly dependent p-games over a p-game $\Gamma$ such that $L\trianglelefteqslant_{\Gamma}R$.

If $\psi:\Pi_{\ell}(\Gamma,L)$, then $\psi:\Pi_{\ell}(\Gamma,R)$; 2. 2.

If $\psi:\Pi_{\ell}(\Gamma,L)$ is winning (resp. w.b.), then so is $\psi:\Pi_{\ell}(\Gamma,R)$.

Further, $\trianglelefteqslant_{\Gamma}$ satisfies the last axiom as well by:

Lemma 4.27** (Preservation of predicate liveness ordering).**

If $\Delta\trianglelefteqslant\Delta^{\prime}$ and $\Gamma\trianglelefteqslant\Gamma^{\prime}$, then $\Delta\otimes\Gamma\trianglelefteqslant\Delta^{\prime}\otimes\Gamma^{\prime}$, $\Delta\mathbin{\&}\Gamma\trianglelefteqslant\Delta^{\prime}\mathbin{\&}\Gamma^{\prime}$, $\oc\Delta\trianglelefteqslant\oc\Delta^{\prime}$ and $\Delta^{\prime}\multimap\Gamma\trianglelefteqslant\Delta\multimap\Gamma^{\prime}$. Moreover, if $A\trianglelefteqslant_{\Gamma}A^{\prime}$ and $B\trianglelefteqslant_{\Gamma.A^{\prime}}B^{\prime}$, then $\Pi(A^{\prime},B)\trianglelefteqslant_{\Gamma}\Pi(A,B^{\prime})$ and $\Sigma(A,B)\trianglelefteqslant_{\Gamma}\Sigma(A^{\prime},B^{\prime})$. (N.b., strictly, the pair $(|B|,\|B\|\upharpoonright\Gamma.A)$, where $\|B\|\upharpoonright\Gamma.A$ is the restriction of $\|B\|$ to $\mathrm{st}(\Gamma.A)\subseteq\mathrm{st}(\Gamma.A^{\prime})$, not $B$ itself, is an element of $\mathscr{D}(\Gamma.A)$, and similarly for $B^{\prime}$.)

Proof.

For the first part, we focus on linear implication $\multimap$ since the cases of the other constructions are simpler. First, observe $|\Delta^{\prime}\multimap\Gamma|=|\Delta^{\prime}|\multimap|\Gamma|=|\Delta|\multimap|\Gamma^{\prime}|=|\Delta\multimap\Gamma^{\prime}|$. Next, let $\phi:|\Delta^{\prime}\multimap\Gamma|$; it remains to show $(\Delta^{\prime}\multimap\Gamma)(\phi)\preccurlyeq(\Delta\multimap\Gamma^{\prime})(\phi)$, but it follows from $\Delta\trianglelefteqslant\Delta^{\prime}$ and $\Gamma\trianglelefteqslant\Gamma^{\prime}$ by induction on the lengths of positions, where the symmetry (between O and P) of the liveness ordering $\preccurlyeq$ is crucial.

Finally, we show the second part by essentially the same way as the first part. ∎

Hence, we have finally shown:

Corollary 4.28** (Game semantics of subtyping).**

$\mathbb{WPG}$* supports subtyping.*

Acknowledgements

The author acknowledges the financial support from the Funai Foundation, and he is grateful to fruitful discussions with Samson Abramsky and Thierry Coquand.