Frage

Ich habe von (struktureller) Induktion gehört. Es ermöglicht Ihnen, endliche Strukturen von kleineren aufzubauen, und gibt Ihnen Beweisprinzipien für die Argumentation über solche Strukturen. Die Idee ist klar genug.

Aber was ist mit Koinktion? Wie funktioniert es? Wie kann man etwas Schlussfolgerendes über eine unendliche Struktur sagen?

Es gibt (mindestens) zwei Winkel, nämlich Koinktion als eine Möglichkeit, Dinge und als Beweistechnik zu definieren.

In Bezug auf Koinktion als Beweistechnik besteht die Beziehung zwischen Koinktion und Bissimulation?

War es hilfreich?

Lösung

Erstens, um eine mögliche kognitive Dissonanz zu zerstreuen: Das Denken über unendliche Strukturen ist kein Problem, wir tun es ständig. Solange die Struktur endlich beschreibt, ist das kein Problem. Hier sind einige häufige Arten von unendlichen Strukturen:

  • Sprachen (Saiten über ein Alphabet, die endlich sein können);
  • Baumsprachen (Bäumensätze über einem Alphabet);
  • Ausführungsspuren eines nicht deterministischen Systems;
  • reale Nummern;
  • Zahlensätze;
  • Funktionen von Funktionen von Ganzzahlen zu Ganzzahlen; …

Koindualität als größter Fixpoint

Wenn induktive Definitionen eine Struktur aus elementaren Bausteinen bauen, formen koinduktive Definitionen Strukturen aus der Art und Weise, wie sie dekonstruiert werden können. Zum Beispiel die Art der Listen, deren Elemente in einem Satz enthalten sind A wird wie folgt in CoQ definiert:

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

Informell die list Typ ist der kleinste Typ, der alle aus dem erstellten Werte enthält nil und cons Konstruktoren mit dem Axiom, dass $ forall x , y, : mathtt {nil} ne mathtt {cons} : x : y $. Umgekehrt können wir den größten Typ definieren, der alle aus diesen Konstruktoren entstandenen Werte enthält, wodurch das Diskriminierungs -Axiom beibehalten wird:

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

list ist isomorph zu einer Teilmenge von colist. Zusätzlich, colist Enthält unendliche Listen: Listen mit cocons auf cocons.

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

flipflop ist die unendliche (Rundschreibenliste) $ 1 :: 2 :: 1 :: 2 :: ldots $; from 0 Ist die unendliche Liste der natürlichen Zahlen $ 0 :: 1 :: 2 :: ldots $.

Eine rekursive Definition ist gut geformt, wenn das Ergebnis aus kleineren Blöcken erstellt wird: Rekursive Anrufe müssen bei kleineren Eingaben funktionieren. Eine korresive Definition ist gut geformt, wenn das Ergebnis größere Objekte erstellt. Die Induktion untersucht Konstrukteure, die Koinduktion untersucht Zerstörer. Beachten Sie, wie sich die Dualität nicht nur zu größerem, sondern auch in die Ausgänge ändert. Zum Beispiel der Grund der Grund flipflop und from Die obigen Definitionen sind gut geformt, dass der corecursive Anruf durch einen Anruf an die bewacht wird cocons Konstruktor in beiden Fällen.

Wenn Aussagen zu induktiven Objekten induktive Beweise haben, haben Aussagen über koinduktive Objekte koinduktive Beweise. Lassen Sie uns beispielsweise das unendliche Prädikat auf Colisten definieren. Intuitiv sind die unendlichen Colisten diejenigen, die nicht enden conil.

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

Um zu beweisen, dass Colisten der Form from n sind unendlich, wir können durch Koinktion argumentieren. from n ist gleich cocons n (from (1 + n)). Dies zeigt, dass from n ist größer als from (1 + n), was durch die Koinduktionshypothese unendlich ist, daher from n ist unendlich.

Bisimilarity, ein koinduktives Eigentum

Die Koinktion als Beweistechnik gilt auch für fünzige Objekte. Intuitiv sprechend, basieren induktive Beweise für ein Objekt auf der Erstellung des Objekts. Koinduktive Beweise basieren darauf, wie das Objekt zersetzt werden kann.

Bei der Untersuchung deterministischer Systeme ist es üblich, die Äquivalenz durch induktive Regeln zu definieren: Zwei Systeme sind gleichwertig, wenn Sie durch eine Reihe von Transformationen von einem zum anderen erreichen können. Solche Definitionen neigen dazu, die vielen verschiedenen Arten nicht zu erfassen, wie nicht deterministische Systeme trotz unterschiedlicher interner Struktur das gleiche (beobachtbare) Verhalten aufweisen können. (Koinktion ist auch nützlich, um nicht terminierende Systeme zu beschreiben, auch wenn sie deterministisch sind, aber darauf werde ich mich hier nicht konzentrieren.)

