Game semantics for coinductive predicates

Question

Does anyone know of any work on game semantics for coinductive predicates?

A coinductive predicate is one where the predicate itself is called in the body of the predicate, and we are taking the meaning of the predicate to be the greatest fixed point of the underlying definition. Such a predicate will be defined over an infinite data structure, such as a stream or infinite tree or labelled transition system and so forth.

An overly simple example is the following (in Haskell):

data Cat = BlackCat | WhiteCat
data Stream a = Stream a (Stream a)

allBlacks :: Stream Cat -> Bool
allBlacks (Stream cat rest) = cat == BlackCat && allBlacks rest

I can define the stream of all black cats as:

blackCats :: Stream Cat
blackCats = Stream BlackCat blackCats

and use coinduction to prove:

allBlacks blackCats

One could think of a coinductive predicate as an infinite conjunction or disjunction, simply by imagining that it is unrolled completely. Game semantics in this setting would be straightforward: for an infinite conjunction, the Falsifier needs to select which conjunct to falsify in order to win the game; for an infinite disjunction, the Verifier needs to select which disjunct to satisfy in order to win the game.

There is, however, a natural order in 'evaluating' the coinductive predicate which is ignored when considering it as an infinite conjunction or disjunction, and I would like this ordering to be captured in the game semantics, namely that the game proceeds by playing each disjunct/conjunct in turn.

One additional problem I have is understanding which winning condition to use to capture the infinite nature of the predicate. Or to put it in lay persons terms: how do I know that there is no white cat in this supposed infinite stream of black cats––it could merely be after the point I stop looking?

additional example

Consider the following data type (again in Haskell):

data Tree a = Tree (a -> Maybe (Tree a))

Tree A corresponds to the greatest fixed point of the functor $F(X) = (X+1)^A$.

Now assume that there is some relation $R:\subseteq A\times A$. This has no intrinsic meaning, and is just used to formulate the following coinductive predicate. Thinking of $R$ as $\le$ is sufficient.

Consider the following coinductive predicate $covers\subseteq$Tree A$\times$Tree A (defined corecursively):

$\mathit{covers}(\alpha,\beta) = $ $\qquad \forall a\in A\mbox{ if } \alpha(a)\neq\bot \mbox{ then } \exists b\in B \mbox{ such that } a R b \mbox{ and } \beta(b)\neq\bot \mbox{ and } \mathit{covers}(\alpha(a),\beta(b))$.

I'm looking for a formalism for expressing such predicates in terms of game-theoretic semantics. A link to existing work would be greatly appreciated. The main thing I'm having trouble getting my head around is the winning condition (as discussed in some of the comments below). Even though the game goes forever, infinite plays do not constitute a draw.

Answer 1

Vicious Circles by Barwise and Moss is a cornucopia of co-algebraic/co-inductive reasoning, and includes material on co-inductive games.

Not sure if it will help you out in your specific need, but might be the source of some inspiration in this line of reasoning.

Edit (x2):

I think you can follow a modified Ehrenfeucht-Fraïssé style approach like this: Falsifier gets to select any item from the stream/disjunction/conjunction. Verifier then has to show that any such item must be a black cat.

(You could put ordering or number of choices restrictions on Falsifier without loss of generality for a finite set of coinductive rules.)

If you think of coinduction as just induction without a base case, it is obvious that the only (co-)induction rule you have on blackCats is cat == BlackCat, so what else could an individual cat be in that stream? Any cat that Falsifier selects will have to conform to that rule, so Verifier wins.

Obviously this would scale to more numerous and complex coinductive rules, where the "challenge" for Verifier becomes to choose the appropriate rule for whatever item Falsifier chooses.

Colin Sterling's Bisimulation, Model Checking and Other Games, should help you out. His book Modal and Temporal Properties of Processes has similar material, though in less detail.

Answer 2

As a nitpick, you mean data Stream a = ... rather than data Stream a :: ....

Your allBlacks is only a semidecidable predicate, so there is a strategy which leads to a non-terminating game whereby you keep playing BlackCat. From the domain theory perspective, the computation isn't productive in that there is no information increase upon consuming an element from the stream when it equals BlackCat. For that reason I don't think the predicate can really be called coinductive, can it? My suspicion is that this is what underlies your confusion about winning conditions: indefinite stalling is a draw.