Quantoren
Allquantor
Mit Hilfe des Allquantors ∀ lässt sich einfach überprüfen, ob ein gegebenes Prädikat 𝓅 für alle Elemente x einer Sammlung von Elementen erfüllt ist.
| ∀(x ∈ C) (𝓅(x)) | Für alle x aus C gilt 𝓅. |
Der gegebene Ausdruck ist also nur dann true, wenn die Bedingung für alle Elemente erfüllt ist und schon dann false, wenn ein einziges Element die Bedingung nicht erfüllt.
| assert ∀(x ∈ {2, 4, 6}) (2 ∣ x) | Alle Elemente sind durch 2 teilbar. |
| assert ¬ ∀(x ∈ {2, 3, 4}) (2 ∣ x) | Nicht alle Elemente sind durch 2 teilbar. |
Bei der zweiten Anweisung bezieht sich die Negation auf den ganzen Ausdruck, da die Juxtaposition von Quantor und Prädikat Vorrang vor dem Präfixoperator ¬ hat.
Genügt einer der Elemente nicht der Bedingung, so führt dies in der Regel zu einem unmittelbaren Abbruch der hinter dem Allquantor stehenden Implementierung. Dies beutet insbesondere für eine Bedingung, die wider Erwarten wie auch immer geartete Nebeneffekte hat, dass diese möglicherweise nicht für alle Elemente aufgerufen wird. Um das Ergebnis true liefern zu können müssen in der Regel also alle Elemente durchlaufen werden, was bei n Element einen Aufwand von O(n) bedeutet.
Existenzquantor
Genügt es, dass mindestens ein Element die gewünschte Bedingung 𝓅 erfüllt, so kann der Existenzquantor genutzt werden.
| ∃(x ∈ C) (𝓅(x)) | Für mindestens ein x aus C gilt 𝓅. |
Der gegebene Ausdruck ist also dann true, wenn die Bedingung schon für ein Element erfüllt ist und erst dann false, wenn alle Element die Bedingung nicht erfüllen.
| assert ∃(x ∈ {1, 3, 5, 6, 7}) (2 ∣ x) | Mindestens ein Element ist durch 2 teilbar. |
| assert ¬ ∃(x ∈ {1, 3, 5, 7}) (2 ∣ x) | Noch nicht einmal ein Element ist durch 2 teilbar, |
| | also alle Elemente sind nicht durch 2 teilbar. |
Sprachlich kann es gelegentlich einfacher sein, darüber zu sprechen, dass es kein Element mit einer vorgegebenen Eigenschaft gibt. Dankbarer Weise gibt es dafür auch ein eigenes Symbol.
Anzahlquantoren
Gelegentlich spielt die konkrete Anzahl der Elemente, die die gewünschte Eigenschaft erfüllen, eine Rolle. So wird oft danach gefragt, ob genau ein Element die Eigenschaft erfüllt. Beispielsweise kann es beim eindeutigen Gewinnen nur genau einen geben, andernfalls müssen sich zwei oder gar mehrere den 1. Platz teilen.
| has_unique_winner :← ∃!(a ∈ attendees) ∀(a′ ∈ attendees, a′ ≠ a) (a.points > a′.points) |
Allgemein kann die gewünschte Anzahl n beim Existenzquantor als Superskript festgelegt werden: ∃n. Dementsprechend ist ∃! äquivalent zu ∃¹.
| assert ∃¹(x ∈ C) = ∃!(x ∈ C) |
| assert ∃³(x ∈ {1, … , 10}) (3∣x) |
Gleichermaßen können auch Bereiche angegeben werden, wobei die Notation der von Grammatiken, regulären Ausdrücken und Vektoren folgt:
| ∃n | Es gibt genau n … |
| ∃(n, …) | Es gibt mindestens n … |
| ∃(1, …, m) | Es gibt höchstens m … |
| ∃(n, …, m) | Es gibt mindestens n aber höchstens m … |
Dabei kann allein bei der Mindestangabe ∃(n, …) vorzeitig abgebrochen werden; alle anderen Anzahlwuantoren erfordern das Durchlaufen aller Möglichkeiten.
Die Beziehung zwischen den Quantoren
Das zweite Anweisung im letzten Beispiel zeigt sehr schön die Beziehung zwischen Existenz- und Allquantor: Wird die Bedingung 𝓅 negiert, so kann der Existenzquantor durch den Allquantor ersetzt werden und umgekehrt.
| ∀(x ∈ C) 𝓅(x) ⇔ ¬ ∃(x ∈ C) ¬ 𝓅(x) |
| ∃(x ∈ C) 𝓅(x) ⇔ ¬ ∀(x ∈ C) ¬ 𝓅(x) |
| ∄(x ∈ C) 𝓅(x) ⇔ ∀(x ∈ C) ¬ 𝓅(x) |
Filter für die zu quantifizierenden Elemente
Die bei den Quantoren durchlaufenen Elemente können – wie auch bei der allgemeinen Notation für Ansammlungen – durch eine oder mehrere Bedingungen ergänzt werden, mit deren Hilfe die Prüfung des Prädikats auf bestimmte Elemente eingeshränkt werden können. Damit lässt sich gelegentlich besser ausdrücken, was für den Quantor wesentlich ist.
| ∀(x ∈ C, 𝒸₁(x), … , 𝒸n(x)) (𝓅(x)) |
Diese Form des Filterns kann immer durch eine Implikation mit negiertem Filter ersetzt werden
| ∀(x ∈ C, 𝒸(x)) (𝓅(x)) ⇔ ∀(x ∈ C) (¬𝒸(x) →̇ 𝓅(x)) |
Welche der beiden Formen die bessere ist, hängt davon ab, was man zum Ausdruck bringen möchte. Ist beispielsweise ein Element c aus einer Menge M bekannt und man möchte wissen, ob ein bestimmtes Attribut e auch noch bei einem anderen Element aus M vorhanden ist, so kann man nicht die ganze Menge mit dem Existenzquantor durchsuchen, sondern muss das bereits bekannte c ausschließen.
| ∃(x ∈ M, x ≠ c) (x.e = c.e) |
Es gibt einen wesentlichen Unterschied zwischen den beiden Varianten: Ein an die Elemente des Quantoren gekoppelter Filter kann unter Umständen von dem Elementbehälter selbst ausgewertet werden. Beispielsweise ist die Menge ℕ (wenn man vom begrenzten Speicherplatz absieht) unbegrenzt. Das bedeutet, dass ein Quantor möglicherweise nicht terminiert. Werden die Elemente jedoch gefiltert, kann aus der unendlichen Menge eine endliche werden.
| ∀(x ∈ ℕ, x ≤ 100) (𝓅(x)) ⇔ ∀(x ∈ {0, … , 100}) (𝓅(x)) |
Erweiterung des Skopus
Mit einem Quantor wir ein neuer Skopus angelegt, in dem die an den Quantor gebundene Variable (die Laufvariable) bekannt ist. Die Laufvariable kann demnach ab diesem Zeitpunkt für den Prädikatsausdruck 𝓅 verwendet werden – natürlich auch, wenn dieser wieder Quantoren enthält. Gelegentlich werden aber zusätzliche Variablen benötigt, die über die gesamte Lebensdauer hinweg unverändert bleiben. Dies kann über die where-Klausel erledigt werden.
Beispielhaft soll hier geprüft werden, ob bei allen Elementen x ∈ C die Eigentschaft e gleich ist.
| ∀(x ∈ C where c′ := arb(C)) (c.e = c′.e) |
Wie so oft ist auch hier Vorsicht geboten: Die where-Klausel bezieht sich nur auf den Teil, in dem sie definiert wurde. In dem nachfolgenden Beispiel bezieht sich die where-Klausel nur auf den Filter.
| ∀(x ∈ C, c ≠ c′ where c′ := arb(C)) (isSquare(x)) |
Dies bedeutet, dass hier für jedes Element x aus C ein beliebiges Element c′ aus C bestimmt wird, um den Test c ≠ c′ durchzuführen; c′ kann also, je nachdem wie arb für C implementiert ist, für jedes x verschieden sein.
Optimierungen
Oft soll bei einem Quantor ein bestimmtes Element ausgeschlossen werden. Das kann natürlich durch Entfernen des Elements aus der Menge geschehen, wenngleich das sehr aufwendig sein kann.
| ∃(x ∈ A) ∀(y ∈ B ∖ {e}) 𝓅(x) |
Einfacher ist es oft, das Element gezielt auszufiltern.
| ∃(x ∈ A) ∀(y ∈ B, x ≠ e) 𝓅(x) |
Dabei kann es günstiger sein, das Objekt auf seine (strikte) Identität hin zu prüfen, da dies – insbesondere bei zusammengesetzten Objekten – oft um ein Vielfaches schneller ist.
| ∃(x ∈ C) ∀(y ∈ C, x ≣̸ e) 𝓅(x) |
Darüber hinaus kann sich der Übersetzter zumindest bei Mengen zu Nutze machen, dass die Ungleichheit sehr wahrscheinlich ist, nämlich nur genau ein Mal bezogen auf alle Werte.
Beispiel
Mit Hilfe der Quantoren soll die Wertigkeit eines Pokerblatts bestimmt werden. Das ist zwar nicht in allen Fällen sinnvoll, ist aber nichtsdestoweniger dazu geeignet, deren Funktionsweise zu erläutern. Darüber hinaus ist mit fünf aus 52 Karten die Menge so klein, dass sich viele algorithmische Optimierungen einfach nicht lohnen.
Über eine geschickte Wahl der Datenstrukturen, insbesondere der Gestaltung der Hand lassen sich viele der unten stehenden Funktionen in O(1) oder O(n) statt O(n²) oder schlimmer erledigen.
| Suit | :≡ ⟦ordered⟧ {♥, ♦, ♣, ♠} |
| Rank | :≡ ⟦ordered⟧ {𝐀, 𝐊, 𝐐, 𝐉, 𝟏𝟎, 𝟗, 𝟖, 𝟕, 𝟔, 𝟓, 𝟒, 𝟑, 𝟐} |
| Card | :≡ ⟦ordered⟧ (suit : Suit, rank : Rank) |
| Hand | :≡ Set⟦Card⟧ | Steht stellvertretend für einen Satz von fünf Karten. |
Alle Werte sind verschieden
| function differentRanks(cards : Set⟦Card⟧) → 𝔹 is |
| return ∀(c ∈ cards) ∄(c′ ∈ cards, c′≠ c) c.rank = c′.rank |
„Flush“ (alle Farben sind gleich)
| ∀(c ∈ cards) ∀(c′ ∈ cards) c.suit = c′.suit |
| function sameSuits(cards : Hand) → 𝔹 is |
| return ∀(c ∈ cards where c′ := arb(cards)) c.suit = c′.suit |
„Straight“ (alle Werte in Folge)
| function isSucc(r₁ : Rank, r₂ : Rank) → 𝔹 is |
| return (r₁.ord = r₂.ord + 1) ⩒ (r₁ = 𝐀 ⩑ r₂ = 𝟐) |
| function isStraight(hand : Hand) → 𝔹 requires {∣hand∣ = 5} is |
| ∃(card ∈ hand) card.rank ∈ {𝟓, 𝟔, 𝟕, 𝟖, 𝟏𝟎} |
| ⩑ |
| ∃(cards ∈ ℘=(hand, 4)) ∀(c ∈ cards) ∃(c′ ∈ hand) isSucc(c.rank, c′.rank) |
| function isStraight(hand : Hand) → 𝔹 requires {∣hand∣ ≤ 7} is |
| n := ∣hand∣ |
| S := {Rank.findByOrdinal(n), … , Rank.findByOrdinal(15 − n)} |
| return ( |
| ∃(card ∈ hand) card.rank ∈ S |
| ⩑ |
| ∃(subset ∈ ℘=(cards, n − 1)) ∀(c ∈ subset) ∃(c′ ∈ cards) isSucc(c.rank, c′.rank) |
| function isRoyal(hand : Hand) → 𝔹 requires {isStraigh(hand)} is |
| ∃(c ∈ hand) ∀(c′ ∈ hand) (c.rank ≥ c′.rank) |
| ⩑ |
| (c.rank = 𝐀) |
Vierling (vier gleiche Werte)
| function sameRank(cards : Set⟦Card⟧) → 𝔹 is |
| return ∀(c ∈ cards where c′:= arb(cards)) (c.rank = c′.rank) |
| function fourOfAKind(cards : Hand) → 𝔹 is |
| return ∃(subset ∈ ℘=(cards, 4)) (sameRank(subset)) |
„Full House“ (ein Drilling und ein Paar)
| function fullHouse(cards : Hand) → 𝔹 is |
| return ∃(subset ∈ ℘=(cards, 3)) (sameRank(subset)) |
| ⩑ |
| sameRank(cards ∖ subset) |
Drilling (drei gleiche Werte)
Bei einem Drilling tritt das Problem auf, dass man sicher stellen muss, es weder mit einem Vierling noch mit einem „Full House“ zu tun zu haben. Das Vierlingsproblem lässt sich auf zweierlei Art lösen: Entweder wird sichergestellt, dass nur genau eine Dreierkombination existiert oder die Sonderfälle müssen ausgeschlossen werden. Letzeres muss ja ohnehin irgendwie gemacht werden, da die Verbleibenden Karten kein Paar sein dürfen.
| function threeOfAKind(hand : Hand) → 𝔹 ⁌
⁍ is |
| ∃!(cards ∈ ℘=(hand, 3)) (sameRank(cards)) |
| ⩑ |
| ¬ sameRank(hand ∖ cards) |
| function threeOfAKind(hand : Hand) → 𝔹 ⁌
⁍ is |
| ∃(triple ∈ ℘=(hand, 3)) (sameRank(triple)) |
| ⩑ |
| (¬ sameRank(rest) where rest := hand ∖ triple) |
| ⩑ |
| ∄(card ∈ rest where c := arb(triple)) (card.rank = c.rank) |
Zwei Paare (zwei mal zwei gleiche Werte)
| function twoPairs(cards : Hand) → 𝔹 is |
| ∃(first_pair ∈ ℘=(cards, 2)) (sameRank(first_pair)) |
| ⩑ |
| ∃(second_pair ∈ ℘=(rest, 2) where rest := cards ∖ first_pair) (sameRank(second_pair)) |
| ⩑ |
| (cr ≠ cr′ where cr := arb(subset).rank where cr′ := arb(subset′).rank) |
| ⩑ |
| (r ≠ cr ⩑ r ≠ cr′ where r := arb(rest ∖ second_pair).rank) |
Ein Paar (zwei gleiche Werte)
| function onePair(hand : Hand) → 𝔹 is |
| ∃!(pair ∈ ℘=(hand, 2)) (sameRank(pair)) |
| ⩑ |
| differentRanks(hand ∖ pair) |
Es gibt genau ein Triple, bei dem alle Karten den gleichen Rang haben, und die restlichen beiden Karten sind kein Paar mit gleichem Rang.