Semantics and Games

Geometry of Computation 2006

Marseille - Luminy
February 20 - 24, 2006

Monday

• 9h00 - 10h30 : Games and geometry of interaction tutorial (Laurent Regnier)

• 11h00 - 12h30 : Categories and geometry of interaction tutorial (Phil Scott)

• 14h00 - 14h45 : An abstract category-theoretic formulation of substitution and binding (John Power)
  A fundamental construction in Andre Joyal's species was that of a substitution monoidal structure on the category [P,Set], where P is the category of natural numbers and permutations. That monoidal structure can be used in the analysis of linear calculi to model substitution for linear contexts, with closedness used to model binding. That idea was investigated by Miki Tanaka, following on work by Fiore, Plotkin and Turi, who used the category F of finite sets and all functions in a similar way to model cartesian contexts and cartesian binding. But this category theoretic analysis of substitution can be done much more generally: for an arbitrary pseudo-monad S on Cat, S1 models generalised contexts, and, given a pseudo-distributive law of S over the (partial) pseudo-monad for free cocompletions, there is a canonical substitution monoidal structure on the category [(S1)^op,Set]. One can give a concrete description of the substitution monoidal structure, then an axiomatic definition of a binding signature, extending the definitions for cartesian and linear contexts and yielding initial algebra semantics for binding signatures. This allows one to include structures such as those involved with the Logic of Bunched Implications.
  This is joint work with Miki Tanaka.
• 14h45 - 15h30 : Semantics of lambda calculi by analytic functors and twiners (Ryu Hasegawa)
  We overview analytic functors and twiners, and the semantics of lambda calculi using these concepts. Historically, analytic functors are used first by Girard in construction of models of lambda calculi. Analytic functors are closely related to formal power series, thus especially to enumerative combinatorics and mathematical analysis. We discuss the fixed-point combinator and its analytical interpretation. Twiners are 2-categorical extension of analytic functors and are connected to group-theoretical concepts. We sketch the semantics of the polymorphic lambda calculus using twiners.

• 16h00 - 16h45 : Parity games and inductive/coinductive types (Luigi Santocanale)
  We propose parity games, standard tools in verication, to model inductive and coinducitve types.
• 16h45 - 17h30 : Semantics-directed abstraction and refinement (Dan Ghica)
  Game semantics provides a new method for extracting finite-state models from open programs that exhibit non-trivial interactions between procedures and state. However, the problem of state-space growth is as acute in the case of game models as is in the case of models obtained using traditional, operational, methods. Two of the most successful techniques dealing with this problem are abstract interpretation and counterexample-guided refinement. I will present recent advances in applying these ideas within the game-semantic framework, from foundations to tool implementations.
• 17h30 - 18h00 : On probabilistic program equivalence and refinement (Andrzej Murawski)
  We study notions of equivalence and refinement for probabilistic programs formalized in the second-order fragment of Probabilistic Idealized Algol. Probabilistic programs implement randomized algorithms: a given input yields a probability distribution on the set of possible outputs. Intuitively, two programs are equivalent if they give rise to identical distributions for all inputs. We show that equivalence is decidable by studying the fully abstract game semantics of probabilistic programs and relating it to probabilistic finite automata. For terms in beta-normal form our decision procedure runs in time exponential in the syntactic size of programs; it is moreover fully compositional in that it can handle open programs (probabilistic modules with unspecified components).
  In contrast, we show that the natural notion of program refinement, in which the input-output distributions of one program uniformly dominate those of the other program, is undecidable.
  This is joint work with Joel Ouaknine.

Tuesday

• 14h00 - 14h45 : A Semantics for Concurrent Separation Logic (Stephen Brookes)
  Concurrent separation logic is an extension of separation logic to the shared-memory setting, allowing syntax-directed reasoning about parallel programs that share mutable state, as proposed by Peter O'Hearn. The logic allows correctness proofs in which "ownership" of a piece of state such as a pointer is deemed to transfer dynamically between processes and resources, in a manner governed by resource invariants, with mutual exclusion for critical shared data ensured by careful use of separating conjunction in the logical inference rules.
  We present a denotational semantics based on action traces, and a more abstract semantics based on "footstep traces", each of which can be used to formalize the notion of ownership transfer and to prove soundness of concurrent separation logic. As a consequence of the soundness proof, we show that every provable program is race-free when executed from a state satisfying the relevant pre-condition.
