O que é coindução?

Já ouvi falar em indução (estrutural). Ele permite que você construa estruturas finitas a partir de estruturas menores e fornece princípios de prova para raciocinar sobre essas estruturas. A ideia é clara o suficiente.

Mas e a coindução? Como funciona? Como alguém pode dizer algo conclusivo sobre uma estrutura infinita?

Existem (pelo menos) dois ângulos a serem abordados, a saber, a coindução como uma maneira de definir as coisas e como uma técnica de prova.

Em relação à coindução como técnica de prova, qual é a relação entre coindução e bimimulação?

Primeiro, dissipar uma possível dissonância cognitiva: raciocinar sobre estruturas infinitas não é um problema, fazemos isso o tempo todo. Desde que a estrutura seja finamente descritível, isso não é um problema. Aqui estão alguns tipos comuns de estruturas infinitas:

• idiomas (conjuntos de strings sobre algum alfabeto, que podem ser finitos);
• linguagens de árvores (conjuntos de árvores sobre algum alfabeto);
• traços de execução de um sistema não determinístico;
• numeros reais;
• conjuntos de números inteiros;
• conjuntos de funções de números inteiros para números inteiros; ...

Coindutividade como o maior ponto fixo

Onde as definições indutivas constroem uma estrutura a partir de blocos de construção elementares, as definições coindutivas moldam as estruturas de como elas podem ser desconstruídas. Por exemplo, o tipo de lista cujos elementos estão em um conjunto Aé definido da seguinte forma em Coq:

Inductive list (A:Set) : Set :=
  | nil : list A
  | cons : A -> list A -> list A.

Informalmente, o listtipo é o menor que contém todos os valores criados pelos construtores nile cons, com o axioma que . Por outro lado, podemos definir o maior tipo que contém todos os valores criados a partir desses construtores, mantendo o axioma da discriminação:$\forall x \, y, \: \mathtt{nil} \ne \mathtt{cons} \: x \: y$

CoInductive colist (A:Set) : Set :=
  | conil : colist A
  | cocons : A -> colist A -> colist A.

listé isomórfico para um subconjunto de colist. Além disso, colistcontém listas infinitas: listas com coconsupon cocons.

CoFixpoint flipflop : colist ℕ := cocons 1 (cocons 2 flipflop).
CoFixpoint from (n:ℕ) : colist ℕ := cocons n (from (1 + n)).

flipflopé o infinito (lista circular) ; é a lista infinita de números naturais .$1::2::1::2::\ldots$from 0$0::1::2::\ldots$

Uma definição recursiva é bem formada se o resultado for construído a partir de blocos menores: as chamadas recursivas devem funcionar com entradas menores. Uma definição corecursiva é bem formada se o resultado criar objetos maiores. A indução olha para os construtores, a coindução olha para os destruidores. Observe como a dualidade não apenas muda de menor para maior, mas também de entradas para saídas. Por exemplo, a razão pela qual as definições flipflope fromacima são bem formadas é que a chamada corecursiva é protegida por uma chamada ao coconsconstrutor nos dois casos.

Onde declarações sobre objetos indutivos têm provas indutivas, declarações sobre objetos coindutivos têm provas coindutivas. Por exemplo, vamos definir o predicado infinito nas colistas; intuitivamente, os colistas infinitos são os que não terminam conil.

CoInductive Infinite A : colist A -> Prop :=
  | Inf : forall x l, Infinite l -> Infinite (cocons x l).

Para provar que os colistas da forma from nsão infinitos, podemos raciocinar por coindução. from né igual a cocons n (from (1 + n)). Isso mostra que from né maior que from (1 + n), que é infinito pela hipótese de coindução, portanto from né infinito.

Bisimilaridade, uma propriedade coindutora

A coindução como técnica de prova também se aplica a objetos financeiros. Intuitivamente, as provas indutivas sobre um objeto são baseadas em como o objeto é construído. As provas coindutivas são baseadas em como o objeto pode ser decomposto.

