Domänentheorie - Domain theory

Die Domänentheorie ist ein Zweig der Mathematik , der spezielle Arten von teilweise geordneten Mengen (Posets) untersucht, die üblicherweise als Domänen bezeichnet werden . Folglich kann die Domänentheorie als Zweig der Ordnungstheorie betrachtet werden . Das Gebiet hat Hauptanwendungen in der Informatik , wo es zur Spezifizierung der Denotationssemantik verwendet wird , insbesondere für funktionale Programmiersprachen . Die Domänentheorie formalisiert die intuitiven Ideen der Approximation und Konvergenz auf sehr allgemeine Weise und ist eng mit der Topologie verbunden .

Motivation und Intuition

Die Hauptmotivation für das Studium von Domänen, das Ende der 1960er Jahre von Dana Scott initiiert wurde , war die Suche nach einer denotationalen Semantik des Lambda-Kalküls . In diesem Formalismus betrachtet man "Funktionen", die durch bestimmte Begriffe in der Sprache spezifiziert sind. Rein syntaktisch kann man von einfachen Funktionen zu Funktionen wechseln, die andere Funktionen als Eingabeargumente verwenden. Wenn man wieder nur die syntaktischen Transformationen verwendet, die in diesem Formalismus verfügbar sind, kann man sogenannte Festkomma-Kombinatoren erhalten (der bekannteste davon ist der Y-Kombinator ); diese haben per Definition die Eigenschaft, dass f ( Y ( f )) = Y ( f ) für alle Funktionen f .

Um eine solche Denotationssemantik zu formulieren, könnte man zunächst versuchen, ein Modell für den Lambda-Kalkül zu konstruieren , in dem jedem Lambda-Term eine echte (Gesamt-) Funktion zugeordnet ist. Ein solches Modell würde eine Verbindung zwischen dem Lambda-Kalkül als rein syntaktischem System und dem Lambda-Kalkül als Notationssystem zur Manipulation konkreter mathematischer Funktionen formalisieren. Die Kombinatorrechnung ist ein solches Modell. Die Elemente der Kombinatorrechnung sind jedoch Funktionen von Funktionen zu Funktionen; Damit die Elemente eines Modells der Lambda-Rechnung eine beliebige Domäne und einen beliebigen Bereich haben, können sie keine wahren Funktionen sein, sondern nur Teilfunktionen .

Scott hat diese Schwierigkeit umgangen, indem er den Begriff "partielle" oder "unvollständige" Informationen formalisiert hat, um Berechnungen darzustellen, die noch kein Ergebnis geliefert haben. Dies wurde modelliert, indem für jede Berechnungsdomäne (z. B. die natürlichen Zahlen) ein zusätzliches Element berücksichtigt wurde, das eine undefinierte Ausgabe darstellt, dh das "Ergebnis" einer Berechnung, die niemals endet. Zusätzlich ist der Berechnungsbereich mit einer Ordnungsbeziehung ausgestattet , in der das "undefinierte Ergebnis" das kleinste Element ist .

Der wichtige Schritt, um ein Modell für die Lambda-Rechnung zu finden, besteht darin, nur die Funktionen (auf einer solchen teilweise geordneten Menge) zu berücksichtigen, bei denen garantiert die geringsten Fixpunkte vorliegen . Die Menge dieser Funktionen ist zusammen mit einer entsprechenden Reihenfolge wieder eine "Domäne" im Sinne der Theorie. Die Beschränkung auf eine Teilmenge aller verfügbaren Funktionen hat jedoch einen weiteren großen Vorteil: Es ist möglich, Domänen zu erhalten, die ihre eigenen Funktionsräume enthalten , dh Funktionen, die auf sich selbst angewendet werden können.

Neben diesen wünschenswerten Eigenschaften ermöglicht die Domänentheorie auch eine ansprechende intuitive Interpretation. Wie oben erwähnt, sind die Berechnungsbereiche immer teilweise geordnet. Diese Reihenfolge repräsentiert eine Hierarchie von Informationen oder Wissen. Je höher ein Element in der Reihenfolge ist, desto spezifischer ist es und desto mehr Informationen enthält es. Niedrigere Elemente stehen für unvollständiges Wissen oder Zwischenergebnisse.

Die Berechnung wird dann modelliert, indem monotone Funktionen wiederholt auf Elemente der Domäne angewendet werden, um ein Ergebnis zu verfeinern. Das Erreichen eines festen Punktes entspricht dem Beenden einer Berechnung. Domänen bieten eine überlegene Einstellung für diese Ideen, da das Vorhandensein von Fixpunkten monotoner Funktionen garantiert und unter zusätzlichen Einschränkungen von unten angenähert werden kann.

