<p><a href="http://www-csli.stanford.edu/pubs/" rel="nofollow">Vicious Circles</a> by Barwise and Moss is a cornucopia of co-algebraic/co-inductive reasoning, and includes material on co-inductive games.</p>

<p>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.</p>

<p><strong>Edit (x2):</strong> </p>

<p>I think you can follow a modified <a href="http://en.wikipedia.org/wiki/Ehrenfeucht%E2%80%93Fra%C3%AFss%C3%A9_game" rel="nofollow">Ehrenfeucht-Fra&iuml;ss&eacute;</a> style approach like this: <em>Falsifier</em> gets to select any item from the stream/disjunction/conjunction.
<em>Verifier</em> then has to show that any such item must be a black cat.</p>

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

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

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

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

CC BY-SA 2.5
2010-09-25T12:57:41.020Z
Thanks Mark. There's certainly some material in the book to help me. Well, more than some.
Dave Clarke
CC BY-SA 2.5
2010-09-25T16:55:15.950Z
I meant to say "Marc".
Dave Clarke
CC BY-SA 2.5
2010-09-29T08:11:14.103Z
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
CC BY-SA 2.5
2010-09-29T12:20:17.620Z
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
CC BY-SA 2.5
2010-09-24T15:31:10.620Z
2010-09-30T07:49:26.610Z
2010-09-30T07:49:26.610Z
Marc Hamann
<p>As a nitpick, you mean <code>data Stream a = ...</code> rather than <code>data Stream a :: ...</code>.</p>

<p>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.</p>

CC BY-SA 2.5
2010-09-27T11:06:59.513Z
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
CC BY-SA 2.5
2010-09-27T11:11:28.913Z
@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
CC BY-SA 2.5
2010-09-27T11:18:03.623Z
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
CC BY-SA 2.5
2010-09-27T18:25:24.493Z
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
CC BY-SA 2.5
2010-09-27T10:46:30.393Z
2010-09-27T11:04:41.523Z
2010-09-27T11:04:41.523Z
Per Vognsen
<p>Does anyone know of any work on game semantics for coinductive predicates? </p>

<p>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.</p>

<p>An overly simple example is the following (in Haskell):</p>

<pre><code>data Cat = BlackCat | WhiteCat
data Stream a = Stream a (Stream a)

allBlacks :: Stream Cat -&gt; Bool
allBlacks (Stream cat rest) = cat == BlackCat &amp;&amp; allBlacks rest
</code></pre>

<p>I can define the stream of all black cats as:</p>

<pre><code>blackCats :: Stream Cat
blackCats = Stream BlackCat blackCats
</code></pre>

<p>and use coinduction to prove:</p>

<pre><code>allBlacks blackCats
</code></pre>

<p>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 <em>Falsifier</em> needs to select which conjunct to falsify in order to win the game; for an infinite disjunction, the <em>Verifier</em> needs to select which disjunct to satisfy in order to win the game.</p>

<p>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 <em>playing</em> each disjunct/conjunct in turn.</p>

<p>One additional problem I have is understanding which <em>winning condition</em> 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?</p>

<p><strong>additional example</strong></p>

<p>Consider the following data type (again in Haskell):</p>

<pre><code>data Tree a = Tree (a -&gt; Maybe (Tree a))
</code></pre>

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

<p>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.</p>

<p>Consider the following coinductive predicate $covers\subseteq$<code>Tree A</code>$\times$<code>Tree A</code> (defined corecursively):</p>

<blockquote>
  <p>$\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))$.</p>
</blockquote>

<p>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 <em>winning condition</em> (as discussed in some of the comments below). Even though the game goes forever, infinite <em>plays</em> do not constitute a draw.</p>

CC BY-SA 2.5
2010-09-29T16:16:09.373Z
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
CC BY-SA 2.5
2010-09-30T07:48:48.123Z
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
<lo.logic>
Game semantics for coinductive predicates
Dave Clarke
# Game semantics for coinductive predicates

(Asked by: username_0 on 2010-09-24)

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.

**Tags:** lo.logic

> **Comments:**
> **username_1**: 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.  
> **username_0**: 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.  

---

## 2 answers

### Answer by username_1 on 2010-09-24. Score: 5 | Accepted answer

[Vicious Circles](http://www-csli.stanford.edu/pubs/) 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é](http://en.wikipedia.org/wiki/Ehrenfeucht%E2%80%93Fra%C3%AFss%C3%A9_game) 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.

> **Comments:**
> **username_0**: Thanks Mark. There's certainly some material in the book to help me. Well, more than some.  
> **username_0**: I meant to say "Marc".  
> **username_0**: 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.  
> **username_1**: 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. ;-)  

---

### Answer by username_2 on 2010-09-27. Score: 1

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.

> **Comments:**
> **username_0**: 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.  
> **username_2**: @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$.  
> **username_0**: 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.  
> **username_1**: 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".  

---