Ao estudar sistemas determinísticos, é comum definir equivalência por meio de regras indutivas: dois sistemas são equivalentes se você puder passar de um para o outro por uma série de transformações. Tais definições tendem a falhar em capturar as muitas maneiras diferentes que os sistemas não determinísticos podem acabar tendo o mesmo comportamento (observável), apesar de terem uma estrutura interna diferente. (A coindução também é útil para descrever sistemas sem terminação, mesmo quando são determinísticos, mas não é nisso que vou focar aqui.)

Sistemas não determinísticos, como sistemas concorrentes, geralmente são modelados por sistemas de transição rotulados . Um LTS é um gráfico direcionado no qual as bordas são rotuladas. Cada aresta representa uma possível transição do sistema. Um traço de um LTS é a sequência de rótulos de arestas ao longo de um caminho no gráfico.

Dois LTS podem se comportar de forma idêntica, na medida em que possuem os mesmos traços possíveis, mesmo que sua estrutura interna seja diferente. O isomorfismo do gráfico é muito forte para definir sua equivalência. Em vez disso, é dito que um LTS simula outro LTS se toda transição do segundo LTS admitir uma transição correspondente no primeiro. Formalmente, seja a união disjunta dos estados dos dois LTS, o conjunto (comum) de rótulos e a relação de transição. A relação é uma simulação se $\mathscr{A}$$\mathscr{B}$$S$$L$$\rightarrow$$R \subseteq S \times S$

$\mathscr{A}$ simula se houver uma simulação em que todos os estados de estejam relacionados a um estado em . Se é uma simulação em ambas as direções, isso é chamado de bisimulação . A simulação é uma propriedade coindutiva: qualquer observação de um lado deve corresponder do outro lado.$\mathscr{B}$$\mathscr{B}$$\mathscr{A}$$R$

Há potencialmente muitos bisimulations em um LTS. Bissimulações diferentes podem identificar estados diferentes. Dadas duas bisimulations e , a relação tomado como o sindicato dos gráficos de relações é em si um bissimulação, já que estados relacionados dão origem a estados relacionados para ambas as relações. (Isso também vale para uniões infinitas. A relação vazia é uma bisimulação incessante, assim como a relação de identidade.) Em particular, a união de todas as bissimulações é ela própria uma bimimulação, chamada bisimilaridade. A bisimilaridade é a maneira mais grosseira de observar um sistema que não distingue entre estados distintos.$R_1$$R_2$$R_1 \cup R_2$

A bisimilaridade é uma propriedade coindutora. Ele pode ser definido como o maior ponto fixo de um operador: é a maior relação que, quando estendida para identificar estados equivalentes, permanece a mesma.

Referências

• Coq e o cálculo de construções indutivas

  • Yves Bertot e Pierre Castéran. Provas de Teoremas Interativos e Desenvolvimento de Programas - Coq'Art: O Cálculo de Construções Indutivas . Springer, 2004. Ch. 13. [ site ] [ Amazon ]
  • Eduardo Giménez. Uma aplicação de tipos co-indutivos em coq: verificação do protocolo de bits alternados . No Workshop sobre tipos de provas e programas , número 1158 em Notas de aula em ciência da computação , páginas 135–152. Springer-Verlag, 1995. [ Google Livros ]
  • Eduardo Giménez e Pierre Castéran. Um tutorial sobre tipos [co-] indutivos em Coq. 2007. [ PDF ]

• Sistemas de transição e bimitação rotulados

  • Robin Milner. Comunicação e simultaneidade . Prentice Hall, 1989.
  • Davide Sangiorgi. Sobre as origens da bisimulação e coindução . Transações da ACM em linguagens e sistemas de programação (TOPLAS), volume 31, edição 4, maio de 2009. [ PDF ] [ ACM ] Slides de cursos associados: [ PDF ] [ CiteSeer ]

  • Davide Sangiorgi. O cálculo Pi: uma teoria dos processos móveis . Cambridge University Press, 2003. [ Amazônia ]

    • Mais referências sugeridas por Anton Trunov

  • Um capítulo em Programação Certificada com Tipos Dependentes, de A. Chlipala

  • D. Sangiorgi. "Introdução à bisimulação e coindução". 2011. [ PDF ]
  • D. Sangiorgi e J. Rutten. Tópicos Avançados em Bisimulação e Coindução . Cambridge University Press, 2012. [ CUP ]

