Co to jest koindukcja?

Słyszałem o indukcji (strukturalnej). Pozwala budować struktury skończone z mniejszych i zapewnia zasady dowodowe dla uzasadnienia takich struktur. Pomysł jest wystarczająco jasny.

A co z koindukcją? Jak to działa? Jak można powiedzieć coś rozstrzygającego o nieskończonej strukturze?

Są (przynajmniej) dwa kąty, którymi należy się zająć, a mianowicie koindukcja jako sposób definiowania rzeczy i jako technika dowodowa.

Jeśli chodzi o koindukcję jako technikę dowodową, jaki jest związek między koindukcją a bisimulacją?

Po pierwsze, aby rozproszyć możliwy dysonans poznawczy: rozumowanie o nieskończonych strukturach nie stanowi problemu, robimy to cały czas. Tak długo, jak struktura jest w pełni opisywalna, nie stanowi to problemu. Oto kilka popularnych typów nieskończonych struktur:

• języki (zestawy ciągów znaków nad pewnym alfabetem, które mogą być skończone);
• języki drzew (zestawy drzew nad pewnym alfabetem);
• ślady wykonania systemu niedeterministycznego;
• liczby rzeczywiste;
• zestawy liczb całkowitych;
• zestawy funkcji od liczb całkowitych do liczb całkowitych; …

Koinduktywność jako największy punkt stały

Tam, gdzie definicje indukcyjne budują strukturę z elementarnych elementów budulcowych, definicje koindukcyjne kształtują struktury na podstawie tego, w jaki sposób można je rozłożyć. Na przykład typ list, których elementy są w zestawie, Azdefiniowano w Coq w następujący sposób:

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

Nieformalnie listtyp jest najmniejszym typem, który zawiera wszystkie wartości zbudowane z konstruktorów nili cons, z aksjomatem . I odwrotnie, możemy zdefiniować największy typ, który zawiera wszystkie wartości zbudowane z tych konstruktorów, zachowując aksjomat dyskryminacji:$\forall x \, y, \: \mathtt{nil} \ne \mathtt{cons} \: x \: y$

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

listjest izomorficzny dla podzbioru colist. Ponadto colistzawiera nieskończone listy: listy z coconsna cocons.

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

flipflopjest nieskończony (lista okrągły) ; jest nieskończona lista liczb naturalnych 0 : : 1 : : 2 : : ... .$1::2::1::2::\ldots$from 0$0::1::2::\ldots$

Definicja rekurencyjna jest dobrze sformułowana, jeśli wynik jest zbudowany z mniejszych bloków: wywołania rekurencyjne muszą działać na mniejszych danych wejściowych. Definicja corecursive jest poprawnie sformułowana, jeśli wynik tworzy większe obiekty. Indukcja spogląda na konstruktory, koindukcja spogląda na destruktory. Zwróć uwagę, jak dualność zmienia się nie tylko z mniejszych na większe, ale także z wejściami na wyjścia. Na przykład powodem, dla którego powyższe definicje flipflopi fromdefinicje są dobrze sformułowane, jest to, że wywołanie corecursive jest chronione przez wywołanie do coconskonstruktora w obu przypadkach.

Tam, gdzie stwierdzenia o obiektach indukcyjnych mają dowody indukcyjne, stwierdzenia o obiektach koindukcyjnych mają dowody koindukcyjne. Na przykład zdefiniujmy nieskończony predykat na kolistach; intuicyjnie, nieskończeni koloni to ci, którzy się nie kończą conil.

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

Aby udowodnić, że koloni formy from nsą nieskończone, możemy wnioskować przez koindukcję. from njest równy cocons n (from (1 + n)). To pokazuje, że from njest większy niż from (1 + n), który jest nieskończony przez hipotezę koindukcji, a zatem from njest nieskończony.

Różnorodność, właściwość koindukcyjna

Koindukcja jako technika dowodowa dotyczy również obiektów skończonych. Intuicyjnie, dowody indukcyjne na temat obiektu oparte są na jego budowie. Dowody koindukcyjne opierają się na tym, jak można rozłożyć obiekt.

