Grounding Game Semantics in Categorical Algebra

TL;DR

This paper establishes a formal link between algebraic effects and game semantics, showing how strategies can model computations with side-effects within a categorical algebra framework, enhancing understanding and verification methods.

Contribution

It introduces a categorical algebraic model of game semantics, connecting strategies with free algebras in cpos, and extends the framework to multi-sorted signatures for broader applicability.

Findings

Strategies form the free algebra for algebraic signatures in cpos.

Operational aspects of game semantics are reflected in algebraic structures.

Framework extension to multi-sorted signatures broadens applicability.

Abstract

I present a formal connection between algebraic effects and game semantics, two important lines of work in programming languages semantics with applications in compositional software verification. Specifically, the algebraic signature enumerating the possible side-effects of a computation can be read as a game, and strategies for this game constitute the free algebra for the signature in a category of complete partial orders (cpos). Hence, strategies provide a convenient model of computations with uninterpreted side-effects. In particular, the operational flavor of game semantics carries over to the algebraic context, in the form of the coincidence between the initial algebras and the terminal coalgebras of cpo endofunctors. Conversely, the algebraic point of view sheds new light on the strategy constructions underlying game semantics. Strategy models can be reformulated as ideal completions of partial strategy trees (free dcpos on the term algebra). Extending the framework to multi-sorted signatures would make this construction available for a large class of games.