• 14h45 - 15h30 : Modular automatic assertion checking with separation logic (Cristiano Calcagno)
  Separation logic is a program logic for reasoning about programs that manipulate pointer data structures.
  We describe a tool, Smallfoot, for checking certain separation logic specifications.
  The assertions describe the shapes of data structures rather than their detailed contents, and this allows reasoning to be fully automatic.
  We illustrate what the tool can do via a sequence of examples which are oriented around novel aspects of separation logic, namely: avoidance of frame axioms (which say what a procedure does not change); embracement of ``dirty'' features such as memory disposal and address arithmetic; information hiding in the presence of pointers; and modular reasoning about concurrent programs.

• 16h00 - 16h45 : Two ways of adding promotion to differential nets (Thomas Ehrhard)
  Differential nets are an extension of multiplicative proof-nets of linear logic by expenential links: half of these (associated to "?") are standard (weakening, dereliction and contraction) and half (associated to "!") are new (co-weakening, co-dereliction and co-contraction). This formalism, which is a linear logic version of Boudol's resource lambda-calculs, is essentially finitary: strong normalization holds in the untyped case. For obtaining the expressive power of the lambda-calculus, the system must be endowed with a promotion construction. We discuss two ways of dowing so: the standard one (exponential boxes) and another one, similar to the "!t = t|!t" congruence of pi-calculi (and resource calculi).
• 16h45 - 17h30 : L-nets, parallel strategies and proof-nets (Claudia Faggian)
  We present Ludics nets (L-nets) as a game model allowing for concurrent interaction.
  L-nets have been developed in the context of Ludics (Girard 2001), which could be seen as a game model of sequential interaction, abstracting away from proof-theory. L-nets can be seen both as parallel strategies (in game-semantical terms) and as an abstract form of proof nets.
  Strategies capturing sequential interaction, such as Hyland-Ong innocent strategies or Girard's designs, are based on trees; during an interaction (play, or run) the order between the actions is totally specified. L-nets on the contrary are based on graphs, and interactions are partial orders; the intuitionis that some actions can be performed in parallel (or scheduled in any order), while there are tasks which depend upon other tasks.
  When taking a proof-theoretical point of view, a tree strategy can be seen as an abstract sequent calculus derivations, while an L-net appears as an abstract (multiplicative-additive) proof-net. Moreover, as a tree strategy is a particular case of L-net, we have a homogeneus setting, in which it is possible to move between different degrees of sequentiality (both on the syntactical and on the semantical side).
  This talk is based on work in collaboration with Francois Maurel and with Pierre-Louis Curien.

Wednesday

• 9h00 - 9h45 : Socially responsive, environmentally friendly logic (Samson Abramsky)
  We consider the following questions: What kind of logic has a natural semantics in multi-player (rather than 2-player) games? How can we express branching quantifiers, and other partial-information constructs, with a properly compositional syntax and semantics? We develop a logic in answer to these questions, with a formal semantics based on multiple concurrent strategies, formalized as closure operators on Kahn-Plotkin concrete domains. Partial information constraints are formalized as co-closure operators.
  We address the syntactic issues by treating syntactic constituents, including quantifiers, as arrows in a category, with arities and co-arities. This enables a fully compositional account of a wide range of features in a multi-agent, concurrent setting, including IF-style quantifiers.
• 9h45 - 10h30 : Extensions of innocence (Martin Hyland)
  How do strategies compose and why do they compose associatively? Early accounts of game semantics treated these questions in a direct fashion. However both the discovery of implementations by abstract machines, and experience with abstract games suggest a range of other points of view.
  I shall outline two further categorical contexts, one related to simple strategies, and one dealing with innocent strategies. I shall indicate one might develop these ideas to extend the notion of innocence.

• 11h00 - 11h45 : Game semantics and higher-order pushdown automata with links (Luke Ong)
  Knapik et al have recently shown that, as generators of trees, higher-order pushdown automata (HOPDA) are equivalent to higher-order recursion schemes that satisfy a syntactic constraint called safety. We study a variant class of HOPDAs in which items in the stack (level-n, say) may have links (or pointers) to m-stacks (m <= n) lower down. When such an item is on top_1 of the n-stack, the effect of a special "collapse" instruction is pop the appropriate top stacks, so as to cause the m-stack that is pointed to to surface to the top. We show that such machines may be regarded as an automata-theoretic characterization of higher-order recursion schemes (whether safe or not) in that they compute precisely the innocent game semantics of these schemes.
