Rechnen mit Intervallen.

Ein Intervall [a, b] steht für jeden Wert dazwischen. Rechnet man mit Intervallen, ist das Ergebnis wieder ein Intervall, das jedes mögliche Ergebnis einschließt: Für die Summe gilt [a, b] + [c, d] = [a + c, b + d], für das Produkt nimmt man Minimum und Maximum der vier Produkte der Ränder.

Eine Messung mit Unsicherheit wird so direkt zur Eingabe: Ein Sensor mit bekannter Fehlergrenze liefert ein Intervall, keinen Punkt. Liegt das Ergebnisintervall ganz innerhalb einer Grenze, ist die Aussage für jeden Wert innerhalb der Unsicherheit bewiesen.

Intervallarithmetik überschätzt, wenn eine Größe mehrfach vorkommt: x − x ergibt nicht null, sondern ein Intervall um null, weil die Rechnung nicht weiß, dass beide x derselbe Wert sind. Dieses Abhängigkeitsproblem wird kleiner, je kleiner die Boxen werden, in die man den Raum zerlegt.

Gleitkommazahlen nach IEEE 754 können die meisten Dezimalwerte nicht exakt darstellen, und jede Rechnung rundet. Damit ein Intervall den wahren Wert sicher einschließt, wird die Untergrenze nach unten und die Obergrenze nach oben gerundet. IEEE 754 sieht diese gerichteten Rundungsarten vor, und die Norm IEEE 1788 beschreibt Intervallarithmetik auf dieser Grundlage. Bibliotheken wie MPFI oder Boost.Interval setzen Intervallarithmetik mit gerichteter Rundung um, nach IEEE 1788 etwa libieeep1788.

Der Demonstrator im Browser rechnet in der Ebene seiner Zeichnung mit gewöhnlichen Gleitkommazahlen. Für die Prüfung im Betrieb ist die gerichtete Rundung vorgesehen, damit kein Rundungsfehler ein Ja erzeugen kann, das die exakte Rechnung nicht trägt.

Für eine Bedingung über mehrere Größen beginnt KALKÜL mit einer Box, dem Produkt der Intervalle aller Größen. Für jede Box gibt es drei Antworten: Die Bedingung gilt in der ganzen Box, sie gilt nirgends in der Box, oder die Intervallrechnung kann es nicht entscheiden. Im dritten Fall wird die Box geteilt, und jede Teilbox wird für sich geprüft. Das Vorgehen ist als Branch and Bound bekannt, für Mengen als SIVIA (Set Inversion via Interval Analysis).

Im Demonstrator ist der Raum eine Zeichenebene mit zwei Größen. Ein Vorschlag ist eine Bahn durch diese Ebene, und seine Unsicherheit wächst entlang der Bahn: Um jeden Punkt liegt ein Kreis, dessen Radius mit der Zeit zunimmt. Zusammen bilden die Kreise eine Röhre aller möglichen Zustände. Drei Regeln ziehen Grenzen: ein Sperrraum als Ellipse, eine Obergrenze und eine Untergrenze.

Die Suche beginnt mit einem Raster aus Quadraten, prüft nur Quadrate, die die Röhre berühren, und viertelt jedes unentschiedene, Ebene für Ebene bis zu einer festen feinsten Kantenlänge. Für die Ellipse ist die Prüfung je Quadrat exakt: Die quadrierten, normierten Koordinaten werden über das Quadrat in Intervalle eingeschlossen; ist die Untergrenze ihrer Summe mindestens eins, liegt das Quadrat ganz außerhalb, ist ihre Obergrenze höchstens eins, ganz innerhalb. Ein Test misst unabhängig an 36 Punkten je Quadrat nach, dass jedes geprüfte Quadrat im erlaubten Raum liegt und jedes Gegenbeispiel im verbotenen.

Liegt jede Box, die mögliche Zustände enthält, ganz im erlaubten Raum, ist die Bedingung bewiesen. Liegt eine Box, die mögliche Zustände enthält, ganz jenseits einer Grenze, ist die Bedingung widerlegt, und die Box ist das Gegenbeispiel. Der Demonstrator hält nach der Ebene an, in der er ein Gegenbeispiel findet, und bestimmt näherungsweise den ersten Zeitpunkt, an dem ein möglicher Zustand eine Regel bricht, indem er den Rand der Röhre an 32 Punkten je Kreis abtastet.

Bleiben nach der feinsten erlaubten Teilung Boxen, die weder ganz erlaubt noch ganz verboten sind, lautet das Ergebnis unentschieden. Unentschieden heißt: keine Freigabe. Genauere Eingaben oder mehr Rechenbudget können die Frage entscheiden; ein Raten zugunsten der Handlung gibt es nicht.

Hängt eine Größe monoton von einem unsicheren Parameter ab, reichen die beiden Ränder des Parameterintervalls: Die Lösungen für den kleinsten und den größten Wert schließen alle dazwischen ein. Auf der Seite von KALKÜL rechnet eine der Szenen so: Eine Größe, die mit einer unsicheren Rate exponentiell abklingt, liegt zwischen den Kurven für die kleinste und die größte Rate, und geprüft wird der Abstand dieser Röhre zu ihren Grenzen.

Ist Monotonie nicht gegeben, braucht es die Zerlegung. Für glatte Funktionen geben die Mittelwertform oder Taylor-Modelle engere Einschlüsse als die einfache Intervallrechnung, und damit weniger Teilungen bis zur Entscheidung.