Transition Systems over Games

Abstract

1. A game, which is essentially a bipartite graph describing the We describe a framework for game semantics combining opera- moves that can be made as play passes between the different tional and denotational accounts. A game is a bipartite graph of positions of the two players. “passive” and “active” positions, or a categorical variant with mor- 2. A strategy for a game, which specifies a particular way of phisms between positions. playing a game, from a given starting position. Formally, it is The operational part of the framework is given by a labelled a set of paths through the graph. transition system in which each state sits in a particular position of 3. A transition system over a game, which is the operational part of the game. From a state in a passive position, transitions are labelled the account. This can be thought of as an abstract machine that with a valid O-move from that position, and take us to a state in performs a strategy. Formally, it is a transition system labelled the updated position. Transitions from states in an active position by legal moves of a game. (The set of legitimate actions changes are likewise labelled with a valid P-move, but silent transitions are over time, by contrast with conventional LTSs.) allowed, which must take us to a state in the same position. The denotational part is given by a “transfer” from one game 4. A way to transfer strategies from one game to another, which to another, a kind of program that converts moves between the two is the denotational part of the account. We take as an example a games, giving an operation on strategies. The agreement between composition operation, which takes two strategies in a particu- the two parts is given by a relation called a “stepped bisimulation”. lar game G and composes them. We understand this as a transfer The framework is illustrated by an example of substitution from the tensor game G ⊗ G (whose strategies are roughly pairs within a lambda-calculus. of strategies) to