Semântica de jogos para predicados coindutivos

Alguém conhece algum trabalho sobre semântica de jogos para predicados coindutivos?

Um predicado coindutivo é aquele em que o próprio predicado é chamado no corpo do predicado, e estamos assumindo que o significado do predicado é o maior ponto fixo da definição subjacente. Esse predicado será definido sobre uma estrutura de dados infinita, como um fluxo ou uma árvore infinita ou um sistema de transição rotulado e assim por diante.

Um exemplo excessivamente simples é o seguinte (em Haskell):

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

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

Eu posso definir o fluxo de todos os gatos pretos como:

blackCats :: Stream Cat
blackCats = Stream BlackCat blackCats

e use a coindução para provar:

allBlacks blackCats

Pode-se pensar em um predicado coindutor como uma conjunção ou disjunção infinita, simplesmente imaginando que ele é desenrolado completamente. A semântica de jogos nesse cenário seria direta: para uma conjunção infinita, o falsificador precisa selecionar qual conjunto falsificar para ganhar o jogo; para uma disjunção infinita, o Verificador precisa selecionar qual disjunção satisfazer para vencer o jogo.

Existe, no entanto, uma ordem natural em 'avaliar' o predicado coindutor que é ignorado quando considerado como uma conjunção ou disjunção infinita, e eu gostaria que essa ordem fosse capturada na semântica do jogo, ou seja, que o jogo prossiga jogando cada disjuntivo / conjunto por sua vez.

Um problema adicional que tenho é entender qual condição vencedora usar para capturar a natureza infinita do predicado. Ou, em termos leigos: como sei que não existe gato branco nesse suposto fluxo infinito de gatos pretos - poderia ser apenas depois do ponto em que parei de procurar?

exemplo adicional

Considere o seguinte tipo de dados (novamente em Haskell):

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

Tree Acorresponde ao maior ponto fixo do functor .$F(X) = (X+1)^A$

Agora vamos supor que existe alguma relação . Isso não tem significado intrínseco e é usado apenas para formular o seguinte predicado coindutor. Pensar em como é suficiente.$R:\subseteq A\times A$$R$$\le$

Considere as seguintes coberturas de predicado coindutivo (definidas corecursivamente):$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))$ .

Estou procurando um formalismo para expressar esses predicados em termos de semântica da teoria dos jogos. Um link para o trabalho existente seria muito apreciado. A principal coisa que estou tendo problemas para entender é a condição vencedora (conforme discutido em alguns dos comentários abaixo). Mesmo que o jogo dure para sempre, jogadas infinitas não constituem empate.

Vicious Circles de Barwise e Moss é uma cornucópia de raciocínio co-algébrico / co-indutivo e inclui material em jogos co-indutivos.

Não tenho certeza se isso o ajudará em sua necessidade específica, mas pode ser a fonte de alguma inspiração nessa linha de raciocínio.

Editar (x2):

Eu acho que você pode seguir uma abordagem modificada do estilo Ehrenfeucht-Fraïssé como esta: O falsificador consegue selecionar qualquer item do fluxo / disjunção / conjunção. O Verifier precisa mostrar que esse item deve ser um gato preto.

(Você pode colocar restrições de pedidos ou número de opções no Falsifier sem perda de generalidade para um conjunto finito de regras coindutoras.)

Se você pensa em coindução apenas como indução sem um caso base, é óbvio que a única regra de (co) indução que você possui blackCatsé cat == BlackCat, então o que mais um gato individual poderia ter nesse fluxo? Qualquer gato que o Falsifier seleciona terá que estar em conformidade com essa regra, então o Verifier vence.

Obviamente, isso seria dimensionado para regras coindutivas mais numerosas e complexas, onde o "desafio" para o Verifier passa a ser a escolha da regra apropriada para qualquer item que o Falsifier escolher.

A bisimulação, a verificação de modelos e outros jogos de Colin Sterling devem ajudá-lo. Seu livro Propriedades Modais e Temporais de Processos tem material semelhante, embora com menos detalhes.

Como nitpick, você quer dizer em data Stream a = ...vez de data Stream a :: ....

Seu allBlacks é apenas um predicado semidecidável; portanto, existe uma estratégia que leva a um jogo sem fim, no qual você continua jogando o BlackCat. Do ponto de vista da teoria do domínio, o cálculo não é produtivo, pois não há aumento de informações ao consumir um elemento do fluxo quando ele é igual ao BlackCat. Por essa razão, não acho que o predicado possa realmente ser chamado de coindutor, pode? Minha suspeita é que isso é o que subjaz à sua confusão sobre as condições de vitória: o empate indefinido é um empate.