二阶同构的刻画是一个纯语法问题，我们建议在博弈语义学的启发下进行研究。我们在二阶$μ$ -演算的情况下研究这个问题，它可以被看作是系统F到经典逻辑的扩展，并且我们为它定义了一个范畴框架：控制超理论。我们的游戏模型的$μ$ -演算是基于多态竞技场（密切相关的休斯的超森林），在发挥（以下的想法Murawski Ong）。我们发现，类型同构与“平等”的舞台上与类型相一致。最后，我们从这个等式推出了型同构的等式刻画。我们也从相同的模型恢复Roberto Di Cosmo对系统F的型同构的刻画。这种方法导致几何理解的问题上的二阶型同构，它可以很容易地扩展到其他一些多态演算，包括额外的编程功能。
英文摘要：
The characterization of second-order type isomorphisms is a purely syntactical problem that we propose to study under the enlightenment of game semantics. We study this question in the case of second-order λ$μ$-calculus, which can be seen as an extension of system F to classical logic, and for which we define a categorical framework: control hyperdoctrines. Our game model of λ$μ$-calculus is based on polymorphic arenas (closely related to Hughes' hyperforests) which evolve during the play (following the ideas of Murawski-Ong). We show that type isomorphisms coincide with the "equality" on arenas associated with types. Finally we deduce the equational characterization of type isomorphisms from this equality. We also recover from the same model Roberto Di Cosmo's characterization of type isomorphisms for system F. This approach leads to a geometrical comprehension on the question of second order type isomorphisms, which can be easily extended to some other polymorphic calculi including additional programming features.
咖喱风格的系统F，即。从程序设计语言的角度来看，系统F没有显式的类型，可以被看作是多态性的核心表示。本文利用一个博弈模型，从语法和博弈语义域两方面给出了该语言类型同构的一个刻画。该模型包括：一个非类型化部分解释术语，一个博弈概念解释类型，一个类型化部分表示一个非类型化策略在一个博弈中起作用的事实。通过分析模型中的同构，我们证明了Curry型系统F的型同构所对应的方程组是Church型同构方程组的推广，并给出了一个新的非平凡方程：对于所有X. A = A[对于所有Y.Y/X]，如果X只在A中出现.
Game semantics and winning strategies offer a potential conceptual bridge between semantics and proof systems of logics. We illustrate this link for hybrid logic -- an extension of modal logic that allows for explicit reference to worlds within the language. The main result is that the systematic search of winning strategies over all models can be finitized and thus reformulated as a proof system.
Logics of non-sense allow a third truth value to express propositions that are \emph{nonsense}. These logics are ideal formalisms to understand how errors are handled in programs and how they propagate throughout the programs once they appear. In this paper, we give a Hintikkan game semantics for logics of non-sense and prove its correctness. We also discuss how a known solution method in game theory, the iterated elimination of strictly dominated strategies, relates to semantic games for logics of nonsense. Finally, we extend the logics of nonsense only by means of semantic games, developing …
We study the first-order axiomatisability of finite semiring interpretations or, equivalently, the question whether elementary equivalence and isomorphism coincide for valuations of atomic facts over a finite universe into a commutative semiring. Contrary to the classical case of Boolean semantics, where every finite structure can obviously be axiomatised up to isomorphism by a first-order sentence, the situation in semiring semantics is rather different, and strongly depends on the underlying semiring. We prove that for a number of important semirings, including min-max semirings, and the sem…
We present new game semantics of Martin-Löf 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 …
Game semantics has proven to be a robust method to give compositional semantics for a variety of higher-order programming languages. However, due to the complexity of most game models, game semantics has remained unapproachable for non-experts. In this paper, we aim at making game semantics more accessible by viewing it as a syntactic translation into a session typed pi-calculus, referred to as metalanguage, followed by a semantics interpretation of the metalanguage into a particular game model. The syntactic translation can be defined for a wide range of programming languages without knowledg…
We use a reformulation of compositional game theory to reunite game theory with game semantics, by viewing an open game as the System and its choice of contexts as the Environment. Specifically, the system is jointly controlled by $n \geq 0$ noncooperative players, each independently optimising a real-valued payoff. The goal of the system is to play a Nash equilibrium, and the goal of the environment is to prevent it. The key to this is the realisation that lenses (from functional programming) form a dialectica category, which have an existing game-semantic interpretation. In the second half o…
This paper presents a case study for the application of semiring semantics for fixed-point formulae to the analysis of strategies in Büchi games. Semiring semantics generalizes the classical Boolean semantics by permitting multiple truth values from certain semirings. Evaluating the fixed-point formula that defines the winning region in a given game in an appropriate semiring of polynomials provides not only the Boolean information on who wins, but also tells us how they win and which strategies they might use. This is well-understood for reachability games, where the winning region is definab…
This work extends the present author's computational game semantics of Martin-Löf type theory to the cumulative hierarchy of universes. This extension completes game semantics of all standard types of Martin-Löf type theory for the first time in the 30 years history of modern game semantics. As a result, the powerful combinatorial reasoning of game semantics becomes available for the study of universes and types generated by them. A main challenge in achieving game semantics of universes comes from a conflict between identity types and universes: Naive game semantics of the encoding of an iden…
TU Wien（维也纳工业大学）；Institute of Logic and Computation（逻辑与计算研究所）
In this paper, we introduce game-theoretic semantics (GTS) for Qualitative Choice Logic (QCL), which, in order to express preferences, extends classical propositional logic with an additional connective called ordered disjunction. Firstly, we demonstrate that game semantics can capture existing degree-based semantics for QCL in a natural way. Secondly, we show that game semantics can be leveraged to derive new semantics for the language of QCL. In particular, we present a new semantics that makes use of GTS negation and, by doing so, avoids problems with negation in existing QCL-semantics.