Vamos considerar a seguinte definição indutiva:

$\qquad \displaystyle \begin{align*} &\phantom{\Rightarrow} \quad \varepsilon \in \mathcal{T} \\ w \in \mathcal{T} \quad &\Rightarrow \quad aw \in \mathcal{T}\\ aw \in \mathcal{T} \quad &\Rightarrow \quad baw \in \mathcal{T} \end{align*}$

O que é ? Claramente, o conjunto de strings sem dois subsequentes , ou seja,$\mathcal{T}$$b$

$\qquad \displaystyle \mathcal{T} =\{\varepsilon, a, aa, ba, aaa, aba, \dots\} = \mathcal{L}\left((ba\mid a)^*\right) \subseteq \Sigma^*.$

Direito? Bem, o que precisamos para isso é a sentença inócua "e é o menor conjunto que atende a essas condições". É verdade, pois caso contrário também funcionaria.$\mathcal{T}$$\mathcal{T}=\{a,b\}^*$

Mas há mais do que isso. Escreva a definição acima como função (monótona) :$f : 2^{\Sigma^\infty} \to 2^{\Sigma^\infty}$

$\qquad f(T) = T \cup \{\varepsilon\} \cup \{aw \mid w\in T\} \cup \{baw \mid aw \in T\}$

Agora é o menor ponto de correção de . De fato, como é monótono e é uma rede completa , o teorema de Knaster-Tarski nos diz que existe um ponto de correção tão pequeno e é uma linguagem adequada. Como isso funciona com qualquer definição indutiva razoável, normalmente não falamos sobre isso. Apenas se encaixa em nossa intuição: começamos com e aplicamos as regras passo a passo; no limite, obtemos . f f ( 2 Σ ∞ , ⊆ ) { ε } $\mathcal{T}$$f$$f$$\left(2^{\Sigma^\infty},\subseteq\right)$$\{\varepsilon\}$$\mathcal{T}$

Agora nós mudamos as coisas. Em vez de dizer "se está incluído, então é ", dizemos "se está incluído, então deve ter sido ". Não podemos virar a âncora, então ela desaparece. Isso nos deixa com um problema: temos que poder tirar prefixos arbitrariamente longos de qualquer palavra em e permanecer em ! Isso não é possível com palavras finitas; Ainda bem que me escondi em acima! Terminamos com o conjunto de palavras infinitas sem um fator (substring) , ou seja, .um w um w $w$$aw$$aw$$w$T ' Σ ∞ bb T ' = L ( ( b um | a ) ω $\mathcal{T}'$$\mathcal{T}'$$\Sigma^\infty$$bb$$\mathcal{T}'=\mathcal{L}\left((ba\mid a)^\omega\right)$

Em termos de , é seu maior ponto de correção². Isso é realmente muito intuitiva: não podemos esperar para bater a partir abaixo , ou seja indutivamente partindo de e acrescentando coisas que cumpre as regras, então nós vamos de cima , ou seja, coinductively iniciando de e removendo coisas que não estão em conformidade com as regras.T ′ T ′ { ε } Σ $f$$\mathcal{T}'$$\mathcal{T}'$$\{\varepsilon\}$$\Sigma^\infty$

Notação:

• $\Sigma^\infty = \Sigma^* \cup \Sigma^\omega$
• $\Sigma^\omega$ é o conjunto de todas as seqüências infinitas sobre .$\Sigma$

¹ Você não tem permissão para fazer coisas como ; a função correspondente não seria monótona. ² Temos que varrer baixo do tapete de alguma forma. { ε $w \in \mathcal{T} \Rightarrow aw \notin \mathcal{T}$
$\{\varepsilon\}$