Podczas badania systemów deterministycznych powszechne jest definiowanie równoważności za pomocą reguł indukcyjnych: dwa systemy są równoważne, jeśli można przejść od jednego do drugiego za pomocą serii transformacji. Takie definicje zwykle nie wychwytują wielu różnych sposobów, w jakie systemy niedeterministyczne mogą mieć takie same (obserwowalne) zachowanie, pomimo różnej struktury wewnętrznej. (Koindukcja przydaje się także do opisywania systemów nie kończących się, nawet jeśli są deterministyczne, ale nie na tym się skupię.)

Systemy niedeterministyczne, takie jak systemy współbieżne, są często modelowane przez oznaczone systemy przejściowe . LTS to ukierunkowany wykres, na którym zaznaczone są krawędzie. Każda krawędź reprezentuje możliwe przejście systemu. Ślad LTS to sekwencja etykiet krawędzi nad ścieżką na wykresie.

$\mathscr{A}$$\mathscr{B}$$S$$L$$\rightarrow$$R \subseteq S \times S$

$$\forall (p,q)\in R, %\forall p'\in S, \forall\alpha\in L, \text{ if } p \stackrel\alpha\rightarrow p' \text{ then } \exists q', \; q \stackrel\alpha\rightarrow q' \text{ and } (p',q')\in R$$

$\mathscr{A}$$\mathscr{B}$$\mathscr{B}$$\mathscr{A}$$R$

$R_1$$R_2$$R_1 \cup R_2$

Podobieństwo jest koindukcyjną właściwością. Można go zdefiniować jako największy punkt stały operatora: jest to największa relacja, która po rozszerzeniu w celu identyfikacji stanów równoważnych pozostaje taka sama.

Bibliografia

• Coq i rachunek konstrukcji indukcyjnych

  • Yves Bertot i Pierre Castéran. Interaktywne dowodzenie twierdzeń i rozwój programu - Coq'Art: rachunek konstrukcji indukcyjnych . Springer, 2004. Ch. 13. [ strona internetowa ] [ Amazon ]
  • Eduardo Giménez. Zastosowanie typów koindukcyjnych w coq: weryfikacja przemiennego protokołu bitowego . W warsztacie na temat typów dowodów i programów , numer 1158 w Notach wykładowych z informatyki , strony 135–152. Springer-Verlag, 1995. [ Google Books ]
  • Eduardo Giménez i Pierre Castéran. Samouczek na temat [Co-] typów indukcyjnych w Coq. 2007. [ PDF ]

• Oznaczone układy przejściowe i bisimulacje

  • Robin Milner. Komunikacja i współbieżność . Prentice Hall, 1989.
  • Davide Sangiorgi. O początkach bisimulacji i koindukcji . Transakcje ACM dotyczące języków i systemów programowania (TOPLAS), tom 31 wydanie 4, maj 2009. [ PDF ] [ ACM ] Powiązane slajdy kursu: [ PDF ] [ CiteSeer ]

  • Davide Sangiorgi. Pi-Calculus: teoria procesów mobilnych . Cambridge University Press, 2003. [ Amazon ]

    • Więcej referencji zasugerował Anton Trunov

  • Rozdział w Certyfikowany Programming z typów zależnych przez A. Chlipala

  • D. Sangiorgi. „Wprowadzenie do bisimulacji i koindukcji”. 2011. [ PDF ]
  • D. Sangiorgi i J. Rutten. Zaawansowane tematy w bisimulacji i koindukcji . Cambridge University Press, 2012. [ CUP ]

Rozważmy następującą definicję indukcyjną:

$\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*}$

$\mathcal{T}$$b$

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

$\mathcal{T}$$\mathcal{T}=\{a,b\}^*$

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

$\mathcal{T}$$f$$f$$\left(2^{\Sigma^\infty},\subseteq\right)$$\{\varepsilon\}$$\mathcal{T}$

$w$$aw$$aw$$w$$\mathcal{T}'$$\mathcal{T}'$$\Sigma^\infty$$bb$$\mathcal{T}'=\mathcal{L}\left((ba\mid a)^\omega\right)$

$f$$\mathcal{T}'$$\mathcal{T}'$$\{\varepsilon\}$$\Sigma^\infty$

---

Notacja:

• $\Sigma^\infty = \Sigma^* \cup \Sigma^\omega$
• $\Sigma^\omega$$\Sigma$

---

$w \in \mathcal{T} \Rightarrow aw \notin \mathcal{T}$
$\{\varepsilon\}$