# Game semantics for coinductive predicates

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?

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.

-
 Have you already looked at game semantic approaches to bisimulation? With those, essentially Verifier wins exactly when play is infinite, i.e. Falsifier was unable to trip her up. – Marc Hamann Sep 29 '10 at 16:16 Indeed, Colin Sterling's Bisimulation, Model Checking and Other Games, should help me out. His book Modal and Temporal Properties of Processes has similar material, though in less detail. – Dave Clarke♦ Sep 30 '10 at 7:48

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.

-
 Thanks Mark. There's certainly some material in the book to help me. Well, more than some. – Dave Clarke♦ Sep 25 '10 at 12:57 I meant to say "Marc". – Dave Clarke♦ Sep 25 '10 at 16:55 Thanks again Marc. The problem I want to avoid is having the Falsifier able to jump into the middle of the stream to find the counter-example. They need to play the game out step by step. What I'm lacking is the winning condition. I now realise that my example is too small. I'll come up with a larger one soon. – Dave Clarke♦ Sep 29 '10 at 8:11 As I alluded to in my parenthetical comment, I think you can insist that Falsifier selects the head of the stream. In that case you would probably want to let him choose k the number of turns they will play. Then Verifier's job is to show that for all k, she can always verify blackness. However, I'll look forward to your expanded example rather than bombard you with things you may already have thought of. ;-) – Marc Hamann Sep 29 '10 at 12:20

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.

-
 Code now fixed. I think it is possible to fully specify a game for this predicate, but I don't know the details. In any case, I will incorporated some of your doubts in the question. – Dave Clarke♦ Sep 27 '10 at 11:06 @supercooldave: Sure, you can fully specify a game-theoretic meaning for this program, but the games can go on forever. A non-terminating game always counts as a draw; a draw is the game equivalent of domain theory's $\bot$. – Per Vognsen Sep 27 '10 at 11:11 This is not always true. As I understand it, the various acceptance conditions of Büchi, Müller, Rabin and Streett and the parity condition all make infinite games determined, meaning that there is no draw. I'm still coming to grips with these notions, though, I admit. – Dave Clarke♦ Sep 27 '10 at 11:18 Infinite games are usually defined so that one of the players (typically the one known as Eloise, Duplicator or Verifier, take your pick) will win so long as she can always make a valid move in response to the other player, who wins iff he can block her. Think of a game semantics for bisimulation or even a game semantics of Turing's original concept of "circle-free" TMs and you can see how this might be a useful and meaningful notion of "winning". – Marc Hamann Sep 27 '10 at 18:25