Ein Verfahren zur Definition und Begründung über potentiell unendliche oder zirkuläre Strukturen und Verhaltensweisen, indem diese als größte Fixpunkte von Operatoren charakterisiert werden und Eigenschaften mittels koinduktiver Annahmen wie Bisimulationen und Beobachtungen bewiesen werden.

Prinzip

Koinduktion stellt die Zugehörigkeit oder Äquivalenz zu einer größten Fixpunktmenge fest: Um zu beweisen, dass ein Objekt eine koinduktive Eigenschaft erfüllt, zeigt man, dass es die beobachtbaren Verhaltensweisen aufweist, die durch die koinduktive Definition erhalten bleiben (oft durch Nachweis einer Bisimulation oder einer Erhaltungsbedingung).

Demonstration

Ströme (infinite Sequenzen) werden oft koinduktiv behandelt: Um zu beweisen, dass zwei Ströme s und t gleich sind, definiert man eine Bisimulationsrelation R und zeigt (s,t) ∈ R und dass R beim Bilden von Kopf und Schwanz erhalten bleibt, sodass koinduktiv s = t folgt.

Fehlanwendung

Induktionsartige Argumente über endliche Konstruktionen auf grundlegend nicht wohlgegründete Strukturen anzuwenden oder Koinduktion zu nutzen, ohne die Erhaltungs-/Invarianzbedingung zu prüfen (und so Eigenschaften anzunehmen, die nicht unter coalgebraischer Entfaltung geschlossen sind), ist Fehlgebrauch.

Konsequenz

Koinduktives Schließen ermöglicht korrekte, kompositionelle Beweise über unendliche Daten, reaktive Systeme und Verhaltensweisen (z. B. Ströme, Prozesse, unendliche Bäume) und stützt Definitionen durch beobachtbares Verhalten statt Konstruktion.

Umkehrung

Die Induktion (kleinstes Fixpunkt-Schließen) ist das Dual: sie beweist Zugehörigkeit durch endliche Konstruktion aus Basisfällen und Konstruktoren, während Koinduktion Zugehörigkeit zeigt, indem sie die Ununterscheidbarkeit eines Elements von Mitgliedern der koinduktiven Menge durch beobachtbare Schritte demonstriert.

Abgrenzung

Anwendbar auf nichtwohlbegründete oder corekursive Domänen, modelliert als Koalgebren, und auf Systeme, die durch größte Fixpunkte spezifiziert sind; ungeeignet für Eigenschaften, die endliche Terminierung oder wohlfundierte Induktion erfordern, ohne zusätzliche Rechtfertigung.

Semantische Spannung

Spannung entsteht zwischen der extensionalen Behandlung von Objekten (durch beobachtbares Verhalten, Koinduktion) und der intensionalen (durch Konstruktion, Induktion); manche Beweise sind nur unter zusätzlichen Endlichkeits- oder Guard-Bedingungen zwischen beiden überführbar.

Synthese

Koinduktives Schließen ist die Praxis, Eigenschaften unendlicher oder zirkulärer Strukturen zu beweisen, indem die Erhaltung des beobachtbaren Verhaltens bei Entfaltung nachgewiesen wird; es ergänzt die Induktion durch Fokussierung auf größte Fixpunktcharakterisierungen und erlaubt das Schließen über fortlaufende Prozesse und unendliche Daten.