Dynamic game semantics
Norihiro Yamada, Samson Abramsky · Mathematical Structures in Computer Science · 2020
Abstract The present work achieves a mathematical, in particularsyntax-independent, formulation ofdynamicsandintensionalityof computation in terms ofgamesandstrategies. Specifically, we givegame semanticsof a higher-order programming language that distinguishes programmes with the same value yet different algorithms (or intensionality) and thehiding operationon strategies that precisely corresponds to the (small-step) operational semantics (or dynamics) of the language. Categorically, our games and strategies give rise to acartesian closed bicategory, and our game semantics forms an instance of a bicategorical generalisation of the standard interpretation of functional programming languages in cartesian closed categories. This work is intended to be a step towards a mathematical foundation of intensional and dynamic aspects of logic and computation; it should be applicable to a wide range of logics and computations.