Semántica del juego para predicados coinductores

¿Alguien sabe de algún trabajo en la semántica de juegos para predicados coinductores?

Un predicado coinductivo es aquel en el que el predicado en sí se llama en el cuerpo del predicado, y estamos tomando el significado del predicado como el mayor punto fijo de la definición subyacente. Dicho predicado se definirá sobre una estructura de datos infinita, como una secuencia o árbol infinito o un sistema de transición etiquetado, etc.

Un ejemplo demasiado simple es el siguiente (en Haskell):

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

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

Puedo definir el flujo de todos los gatos negros como:

blackCats :: Stream Cat
blackCats = Stream BlackCat blackCats

y usar coinducción para probar:

allBlacks blackCats

Uno podría pensar en un predicado coinductivo como una conjunción o disyunción infinita, simplemente imaginando que se desenrolla por completo. La semántica del juego en esta configuración sería sencilla: para una conjunción infinita, el Falsificador necesita seleccionar qué conjunción falsificar para ganar el juego; para una disyunción infinita, el Verificador necesita seleccionar qué disyunción satisfacer para ganar el juego.

Sin embargo, existe un orden natural en la 'evaluación' del predicado coinductivo que se ignora cuando se considera como una conjunción o disyunción infinita, y me gustaría que este orden se capture en la semántica del juego, a saber, que el juego continúa jugando cada disyunct / conjunct a su vez.

Un problema adicional que tengo es entender qué condición ganadora usar para capturar la naturaleza infinita del predicado. O para decirlo en términos de laicos: ¿cómo sé que no hay un gato blanco en esta supuesta corriente infinita de gatos negros? ¿Podría ser simplemente después del punto en que dejo de buscar?

ejemplo adicional

Considere el siguiente tipo de datos (nuevamente en Haskell):

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

Tree A$F(X) = (X+1)^A$

$R:\subseteq A\times A$$R$$\le$

$covers\subseteq$Tree A$\times$Tree A

$\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))$

Estoy buscando un formalismo para expresar tales predicados en términos de semántica de teoría de juegos. Un enlace al trabajo existente sería muy apreciado. Lo principal que tengo problemas para entender es la condición ganadora (como se discute en algunos de los comentarios a continuación). Aunque el juego dura para siempre, las jugadas infinitas no constituyen un empate.

Vicious Circles de Barwise and Moss es una cornucopia de razonamiento co-algebraico / co-inductivo, e incluye material sobre juegos co-inductivos.

No estoy seguro de si lo ayudará en su necesidad específica, pero podría ser la fuente de inspiración en esta línea de razonamiento.

Editar (x2):

Creo que puede seguir un enfoque modificado de estilo Ehrenfeucht-Fraïssé como este: Falsifier puede seleccionar cualquier elemento de la secuencia / disyunción / conjunción. El verificador entonces tiene que mostrar que cualquier artículo debe ser un gato negro.

(Puede aplicar restricciones de pedido o de número de opciones en Falsifier sin pérdida de generalidad para un conjunto finito de reglas coinductivas).

Si piensas en la coinducción como solo inducción sin un caso base, es obvio que la única regla de (co) inducción que tienes blackCatses cat == BlackCat, entonces, ¿qué otra cosa podría estar un gato individual en esa corriente? Cualquier gato que seleccione Falsifier tendrá que cumplir con esa regla, por lo que Verifier gana.

Obviamente, esto se escalaría a reglas coinductivas más numerosas y complejas, donde el "desafío" para Verifier es elegir la regla apropiada para cualquier elemento que elija Falsifier .

Bisimulación de Colin Sterling , Model Checking y otros juegos , deberían ayudarte. Su libro Modal and Temporal Properties of Processes tiene un material similar, aunque con menos detalles.

Como un punto culminante, quieres decir en data Stream a = ...lugar de data Stream a :: ....

Your allBlacks es solo un predicado semidecidible, por lo que hay una estrategia que conduce a un juego sin final por el cual sigues jugando BlackCat. Desde la perspectiva de la teoría de dominio, el cálculo no es productivo ya que no hay aumento de información al consumir un elemento de la secuencia cuando es igual a BlackCat. Por esa razón, no creo que el predicado realmente pueda llamarse coinductivo, ¿verdad? Mi sospecha es que esto es lo que subyace a su confusión sobre las condiciones ganadoras: el estancamiento indefinido es un empate.