Ein Leitfaden zu den formalen Definitionen

In diesem Abschnitt werden die zentralen Konzepte und Definitionen der Domänentheorie vorgestellt. Die obige Intuition von Domänen als Informationsreihenfolge wird hervorgehoben, um die mathematische Formalisierung der Theorie zu motivieren. Die genauen formalen Definitionen finden Sie in den entsprechenden Artikeln zu jedem Konzept. Eine Liste allgemeiner ordnungstheoretischer Definitionen, die auch domänentheoretische Begriffe enthalten, finden Sie im Glossar der Ordnungstheorie . Die wichtigsten Konzepte der Domänentheorie werden dennoch im Folgenden vorgestellt.

Gerichtete Sätze als konvergierende Spezifikationen

Wie bereits erwähnt, befasst sich die Domänentheorie mit teilweise geordneten Mengen , um eine Berechnungsdomäne zu modellieren. Ziel ist es, die Elemente einer solchen Reihenfolge als Informationen oder (Teil-) Ergebnisse einer Berechnung zu interpretieren , wobei Elemente, die in der Reihenfolge höher sind, die Informationen der darunter liegenden Elemente auf konsistente Weise erweitern. Aus dieser einfachen Intuition geht bereits hervor, dass Domänen häufig nicht das größte Element haben , da dies bedeuten würde, dass es ein Element gibt, das die Informationen aller anderen Elemente enthält - eine eher uninteressante Situation.

Ein Konzept, das in der Theorie eine wichtige Rolle spielt, ist das einer gerichteten Teilmenge einer Domäne; Eine gerichtete Teilmenge ist eine nicht leere Teilmenge in der Reihenfolge, in der zwei beliebige Elemente eine Obergrenze haben, die ein Element dieser Teilmenge ist. In Anbetracht unserer Intuition über Domänen bedeutet dies, dass zwei beliebige Informationen innerhalb der gerichteten Teilmenge konsistent um ein anderes Element in der Teilmenge erweitert werden. Daher können wir gerichtete Teilmengen als konsistente Spezifikationen betrachten , dh als Mengen von Teilergebnissen, in denen keine zwei Elemente widersprüchlich sind. Diese Interpretation kann mit dem Begriff einer konvergenten Sequenz in der Analyse verglichen werden , bei der jedes Element spezifischer ist als das vorhergehende. In der Theorie der metrischen Räume spielen Sequenzen in vielerlei Hinsicht eine Rolle, die der Rolle gerichteter Mengen in der Domänentheorie entspricht.

Nun, wie im Fall von Sequenzen, interessieren wir uns für die Grenze einer gerichteten Menge. Nach dem, was oben gesagt wurde, wäre dies ein Element, das die allgemeinste Information ist, die die Information aller Elemente der gerichteten Menge erweitert, dh das eindeutige Element, das genau die Information enthält , die in der gerichteten Menge vorhanden war, und nichts mehr. Bei der Formalisierung der Ordnungstheorie ist dies nur die kleinste Obergrenze der gerichteten Menge. Wie bei Sequenzgrenzen existieren nicht immer die kleinsten Obergrenzen gerichteter Mengen.

Natürlich hat man ein besonderes Interesse an solchen Berechnungsbereichen, in denen alle konsistenten Spezifikationen konvergieren , dh in Reihenfolgen, in denen alle gerichteten Mengen eine kleinste Obergrenze haben. Diese Eigenschaft definiert die Klasse der gerichteten vollständigen Teilaufträge , kurz dcpo . In der Tat berücksichtigen die meisten Überlegungen der Domänentheorie nur Ordnungen, die zumindest vollständig gerichtet sind.

Aus der zugrunde liegenden Idee, dass teilweise spezifizierte Ergebnisse unvollständiges Wissen darstellen, leitet man eine andere wünschenswerte Eigenschaft ab: die Existenz eines kleinsten Elements . Ein solches Element modelliert diesen Zustand ohne Informationen - den Ort, an dem die meisten Berechnungen beginnen. Es kann auch als Ausgabe einer Berechnung angesehen werden, die überhaupt kein Ergebnis zurückgibt.

Berechnungen und Domänen

Nachdem wir nun einige grundlegende formale Beschreibungen darüber haben, was eine Berechnungsdomäne sein sollte, können wir uns den Berechnungen selbst zuwenden. Es ist klar, dass dies Funktionen sein müssen, die Eingaben aus einer Berechnungsdomäne übernehmen und Ausgaben in einer (möglicherweise anderen) Domäne zurückgeben. Man würde jedoch auch erwarten, dass die Ausgabe einer Funktion mehr Informationen enthält, wenn der Informationsgehalt der Eingabe erhöht wird. Formal bedeutet dies, dass eine Funktion monoton sein soll .

