Dynamic Games and Strategies.
Norihiro Yamada, Samson Abramsky · arXiv (Cornell University) · 2016
The present paper aims to provide a mathematical and syntax-independent formulation of dynamics and intensionality of computation; our approach is based on mathematical structures developed in game semantics. Specifically, we give a new game semantics of a prototypical programming language that distinguishes terms with the same value yet different algorithms, capturing intensionality of computation, equipped with the hiding operation on strategies that exactly corresponds to the (small-step) operational semantics of the programming language, modeling dynamics of computation. Categorically, our games and strategies give rise to a certain kind of a cartesian closed bicategory (CCB), and our game semantics forms an instance of a bicategorical refinement of the standard interpretation of functional languages in cartesian closed categories (CCCs) by CCBs. This work is intended to be a mathematical foundation of operational aspects of computation; our approach should be applicable to a wide range of logics and computations.