• 11h45 - 12h30 : Second-order type isomorphisms through game semantics (Joachim de Lataillade)
  The characterization of second-order type isomorphisms is a purely syntactical problem (already solved by Roberto Di Cosmo in 1994) that we popose to study under the enlightenment of game semantics. We define a new game model of system F based on hyperforests (starting from ideas of Hughes and Murawski-Ong) in which we show that isomorphisms coincide with the "equality" on hyperforests associated with types. Finally we recover Di Cosmo's equational characterization of type isomorphisms from this equality.
  This new approach leads to a more geometrical proof of the result. Moreover, taking advantage of the high flexibility of game models, our proof is general enough to be easily applied to different programming features (like fix point operators and control) and thus leads to new results.
  In this talk I will present the main ideas of the proof, describe the structure of the model and its extensions, and give some directions towards a game semantics approach of some open problems like Curry-style type isomorphisms.

Thursday

• 14h00 - 14h30 : Analysing innocent interaction (Russ Harmer)
  We analyse the PAM via game semantics. We formalize the role of the PAM as that of a "referee" mediating between the interacting terms/strategies. In this way, we see that we can equivalently compute the "execution trace" (a run of the PAM) as a sequence of moves or in desequentialized form as a kind of tree. If we restrict our attention to innocent strategies satisfying a stronger visibility condition than usual, we can simplify the PAM by eliminating the referee. The resulting machine (the CPAM or cellular PAM) correctly computes interaction between these constrained innocent strategies.
  We then show that the CPAM essentially behaves as an abstract machine for cellular lambda-terms (and lambda-mu-terms), hence its name. Cellular lambda-terms [Padovani, Loader] serve as canonical representatives for contextual equivalence classes in unary PCF: any term of unary PCF can be "cellularized" to find such a representative. This observation leads to the listing algorithm which establishes the effective presentability of the (simple, set-theoretic) model of unary PCF and, as a consequence, that contextual equivalence is decidable.
  This "syntactic cellularization" has a semantic counterpart: given an innocent strategy, we can "cellularize" it. However, unlike in the syntactic case, we can cellularize *any* innocent strategy; this doesn't contradict the undecidability of, say, boolean PCF since the semantic cellularization doesn't preserve the bracketing condition. So, any run of the PAM can be simulated by a (typically much longer) run of the CPAM operating on the cellularized strategies.
• 14h30 - 15h00 : Game semantics using function inventories (Paul Blain Levy)
  This talk presents work in progress. We analyze the semantics of higher-order references presented by Abramsky, Honda and McCusker, and see that a term's denotation can be obtained directly from operational semantics. (By contrast with earlier work, it is not necessary for the term to be eta-long.) The principle is that players pass each other functions, so that each player's inventory of functions grows over time. This gives a convenient operational technique for proving observational equivalence. It also give an account of the denotational semantics using the set of strategies is given by a domain equation, and pointers between moves are no longer required. And there are variant domain equations for the various constraints (bracketing, visibility, innocence) that may be imposed.
  This is joint work with Soren Lassen.