Wenn es um dcpos geht , möchte man vielleicht auch, dass Berechnungen mit der Bildung von Grenzen einer gerichteten Menge kompatibel sind. Formal bedeutet dies, dass für eine Funktion f das Bild f ( D ) einer gerichteten Menge D (dh die Menge der Bilder jedes Elements von D ) erneut gerichtet ist und als kleinste Obergrenze das Bild der geringsten hat Obergrenze D . Man könnte auch sagen, dass f das gerichtete Suprema bewahrt . Beachten Sie auch, dass eine solche Funktion unter Berücksichtigung gerichteter Mengen von zwei Elementen auch monoton sein muss. Diese Eigenschaften lassen den Gedanken einer Scott-kontinuierlichen Funktion entstehen. Da dies oft nicht mehrdeutig ist, kann man auch von stetigen Funktionen sprechen .

Annäherung und Endlichkeit

Die Domänentheorie ist ein rein qualitativer Ansatz zur Modellierung der Struktur von Informationszuständen. Man kann sagen, dass etwas mehr Informationen enthält, aber die Menge der zusätzlichen Informationen ist nicht angegeben. Es gibt jedoch Situationen, in denen man über Elemente sprechen möchte, die in gewissem Sinne viel einfacher (oder viel unvollständiger) sind als ein bestimmter Informationszustand. Beispielsweise ist in der natürlichen Reihenfolge der Einbeziehung von Teilmengen auf einem Powerset jedes unendliche Element (dh jede Menge) viel "informativer" als jede seiner endlichen Teilmengen.

Wenn man eine solche Beziehung modellieren möchte, kann man zuerst die induzierte strenge Ordnung <einer Domäne mit der Ordnung ≤ betrachten. Dies ist zwar ein nützlicher Begriff bei Gesamtbestellungen, sagt jedoch bei teilweise bestellten Sätzen nicht viel aus. Unter erneuter Berücksichtigung der Einschlussreihenfolge von Mengen ist eine Menge bereits streng kleiner als eine andere, möglicherweise unendliche Menge, wenn sie nur ein Element weniger enthält. Man würde jedoch kaum zustimmen, dass dies den Begriff "viel einfacher" erfasst.

Weit unter der Beziehung

Ein ausgefeilterer Ansatz führt zur Definition der sogenannten Approximationsordnung , die suggestiver auch als " Way-Below" -Relation bezeichnet wird . Ein Element x liegt weit unter einem Element y , wenn für jede gerichtete Menge D mit Supremum so, dass

,

es gibt ein Element d in D, so dass

.

Dann sagt man auch , dass x annähert y und schreibt

.

Dies impliziert das

,

da die Singleton-Menge { y } gerichtet ist. Zum Beispiel liegt bei einer Reihenfolge von Mengen eine unendliche Menge weit über einer ihrer endlichen Teilmengen. Betrachten Sie andererseits die gerichtete Menge (tatsächlich die Kette ) endlicher Mengen

Da das Supremum dieser Kette die Menge aller natürlichen Zahlen N ist , zeigt dies, dass keine unendliche Menge weit unter N liegt .

Weit unter einem Element zu sein, ist jedoch ein relativer Begriff und sagt nicht viel über ein Element allein aus. Zum Beispiel möchte man endliche Mengen ordnungstheoretisch charakterisieren, aber selbst unendliche Mengen können weit unter einer anderen Menge liegen. Die besondere Eigenschaft dieser finiten Elemente x ist, dass sie weit unter sich liegen, dh

.

Ein Element mit dieser Eigenschaft wird auch als kompakt bezeichnet . Solche Elemente müssen jedoch in keiner anderen mathematischen Verwendung der Begriffe "endlich" oder "kompakt" sein. Die Notation ist jedoch durch bestimmte Parallelen zu den jeweiligen Begriffen in Mengenlehre und Topologie motiviert . Die kompakten Elemente einer Domäne haben die wichtige besondere Eigenschaft, dass sie nicht als Grenze einer gerichteten Menge erhalten werden können, in der sie nicht bereits aufgetreten sind.

Viele andere wichtige Ergebnisse in Bezug auf die unten stehende Beziehung stützen die Behauptung, dass diese Definition geeignet ist, viele wichtige Aspekte einer Domäne zu erfassen.

Grundlagen von Domains

