We propose a fibred monoidal closed category of alternating tree automata. Our notion is based on Dialectica-like categories, suggested by the specific logical form of the transitions of alternating automata. The basic monoidal closed structure gives a realizability interpretation of proofs of a first-order multiplicative linear logic as winning strategies in corresponding acceptance games.
Moreover, we show that the usual powerset operation translating an alternating automaton to an equivalent non-deterministic one satisfies the deduction rules of the '!' modality of linear logic. We thus get a deduction system for intuitionistic linear logic, which in particular gives deduction for minimal intuitionistic predicate logic via the Girard translation. Using a suitable negative translation based on the '?' modality, we can interpret proofs of minimal classical logic, and also get a weak form of completeness of our realizers wrt language inclusion.
I shall present a modification of the Abramsky-Jagadeesan games model to allow sequences of moves indexed by transfinite ordinals. The motivation for this construction is work arising from work by Laird and Churchill in [1,2] concerning the sequoid operator. In , the authors construct an exponential in the category of games that is a cofree commutative comonoid for the 'tensor on the left' functor and a final coalgebra for the 'sequoid on the left' functor. In the category of finite games and strategies, this exponential can be constructed from the sequoid functor as the limit of a diagram indexed by the ordinal w. If we try to extend this result to the 'sequoidal categories' introduced in , then we find that this construction does not always produce a final coalgebra, but that for natural categories of games a similar construction using a higher ordinal will work. We show that if the lengths of plays in an ordinal game can be bounded by a limit ordinal k then we may construct the final coalgebra for the sequoid using a suitable diagram indexed by k. Conversely, we show that if a game contains plays greater than an ordinal k then the limit of the natural diagram indexed by k does not have the natural structure of a coalgebra.
There is a sizeable body of research in the field of games with plays indexed by transfinite ordinals (sometimes called 'long games'). In , Itay Neeman presents results concerning whether or not such games are determined. More recently, Laird has applied a similar model to the study of unbounded determinism in . The construction given in this talk is a straightforward extension of the games model outlined in [1,5]. A nice feature of the construction is that it includes as special cases both the 'games with winning condition on infinite plays', given in , and the pure finite games introduced by Blass in .
After shifting focus from finite to infinite ordinals, it becomes convenient to treat plays (ordinal sequences of moves), rather than moves, as primitive, and one possible formulation is to define a game to be a sheaf of sets on some given ordinal k, where the ordinal b < k is sent to the set of legal plays of length b. In contrast to the Abramsky-Jagadeesan model, in which moves are designated as Player-moves or Opponent-moves, we have a function that designates plays as Player-plays or Opponent-plays. If a play is indexed by a limit ordinal, then it has no last move, so this distinction is important. For example, in the case of games played over the ordinal w + 1, we are free to specify whether a play of length w should belong to Player or to Opponent, and this corresponds exactly to choosing a set of infinite plays that are Player-winning, as in .
I shall outline the motivation and construction for games played over transfinite ordinals, and shall discuss briefly some tentative questions about links to ordinals occurring elsewhere in the theory - in particular, game-value ordinals for winning positions and consistency-strength ordinals in proof theory.
: Martin Churchill, James Laird and Guy McCusker. Imperative programs as proofs via game semantics. LICS 2011: 65-74, June 2011
: James Laird. A Categorical Semantics of Higher Order Store, CTCS 2002. Proceedings of CTCS '02, Elsevier, 2002
: Itay Neeman. The Determinacy of Long Games. De Gruyter Series in Logic and its Applications, 1972
: James Laird. Sequential Algorithms for Unbounded Nondeterminism. MFPS XXXI: 271-287, 2015
: Samson Abramsky, Radha Jagadeesan. Games and full completeness for multiplicative linear logic. Journal of Symbolic Logic 59 (02): 543-574, 1994
: A. Blass. A game semantics for linear logic. Annals of Pure and Applied Logic, 56(1-3): 183 - 220, 1992
Interaction Graphs models were introduced as a generalisation of Girard's Geometry of Interaction constructions based on the interpretation of proofs as (finite, weighted) graphs. Recent results use these models to bring into vision a new relation between dynamic and denotational semantics, providing formal grounds to the claim that Interaction Graphs models can be understood as a quantitative generalisation of dynamic semantics.
We present a probabilistic game semantics for differential privacy verification. We limit ourselves to games for finitary data types and second order strategies. The latter notoriously correspond to regular languages and are hence decidable. Such decidability result enables automated techniques to be applied to the verification of differential privacy.
The standard (Ghica-Murawski) game semantics for concurrent programs follow an interleaving approach: strategies are sets of linear orders, and two programs running in parallel are interpreted as the set of interleavings of the corresponding strategies. We get full abstraction for may-testing (e.g. for Idealized Parallel Algol), but at the price of an explosion of the size of strategies and an obfuscation of their behaviour. More recently, Rideau and Winskel outlined a different approach: strategies are partial orders, often smaller in size, and retain information about causality.
In this talk, I will investigate the relationship between these two approaches, and the possibility of keeping the best of both worlds. After recalling the two approaches in an affine setting, I will show that the Ghica-Murawski model is the may-testing collapse of the Rideau-Winskel model. I will then present some positive (and negative) results about the representation of Ghica-Murawski strategies as Rideau-Winskel strategies, addressing in particular the existence of minimal representations.
Winskel has pointed out that concurrent strategies in his game model can be seen as profuctors and that this extends to a lax functor. We discuss a similar result for the category of HO/N games, utilising the correspondence between Conduche functors and pseudo functors into Prof, a similar correspondence to that between fibrations and indexed categories.
Our starting point is a construction reminiscent of the "category of elements" applied to the category of sets and relations: the resulting category has as an object a pair (a, A) of a set A and an element a in A and, as a morphism from (a, A) to (b, B), a pair ((a, b), R) of a relation R in B and an element (a, b) in R. We study an analogous construction for the category of HO/N games: a morphism (s, σ) is a pair of a deterministic innocent strategy σ and a play s in σ, and an object is a pair (J, A) of an arena A and a multiset J of A-moves with justication pointers (i.e. a play without sequential structure). Then obvious forgetful functor to the category of HO/N games is a Conduche functor and, as a consequence, there is a pseudofunctor from the category of HO/N games to the bicategory of profunctors.
In this talk, we will explain how to connect the sequential algorithm model designed by Berry and Curien in the early 1980s with the more recent notion of dialogue game . To that purpose, we start from the graph game model of intuitionistic linear logic designed by Hyland and Schalk in the early 2000s.
We present a direct interpretation of classical arithmetic in game semantics in which atomic formulas are interpreted with the one-move arena. This interpretation is not equivalent to the usual direct or indirect interpretations. Extraction of computational content from existential formulas is performed through an exception-like mechanism.
I will describe some recent results establishing the relative computational power of various kinds of iteration and recursion. Many of these results were first obtained in the setting of (sublanguages of) PCF, but more recently we have extended the ideas to other languages such as Idealized Algol, drawing inspiration from the known game models for these languages. The talk will emphasize the complementary perspectives offered by interaction of strategies and by direct manipulation of Böhm trees.
We introduce a trace semantics for a call-by-value language with full polymorphism and higher-order references. This is an operational game semantics model based on a nominal interpretation of parametricity whereby polymorphic values are abstracted with special kinds of names.
The use of references that can have polymorphic types leads to violations of parametricity which we counter by closely recording the disclosure of typing information during the interaction between the two players. We prove the model sound for the full language and strengthen our result to full abstraction for a large fragment where polymorphic references obey specific inhabitation conditions.
The simply-typed call-by-value language RML may be viewed as a canonical restriction of Standard ML to ground-type references, augmented by a “bad variable” construct in the style of Reynolds. We consider the finitary version of RML (finite ground types, looping instead of recursion) and ask at which types the associated problem of contextual equivalence is decidable. While this issue has been fully resolved in the call-by-name case of Idealized Algol, it has turned out much harder to classify the decidable fragments of RML. I will report on the latest findings in that strand of work. In particular, I will explain how class memory automata (an automata model recently proposed in the context of database theory) can be used to represent justification pointers in game models.
The talk will be based on joint work with Conrad Cotton-Barratt, David Hopkins, Luke Ong (FOSSACS'15) and Nikos Tzevelekos (ICALP'12).
It is possible to build a lambda calculus interpreter with none of the traditional implementation machinery: β-reduction; environments binding variables to values; or “closures” and “thunks” for function calls and parameters?
Techniques involve Ong's traversal-based lambda expression normaliser, based on game semantics; and a novel application of partial evaluation to the normaliser program, to compile lambda expressions into a (relatively) low-level code.
In this talk, I will use recent developments in game semantics based on partial-orders to build a denotational semantics for weak memory models. By using game semantics, it is very easy to tweak the control flow to reorder read and write instructions. I will show how to design concurrent strategies for reading and writing on a reference that can inspect the continuation to insert the right causal links that are preserved by a given architecture.
Moreover, the usual cell strategy that is used to interpret the new construction can also be changed to a concurrent version that allows for writes not to propagate immediately to other threads.
Bundled together, this gives a new and interesting denotational semantics for weak memory models. Since the language of interest is essentially first-order, we can make drastic simplifications and get a self-contained semantics based on event structures where no game semantics occurs explicitly. Moreover, this model uses event structures and as such is more compact than the usual trace models.
In previous work on concurrent game semantics, the second author has described a general construction which takes as input a pseudo double category with extra structure -- there called a playground, and outputs a notion of concurrent strategy. This has been applied to CCS and the pi-calculus, using very similar pseudo double categories.
This work proposes a general construction of these pseudo double categories from more basic data. Our main contribution is to show that under suitable hypotheses, the resulting pseudo double category satisfies a crucial property of playgrounds -- the fibredness of the title. As an application, we construct a new pseudo double category, which we intend to use in future work to recover Ong and Tsukada's recent sheaf model of a simply-typed lambda-calculus.