Dynamic Game Semantics
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.
Keywords
Cite
@article{arxiv.1601.04147,
title = {Dynamic Game Semantics},
author = {Norihiro Yamada and Samson Abramsky},
journal= {arXiv preprint arXiv:1601.04147},
year = {2021}
}