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:∀xy,nil≠consxy
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::…from 00::1::2::…
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.
ABSL→R⊆S×S
∀(p,q)∈R, if p→αp′ then ∃q′,q→αq′ and (p′,q′)∈R
ABBAR
R1R2R1∪R2
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