Nichtdeterministische Systeme wie gleichzeitige Systeme werden häufig von modelliert Bezeichnete Übergangssysteme. Ein LTS ist ein gerichtetes Diagramm, in dem die Kanten gekennzeichnet sind. Jede Kante stellt einen möglichen Übergang des Systems dar. Eine Spur eines LTS ist die Abfolge von Kantenbezeichnungen über einem Pfad im Diagramm.

Zwei LTs können sich identisch verhalten, da sie die gleichen möglichen Spuren haben, auch wenn ihre interne Struktur unterschiedlich ist. Graph -Isomorphismus ist zu stark, um ihre Äquivalenz zu definieren. Stattdessen wird ein LTS $ mathscr {a} $ zu sagen simulieren Ein weiterer LTS $ mathscr {b} $ Wenn jeder Übergang des zweiten LTS im ersten einen entsprechenden Übergang zulässt. Offiziell, sei $ s $ die disjoint Union der Staaten der beiden LTs, $ l $ die (gemeinsame) Etiketten und $ rightarrow $ die Übergangsbeziehung. Die Beziehung $ r subseteq s mal s $ ist eine Simulation, wenn $$ forall (p, q) in r, % forall p ' in s, forall alpha in l, text {if} p stackrel alpha rightarrow p ' text {dann} existiert Q', ; q stackrel alpha rightarrow q ' text {und} (p', q ') in r $$

$ mathscr {a} $ simuliert $ mathscr {b} $ Wenn es eine Simulation gibt, in der alle Zustände von $ mathscr {b} $ mit einem Zustand in $ mathscr {a} $ verwandt sind. Wenn $ R $ eine Simulation in beide Richtungen ist, wird es als a genannt Halbierung. Simulation ist eine koinduktive Eigenschaft: Jede Beobachtung auf der einen Seite muss auf der anderen Seite ein Übereinstimmung haben.

Es gibt potenziell viele Bissimulationen in einem LTS. Unterschiedliche BISImulationen können unterschiedliche Zustände identifizieren. Angesichts von zwei Bissimulationen $ r_1 $ und $ r_2 $ ist die Beziehung, die die Vereinigung der Beziehungsgraphen $ R_1 Cup R_2 $ einnimmt, selbst eine Bissimulation, da verwandte Zustände zu verwandten Zuständen für beide Beziehungen führen. (Dies gilt auch für unendliche Gewerkschaften. Die leere Beziehung ist eine uninterstierende Bissimulation, ebenso wie die Identitätsbeziehung.) Insbesondere ist die Vereinigung aller Bissimulationen selbst eine Bissimilität, die als Bisimilarität bezeichnet wird. Bisimilarity ist der grobe Weg, um ein System zu beobachten, das nicht zwischen verschiedenen Zuständen unterscheidet.

Bissimailarity ist ein koinduktives Eigentum. Es kann als der größte Fixpoint eines Bedieners definiert werden: Es ist die größte Beziehung, die, wenn sie erweitert werden, um äquivalente Zustände zu identifizieren, gleich bleibt.

Verweise

  • CoQ und der Kalkül induktiver Konstruktionen

    • Yves Bertot und Pierre Castéran. Interaktive Theorem -Beweis- und Programmentwicklung - Coq'Art: Der Kalkül induktiver Konstruktionen. Springer, 2004. Ch. 13. [Webseite] [Amazonas]
    • Eduardo Giménez. Eine Anwendung ko-induktiver Typen in COQ: Überprüfung des Wechselbitprotokolls. Im Workshop über Typen für Beweise und Programme, Nummer 1158 in Vorlesungsnotizen in Informatik, Seiten 135–152. Springer-Verlag, 1995. [Google Bücher]
    • Eduardo Giménez und Pierre Castéran. Ein Tutorial zu [Co-]-induktiven Typen in Coq. 2007. [PDF]

  • Beschriftete Übergangssysteme und Bissimulationen

    • Robin Milner. Kommunikation und Parallelität. Prentice Hall, 1989.
    • Davide Sangiorgi. Über die Ursprünge der Brutbisimulation und Koinktion. ACM -Transaktionen zu Programmiersprachen und Systemen (Toplas), Band 31 Ausgabe 4, Mai 2009. [PDF] [ACM] Zugeordnete Kursrutschen: [PDF] [Citeseer]

    • Davide Sangiorgi. Der Pi-Kalkulus: Eine Theorie mobiler Prozesse. Cambridge University Press, 2003. [Amazonas]

    • EIN Kapitel in Zertifizierte Programmierung mit abhängigen Typen Von A. Chlipala

    • D. Sangiorgi. "Einführung in Bissimulation und Koinktion". 2011. [PDF]
    • D. Sangiorgi und J. Rutten. Fortgeschrittene Themen in der Bisimulation und Koinktion. Cambridge University Press, 2012. [TASSE]

