Typen und vollständige partielle Ordungen

definiert einen Wertebereich

Beim Ableiten von Eigenschaften (Korrektheit, Terminierung, ...) aus einem Programm (einer Funktion, eines Ausdrucks) muss der Fall ⊥ mit betrachtet werden.

Die Wertebereiche von einfachen Datentypen besitzen in der Theorie neben den eigentlichen Werten noch einen weiteren Wert ⊥

Der Wertebereich der Wahrheitswerte besteht also aus drei Werten.

Bei zusammengesetzten Wertebereichen (Summen- und Produkt-Datentypen) wird die Situation komplexer.

Es wird möglich, dass nur einzelne Komponenten oder Varianten eines Wertes nicht definiert sind.

Wieviel von einem Wert ist definiert?

Ist ein Wert mehr definiert als ein anderer?

vollständige partielle Ordnung
vollständige Halbordnung

complete partial order
CPO

vollständige partielle Ordnung

partielle Ordnung bei der jede aufsteigende Kette
x1 ⊑ x2 ⊑ x3 ⊑ x4 ⊑ ...
eine obere Schranke (Supremum) besitzt.

Jede vollständige partielle Ordnung besitzt ein kleinstes Element.

Ein Wertebereich in Haskell einschließlich ⊥ bildet eine vollständige partielle Ordnung.
⊥ ist das kleinste Element.