• 15h00 - 15h30 : Control games: the HON game model in Krivine's realisability (Olivier Laurent)
  We show how the notion of games introduced recently by J.-L. Krivine in its classical realisability is strongly related with the HON game model.
  A precise analysis of this correspondence allows us to simplify the HON model of the lambda-mu calculus by the introduction of additional pointers: control pointers (related with J. Laird's contingency pointers). This model is equivalent to the appropriate version of the non well-bracketed HON model, and thus fully complete for the lambda-mu calculus. We give a direct proof of this full completeness result.

• 16h00 - 16h45 : Names and games (Ian Stark)
  I'll talk about some applications of nominal sets to game semantics. Nominal sets provide intrinsic notions of names and binding within standard set theory. One use of these is to build game models for languages and situations where names are more or less evident: such as the nu-calculus, ML with references, aliasing of heap-allocated variables, or objects. Quite independently, existing game models already use various name-like constructions: such as pointers within plays, or labels for threads of interaction. Nominal sets also give an opportunity to rationalise this internal machinery, replacing integer tags or explicit quotients with well-behaved nominal concepts.
• 16h45 - 17h30 : Discussion

Friday

• 9h00 - 10h00 : Asynchronous games: the concurrent geometry of proofs (Paul-André Melliès)
  Game semantics has taught us the art of transforming proofs into interactive strategies. These strategies are generally defined in a purely sequential way, as a set of alternating sequences (= plays) exploring the branch of a decision tree. This is reminiscent of interleaving semantics in concurrency theory, where a process generates a set of sequences (= traces).
  Asynchronous games are played on event structures, rather than trees. Shifting to asynchronous games enables to extract the truly concurrent semantics of proofs from their interleaving semantics, by identifying plays modulo permutation of moves --- understood geometrically as an homotopy relation in the n-dimensional space generated by the event structure.
  The truly concurrent nature of innocence in arena games is captured by a pair of diagrammatic properties (forward and backward innocence) formulated in asynchronous games. The analysis reveals that innocent strategies are positional in the game-theoretic sense that they play according to their current position. Positionality together with a payoff or a truth value on positions leads unexpectedly to an innocent game model of propositional linear logic --- with the usual well-bracketed and non well-bracketed models as intuitionistic fragments, and a structure-preserving functor to the relational model.
• 10h00 - 10h30 : Non-alternating innocence in asynchronous games (Samuel Mimram)
  The notion of innocent strategy was introduced by Hyland and Ong in order to capture the interactive behaviour of lambda-terms and PCF programs. An innocent strategy is defined as an alternating strategy with partial memory, in which the strategy plays according to its view. Extending the definition to non-alternating strategies seems problematic because the definition of views is based on the hypothesis that Player and Opponent alternate during the interaction. In this talk, I will take advantage of the diagrammatic reformulation of innocence developed by Melliès in earlier work on asynchronous games, in order to extend the definition of innocence to non-alternating games. I will explain how to construct a *-autonomous category with asynchronous games as objects, and innocent and non-alternating strategies as morphisms - and how to recover the usual category of innocent and alternating strategies as a subcategory. I will conclude my talk by indicating briefly how first and second order linear logic is interpreted in this framework.

• 11h00 - 11h30 : Free comonoids in models of linear logic (Nicolas Tabareau)
  The construction of the free monoid by means of words is a very old practice in mathematics. Once recognized the categorical nature of the concept of monoid, a lot of similar free constructions in mathematics (like tensor algebras, differential graded tensor algebras, free categories, etc) become unified by the same formula inspired by the construction in Set. This formula works because the underlying categories have coproducts and a tensor product which commutes with them.
  We have learned from linear logic that the dual notion of comonoid captures in essence the discharge and copy mechanisms in proofs and programs. It is therefore natural to wonder whether a comonoid !A may be obtained as a free construction from a given object A. Unfortunately, most of the categories giving rise to models of linear logic do not satisfy the dual of the property stated above: their tensor product does not commute with their cartesian product. In this talk, we explain how to deduce a general construction of the free monoid in a monoidal category from the construction of a free pseudomonoid in the surrounding 2-category of categories. This leads us to an alternative formula, in which the free commutative comonoids is computed as a particular categorical limit. We show that the formula works in two extremely different models of linear logic: the category of coherence spaces, in which it reconstructs the well-known modality !A based on multi-cliques; the category of Conway games, in which it generates the free commutative comonoid !A by indexing the copies of the game A in an incremental way.
• 11h30 - 12h00 : Graph games revisited (Andrea Schalk)
  Graph games provide a framework for game semantics where a certain amount of consistency of strategies is built into the game. While the details of proofs can be intricate, once the framework is in place calculations can be carried out without knowing about those: For example, composition of strategies is relational composition, so that equations can easily be established.
• 12h00 - 12h30 : On the role of medial in a Boolean category (Lutz Strassburger)
  In its most general meaning, a Boolean category is to categories what a Boolean algebra is to posets. In a more specific meaning a Boolean category should provide the abstract algebraic structure underlying the proofs in Boolean Logic, in the same sense as a Cartesian closed category captures the proofs in intuitionistic logic and a *-autonomous category captures the proofs in linear logic. However, recent work has shown that there is no canonical axiomatisation of a Boolean category. In this work, we will see a series (with increasing strength) of possible such axiomatisations, all based on the notion of *-autonomous category. We will particularly focus on the medial map, which has its origin in an inference rule in KS, a cut-free deductive system for Boolean logic in the calculus of structures.