Andere Tipps

Betrachten wir die folgende induktive Definition:

$ qquad displaystyle begin {align*} & phantom { rightarrow} quad varepsilon in mathcal {t} w in mathcal {t} quad & rightarrow quad aw aw in in in in in in in in in in in in in in in in in in in in in in in in in in in in mathcal rightarrow in in in in in mathcal rightarrow. mathcal {t} aw in mathcal {t} quad & rightarrow quad baw in mathcal {t} end {align*} $

Was ist $ mathcal {t} $? Offensichtlich die Saiten ohne zwei nachfolgende $ b $, dh

$ qquad displaystyle mathcal {t} = { varepsilon, aa, aa, ba, aaa, aba, dots } = mathcal {l} links ((ba mid a)^* rechts) subseteq sigma^*. $

Recht? Nun, was wir dafür brauchen, ist der harmlose Satz "und $ mathcal {t} $ ist der kleinste Satz, der diese Bedingungen erfüllt". Richtig genug, wie sonst $ mathcal {t} = {a, b }^*$ würde auch funktionieren.

Aber es steckt mehr als das. Schreiben Sie die obige Definition als (monotone) Funktion $ f: 2^{ sigma^ infty} bis 2^{ sigma^ Infty} $:

$ qquad f (t) = t cup { varepsilon } cup {aw Mid W in t } cup {baw Mid Aw in t } $

Jetzt ist $ mathcal {t} $ das Kleinstes Fixpoint von $ f $. In der Tat, weil $ f $ monoton und $ links (2^{ sigma^ infty} ist, ist subseteq rechts) $ a Komplettes Gitter, KNASTER-TARSKI-Theorem sagt uns, dass ein so kleinster Fixpoint existiert und eine richtige Sprache ist. Da dies mit einer vernünftigen induktiven Definition funktioniert, sprechen wir normalerweise nicht darüber. Es passt nur zu unserer Intuition: Wir beginnen mit $ { varepsilon } $ und wenden die Regeln Schritt für Schritt an; Im Limit erhalten wir $ mathcal {t} $.

Jetzt drehen wir Dinge um. Anstatt zu sagen, dass "wenn $ W $ enthalten ist, ist $ aw $" wir sagen "Wenn $ AW $ enthalten ist, muss es also $ W $ gewesen sein". Wir können den Anker nicht umdrehen, also geht er weg. Das lässt uns ein Problem: Wir müssen in der Lage sein, nehmen zu können willkürlich lang Präfixe von jedem Wort in $ mathcal {t} '$ und bleiben in $ mathcal {t}' $! Dies ist mit endlichen Wörtern nicht möglich; Gut, dass ich mich in $ sigma^ Infty $ oben geschlichen habe! Am Ende haben wir die unendlichen Wörter ohne Faktor (Substring) $ bb $, dh $ mathcal {t} '= mathcal {l} links ((ba mid a)^ omega rechts) $.

In Bezug auf $ f $, $ mathcal {t} '$ ist es größten Fixpoint². Dies ist eigentlich ziemlich intuitiv: Wir können nicht hoffen, $ mathcal {t} '$ von zu erreichen unter, dh induktiv, wenn $ { varepsilon } $ und Hinzufügen Sachen, die die Regeln erfüllen, also gehen wir aus Oben, dh koinduktiv von $ sigma^ Infty $ und Entfernen Zeug, das tut nicht entsprechen den Regeln.

Notation:

  • $ Sigma^ infty = sigma^* cup sigma^ Omega $
  • $ Sigma^ Omega $ ist das Set von allen unendlich Sequenzen über $ sigma $.

¹ Sie dürfen keine Dinge wie $ w in mathcal {t} rightarrow aw notin mathcal {t} $ machen; Die entsprechende Funktion wäre nicht monoton.
² Wir müssen $ { varepsilon } $ irgendwie unter den Teppich fegen.

Lizenziert unter: CC-BY-SA mit Zuschreibung
Nicht verbunden mit cs.stackexchange
scroll top