Dynamic Game Semantics

TL;DR

This paper develops a mathematical game semantics framework for higher-order programming languages that captures both intensionality and dynamics, aligning operational semantics with strategies in a categorical setting.

Contribution

It introduces a syntax-independent game semantics for higher-order languages that models intensionality and dynamics through strategies and categorical structures.

Findings

Game semantics distinguishes programs with same value but different algorithms.

Hiding operation on strategies corresponds to small-step operational semantics.

Framework forms a cartesian closed bicategory, generalizing standard functional interpretation.

Abstract

The present paper gives a mathematical, in particular, syntax-independent, formulation of intensionality and dynamics of computation in terms of games and strategies. Specifically, we give a game semantics for a higher-order programming language that distinguishes programs with the same value yet different algorithms (or intensionality), equipped with the hiding operation on strategies that precisely corresponds to the (small-step) operational semantics (or dynamics) of the language. Categorically, our games and strategies give rise to a cartesian closed bicategory, and our game semantics forms an instance of a generalization of the standard interpretation of functional programming languages in cartesian closed categories. This work is intended to be the first step towards a mathematical (both categorical and game-semantic) foundation of intensional and dynamic aspects of logic and computation; our approach should be applicable to a wide range of logics and computations.