The present paper introduces a novel notion of `(effective) computability', called viability, of strategies in game semantics in an intrinsic (i.e., without recourse to the standard Church-Turing computability), non-inductive and non-axiomatic manner, and shows, as a main technical achievement, that viable strategies are Turing complete. Consequently, we have given a mathematical foundation of computation in the same sense as Turing machines but beyond computation on natural numbers, e.g., higher-order computation, in a more abstract fashion. As immediate corollaries, some of the well-known theorems in computability theory such as the smn-theorem and the first recursion theorem are generalized. Notably, our game-semantic framework distinguishes `high-level' computational processes that operate directly on mathematical objects such as natural numbers (not on their symbolic representations) and their `symbolic implementations' that define their `computability', which sheds new light on the very concept of computation. This work is intended to be a stepping stone towards a new mathematical foundation of computation, intuitionistic logic and constructive mathematics.
Based on the work on the algebraic theory of actors and game semantics for asynchronous $π$ calculus, we give the full abstraction proof of game semantics for actors.
We introduce operational semantics into games. And based on the operational semantics, we establish a full algebra of games, including basic algebra of games, algebra of concurrent games, recursion and abstraction. The algebra can be used widely to reason on the behaviors of systems (not only computational systems) with game theory supported.
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 define a game semantics for second order classical arithmetic PA2 (with quantifiers over predicates on integers and full comprehension axiom). Our semantics is effective: moves are described by a finite amount of information and whenever there is some winning strategy for the player defending the truth of the formula, then there is some primitive recursive winning strategy. Then we show that our game semantics is sound and complete for the truth assignment for formulas of PA2. In our game model, the value of a predicate variable is some family of "generic" games. This value is "unknown" dur…
咖喱风格的系统F，即。从程序设计语言的角度来看，系统F没有显式的类型，可以被看作是多态性的核心表示。本文利用一个博弈模型，从语法和博弈语义域两方面给出了该语言类型同构的一个刻画。该模型包括：一个非类型化部分解释术语，一个博弈概念解释类型，一个类型化部分表示一个非类型化策略在一个博弈中起作用的事实。通过分析模型中的同构，我们证明了Curry型系统F的型同构所对应的方程组是Church型同构方程组的推广，并给出了一个新的非平凡方程：对于所有X. A = A[对于所有Y.Y/X]，如果X只在A中出现.
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 …
This paper revisits the well-established relationship between the modal mu calculus and parity games to show that it is even more robust than previously known. It addresses the question of whether the descriptive complexity of modal mu model-checking games, previously known to depend on the syntactic complexity of a formula, depends in fact on its semantic complexity. It shows that up to formulas of semantic co-Büchi complexity, the descriptive complexity of their model-checking games coincides exactly with their semantic complexity. Beyond co-Büchi, the descriptive complexity of the model-che…
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…
This article presents a new game semantics for Martin-Löf type theory (MLTT), in which each game is equipped with selected isomorphism strategies that represent (computational) proofs for (intensional) equality between strategies on the game. These isomorphism strategies interpret propositional equalities in MLTT. As a main result, we have obtained a first game semantics for MLTT that refutes the principle of uniqueness of identity proofs (UIP) and validates univalence axiom (UA) though it does not model non-trivial higher equalities. Categorically, our model forms a substructure of the classi…
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…
The non-commutative sequoid operator $\oslash$ on games was introduced to capture algebraically the presence of state in history-sensitive strategies in game semantics, by imposing a causality relation on the tensor product of games. Coalgebras for the functor $A \oslash \_$ - i.e. morphisms from $S$ to $A \oslash S$ - may be viewed as state transformers: if $A \oslash \_$ has a final coalgebra, $!A$, then the anamorphism of such a state transformer encapsulates its explicit state, so that it is shared only between successive invocations. We study the conditions under which a final coalgebra $…
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…
We present abstract complexity results about Coquand and Hyland-Ong game semantics, that will lead to new bounds on the length of first-order cut-elimination, normalization, interaction between expansion trees and any other dialogical process game semantics can model and apply to. In particular, we provide a novel method to bound the length of interactions between visible strategies and to measure precisely the tower of exponentials defining the worst-case complexity. Our study improves the old estimates on average by several exponentials.
We introduce versions of game-theoretic semantics (GTS) for Alternating-Time Temporal Logic (ATL). In GTS, truth is defined in terms of existence of a winning strategy in a semantic evaluation game, and thus the game-theoretic perspective appears in the framework of ATL on two semantic levels: on the object level in the standard semantics of the strategic operators, and on the meta-level where game-theoretic logical semantics is applied to ATL. We unify these two perspectives into semantic evaluation games specially designed for ATL. The game-theoretic perspective enables us to identify new va…
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…
Combinatorial games are widely used in finite model theory, constraint satisfaction, modal logic and concurrency theory to characterize logical equivalences between structures. In particular, Ehrenfeucht-Fraisse games, pebble games, and bisimulation games play a central role. We show how each of these types of games can be described in terms of an indexed family of comonads on the category of relational structures and homomorphisms. The index k is a resource parameter which bounds the degree of access to the underlying structure. The coKleisli categories for these comonads can be used to give …
University of Oxford（牛津大学）；University of Amsterdam（阿姆斯特丹大学）
In categorical compositional semantics of natural language one studies functors from a category of grammatical derivations (such as a Lambek pregroup) to a semantic category (such as real vector spaces). We compositionally build game-theoretic semantics of sentences by taking the semantic category to be the category whose morphisms are open games. This requires some modifications to the grammar category to compensate for the failure of open games to form a compact closed category. We illustrate the theory using simple examples of Wittgenstein's language-games.
We introduce a new game-theoretic semantics (GTS) for the modal mu-calculus. Our so-called bounded GTS replaces parity games with alternative evaluation games where only finite paths arise; infinite paths are not needed even when the considered transition system is infinite. The novel games offer alternative approaches to various constructions in the framework of the mu-calculus. For example, they have already been successfully used as a basis for an approach leading to a natural formula size game for the logic. While our main focus is introducing the new GTS, we also consider some application…
The present paper gives a mathematical, in particular, syntax-independent, formulation of intensionality and dynamics of computation in terms of games and strategies. Specifically, we give a game semantics for a higher-order programming language that distinguishes programs with the same value yet different algorithms (or intensionality), equipped with the hiding operation on strategies that precisely corresponds to the (small-step) operational semantics (or dynamics) of the language. Categorically, our games and strategies give rise to a cartesian closed bicategory, and our game semantics form…
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.
In the previous work, we have given a novel, game-semantic model of computation in an intrinsic, non-inductive and non-axiomatic manner, which is similar to Turing machines but beyond computation on natural numbers, e.g., higher-order computation. As the main theorem of the work, it has been shown that the game-semantic model may execute all the computation of the programming language PCF. The present paper revisits this result from an automata-theoretic perspective: It shows that deterministic non-erasing pushdown automata whose input tape is equipped with simple directed edges between cells …
In this paper, we develop a game-theoretic account of concurrent separation logic. To every execution trace of the Code confronted to the Environment, we associate a specification game where Eve plays for the Code, and Adam for the Environment. The purpose of Eve and Adam is to decompose every intermediate machine state of the execution trace into three pieces: one piece for the Code, one piece for the Environment, and one piece for the available shared resources. We establish the soundness of concurrent separation logic by interpreting every derivation tree of the logic as a winning strategy …
Game semantics has provided adequate models for a variety of programming languages, in which types are interpreted as two-player games and programs as strategies. Melliès (2018) suggested that such categories of games and strategies may be obtained as instances of a simple abstract construction on weak double categories. However, in the particular case of simple games, his construction slightly differs from the standard category. We refine the abstract construction using factorisation systems, and show that the new construction yields the standard category of simple games and strategies. Anoth…
An extension of QPTL is considered where functional dependencies among the quantified variables can be restricted in such a way that their current values are independent of the future values of the other variables. This restriction is tightly connected to the notion of behavioral strategies in game-theory and allows the resulting logic to naturally express game-theoretic concepts. The fragment where only restricted quantifications are considered, called behavioral quantifications, can be decided, for both model checking and satisfiability, in 2ExpTime and is expressively equivalent to QPTL, th…
We introduce a new game-theoretic semantics (GTS) for the modal mu-calculus. Our so-called bounded GTS replaces parity games with alternative evaluation games where only finite paths arise; infinite paths are not needed even when the considered transition system is infinite. The novel games offer alternative approaches to various constructions in the framework of the mu-calculus. For example, they have already been successfully used as a basis for an approach leading to a natural formula size game for the logic. While our main focus is introducing the new GTS, we also consider some application…
We prove consistency of intensional Martin-Löf type theory (MLTT) with formal Church's thesis (CT), which was open for at least fifteen years. The difficulty in proving the consistency is that a standard method of realizability à la Kleene does not work for the consistency, though it validates CT, as it does not model MLTT; specifically, the realizability does not validate MLTT's congruence rule on pi-types (known as the $ξ$-rule). We overcome this point and prove the consistency by novel realizability à la game semantics, which is based on the author's previous work.
We develop game-theoretic semantics (GTS) for the fragment ATL+ of the full Alternating-time Temporal Logic ATL*, essentially extending a recently introduced GTS for ATL. We first show that the new game-theoretic semantics is equivalent to the standard semantics of ATL+ (based on perfect recall strategies). We then provide an analysis, based on the new semantics, of the memory and time resources needed for model checking ATL+. Based on that, we establish that strategies that use only a very limited amount of memory suffice for ATL+. Furthermore, using the GTS we provide a new algorithm for mod…
We propose "semantic labelling" as a novel ingredient for solving games in the context of LTL synthesis. It exploits recent advances in the automata-based approach, yielding more information for each state of the generated parity game than the game graph can capture. We utilize this extra information to improve standard approaches as follows. (i) Compared to strategy improvement (SI) with random initial strategy, a more informed initialization often yields a winning strategy directly without any computation. (ii) This initialization makes SI also yield smaller solutions. (iii) While Q-learning…
