27 April 2004

2:30 - 4:00  Andrea Schalk
             Games Played on Graphs
             (joint work with Martin Hyland)


ABSTRACT:
Games have been used very successfully to model both, proofs and
computations. For some applications we want to be able to identify
positions in a game tree. For example, when playing Chess we might
only want to know which board position we're in, but now how we got
there. In a natural way this leads to games played on graphs rather
than trees. Our games have two players which move alternatingly as is
standard in game semantics. We do not allow the game to contain
cycles. 

In order for composition to be well-defined, strategies have to
satisfy a new condition we call `conflict-freeness'. This amounts to
the idea that if a Player strategy is prepared to reach some
Player-position then he must be committed to doing so: Whenever it is
Player's turn at a position from which he can reach a P-position
which he is prepared to reach (by some other path in the game graph),
then his answer must move towards this position.

A good example for this are games were Opponent moves consist of
questions regarding data and Player moves of supplying data, such as
Curien's sequential data structures, or concrete data structures if we
want to be more general.

We will outline the structure which makes our graph games a model for
intuitionistic linear logic, and how a closely related category of
abstract games can be obtained.