Coinduction

In Haskell: Unendliche Listen. ones = 1 : ones. (Eine Liste von unendlich vielen Einsen). Wenn du versuchst, sie ganz zu drucken, stürzt der PC ab. Aber mit Coinduktion (Lazy Evaluation) kannst du sagen: take(5, ones). Der PC berechnet nur die ersten 5 Elemente. Server-Prozesse sind auch coinduktiv: Sie laufen (hoffentlich) ewig und reagieren auf Requests.

1. Bisimulation

Wann sind zwei unendliche Prozesse gleich? Man kann nicht bis zum Ende warten (es gibt keins). Man nutzt Bisimulation: "Wenn beide beim ersten Schritt das Gleiche tun, und danach in Zustände übergehen, die sich wieder gleich verhalten.... dann sind sie gleich." Das nutzt man z. B. um zu beweisen, dass zwei verschiedene Server-Implementierungen das gleiche Protokoll sprechen.

1. Kategorientheorie (Category Theory)

In der abstrakten Mathematik sind Induktion und Koinduktion duale Konzepte innerhalb der Kategorientheorie. Induktion beschreibt initiale Algebren (Least Fixed Point, $\mu X$). Man fängt beim Nichts an und baut Strukturen "bottom-up" auf (wie Peano-Zahlen: $0$, $S(0)$, $S(S(0))$). Koinduktion beschreibt finale Coalgebren (Greatest Fixed Point, $\nu X$). Man startet mit dem gigantischen, unendlichen Alles und beobachtet Destruktoren "top-down", wie das Entnehmen des Kopfes (Head) eines Unendlichkeits-Streams (Stream<T> -> T * Stream<T>). Dies ist das formale Fundament für Lazy Evaluation und Endlos-Automaten.

2. Bisimulation und Zustand

Da man unendliche Systeme (wie Betriebssystem-Scheduler oder Netzwerkprotokolle) nicht durch Abzählen auf Gleichheit prüfen kann (Induktionsbeweis versagt), nutzt man die Bisimulation (von Robin Milner, $\pi$-Kalkül). Zwei Systeme $p$ und $q$ sind bisimilar ($p \sim q$), wenn für jeden Schritt von $p$ nach $p'$ durch ein Event $a$, das System $q$ denselben Schritt $a$ nach $q'$ nachspielen kann, sodass $p' \sim q'$ (und vice versa). Dies dient in der theoretischen Informatik zum Verifizieren, dass eine hoch-komplexe, performance-optimierte Netzwerk-Implementation sich nach außen exakt verhält wie die langsame Referenz-Spezifikation. Man beweist keine Terminierung, sondern konstante Verhaltens-Äquivalenz.

3. Corecursion in funktionalen Sprachen

Die praktische Umsetzung von Koinduktion nennst sich Corecursion. Während bei Rekursion ein Base Case die Terminierung erzwingt, produziert Corecursion mit jedem Schritt verlässlich Daten (Productive Recursion). Ein klassischer Fibonacci-Stream in Scala oder Haskell: val fibs: Stream[Int] = 0 #:: 1 #:: fibs.zip(fibs.tail).map{case (a,b) => a+b}. Dieses Konstrukt terminiert niemals intern. Es obliegt dem aufrufenden Kontext (dem Konsumenten), via take(n) zu entscheiden, wann genug beobachtet wurde. Würde die Iteration einmal nichts produzieren (Endlosschleife im Generator), würde das Bottom-Up Paradigma abstürzen (Livelock).