Die vorherigen Gedanken werfen eine andere Frage auf: Ist es möglich zu garantieren, dass alle Elemente einer Domäne als Grenze für viel einfachere Elemente erhalten werden können? Dies ist in der Praxis sehr relevant, da wir keine unendlichen Objekte berechnen können, aber dennoch hoffen können, sie willkürlich genau zu approximieren.

Generell möchten wir uns auf eine bestimmte Teilmenge von Elementen beschränken, die ausreicht, um alle anderen Elemente als Mindestobergrenzen zu erhalten. Daher definiert man eine Basis eines Posets P als eine Teilmenge B von P , so dass für jedes x in P die Menge von Elementen in B , die weit unter x liegen, eine gerichtete Menge mit dem höchsten x enthält . Der Poset P ist ein kontinuierlicher Poset, wenn er eine Basis hat. Insbesondere ist P selbst eine Basis in dieser Situation. In vielen Anwendungen beschränkt man sich auf kontinuierliche (d) cpos als Hauptstudienobjekt.

Schließlich wird eine noch stärkere Beschränkung einer teilweise geordneten Menge gegeben, indem die Existenz einer Basis von finiten Elementen vorausgesetzt wird . Ein solcher Poset heißt algebraisch . Unter dem Gesichtspunkt der Denotationssemantik verhalten sich algebraische Posets besonders gut, da sie die Annäherung aller Elemente ermöglichen, auch wenn sie auf endliche beschränkt sind. Wie bereits erwähnt, ist nicht jedes finite Element im klassischen Sinne "endlich", und es kann durchaus sein, dass die finiten Elemente eine unzählige Menge bilden.

In einigen Fällen ist jedoch die Basis für einen Poset zählbar . In diesem Fall spricht man von einem ω-kontinuierlichen Poset. Wenn dementsprechend die zählbare Basis vollständig aus finiten Elementen besteht, erhalten wir eine Ordnung, die ω-algebraisch ist .

Spezielle Arten von Domains

Ein einfacher Sonderfall einer Domäne wird als elementare oder flache Domäne bezeichnet . Dies besteht aus einer Reihe unvergleichlicher Elemente, wie z. B. den ganzen Zahlen, sowie einem einzelnen "unteren" Element, das als kleiner als alle anderen Elemente angesehen wird.

Man kann eine Reihe anderer interessanter spezieller Klassen geordneter Strukturen erhalten, die als "Domänen" geeignet sein könnten. Wir haben bereits kontinuierliche und algebraische Posets erwähnt. Speziellere Versionen von beiden sind kontinuierliche und algebraische cpos . Wenn man noch weitere Vollständigkeitseigenschaften hinzufügt , erhält man kontinuierliche Gitter und algebraische Gitter , die nur vollständige Gitter mit den jeweiligen Eigenschaften sind. Für den algebraischen Fall findet man breitere Klassen von Posets, die es noch wert sind, untersucht zu werden: Historisch gesehen waren die Scott-Domänen die ersten Strukturen, die in der Domänentheorie untersucht wurden. Noch breitere Klassen von Domänen bestehen aus SFP-Domänen , L-Domänen und Bifinit-Domänen .

Alle diese Ordnungsklassen können in verschiedene Kategorien von DCpos eingeteilt werden, wobei Funktionen verwendet werden, die monoton, Scott-kontinuierlich oder als Morphismen noch spezialisierter sind . Schließlich ist zu beachten, dass der Begriff Domäne selbst nicht genau ist und daher nur dann als Abkürzung verwendet wird, wenn zuvor eine formale Definition gegeben wurde oder wenn die Details irrelevant sind.

Wichtige Ergebnisse

Ein Poset D ist genau dann ein DCPO, wenn jede Kette in D ein Supremum hat. (Die Wenn-Richtung hängt vom Axiom der Wahl ab .)

Wenn f eine stetige Funktion in einer Domäne D ist, hat es einen kleinsten Fixpunkt, der als kleinste Obergrenze aller endlichen Iterationen von f auf dem kleinsten Element ⊥ angegeben wird:

.

Dies ist der Kleene-Fixpunktsatz . Das Symbol ist die gerichtete Verknüpfung .

Verallgemeinerungen

  • "Synthetische Domänentheorie". CiteSeerX   10.1.1.55.903 . Zitierjournal benötigt |journal= ( Hilfe )
  • Topologische Domänentheorie
  • Ein Kontinuitätsraum ist eine Verallgemeinerung von metrischen Räumen und Posets , mit der die Begriffe von metrischen Räumen und Domänen vereinheitlicht werden können.

Siehe auch

Weiterführende Literatur

Externe Links