Least and greatest fixpoints in game semantics

TL;DR

This paper introduces a game semantics framework with loops and winning strategies to compute recursive solutions, providing a new approach to fixed points with applications in logic and semantics.

Contribution

It develops a novel game semantics model with loops and winning strategies, and extends logic with fixed points, offering new tools for recursive definitions.

Findings

Loops in arenas enable natural solutions to recursive equations

Winning functions and strategies characterize initial algebras and terminal coalgebras

The sequent calculus with fixed points is sound and weakly complete in the model

Abstract

We show how solutions to many recursive arena equations can be computed in a natural way by allowing loops in arenas. We then equip arenas with winning functions and total winning strategies. We present two natural winning conditions compatible with the loop construction which respectively provide initial algebras and terminal coalgebras for a large class of continuous functors. Finally, we introduce an intuitionistic sequent calculus, extended with syntactic constructions for least and greatest fixed points, and prove it has a sound and (in a certain weak sense) complete interpretation in our game model.