Strong functors and interleaving fixpoints in game semantics
Pierre Clairambault · RAIRO - Theoretical Informatics and Applications · 2013
We describe a sequent calculusμLJwith primitives for inductive and coinductive datatypes and equip it with reduction rules allowing a sound translation of Gödel’s system T. We introduce the notion of aμ-closed category, relying on a uniform interpretation of openμLJformulas as strong functors. We show that anyμ-closed category is a sound model forμLJ. We then turn to the construction of a concreteμ-closed category based on Hyland-Ong game semantics. The model relies on three main ingredients: the construction of a general class of strong functors calledopen functorsacting on the category of games and strategies, the solution of recursive arena equations by exploitingcyclesin arenas, and the adaptation of the winning conditions of parity games to build initial algebras and terminal coalgebras for many open functors. We also prove a weak completeness result for this model, yielding a normalisation proof forμLJ.