Was bedeutet "⊥" in "The Strictness Monad" von P. Wadlers Papier?

Question

Kann mir jemand helfen, die folgende Definition aus Wadlers Aufsatz mit dem Titel "Comprehending Monads" zu verstehen? (Auszug ist aus dem Abschnitt 3.2/Seite 9, das heißt der „Strikt Monad“ Abs.)

---

Manchmal ist es notwendig, um die Bewertung in einem faulen Funktionsprogramm zu steuern. Dies wird in der Regel mit der berechenbaren Funktion erreicht strenge, definiert durch

strengefx = wenn x ≠ ⊥ dann fx sonst ⊥.

Operativ strengefx wird durch zuerst reduziert x schwachen Kopf Normalform (WHNF) reduziert und dann Reduzieren der Anwendung fx. Alternativ ist es sicher x und fx parallel zu reduzieren, aber keinen Zugriff auf das Ergebnis erlauben, bis x ist in WHNF.

---

In dem Papier haben wir noch die Verwendung des Symbols aus den beiden senkrechten Linien (nicht sicher, was es heißt), um zu sehen, so dass es Art kommt aus dem Nichts heraus.

Vorausgesetzt, dass Wadler weiter zu sagen, dass "wir [strenge] Verständnis verwenden, um die Bewertung von faulen Programmen zu kontrollieren", scheint es ein ziemlich wichtiges Konzept zu verstehen.

Answer 1

Das von Ihnen beschriebene Symbol ist "unten". Es kommt aus der Ordnungstheorie (insbesondere Gittertheorie). Das "unterste" Element einer teilweise geordneten Menge ist, wenn eines existiert, dasjenige, das allen anderen vorangeht. In der Semantik der Programmiersprache bezieht es sich auf einen Wert, der "weniger definiert" ist als jeder andere. Es ist üblich, den "unteren" Wert jeder Berechnung zuzuordnen, die entweder einen Fehler erzeugt oder nicht beendet werden kann, weil der Versuch, diese Bedingungen zu unterscheiden, die Mathematik stark schwächt und die Programmanalyse erschwert.

Um die Dinge in eine andere Antwort einzubinden, ist der logische "falsche" Wert das untere Element eines Gitters von Wahrheitswerten, und "wahr" ist das oberste Element. In der klassischen Logik sind dies die einzigen beiden, aber man kann auch Logiken mit unendlich vielen Wahrhaftigkeitswerten betrachten, wie Intuitionismus und verschiedene Formen des Konstruktivismus. Diese nehmen die Begriffe in eine andere Richtung.

Answer 2

In Standard Boolesche Logik, das Symbol ⊥, lesen falsum oder Boden, ist einfach eine Aussage, die immer falsch ist, das Äquivalent der false Konstante in Programmiersprachen. Das Formular ist eine umgekehrte (umgekehrte) Version des Symbols ⊤ (Verum oder oben), das entspricht true - und es gibt mnemonische Wert in der Tatsache, dass das Symbol wie ein Großbuchstabe T aussieht. Die Namen verum und falsum sind lateinisch für "wahr" und "falsch"; die Namen "oben" und "unten" stammen aus der Verwendung der Symbole in der Theorie der geordneten Mengen, wo sie auf der Grundlage der Position der horizontalen Kreuzschiene.)

In der Berechenbarkeitstheorie ist ⊥ auch der Wert einer unberechenbaren Berechnung, so dass Sie es auch als den undefinierten Wert vorstellen können. Es spielt keine Rolle, warum die Berechnung unberechenbar ist - sei es, weil sie nicht definierte Eingaben hat oder niemals endet oder was auch immer. Ihr Snippet ist eine Formalisierung dieses ersten Grundes: es definiert strikt als eine Funktion, die jede Berechnung (eine andere Funktion) undefiniert macht, wenn ihre Eingaben (Argumente) undefiniert sind.