Die Snack-Potenzkonstruktion: Grundlage einer Semantik genesteter Datenbanken

Vom Fachbereich Mathematik der Technischen Hochschule Darmstadt

zur Erlangung des akademischen Grades eines

Doktors der Naturwissenschaften (Dr. rer. nat.) genehmigte Dissertation

von

Hermann Puhlmann

aus Frankfurt am Main

Referent: Priv. Doz. Dr. A. Jung 1. Korreferent: Prof. Dr. K. Keimel 2. Korreferent: Prof. Dr. J. Adámek Tag der Einreichung: 26. April 1995 Tag der mündlichen Prüfung: 14. Juli 1995

Darmstadt 1995 D 17

Inhaltsverzeichnis

Einleitung 3

1 Grundlagen 7 1.1 Einige mathematische Grundbegriffe . . . . . . . . . . . . . . . . . . 7 1.2 Das bereichstheoretische Datenbankmodell . . . . . . . . . . . . . . . 8

2 Die Snack-Potenzkonstruktion 13 2.1 Potenzbereiche . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.2 Der Snack-Potenzbereich . . . . . . . . . . . . . . . . . . . . . . . . . 19

2.2.1 Snacks und Ordnung . . . . . . . . . . . . . . . . . . . . . . . 19 2.2.2 Operationen auf Snacks . . . . . . . . . . . . . . . . . . . . . 26 2.2.3 Die Snackalgebra . . . . . . . . . . . . . . . . . . . . . . . . . 28

2.3 Das Snack-Potenzlokal . . . . . . . . . . . . . . . . . . . . . . . . . . 35

3 Ein Typsystem für Datenbanken 47 3.1 Unterstrukturen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 3.2 Typen und ihre Interpretation . . . . . . . . . . . . . . . . . . . . . . 56 3.3 Subtypen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60

4 Übergänge zwischen genesteten Relationen 65 4.1 Nesten und Entnesten genesteter Relationen . . . . . . . . . . . . . . 66 4.2 Nesten und Entnesten für Bereichsdatenbanken . . . . . . . . . . . . 68

4.2.1 Die Funktion Nest . . . . . . . . . . . . . . . . . . . . . . . . 70 4.2.2 Die Funktion Unnest . . . . . . . . . . . . . . . . . . . . . . . 73 4.2.3 Das Einbettungs-Projektionspaar . . . . . . . . . . . . . . . . 75

A Semifaktoren im Snack-Potenzbereich 79

Literaturverzeichnis 85 2 INHALTSVERZEICHNIS

Einleitung

Möchte man mathematische Strukturen in einem Computer implementieren, so sieht man sich sehr schnell mit den Einschränkungen konfrontiert, die aus der Endlichkeit aller im Computer darstellbarer Objekte erwachsen. Auch wenn der Datentyp real in höheren Programmiersprachen suggeriert, man könne im Computer mit reellen Zahlen rechnen, so steht tatsächlich doch nur eine endliche Menge rationaler Zahlen zur Verfügung, so daß man sich mit Approximationen reeller Zahlen begnügen muß. Auch wenn die Approximationen durch rationale Zahlen gegeben sind, so können wir sie uns als Intervalle denken, in denen die approximierten reellen Zahlen liegen, indem wir z. B. jede rationale Zahl als das Intervall zwischen dieser und der nächstgrößeren im Rechner darstellbaren rationalen Zahl lesen. Durch eine Erhöhung der Stellenzahl, mit der gerechnet wird, lassen sich diese Intervalle jedoch verkleinern, also die Approximationen verbessern; ja, es läßt sich im Prinzip jede gewünschte Genauigkeit durch endliche Approximationen erreichen.

Der Gedanke der Approximation durch endliche Darstellungen wird durch die Theorie der Bereiche (algebraischen dcpo’s, algebraischen gerichtet-vollständigen geordneten Mengen) in einen mathematischen Rahmen gestellt, der auch anderen Datentypen gerecht wird. Die Idee ist dabei, daß die Approximationen der Elemente der zu implementierenden Struktur eine geordnete Menge bilden, deren maximale Elemente die Elemente der Struktur selbst sind (oder zu diesen eineindeutig in Beziehung stehen). Jedes maximale Element ist darin das Supremum seiner Approximationen. Wir gehen hier nicht auf die weiteren Eigenschaften der Bereiche ein und auch nicht darauf, weshalb sie den Approximationsgedanken gut modellieren. Hierfür sei auf die Literatur, insbesondere [Sco70, Sco81, Sco82, Plo81] verwiesen.

Statt dessen lenken wir unser Augenmerk nun auf die Darstellung von Mengen im Rechner, wobei es stets um Mengen von Objekten eines gemeinsamen Typs gehen soll. Programmiersprachen wie Pascal stellen hierfür zwar einen Typkonstruktor set of zur Verfügung. Dadurch sind jedoch nur Teilmengen kleiner endlicher Mengen darstellbar. Durch die Verwendung von Listen anstelle der set-Typen kann man zwar größere Mengen darstellen (wobei man selbst eventuelle Duplikate aus den Listen entfernen muß), bleibt aber an die Endlichkeit gebunden. Zur Darstellung unendlicher Mengen oder sehr großer endlicher Mengen bleibt man wie im Falle der reellen Zahlen auf Approximationen angewiesen. Genauso wird man selbst eine kleine endliche Menge nur approximativ angeben können, wenn für ihre Elemente nur Approximationen vorliegen. Nun stellt sich die Frage, wie man geeignete Approximationen von Mengen findet, deren Elemente möglicherweise nur approximativ, d. h. partiell beschrieben sind. Für die Bereichstheorie bedeutet dies, daß eine Konstruktion zu finden ist, die einen (Grund-)Bereich in einen sogenannten Potenzbereich überführt, dessen Elemente Approximationen von Teilmengen der Menge der maximalen Elemente des Grundbereichs sind.

Vor dem Hintergrund der Verallgemeinerung relationaler Datenbanken durch Bereiche [BJO91] hat Buneman hierzu den Snack-Potenzbereich vorgeschlagen. Gegenstand dieser Arbeit ist die Untersuchung dieser Snack-Konstruktion und ihrer Anwendbarkeit zur Modellierung von Datenbanken.

Dazu gehen wir folgendermaßen vor:

In Kapitel 1 klären wir zunächst die Verwendung einiger mathematischer Begriffe. Insbesondere sei darauf hingewiesen, daß unter einem Bereich stets eine algebraische dcpo mit kleinstem Element verstanden werden soll, in der jede nach oben beschränkte Menge ein Supremum hat. Solche Bereiche sind aus der Literatur auch als Scott-Bereiche bekannt. Buneman et al. verwenden diese Klasse von Bereichen für die angesprochene Verallgemeinerung relationaler Datenbanken. Im zweiten Abschnitt des ersten Kapitels erläutern wir kurz die zugrundeliegende Idee.

Die Snack-Potenzkonstruktion ist das Hauptthema von Kapitel 2. Im ersten Abschnitt stellen wir informell die anderen bisher bekannten Potenzbereiche vor. Wir zeigen, welche Nachteile sie bei der Modellierung mengenwertiger Typen haben, und geben im zweiten Abschnitt den Snack-Potenzbereich an, der die geschilderten Probleme überwindet. Für die Verwendung in Bunemans bereichstheoretischem Datenbankmodell scheint er deshalb besonders gut geeignet, weil sich mit ihm eine reiche Auswahl von Mengen des Grundtyps approximieren läßt und die verwendete Klasse von Bereichen unter der Konstruktion abgeschlossen ist. Wir präzisieren dies im Verlauf von Kapitel 2.2, ehe wir die Charakterisierung des Snack-Potenzbereichs als freien Bi-Halbverband angeben, die wir auch in [Puh93] schon formulierten. Im dritten Abschnitt wenden wir uns einer alternativen Beschreibung der Snack-Konstruktion zu. Wir nutzen die Stone-Dualität zwischen Bereichen und Scott-Prälokalen aus (vgl. hierzu [Abr91b, AJ95, Vic89, Joh82, GHK^{+}80]) und geben mit dem Snack-Potenzlokal die lokalische Beschreibung des Snack-Potenzbereichs an. Diese können wir als eine Logik verstehen, die über Eigenschaften der Elemente des Bereichs spricht, so daß wir im weiteren wahlweise direkt mit den Elementen oder mit ihren Eigenschaften argumentieren können.

Mit der Snack-Potenzkonstruktion ist eine Darstellung für approximativ gegebene Mengen gefunden. Eine Datenbank ist jedoch recht nutzlos, wenn in ihr Daten nur gespeichert und nicht verarbeitet werden können. Zur Verarbeitung bieten relationale Datenbanken die Operationen der Relationenalgebra, die für das bereichstheoretische Datenbankmodell geeignet zu verallgemeinern sind. Eine erste Anforderung hierbei ist, daß man Einschränkungen von Datenobjekten bezüglich einer in ihnen enthaltenen Teilinformation betrachten kann. Für die Interpretation der Datenobjekte durch Bereiche oder Prälokale bedeutet dies, daß in ihnen Unterstrukturen zu definieren sind, deren Elemente den Objekten entsprechen, in denen nur diese Teilinformation gegeben ist. Hierzu führen wir im Kapitel 3 starke Unterbereiche und starke Subprälokale ein und zeigen, daß dies äquivalente Begriffe für die bereichstheoretische und die lokalische Betrachtungsweise sind. Anschließend wenden wir in Kapitel 3.2 die zuvor entwickelten Strukturen zur Interpretation eines konkreten Typsystems für Datenbanken an. Das Typsystem umfaßt verschiedene in Programmiersprachen übliche Typkonstruktoren, deren lokalische Interpretation Abramsky [Abr91b] angegeben hat. Wir fügen einen Mengenkonstruktor hinzu, der durch die Snack-Potenzkonstruktion interpretiert wird. Zur Formalisierung des Aspekts der Teilinformation definieren wir eine Subtyprelation, die durch starke Unterbereiche bzw. starke Subprälokale interpretiert wird. Hierzu weisen wir nach, daß die Konstruktionen auf Bereichen und Prälokalen, die zu den Typkonstruktoren korrespondieren, die Unterstrukturen bewahren. Die Ergebnisse dieses Kapitels haben wir teilweise auch in [JP95] vorgestellt.

Durch das in Kapitel 3 gegebene Typsystem werden nicht nur relationale Datenbanken verallgemeinert; die Typen umfassen auch die sogenannten genesteten Relationen, die in den 80er Jahren im Darmstädter Datenbanksystem [SS86, Sch88] implementiert wurden. Gegenüber dem klassischen Relationenmodell unterscheiden sich genestete Relationen im wesentlichen dadurch, daß Elemente von Relationen selbst wieder Relationen enthalten dürfen. Zum Übergang zwischen Relationen verschiedener Schachtelungstiefe kommen zur klassischen Relationenalgebra nun die Operationen Nest und Unnest [JS82] hinzu. Daß diese keine befriedigende Semantik haben, konnten wir in [Puh91] zeigen. Hier zeigt sich nun die Stärke des bereichstheoretischen Ansatzes. Für unser Typsystem, in dem Relationen im Snack-Potenzbereich interpretiert werden, gelingt nämlich in Kapitel 4.2 die Definition eines Nestungsund Entnestungsoperators, die zusammen ein Einbettungs-Projektionspaar bilden. Wir können sie damit als die bestmögliche Verbindung zwischen genesteten Relationen verschiedener Schachtelungstiefe verstehen, und zwar in dem Sinne, daß beim Übergang durch Nest keine Information verlorengeht und beim Übergang durch Unnest nur der Informationsgehalt aufzugeben ist, der auf der reicheren Struktur des genesteten Ausgangsbereichs beruht.

Schließlich geben wir im Anhang noch den Beweis eines Ergebnisses aus Kapitel 3, mit dem wir zeigen, daß die gegenüber unseren starken Unterbereichen restriktivere Unterstruktur des Semi-Faktors, die von Buneman [BJO91] eingeführt wurde, nicht für die Modellierung der Subtyprelation geeignet ist, wenn im Typsystem ein Mengenkonstruktor vorgesehen ist, der durch den Snack-Potenzbereich interpretiert wird.

An dieser Stelle möchte ich mich bei all jenen bedanken, die mich während der Arbeit an dieser Dissertation unterstützt haben. Hierzu zählen die Mitglieder der Darmstädter AG Domains, inbesondere Dr. Andrea Schalk und Dr. Philipp Sünderhauf, die sich während der letzten Jahre immer wieder mit mir in die Snack-Konstruktion hineingedacht haben und mir wertvolle Ratschläge geben konnten. Dr. Michael Tischendorf, Dr. Gerhard-Wilhelm Weber, Anatoli Reibold und Steffi Keller, die auch einen Teil des Manuskripts abtippte, waren mir beim Korrekturlesen behilflich.

Professor Dr. Klaus Keimel war stets eine gute Anlaufstelle zur Klärung mathematischer Fragen; er und Professor Dr. Jiří Adámek unterzogen sich der mühsamen Aufgabe der Korreferenten.

Mein besonderer Dank indessen gilt Dr. Achim Jung für die Betreuung dieser Arbeit. Er führte mich in die Idee ein, die Bereichstheorie zur Modellierung von Datenbanken zu verwenden, und begleitete meine Schritte durch richtungsweisende Fragestellungen sowie intensive Diskussion einzelner Ergebnisse. Ich wünsche ihm noch zahlreiche Doktoranden.

Kapitel 1

Grundlagen

1.1 Einige mathematische Grundbegriffe

Es würde den Rahmen dieser Arbeit sprengen, eine Einführung in die Theorie der Bereiche zu geben. Als Quelle für die mathematischen Grundlagen dieser Arbeit seien daher [GHK^{+}80] und [AJ95] genannt. An dieser Stelle sei lediglich auf einige sprachliche Konventionen und elementare Ergebnisse hingewiesen, die im folgenden verwendet werden.

Unter einer unteren Menge A in einer geordneten Menge D verstehen wir eine Menge A ⊆ D, für die ((a ∈ A und a′ ≤ a) ⇒ a′ ∈ A) gilt. Dual hierzu ist der Begriff obere Menge definiert.

Eine Funktion f: D → E zwischen geordneten Mengen heißt monoton oder ordnungserhaltend, falls aus x ≤ x′ (in D) die Beziehung f(x) ≤ f(x′) folgt. Ist x ≤ x′ für alle x, x′ ∈ D mit f(x) ≤ f(x′), so heißt die Funktion ordnungsreflektierend.

Die Worte gerichtet und beschränkt verwenden wir im Sinne von ”nach oben gerichtet“ und ”nach oben beschränkt“.

Unter einer dcpo verstehen wir eine geordnete Menge mit einem kleinsten Element, in der jede gerichtete Teilmenge ein Supremum hat. Die Menge der kompakten Elemente einer dcpo D bezeichnen wir mit KD. Ist für jedes x ∈ D die Menge KD∩↓x gerichtet und hat x als Supremum, so heißt die dcpo algebraisch. Eine algebraische dcpo, in der jede beschränkte Teilmenge ein Supremum hat, nennen wir Bereich. Bereiche sind aus der Literatur auch unter den Namen Scott-Bereich oder Scott-domain bekannt.

Unter kompakten Teilmengen eines Bereichs verstehen wir solche Teilmengen, die die Heine-Borel-Überdeckungseigenschaft bezüglich der Scott-Topologie auf dem Bereich erfüllen. Das Hausdorffsche Trennungsaxiom setzen wir nicht voraus.

Schließlich sei noch angemerkt, daß die kompakt-offenen Teilmengen eines Bereichs genau diejenigen oberen Mengen sind, die von endlich vielen kompakten Elementen des Bereichs erzeugt werden. Darüber hinaus gilt (vgl. [BJO91]):

Proposition 1.1.1 Seien F und F′ endliche Mengen kompakter Elemente eines Bereichs. Der Schnitt der kompakt-offenen Mengen ↑F und ↑F′ ist kompakt-offen, und es gilt

↑F ∩ ↑F′ = {x ∨ y | x ∈ F, y ∈ F′, {x, y} beschränkt} .

1.2 Das bereichstheoretische Datenbankmodell

In [BJO91] schlagen Buneman, Jung und Ohori eine Verallgemeinerung des relationalen Datenbankmodells durch die Verwendung Scottscher Bereiche vor. In diesem Abschnitt wollen wir die Idee, die diesem bereichstheoretischen Datenbankmodell zugrunde liegt, noch einmal kurz entwickeln.

Im Relationenmodell werden Informationen über Objekte der realen Welt in Tabellenform dargestellt. Dabei ist eine Tabelle letztlich eine (endliche) Teilmenge des direkten Produkts vorgegebener Wertemengen. Deshalb heißen die Tabellen auch Relationen; beide Begriffe werden synonym gebraucht.

Werfen wir zunächst einen Blick auf den Aufbau der Tabellen. Eine Tabelle soll Informationen über eine gewisse Menge von Merkmalen (Attributen) der Objekte enthalten. Für jedes Attribut hat die Tabelle eine Spalte, die mit dem Attributnamen (Spaltennamen) bezeichnet ist und für die es eine Menge zulässiger Werte gibt. Die Menge der Spaltennamen heißt Schema. Für jedes Objekt gibt es in der Tabelle eine Zeile, die in jeder Spalte den Eintrag zum entsprechenden Attribut enthält. Ein Zeileneintrag wird auch Tupel genannt.

Wir wollen die Begriffe anhand der Beispielrelation aus Abbildung 1.1 veranschaulichen. In der Tabelle werden Namen, Adressen (Straße) und Telefonnummern von Personen erfaßt. Das Schema ist die Menge der Spaltennamen ”Name, Straße, Telefon“. Die Menge der zulässigen Werte für ”Name“ und ”Straße“ könnte beispielsweise die Menge aller Zeichenketten, die für ”Telefon“ die Menge aller Ziffernfolgen einer maximalen Länge sein. Eine Zeile (Tupel) enthält dann Namen, Adresse und Telefonnummer einer Person. Der Beispielrelation entnimmt man so etwa, daß Otto Wasserratte in der Seestraße 15 wohnt und die Telefonnummer 61234 hat.

Name  Straße  Telefon
Otto Wasserratte Seestraße 15  61234
Fritz Flitz  Am Sportpark 2  ?

Abbildung 1.1: Eine Beispielrelation

Das Tupel in der zweiten Zeile der Beispielrelation enthält für die Telefonnummer ein Fragezeichen, um zu symbolisieren, daß hierfür kein Eintrag vorliegt. Somit ist dieses Tupel kein Element des Produkts der Wertemengen, die den einzelnen Attributen zugeordnet sind, und die Tabelle ist keine Relation zwischen diesen Mengen. In der Tat verbietet das Relationenmodell in seiner ursprünglichen Formulierung solche nur partiell bestimmten Einträge; will man für ein Objekt ein Tupel anlegen, so muß man für alle vorgesehenen Attribute einen Wert angeben. Daß dies eine starke Einschränkung ist, liegt auf der Hand. Bei Einhaltung dieser Restriktion wäre es nicht möglich gewesen, die vorhandene Information über Fritz Flitz, nämlich die über seinen Wohnort, in der Beispielrelation abzulegen.

Dies führt dazu, die Forderung fallenzulassen, daß Tupel vollständig bestimmt sein müssen. Man erlaubt außer den Einträgen, die eine wirkliche Information darstellen, auch den Eintrag ”keine Information“. Faßt man dies als eine Erweiterung der Wertemengen der Attribute auf, so kann man nach wie vor von Relationen sprechen, denn auch die partiellen Einträge sind nun Elemente eines Produkts von Wertemengen. Durch dieses Vorgehen wird in natürlicher Weise eine Ordnung auf den für ein Attribut zulässigen Werten induziert: Ist M die Menge der Einträge, die eine echte Information bedeuten, und steht das Symbol ⊥ für ”keine Information“, so ist auf M ∪ {⊥} die Informationsordnung ≤ erklärt durch x ≤ y :⇔ x = y oder x = ⊥. Ein Element ist in dieser Ordnung also größer (oder besser) als ein anderes, wenn es mehr Information enthält. Die so geordnete Wertemenge für ein einzelnes Attribut ist ein sogenannter ”flacher Bereich“.

Die Ordnungen auf den einzelnen Wertemengen übertragen sich auf das Produkt der Wertemengen. Damit erhält man eine Ordnung zwischen den Tupeln: Ein Tupel ist besser als (oder genauso gut wie) ein anderes, wenn es in allen Attributen besser (oder genauso gut) ist. Das Produkt flacher Bereiche ist bereits wesentlich stärker strukturiert als die flachen Bereiche, wie Abbildung 1.2 zeigt.

\begin{aligned}& = \\ × \end{aligned}

Abbildung 1.2: Das Produkt des flachen Bereichs der Wahrheitswerte mit sich selbst.

Die Hinzunahme von Elementen partieller Information zu den eigentlichen Wertemengen ist in der Literatur unter dem Stichwort ”Nullwerte“ von zahlreichen Autoren untersucht worden. Eine Zusammenfassung verschiedener Aspekte der Nullwerte findet sich in [Zan84]. Hier findet sich auch die Baumstruktur aus Abbildung 1.3, die für das Attribut ”Telefonnummer“ geeigneter erscheint als ein flacher Bereich, da hiermit auch ausgedrückt werden kann, daß eine Person keinen Telefonanschluß hat.

keine Information Nummer unbekannt 61234  . . . . . . kein Telefonanschluß  Telefon vorhanden, aber

Abbildung 1.3: Ein Wertebereich für das Attribut ”Telefon“

Um verschiedene Aspekte partieller Information zu modellieren, erhält man so bereits für die Wertemengen einzelner Attribute stärker strukturierte Bereiche. Entsprechend reichhaltig wird die Ordnungsstruktur der Produkte, d. h. der Wertemengen für die Tupel.

Der entscheidende Abstraktionsschritt in [BJO91] ist nun, darauf zu verzichten, daß die Tupel Elemente eines Produkts sein müssen. Die Idee ist, daß die Beschreibungen aller möglichen Objekte bezüglich ihres Informationsgehalts geordnet sind, ohne daß die Information notwendigerweise in Portionen unterteilt ist, die zu gewissen Attributen korrespondieren. Buneman et al. verlangen lediglich, daß die Wertemenge für die Elemente einer ”Relation“ die Ordnungsstruktur eines Bereichs hat. Ein ”verallgemeinertes Tupel“ ist damit ein Element eines Bereichs.

Während bei der Diskussion um Nullwerte mit jedem neuen Aspekt der Partialität das Datenbankmodell für neue Typen von Wertemengen zurechtgeschneidert werden muß (was insbesondere eine neue Definition sämtlicher Datenbankoperationen nach sich zieht), ist das Bestreben hier, eine sehr allgemeine Formulierung anzugeben, aus der konkrete Implementierungen durch Spezialisierung hervorgehen. Die zentrale Idee ist die Approximierung idealer Objekte durch partielle Information. Die idealen Objekte modelliert man als maximale Elemente eines Bereichs. Dann stellt ein Element eines Bereichs eine Approximation all jener maximalen (d. h. idealen) Objekte des Bereichs dar, die über ihm liegen. Das Ziel ist es, eine Datenbankabfragesprache zu entwickeln, die bereichstheoretische Begriffe verwendet, ohne unnötig weitere Strukturen vorauszusetzen. Damit hätte man eine allgemeine Methode, partielle Information zu verarbeiten. Die einzige Anforderung wäre, daß die betrachteten Formen der Partialität mit Hilfe von Bereichen ausgedrückt werden können. Konkrete Implementierungen werden natürlich nicht beliebige Bereiche als Wertemengen für Datentypen zulassen. Sie werden vielmehr gewisse Grunddatentypen bereitstellen, aus denen mit Hilfe von Typkonstruktoren weitere Typen erzeugt werden können. So müssen im Rechner nur die Bereiche, denen die Elemente der Grunddatentypen entnommen werden, und die Bereichskonstruktionen, die den Typkonstruktoren entsprechen, implementiert werden. Der Vorteil des Ansatzes von Buneman et al. ist hierbei, daß man nur noch überprüfen muß, ob sich die verwendeten Datentypen und Typkonstruktoren gut in den allgemeinen Rahmen einfügen. Dann liefert die allgemeine Theorie automatisch eine Abfragesprache für den konkreten Fall.

12 KAPITEL 1. GRUNDLAGEN

Die Snack-Potenzkonstruktion

Im vorigen Kapitel wurde der Übergang vom relationalen Datenbankmodell zum bereichstheoretischen dargestellt. An die Stelle unstrukturierter Mengen traten geordnete Mengen, genauer: Bereiche, denen die Einträge zur Beschreibung von Objekten entnommen werden. Damit eröffnet sich die Möglichkeit, partielle Beschreibungen anzugeben. Die Elemente vollständiger Information bezüglich eines Datentyps sind die maximalen Elemente in dem Bereich, der dem Datentyp zugeordnet ist. Jedes Element des Bereichs wird als Approximation all jener maximalen Elemente verstanden, die über ihm liegen.

Greift man den für Datenbanktupel dargestellten Approximationsgedanken auch für die Ebene der Datenbankrelationen auf, so führt dies zur Forderung nach einer Konstruktion, die für jeden Bereich D einen Bereich erzeugt, dessen Elemente Teilmengen von D approximieren. Eine verallgemeinerte Relation wird dann ein Element dieses sogenannten Potenzbereichs sein. Mit einer geeigneten Potenzbereichskonstruktion verliert sich auch der konzeptionelle Unterschied zwischen Tupeln und Relationen. Alle Datenbankobjekte sind nun von gleicher Art, nämlich Elemente eines Bereichs. So können Relationen ihrerseits in weitere Typkonstruktionen eingehen, d. h. es ist möglich, ”Tupel“ zu bilden, die mengenwertige Anteile haben.

Damit verallgemeinert das bereichstheoretische Datenbankmodell dann nicht nur das relationale Modell, sondern auch das Modell der ”genesteten Relationen“ [SS86].

Im ersten Abschnitt dieses Kapitels stellen wir zunächst die bisher bekannten Potenzbereiche vor und zeigen auf, weshalb diese zur Modellierung von Datenbanken im bereichstheoretischen Modell ungeeignet sind. Im zweiten Abschnitt führen wir den auf Buneman zurückgehenden Snack-Potenzbereich ein und charakterisieren ihn als freie Algebra. Schließlich geben wir im dritten Abschnitt eine alternative Beschreibung der Snack-Potenzkonstruktion durch logische Formeln an und zeigen die Dualität dieser Beschreibung zur Darstellung in der Sprache der Bereiche.

2.1 Potenzbereiche zur Modellierung mengenwertiger Datentypen

Von der Definition einer Semantik nichtdeterministischer Programmiersprachen her sind die Hoare-, Smyth- und Plotkin-Potenzbereiche bekannt, die in dieser Reihenfolge auch als unterer, oberer bzw. konvexer Potenzbereich bezeichnet werden [Smy78, Plo76]. Buneman et al. zeigen jedoch in [BDW88] auf, daß diese Konstruktionen den Anforderungen zur Modellierung von Datenbanken nicht gerecht werden. Im Sinne der oben skizzierten Interpretation der Bereiche sollen den maximalen Elementen des Potenzbereichs Teilmengen der Menge der maximalen Elemente des Ausgangsbereichs zugeordnet sein; im allgemeinen sollen die Elemente des Potenzbereichs solche Teilmengen approximieren. Hoare- und Smyth-Potenzbereich eines Bereichs D haben jeweils nur ein einziges maximales Element, nämlich die ganze Menge D bzw. die leere Menge. Selbst ein Ausschluß der leeren Menge aus dem Smyth-Potenzbereich verbessert die Situation kaum. In diesem Fall sind die maximalen Elemente die einelementigen Mengen, welche ein maximales Element von D enthalten. Auf diese Weise lassen sich keine reichhaltigen mengenwertigen Typen approximieren.

Dennoch bilden die Ordnungsrelationen ≤^{♭} des Hoare- und ≤^{♯} des Smyth-Potenz-bereichs die Grundbausteine für alle weiteren Potenzkonstruktionen. Für Teilmengen A und B eines durch ≤ geordneten Bereichs D sind sie folgendermaßen definiert:

A ≤^{♭} B ⟺ ∀a ∈ A ∃b ∈ B. a ≤ b ( ⟺ ↓A ⊆ ↓B) (untere oder

Hoare-Ordnung),

A ≤^{♯} B ⟺ ∀b ∈ B ∃a ∈ A. a ≤ b ( ⟺ ↑A ⊇ ↑B) (obere oder

Smyth-Ordnung).

Genau genommen sind dies nur Präordnungen, da sie nicht notwendig antisymmetrisch sind. Dennoch hat es sich eingebürgert, von Ordnungen zu sprechen, da die oft vorgenommene Einschränkung auf untere Mengen (für ≤^{♭}) bzw. obere Mengen (für ≤^{♯}) oder Antiketten (in beiden Fällen) Antisymmetrie garantiert.

Betrachten wir nun, welche Art der Approximation von Mengen durch die beiden Ordnungen ausgedrückt wird. Wenn jedes Element a eines Bereichs D eine Approximation jedes Elementes b ∈ D_{max} mit a ≤ b ist, so kann man eine Teilmenge A ⊆ D als Approximation jeder solchen Teilmenge B ⊆ D_{max} ansehen, für die A ≤^{♭} B oder A ≤^{♯} B gilt. Für die Interpretation mit der Hoare-Ordnung heißt dies, daß jedes Element von A eine Approximation eines Elementes von B ⊆ D_{max} sein muß. Die Menge B kann jedoch weitere Elemente enthalten, die zu keinem Element von A in Beziehung stehen. Abbildung 2.1 illustriert dies: Die Menge A = {a_{1}, a_{2}, a_{3}} approximiert die Menge B = {b_{1}, …, b_{5}} im Hoare-Sinne. Oberhalb jedes Elements von A ist die Menge der maximalen Elemente, die es approximiert, mit einer doppelten Linie dargestellt. In jeder doppelten Linie liegt (mindestens) ein Element der Menge B. Ferner hat die Menge B mit b_{5} ein Element, das von keinem Element der Menge A approximiert wird.

D a_{1}  a_{2}  a_{3} b_{1}  b_{2}  b_{3}  b_{4} b_{5}

Abbildung 2.1: Approximation im Hoare-Sinne

Genau umgekehrt verhält es sich bei der Interpretation mittels der Smyth-Ord-nung. Hier muß es für jedes Element b der zu approximierenden Menge B ein Element in A geben, welches b approximiert. Die Menge A darf aber durchaus auch Elemente enthalten, welche kein Element von B beschreiben. Dies illustriert Abbildung 2.2, in welcher A = {a_{1}, a_{2}, a_{3}} die Menge B = {b_{1}, b_{2}, b_{3}} im Smyth-Sinne approximiert. Man beachte, daß hier über a_{2} keines der Elemente von B liegt.

Die Smyth-Interpretation beschränkt die möglichen approximierten Mengen also nach oben, die Hoare-Interpretation nach unten. Jede Interpretation für sich ist damit nicht sehr aussagekräftig, eine Kombination der beiden Aspekte ist wünschenswert. Im Plotkin-Potenzbereich wird das dadurch erzielt, daß eine Menge A ⊆ D zugleich als ≤^{♯}- als auch als ≤^{♭}-Approximation betrachtet wird. Das hat jedoch eine unschöne

b_{3} a_{1}  a_{2}  a_{3} b_{1}  D b_{2}

Abbildung 2.2: Approximation im Smyth-Sinne

Sonderrolle der leeren Menge zur Folge: Sie läßt sich mit keiner anderen Menge vergleichen, da sie bezüglich ≤^{♭} minimal und bezüglich ≤^{♯} maximal ist. Insbesondere hat dadurch der Plotkin-Potenzbereich nur dann ein kleinstes Element, wenn man die leere Menge ausschließt. Das ist aber in Hinblick auf die Anwendung in Datenbanken nicht wünschenswert.

Gunters Mixed-Potenzbereich [Gun92] löst dieses Problem und erlaubt bezüglich der beiden Interpretationen mehr Freiheit, indem die Approximationen für ≤^{♯} und ≤^{♭} getrennt angegeben werden. Man gibt also ein Paar (U, L) von Mengen an, deren erste man als ≤^{♯}-Approximation und deren zweite man als ≤^{♭}-Approximation versteht. Die Buchstaben U und L sollen an die englischen Bezeichnungen ”upper“ und ”lower“ für die jeweiligen Ordnungen erinnern. Eine Menge B ⊆ D_{max} wird dann durch einen solchen ”Mix“ (U, L) approximiert, wenn U ≤^{♯} B und L ≤^{♭} B. Das heißt, daß B ⊆ ↑U ∩ D_{max} und ↑l ∩ B ≠ ∅ für jedes l ∈ L gelten muß. Die Elemente von L geben demnach Information über Elemente, die garantiert zu B gehören. Diese müssen innerhalb ↑U liegen, und so fordert Gunter für die Mengen U und L eines Mixes die Konsistenzbedingung L ⊆ ↑U. Die leere Menge wird nun von allen Mixen approximiert, deren L-Komponente leer ist, der Mix (∅, ∅) entspricht genau der leeren Menge, und ({⊥}, ∅) ist das kleinste Element.

Der Plotkin-Potenzbereich hat einen weiteren Nachteil, und dieser wird durch die Mixed-Konstruktion nicht beseitigt: Beide überführen Bereiche im allgemeinen nicht in Bereiche, da zwei beschränkte Elemente kein Supremum haben müssen. Sind für eine Menge B ⊆ D_{max} zwei approximierende Mixe gegeben, so brauchen diese daher nicht zu einer kleinsten gemeinsamen Approximation kombinierbar zu sein. Für Mixe gibt Abbildung 2.3 ein Beispiel an. Der abgebildete Bereich liefert auch ein Beispiel für die Plotkin-Konstruktion. Wieder betrachten wir die Mengen {x, y} und {w, z} aus dem abgebildeten Bereich. Für sie sind {b, c} und {a, d} minimale obere Schranken im Plotkin-Sinne.

a  b  c  d w  x  y  z ⊥  \begin{matrix}(\{x, y\}, \\ \{x, y\}) \end{matrix}  \begin{matrix}(\{w, z\}, \\ \{w, z\}) \end{matrix} \begin{matrix}(\{a, b, c, d\}, \\ \{a, d\}) \end{matrix}  \begin{matrix}(\{a, b, c, d\}, \\ \{b, c\}) \end{matrix}

Abbildung 2.3: Die geordnete Menge auf der linken Seite ist ein Bereich, aber die beiden Mixe ({x, y}, {x, y}) und ({w, z}, {w, z}) haben zwei minimale obere Schranken.

Diesen Nachteil weist Bunemans Sandwich-Potenzkonstruktion [BDW88] nicht auf. Sandwiche unterscheiden sich von Mixen nur durch die Konsistenzbedingung. Während für Mixe L ⊆ ↑U gelten muß, wird für Sandwiche lediglich ↑l ∩ ↑U ≠ ∅ für alle l ∈ L verlangt. Ein Element l ∈ L darf also auch Elemente außerhalb von ↑U approximieren, obwohl diese gar nicht zur approximierten Menge gehören können. Es wird nur verlangt, daß auch wenigstens ein Element approximiert wird, das innerhalb von ↑U liegt.^{1}

Tatsächlich haben zwei beschränkte Sandwiche immer ein Supremum. Die Mixe aus Abbildung 2.3 können wir auch als Sandwiche verstehen. Ihr Supremum ist der Sandwich ({a, b, c, d}, {w, x, y, z}). Im allgemeinen ist die erste Komponente des Supremums zweier Sandwiche (U_{1}, L_{1}) und (U_{2}, L_{2}) gegeben durch {u_{1} ∨ u_{2} | u_{1} ∈ U_{1}, u_{2} ∈ U_{2}} (lies: die Menge der existierenden Suprema aus Elementen von U_{1} und U_{2}), d. h. die Menge der Erzeuger von ↑U_{1} ∩ ↑U_{2}. Die zweite Komponente ist L_{1} ∪ L_{2}. Dies ist nicht unbedingt enthalten in ↑U_{1} ∩ ↑U_{2}, so daß das Supremum zweier Sandwiche, selbst wenn diese die Bedingung für Mixe erfüllen, kein Mix sein muß. Die Bedingung für Sandwiche wird aber stets erfüllt sein, wenn (U_{1}, L_{1}) und (U_{2}, L_{2}) beschränkt sind in der durch ≤^{♯} × ≤^{♭} geordneten Menge der Sandwiche.

1Der Name Mix läßt sich dadurch erklären, daß in einem Mix eine Kombination oder Mischung der ≤^{♯}- und der ≤^{♭}-Approximation verwendet wird. Der Name Sandwich ist darauf zurückzuführen, daß durch die beiden Mengen U und L die approximierte Menge gleichsam von zwei verschiedenen Seiten her einfangen wird wie die Wurst zwischen zwei Scheiben Brot.

Da nun schon fünf verschiedene Potenzkonstruktionen angeführt wurden, stellt sich die Frage, welche Eigenschaften wir von einem Potenzbereich verlangen sollen. Zunächst sollen die Elemente des Potenzbereichs Teilmengen des Ausgangsbereichs sein, oder sie sollen, wenn das wie bei Sandwichen oder Mixen nicht der Fall ist, wenigstens als Teilmengen des Ausgangsbereichs gedeutet werden können. Man spricht dann von ”formalen Mengen“ und verlangt wenigstens die Existenz gewisser formaler Mengen: Für jedes Element x des Ausgangsbereichs soll es ein Element {|x|} im Potenzbereich geben, die ”formale einelementig erzeugte Menge“, die dem Element x zugeordnet ist. Außerdem verlangt man eine Halbverbandsoperation, die zwei formale Mengen ”vereinigt“, die ”formale Vereinigung“ ∪. Hat der Potenzbereich auch eine formale leere Menge e, so soll e ein neutrales Element bezüglich ∪ sein. Aber man begnügt sich nicht damit, die Eigenschaften einer Potenzmenge zu imitieren. Der Potenzbereich soll auch die ordnungstheoretischen Eigenschaften des Ausgangsbereichs erben. Dabei wird die jeweilige auf ≤^{♯} und ≤^{♭} zurückgehende Ordnung betrachtet, nicht etwa die aus ∪ durch x ⊂ y ⟺ y = x ∪ y definierbare Ordnung ⊂. Aus den ordnungstheoretischen Eigenschaften lassen sich weitere Bedingungen wie die Existenz gewisser Operationen oder die Gültigkeit gewisser Gleichungen für den Potenzbereich gewinnen. Ziel ist es dann, den Potenzbereich als freie Algebra mit geeigneter Signatur darzustellen. Insbesondere spielen die einelementig erzeugten formalen Mengen die Rolle der Erzeuger der Algebra.

Derartige Darstellungen sind für den Hoare-, Smyth- und Plotkin-Potenzbereich [HP79] sowie den Mixed-Potenzbereich [Gun92] bekannt. Für den Sandwich-Potenz-bereich hat Heckmann [Hec90] eine Darstellung als freie Algebra angegeben, die aber eine partielle Operation verwendet, deren semantische Interpretation problematisch ist.

Eine Konstruktion, die die Vorzüge der Mixe und Sandwiche vereint, hat Buneman mit den von ihm sogenannten Snacks vorgeschlagen. Diese sind in gewissem Sinne eine Verallgemeinerung der Sandwiche, was durch den Namen Snack ausgedrückt werden soll. Eine Semantik der Snacks und Operationen für Snacks hat Ngair [Nga92] untersucht. In [Puh93] konnten wir eine Charakterisierung des Snack-Potenzbereichs als freie Algebra angeben. Dieses Ergebnis stellen wir im nächsten Abschnitt vor.

2.2 Der Snack-Potenzbereich

2.2.1 Snacks und Ordnung

Definition 2.2.1 Es sei D ein Bereich. Die Menge der kompakt-offenen Teilmengen von D bezeichnen wir mit KΩ(D). Ein Snack auf einem Bereich D ist ein Paar (U, L), wobei U ∈ KΩ(D) und L eine endliche Menge nichtleerer kompakt-offener Teilmengen von D ist, die in U enthalten sind und bezüglich der Mengeninklusion eine Antikette bilden.

Man beachte, daß die kompakt-offenen Teilmengen eines Bereichs gerade diejenigen oberen Mengen sind, die von endlich vielen kompakten Elementen erzeugt werden.

Einen typischen Snack zeigt Abbildung 2.4. Die erste Komponente U fassen wir

L_{1}  D  L_{2} U

Abbildung 2.4: Das typische Bild eines Snacks

als äußere Schranke für die zu approximierende Menge M auf. Da es darum geht, Teilmengen von D_{max} zu approximieren, muß M ⊆ U ∩ D_{max} gelten. Hierin unterscheiden sich Snacks nicht von Sandwichen und Mixen. Der Unterschied tritt in der zweiten Komponente auf. In diesem Beispiel besteht sie aus den Mengen L_{1} und L_{2}. Jede dieser Mengen gibt eine Information über die Existenz von Elementen in M, es muß nämlich jede der Mengen L ∈ L ein Element von M enthalten. Die Mengen L ∈ L dürfen von mehreren Elementen erzeugt sein. Damit kann man ausdrücken, daß M ein Element enthält, welches durch einen der Erzeuger approximiert wird, ohne daß man sich festlegen muß, welches der erzeugenden Elemente tatsächlich das Element von M beschreibt. Hierin liegt der Unterschied zu Sandwichen und Mixen, bei denen man sich jeweils auf ein Element festlegen muß.

Die Nebenbedingungen für die Mengen U und L ∈ L lassen sich leicht erläutern. Zunächst müssen alle L ∈ L nichtleer sein, da in ihnen ja Elemente von M liegen sollen. Stünden zwei Mengen L und L′ aus L in der Beziehung L ⊆ L′, so gäbe L′ keine Information über M, die nicht schon durch L gegeben ist. Somit könnte L′ einfach weggelassen werden. Obwohl unser Bild kein Beispiel hierfür gibt, ist es jedoch zugelassen, daß die in L enthaltenen Mengen nicht disjunkt sind. Schließlich sollen alle L ∈ L in U enthalten sein, da das von einem L ∈ L approximierte Element von M nicht außerhalb von U liegen kann. Selbst wenn es bei einer Datenerfassung in Unkenntnis der Menge M zu einer Menge L käme, die nicht in U enthalten ist, könnte L durch Schnitt mit U nachträglich noch in die gewünschte Form überführt werden, da der Schnitt zweier kompakt-offener Mengen in einem Bereich kompaktoffen ist.

Bedenkt man die Interpretation der Snacks zur Approximation von Teilmengen M von D_{max}, so kann man leicht angeben, wie die Menge der Snacks geordnet werden soll. Um eine genauere Approximation zu erhalten, muß man die äußere Schranke U und jedes L ∈ L verkleinern, da damit auch die Information über in M enthaltene Elemente genauer wird. Zusätzlich darf weitere Information über Elemente von M eingefügt werden, d. h. man darf weitere Mengen zu L hinzufügen.

Abbildung 2.5 zeigt die Umrandungen des Snacks (U, {L_{1}, L_{2}}) aus Abbildung 2.4 und einen besseren Snack (U′, L′) mit L′ = {L′_{1}, L′_{2}, L′_{3}}. Dabei sind U′, L′_{1} und L′_{2} die Verfeinerungen der entsprechenden ungestrichenen Mengen aus dem Ausgangssnack, und L′_{3} ist eine neue Menge in L′.

Daß eine kleinere obere Menge besser ist, wird gerade durch die Smyth-Ord-nung ≤^{♯} ausgedrückt. Daß es zu jeder Menge L ∈ L in einer besseren Approximation eine Menge L′ ∈ L′ mit L ≤^{♯} L′ geben muß (und daß es weitere Mengen zur Approximation existierender Elemente geben darf), drückt die auf ≤^{♯} angewandte Hoare-Ordnung (≤^{♯})^{♭} aus.

Da U und L ∈ L obere Mengen sind, ist ≤^{♯} auf diesen Mengen tatsächlich eine Ordnungsrelation, und zwar ist ”≤^{♯}“ in diesem Fall gleichwertig mit ”⊇“. Die Menge der L ∈ L ist bezüglich ≤^{♯} immer eine Antikette, weshalb auch (≤^{♯})^{♭} (= (⊇)^{♭}) auf

L′_{1}  ^{L′_{3}} D ^{L′_{2}}  ^{U′}

Abbildung 2.5: Die Verfeinerung eines Snacks

den Mengen L eine Ordnungsrelation ist.^{2} Damit wird die Menge der Snacks auf einem Bereich zur geordneten Menge.

Definition 2.2.2 Die Menge der Snacks auf einem Bereich D ordnen wir durch ⊑:=≤^{♯} ×(≤^{♯})^{♭} (=⊇ × ⊇^{♭}); wir bezeichnen diese geordnete Menge mit S(D).

Abbildung 2.6 zeigt ein Beispiel für die geordnete Menge der Snacks auf einem Bereich.

Die geordnete Menge der Snacks ist im allgemeinen noch kein Bereich. Wie es bei allen Potenzbereichen algebraischer Bereiche üblich ist, haben wir die Konstruktion zunächst auf den kompakten Elementen durchgeführt. Durch Idealvervollständigung bekommen wir daraus den eigentlichen Potenzbereich.

Definition 2.2.3 Es sei D ein Bereich. Der Snack-Potenzbereich von D ist die Idealvervollständigung

P^{S}D := idl(S(D))

der Menge S(D) der Snacks auf D.

2Man beachte, daß (⊇)^{♭} von (⊆)^{♭} verschieden ist. Die Symbole ≤^{♯} bzw. ⊇ sind in der Definition der Hoare-Ordnung textuell für das Symbol ≤ zu ersetzen, um die Definition von (≤^{♯})^{♭} bzw. (⊇)^{♭} zu erhalten.

Beispiel: Ein Bereich D und seine nichtleeren kompakt-offenen Teilmengen. Die Namen der Teilmengen haben folgende Bedeutung: B für beide Teiläste von D; B^{⊤} für die maximalen Elemente von B; L für den linken Seitenast; R für den rechten Seitenast; R^{⊤} für die Menge, die das maximale Element von R enthält.

D  R^{⊤} B R  B^{⊤} L

Das folgende Diagramm zeigt die geordnete Menge der Snacks auf D:

(D, ∅) (D, {L, R})  (B, ∅) (B^{⊤}, ∅) (L, ∅) (D, {D}) (D, {B}) (D, {B^{⊤}})  (B, {B}) (B, {B^{⊤}}) (B^{⊤}, {B^{⊤}})  (R, ∅) (R^{⊤}, ∅) (∅, ∅) (D, {B^{⊤}, R}) (B, {L, R}) (B, {B^{⊤}, R})(D, {R^{⊤}}) (B, {R^{⊤}}) (B^{⊤}, {R^{⊤}}) (B, {R}) (D, {R}) (R^{⊤}, {R^{⊤}}) (R, {R^{⊤}}) (R, {R}) (B^{⊤}, {L, R^{⊤}}) (B, {L, R^{⊤}}) (D, {L, R^{⊤}}) (L, {L}) (B^{⊤}, {L}) (B, {L}) (D, {L})

Abbildung 2.6: Beispiel eines Bereichs D und der Menge S(D) der Snacks auf D

Dabei ist idl(M) für eine geordnete Menge M die Menge der Ideale von M, geordnet durch ⊆. (Einzelheiten der Technik der Idealvervollständigung finden sich in [AJ95].)

Die kompakten Elemente von idl(M) sind genau die Hauptideale ↓m, die von Elementen m ∈ M erzeugt werden. Die Mengen M und K(idl(M)) sind isomorph, wobei der Isomorphismus i: M → K(idl(M)) durch i(m) = ↓m gegeben ist.

Durch die Idealvervollständigung erhalten wir aus der Menge der Snacks auf D eine algebraische dcpo P^{S}(D). Wir hatten uns jedoch noch mehr zum Ziel gesetzt: Die Konstruktion sollte einen Bereich erzeugen, dessen maximale Elemente zu einer möglichst reichhaltigen Auswahl von Mengen maximaler Elemente des Ausgangsbereichs korrespondieren. Beide Ziele werden mit dem Snack-Potenzbereich erreicht. Der Snack-Potenzbereich ist ein Bereich, denn je zwei beschränkte Snacks haben ein Supremum:

Lemma 2.2.4 Es sei D ein Bereich, und (U, L) und (U′, L′) seien Snacks auf D, die in S(D) eine gemeinsame obere Schranke haben. Dann existiert in S(D) das Supremum von (U, L) und (U′, L′), und es ist gegeben durch

(U, L) ⊔ (U′, L′) = (U ∩ U′, MIN^{⊆}({L ∩ U ∩ U′ | L ∈ L ∪ L′})) ,  (2.1)

wobei MIN^{⊆} die bezüglich ⊆ minimalen Mengen auswählt.

Beweis: In Proposition 1.1.1 haben wir gesehen, daß der Schnitt zweier kompaktoffener Mengen wieder kompakt-offen ist. Damit sind U∩U′ und L∩U∩U′ (L ∈ L∪L′) kompakt-offen. Natürlich gilt stets L ∩ U ∩ U′ ⊆ U ∩ U′. Durch MIN^{⊆} wird in der zweiten Komponente eine Antikette ausgewählt. Können wir auch noch zeigen, daß L ∩ U ∩ U′ für alle L ∈ L ∪ L′ nicht leer ist, so ist gezeigt, daß der für das Supremum angegebene Ausdruck ein korrekt gebildeter Snack ist.

Um dies zu nachzuweisen, muß man verwenden, daß (U, L) und (U′, L′) eine obere Schranke (Û, L̂) haben. Für diese muß Û ⊆ U ∩ U′ gelten, und für jedes L ∈ L ∪ L′ gibt es notwendigerweise ein L̂ ∈ L̂ mit L̂ ⊆ L und L̂ ≠ ∅. Nun ist L ∩ U ∩ U′ ⊇ L̂, weshalb L ∩ U ∩ U′ ≠ ∅ gelten muß.

Diese Argumentation zeigt zugleich, daß der Ausdruck aus (2.1) kleiner als jede obere Schranke (Û, L̂) ist, denn wenn für jedes L ∈ L ∪ L′ ein L̂ ∈ L̂ existiert mit L̂ ⊆ L, dann ist dies inbesondere für die L ∈ L ∪ L′ der Fall, für die L ∩ U ∩ U′ minimal in {L ∩ U ∩ U′ | L ∈ L ∪ L′} bezüglich ⊆ ist.

Schließlich ist (U ∩ U′, MIN^{⊆}({L ∩ U ∩ U′ | L ∈ L ∪ L′})) offensichtlich eine obere Schranke von (U, L) und (U′, L′), so daß dies wirklich das Supremum ist.

Der Snack (D, ∅) ist für jeden Bereich D der kleinste Snack. Zusammen mit dem gerade Gezeigten folgt hieraus, daß endliche beschränkte Mengen kompakter Elemente des Snack-Potenzbereichs ein Supremum haben. Also hat jede beschränkte Menge M ein Supremum. Es ist das Supremum der gerichteten Menge der Suprema endlicher Mengen kompakter Elemente, die unter Elementen von M liegen.

So können wir zusammenfassen:

Satz 2.2.5 Der Snack-Potenzbereich eines Bereichs ist ein Bereich.

Nun wollen wir noch angeben, was die maximalen Elemente des Snack-Potenzbe-reichs sind. Wir haben bereits ausgeführt, welche Teilmengen von D_{max} wir uns als durch einen Snack (U, L) auf D approximiert denken. Die Menge dieser Teilmengen bezeichnen wir mit apr_{0}(U, L), d. h.

apr_{0}(U, L) = {M ⊆ D_{max} | M ⊆ U und L ∩ M ≠ ∅ für alle L ∈ L}

für jeden Snack (U, L) auf D.

Hieraus gewinnen wir eine Beschreibung apr der Teilmengen von D_{max}, die durch ein Ideal von Snacks approximiert werden. Die Idee ist, daß jeder in dem Ideal enthaltene Snack die fragliche Teilmenge approximieren muß. Ist s ein Ideal von Snacks auf D, so ist

apr(s) = {M ⊆ D_{max} | ∀(U, L) ∈ s. M ∈ apr_{0}(U, L)} = ⋂_{(U,L)∈s} apr_{0}(U, L) .

So erhalten wir zu jedem Element von P^{S}(D) gewisse Teilmengen von D_{max}. Umgekehrt findet man aber auch zu jeder Teilmenge M ⊆ D_{max} mit der Menge

sn(M) := {(U, L) ∈ S(D) | M ∈ apr_{0}(U, L)}

der M approximierenden Snacks ein Element von P^{S}(D). In der Tat ist dies ein Ideal: Es ist nicht leer, denn es ist immer (D, ∅) ∈ sn(M), es ist gerichtet, da je zwei Snacks in sn(M) beschränkt sind und ihr Supremum in sn(M) ist, und selbstverständlich ist sn(M) nach unten abgeschlossen.

Damit können wir die maximalen Elemente des Snack-Potenzbereichs charakterisieren. Im Beweis des nachfolgenden Satzes verwenden wir folgendes Korollar zum Hofmann-Mislove-Theorem [HM81, KP94]:

Lemma 2.2.6 Es sei F eine gefilterte Familie nichtleerer kompakter oberer Teilmengen eines Bereichs D. Dann ist ⋂ F eine nichtleere kompakte obere Teilmenge von D. Ist ferner M eine kompakte obere Teilmenge von D, die zum Schnitt ⋂ F disjunkt ist, so gibt es ein F ∈ F mit F ∩ M = ∅.

Beweis: Den Beweis der ersten Behauptung findet man in [KP94].

Der Schnitt zweier kompakter oberer Mengen ist eine kompakte obere Menge. Damit ist F′ := {F ∩ M | F ∈ F} eine gefilterte Menge kompakter oberer Mengen. Wäre F ∩M ≠ ∅ für alle F ∈ F, so wäre nach unserer ersten Aussage auch M ∩⋂ F = ⋂ F′ ≠ ∅, im Widerspruch zur Annahme.

Satz 2.2.7 Es sei D ein Bereich. Die maximalen Elemente im Snack-Potenzbe-reich von D entsprechen den Schnitten Scott-kompakter oberer Teilmengen von D mit D_{max}. Genauer: Es gibt eine Bijektion zwischen der Menge M der Schnitte Scott-kompakter oberer Teilmengen von D mit D_{max} und der Menge der maximalen Elemente von P^{S}(D). Sie ist gegeben durch die Abbildungen f: M → P^{S}(D)_{max} mit f(X) := sn(X) und g: P^{S}(D)_{max} → M mit g(s) := D_{max} ∩ ⋂{U | (U, L) ∈ s}

Beweis: Es sei X der Schnitt einer Scott-kompakten oberen Teilmenge des Bereichs D mit D_{max}.

Ist X = ∅, so ist f(X) = sn(X) = ↓(∅, ∅). Dies ist maximal in P^{S}(D), da (∅, ∅) maximal in S(D) ist, und es gilt g(f(∅)) = ∅.

Von nun an sei X ≠ ∅, und s sei ein Ideal, das sn(X) umfaßt.

Wir zeigen zunächst, daß für die in s enthaltenen Snacks (U, L) stets X ⊆ U gilt. Wäre dies nämlich für (Û, L̂) ∈ s nicht der Fall, so hätten wir ein x ∈ X mit x ∉ Û. Die Menge F der ↑k_{x} mit k_{x} ∈ ↓x ∩ K(D) bildete eine gefilterte Menge kompaktoffener Mengen mit ⋂ F ∩ Û = {x} ∩ Û = ∅, so daß es nach Lemma 2.2.6 ein solches k̂_{x} mit ↑k̂_{x} ∩ Û = ∅ gäbe. Sicher wäre der Snack (D, {↑k̂_{x}}) in sn(X) und wegen s ⊇ sn(X) auch in s enthalten. Nun ist aber s ein Ideal, d. h. (Û, L̂) und (D, {↑k̂_{x}}) müßten beschränkt sein. Wegen ↑k̂_{x} ∩ Û = ∅ wäre dies jedoch nicht der Fall, so daß X ⊆ Û gezeigt ist.

Damit können wir festhalten, daß in den in s und den in sn(X) enthaltenen Snacks dieselben Mengen in der ersten Komponente vorkommen, denn für jede kompaktoffene Obermenge U von X gilt (U, ∅) ∈ sn(X). Es gilt damit ⋂{U | (U, L) ∈ s} = ⋂{U | (U, L) ∈ sn(X)}. Da X der Schnitt von D_{max} mit der Menge der kompaktoffenen Obermengen von X ist, gilt ferner ( ⋂{U | (U, L) ∈ sn(X)})_{max} = X. Vorbehaltlich des noch zu Ende zu führenden Nachweises der Maximalität von f(X) = sn(X) in P^{S}(D) ist damit auch X = g(f(X)) gezeigt.

Um diesen Nachweis zu führen, zeigen wir, daß für jeden in s enthaltenen Snack (Û, L̂) und für jedes L̂ ∈ L̂ der Schnitt L̂∩X nicht leer ist. Da s gerichtet ist, müssen (U, L) und (Û, L̂) für alle (U, L), (Û, L̂) ∈ s beschränkt sein. Insbesondere muß hierzu L̂ ∩ U ≠ ∅ für alle L̂ ∈ L̂ gelten. Da die Menge {U | (U, L) ∈ s} gefiltert ist, folgt L̂ ∩ ⋂{U | (U, L) ∈ s} ≠ ∅. Die hierin betrachteten Mengen sind obere Mengen, so daß auch L̂ ∩ ( ⋂{U | (U, L) ∈ s})_{max} ≠ ∅ gilt. Wegen ⋂{U | (U, L) ∈ s} = ⋂{U | (U, L) ∈ sn(X)} und ( ⋂{U | (U, L) ∈ sn(X)})_{max} = X folgt schließlich L̂ ∩ X ≠ ∅.

Damit approximiert jeder in s enthaltene Snack die Menge X, was s = sn(X) und die Maximalität von sn(X) nachweist.

Nun sei s ∈ P^{S}(D)_{max}. Es ist g(s) = D_{max} ∩ ⋂{U | (U, L) ∈ s}. Der Schnitt ⋂{U | (U, L) ∈ s} ist nach dem Hofmann-Mislove-Theorem (Lemma 2.2.6) eine kompakte obere Menge, da {U | (U, L) ∈ s} eine gefilterte Menge kompakt-offener Mengen ist. Folglich ist g(s) der Schnitt einer Scott-kompakten oberen Menge mit D_{max}. Jeder Snack aus s approximiert die Menge g(s), daher ist s ⊆ sn(g(s)). Da s als maximal in P^{S}(D) vorausgesetzt ist, folgt schließlich wie gewünscht s = sn(g(s)), was den Beweis vollendet.

2.2.2 Operationen auf Snacks

In Abschnitt 2.1 wurde die Interpretation der Elemente eines Potenzbereichs als formale Mengen beschrieben. Nun bildet erst die Idealvervollständigung der geordneten Menge der Snacks auf einem Bereich den Potenzbereich. Da die Menge der Snacks isomorph zur Menge der kompakten Elemente des Potenzbereichs ist, lassen sich die relevanten Überlegungen bezüglich der formalen Mengen dennoch direkt anhand der Snacks durchführen.

Zu jedem kompakten Element x eines Bereichs D erhält man in der Menge S(D) der Snacks auf D eine formale einelementig erzeugte Menge durch die Abbildung

{| · |} : KD → S(D) ,
{|x|} := (↑x, {↑x}) .

Die formale Vereinigung ist gegeben durch

∪ : S(D) × S(D) → S(D) ,
(U, L) ∪ (U′, L′) := (U ∪ U′, MIN^{⊆}(L ∪ L′)) .

Man überzeugt sich leicht, daß das Ergebnis der formalen Vereinigung zweier Snacks tatsächlich wieder ein Snack ist.

Da die formale Vereinigung in beiden Komponenten getrennt eine Mengenvereinigung durchführt und

MIN^{⊆}(L ∪ MIN^{⊆}(L′ ∪ L′′)) = MIN^{⊆}(L ∪ L′ ∪ L′′) = MIN^{⊆}(MIN^{⊆}(L ∪ L′) ∪ L′′) gilt, ist es klar, daß ∪ eine Halbverbandsoperation ist. Weiter ist der Snack (∅, ∅), der die formale leere Menge ist, neutral bezüglich ∪.

Im weiteren werden wir auch benötigen, daß die Operationen auf der Menge der Snacks mit der Ordnung ⊑ verträglich, d. h. monoton bezüglich dieser Ordnung sind. Dies ist für ∪ der Fall: Seien die Snacks (U, L) ⊑ (Û, L̂) und (U′, L′) ⊑ (Û′, L̂′) gegeben. Dann ist wegen Û ⊆ U und Û′ ⊆ U′ auch Û ∪ Û′ ⊆ U ∪ U′. Jedes L ∈ MIN^{⊆}(L∪L′) stammt aus einem der Snacks (U, L) und (U′, L′). Wir können o. B. d. A. annehmen, daß L ∈ L ist. Wegen (U, L) ⊑ (Û, L̂) gibt es ein L̂ ∈ L̂ mit L ⊇ L̂. Nun muß L̂ nicht ⊆-minimal in L̂ ∪ L̂′ sein. Es gibt in MIN^{⊆}(L̂ ∪ L̂′) aber ein L̂′ mit L̂ ⊇ L̂′, also auch L ⊇ L̂′. Damit ist

(U, L) ∪ (U′, L′) = (U ∪ U′, MIN^{⊆}(L ∪ L′))
⊑ (Û ∪ Û′, MIN^{⊆}(L̂ ∪ L̂′)) = (Û, L̂) ∪ (Û′, L̂′)

nachgewiesen.

Im allgemeinen ist das Infimum zweier kompakter Elemente eines Bereichs nicht kompakt. In der geordneten Menge der Snacks jedoch existieren alle binären Infima. Somit erhalten wir aus der Ordnung auf der Menge der Snacks das Infimum ⊓ als weitere Halbverbandsoperation, die folgendermaßen gegeben ist:

⊓ : S(D) × S(D) → S(D)
(U, L) ⊓ (U′, L′) = (U ∪ U′, MIN^{⊆}({L ∪ L′ | L ∈ L, L′ ∈ L′}))

Wir müssen nachweisen, daß dies wirklich das Infimum bezüglich ⊑ ist. Die erste Komponente der Snacks ist durch ⊇ geordnet; bezüglich der Obermengenrelation bildet die Mengenvereinigung das Infimum. Daß MIN^{⊆}({L ∪ L′ | L ∈ L, L′ ∈ L′}) bezüglich ⊇^{♭} eine untere Schranke für L und L′ ist, sieht man leicht: Für jedes der L ∪ L′ hat man sowohl in L als auch in L′ eine kleinere obere Menge, nämlich L in L und L′ in L′. Andererseits muß jedes Element L̂ einer unteren Schranke L̂ wenigstens solch ein L und L′ enthalten, d. h. L̂ ⊇ L ∪ L′ für geeignete L und L′ aus L bzw. L′. Ist L ∪ L′ nicht minimal unter allen solchen Vereinigungen, so gibt es L̄ in L und L̄ in L′ so, daß L̄ ∪ L̄′ diese Eigenschaft hat. Also ist L̂ ⊇ L̄ ∪ L̄′, weshalb MIN^{⊆}({L∪L′ | L ∈ L, L′ ∈ L′}) ⊇^{♭} L̂ ist. Folglich ist MIN^{⊆}({L∪L′ | L ∈ L, L′ ∈ L′}) das Infimum in der zweiten Komponente. Schließlich ist das derart komponentenweise gebildete Infimum wieder ein Snack: Die Vereinigung zweier (nichtleerer) kompaktoffener Mengen ist eine (nichtleere) kompakt-offene Menge, somit sind U ∪U′ und alle L ∪ L′ von der geforderten Form. Ferner gibt es nur endlich viele Vereinigungen der Form L ∪ L′, da L und L′ endlich sind. Unter diesen wird durch MIN^{⊆} eine Antikette ausgewählt.

Als Infimum bezüglich ⊑ ist ⊓ selbstverständlich monoton.

Die beiden Halbverbandsoperationen ∪ und ⊓ sind miteinander verbunden durch die Distributivgesetze

(r ∪ s) ⊓ t = (r ⊓ t) ∪ (s ⊓ t)  (2.2)
und (r ⊓ s) ∪ t = (r ∪ t) ⊓ (s ∪ t) .  (2.3)

Um dies einzusehen, beachte man, daß ∪ und ⊓ auf der ersten Komponente der Snacks gleich definiert sind, es wird hier nämlich eine Mengenvereinigung durchgeführt. So brauchen wir für die erste Komponente nichts zeigen und nur für die zweite Komponente einen Nachweis führen. Dazu seien L^{r}, L^{s} und L^{t} die zweiten Komponenten der Snacks r, s und t. Wir betrachten zunächst (2.2) bezüglich der zweiten Komponente und beginnen mit der linken Seite:

MIN^{⊆}({L ∪ L′|L ∈ MIN^{⊆}(L^{r} ∪ L^{s}), L′ ∈ L^{t}})
= MIN^{⊆}({L ∪ L′|L ∈ L^{r} ∪ L^{s}, L′ ∈ L^{t}})
= MIN^{⊆}({L ∪ L′|L ∈ L^{r}, L′ ∈ L^{t}}
∪ {L ∪ L′|L ∈ L^{s}, L′ ∈ L^{t}})
= MIN^{⊆}(MIN^{⊆}({L ∪ L′|L ∈ L^{r}, L′ ∈ L^{t}})
∪ MIN^{⊆}({L ∪ L′|L ∈ L^{s}, L′ ∈ L^{t}})),

was die zweite Komponente der rechten Seite von (2.2) ist.

Unter Ausnutzung von (2.2) und der Monotonie von ∪ ergibt sich (2.3): Einerseits ist (r ⊓ s) ∪ t ⊑ r ∪ t und (r ⊓ s) ∪ t ⊑ s ∪ t, also (r ⊓ s) ∪ t ⊑ (r ∪ t) ⊓ (s ∪ t). Andererseits gilt (r ∪ t)⊓(s ∪ t) = (r⊓s) ∪ (r⊓t) ∪ (t⊓s) ∪ (t⊓t) ⊑ (r⊓s) ∪ t.

2.2.3 Die Snackalgebra

Ziel dieses Abschnitts ist es, die Menge S(D) der Snacks auf einem Bereich D als freie Algebra zu charakterisieren. Im vorhergehenden Abschnitt wurden Operationen auf der Menge der Snacks und ihre Eigenschaften vorgestellt. Wir sehen nun von der speziellen Struktur der Snacks ab und definieren eine Snackalgebra als geordnete Menge mit solchen Operationen. Auf die partielle Operation des beschränkten Supremums können wir dabei verzichten.

Definition 2.2.8 Eine geordnete Algebra ist eine Algebra, auf deren Trägermenge eine Ordnungsrelation erklärt ist und deren Operationen bezüglich der Ordnung monoton sind.

Definition 2.2.9 Eine Snackalgebra ist eine geordnete Algebra (M, ⊑) zusammen mit zwei Halbverbandsoperationen ∪ , ⊓ : M ×M → M und einer Konstanten e ∈ M so, daß für alle r, s, t ∈ M gilt:

\begin{aligned}r ⊓ s & ⊑ & r & (S0) \\ e ∪ r & = & r & (S1) \\ (r ∪ s) ⊓ t & = & (r ⊓ t) ∪ (s ⊓ t) & (S2) \end{aligned}

Lemma 2.2.10 In einer Snackalgebra gilt auch das Distributivgesetz

(r ⊓ s) ∪ t = (r ∪ t) ⊓ (s ∪ t)  (S3)

Beweis: Daß die Monotonie von ∪ und das Distributivgesetz (S2) zusammen die Beziehung (S3) implizieren, wurde am Ende des letzten Abschnitts gezeigt. Der Beweis nimmt nicht auf konkrete Snacks bezug und läßt sich wortwörtlich übertragen.

Umgekehrt bekommt man aus (S3) die Monotonie von ∪:

((r ⊓ s) ∪ t) ⊓ (r ∪ t) = (r ∪ t) ⊓ (s ∪ t) ⊓ (r ∪ t)
= (r ∪ t) ⊓ (s ∪ t)
= (r ⊓ s) ∪ t .

Man könnte Snackalgebren daher auch als sogenannte Bi-Halbverbände definieren, in denen beide Distributivgesetze gelten und in denen bezüglich der einen Halbverbandsoperation ein neutrales Element existiert. Die Ordnungsrelation gewänne man dann auf die übliche Weise aus der anderen Halbverbandsoperation. Bi-Halbverbände und die dafür möglichen Distributivgesetze wurden z. B. in [Pło67, Rom80] untersucht, jedoch nicht hinsichtlich ihrer Eigenschaften als geordnete Mengen. Gerade diese stehen jedoch für uns im Vordergrund, und auch nach Wegfall der durch die Operationen gegebenen Struktur sollen die Ordnungseigenschaften erhalten bleiben. Dies läßt unsere Wahl bei der Definition auf die Struktur einer geordneten Algebra fallen.

Offenbar ist für einen Bereich D die Menge S(D) der Snacks auf D zusammen mit den Operationen ∪ und ⊓ und dem Snack (∅, ∅) stets eine Snackalgebra. Dies ergibt sich aus dem in Abschnitt 2.2.2 Gesagten.

Wir zeigen nun, daß S(D) durch die Menge {{|k|} | k ∈ KD} erzeugt wird.

Lemma 2.2.11 Es sei D ein Bereich, s = (U, {L_{1}, …, L_{k}}) ∈ S(D), wobei U = ↑{u_{1}, …, u_{n}} und L_{i} = ↑{l_{i1}, …, l_{im_{i}}} (i = 1, …, k; m_{i} ∈ ℕ für alle i = 1, …, k). Dann läßt sich s aus formalen einelementig erzeugten Mengen folgendermaßen aufbauen:

s = ({|u_{1}|} ⊓ … ⊓ {|u_{n}|} ⊓ (∅, ∅)) ∪
({|l_{11}|} ⊓ … ⊓ {|l_{1m_{1}}|}) ∪ … ∪ ({|l_{k1}|} ⊓ … ⊓ {|l_{km_{k}}|}) .

Beweis: Es ist

{|u_{1}|} ⊓ … ⊓ {|u_{n}|} = (↑u_{1}, {↑u_{1}}) ⊓ … ⊓ (↑u_{n}, {↑u_{n}})
= (↑{u_{1}, …, u_{n}}, {↑{u_{1}, …, u_{n}}})
= (U, {U}).

Genauso erhält man für i = 1, …, k die Beziehung

{|l_{i}|} ⊓ … ⊓ {|l_{im_{i}}|} = (L_{i}, {L_{i}}).

Da L_{i} ⊆ U für alle i = 1, …, k folgt

({|u_{1}|} ⊓ … ⊓ {|u_{n}|} ⊓ (∅, ∅)) ∪ ⋃ ; −_{i=1}^{k}({|l_{i1}|} ⊓ … ⊓ {|l_{im_{i}}|})

= ((U, {U}) ⊓ (∅, ∅)) ∪ ⋃ ; −_{i=1}^{k}(L_{i}, {L_{i}})
= (U, ∅) ∪ ⋃ ; −_{i=1}^{k}(L_{i}, {L_{i}})
= (U ∪ ⋃_{i=1}^{k} L_{i}, {L_{1}, …, L_{k}})
= (U, {L_{1}, …, L_{k}}).

Dabei erübrigt es sich, in der zweiten Komponente den Operator MIN^{⊆} zu verwenden, da die L_{i} nach Voraussetzung eine Antikette bilden. Man beachte, daß die Argumentation auch für k = 0 (leere zweite Komponente) oder U = ∅ (leerer Snack) richtig ist.

Bevor wir zum Hauptergebnis dieses Abschnitts kommen, nämlich daß die Menge der Snacks auf einem Bereich eine freie Snackalgebra ist, tragen wir noch einige Hilfssätze zusammen, die wir bei dessen Beweis benötigen. Das folgende Ergebnis ist für konkrete Snacks leicht einzusehen: Das Infimum mit (∅, ∅) ergibt einen Snack mit leerer zweiter Komponente, und auf der ersten Komponente wirken ∪ und ⊓ gleich. Dieser Sachverhalt läßt sich als Gleichung formulieren und abstrakt auf die Elemente einer Snackalgebra übertragen:

Lemma 2.2.12 In einer Snackalgebra gilt für alle Elemente r, s und die Konstante e stets

(r ∪ s) ⊓ e = (r ⊓ s) ⊓ e.

Beweis: Einerseits ist (r ∪ s) ⊓ e ⊒ ((r ⊓ s) ∪ (r ⊓ s)) ⊓ e = r ⊓ s ⊓ e. Andererseits ist (r ∪ s) ⊓ e = (r ⊓ e) ∪ (s ⊓ e) ⊑ r ∪ e = r (analog (r ∪ s) ⊓ e ⊑ s) und (r ∪ s) ⊓ e ⊑ e, womit sich (r ∪ s) ⊓ e ⊑ r ⊓ s ⊓ e ergibt.

Lemma 2.2.13 Es sei {u_{1}, …, u_{n}} Teilmenge einer geordneten Menge M, und f sei eine monotone Abbildung von M in einen ∧-Halbverband. Weiter sei {v_{1}, …, v_{m}} ⊆ ↑{u_{1}, …, u_{n}}. Dann gelten

(i) f(u_{1}) ∧ … ∧ f(u_{n}) ≤ f(v_{1}) ∧ … ∧ f(v_{m}) und

(ii) f(u_{1}) ∧ … ∧ f(u_{n}) ∧ f(v_{1}) ∧ … ∧ f(v_{m}) = f(u_{1}) ∧ … ∧ f(u_{n}).

Lemma 2.2.14 Es seien M eine geordnete Menge und A eine Snackalgebra. Die Abbildung f: M → A sei monoton. In M seien die Teilmengen U = {u_{1}, …, u_{n}}, L′ = {l′_{1}, …, l′_{k}} und L = {l_{1}, …, l_{m}} mit U ≤^{♯} L′ ≤^{♯} L gegeben. Dann gilt

(e ⊓ f(u_{1}) ⊓ … ⊓ f(u_{n})) ∪ (f(l′_{1}) ⊓ … ⊓ f(l′_{k})) ∪ (f(l_{1}) ⊓ … ⊓ f(l_{m}))

= (e ⊓ f(u_{1}) ⊓ … ⊓ f(u_{n})) ∪ (f(l_{1}) ⊓ … ⊓ f(l_{m})).

Beweis: Wir verwenden Lemma 2.2.13 sowie die Monotonie und Idempotenz von ∪. Damit haben wir:

(e ⊓ f(u_{1}) ⊓ … ⊓ f(u_{n})) ∪ (f(l′_{1}) ⊓ … ⊓ f(l′_{k})) ∪ (f(l_{1}) ⊓ … ⊓ f(l_{m}))

≤ (e ⊓ f(u_{1}) ⊓ … ⊓ f(u_{n})) ∪ (f(l_{1}) ⊓ … ⊓ f(l_{m})) ∪ (f(l_{1}) ⊓ … ⊓ f(l_{m}))
= (e ⊓ f(u_{1}) ⊓ … ⊓ f(u_{n})) ∪ (f(l_{1}) ⊓ … ⊓ f(l_{m})).

Ähnlich bekommen wir die andere Ungleichung:

(e ⊓ f(u_{1}) ⊓ … ⊓ f(u_{n})) ∪ (f(l′_{1}) ⊓ … ⊓ f(l′_{k})) ∪ (f(l_{1}) ⊓ … ⊓ f(l_{m}))

≥ (e ⊓ f(u_{1}) ⊓ … ⊓ f(u_{n})) ∪ (f(u_{1}) ⊓ … ⊓ f(u_{n})) ∪ (f(l_{1}) ⊓ … ⊓ f(l_{m}))
≥ (e ⊓ f(u_{1}) ⊓ … ⊓ f(u_{n})) ∪ (e ⊓ f(u_{1}) ⊓ … ⊓ f(u_{n})) ∪ (f(l_{1}) ⊓ … ⊓ f(l_{m}))
= (e ⊓ f(u_{1}) ⊓ … ⊓ f(u_{n})) ∪ (f(l_{1}) ⊓ … ⊓ f(l_{m})).

Mit diesen Hilfsmitteln können wir das Hauptergebnis dieses Abschnitts formulieren:

Satz 2.2.15 Die Menge der Snacks auf einem Bereich D mit den Operationen ∪ und ⊓ und der Konstanten (∅, ∅) ist die von der geordneten Menge KD der kompakten Elemente von D frei erzeugte Snackalgebra, d. h. für jede Snackalgebra A und jede monotone Funktion f : KD → A gibt es einen eindeutig bestimmten Snackalgebra-Homomorphismus f^{+} : S(D) → A, so daß f^{+} ∘ {| · |} = f gilt.

Beweis: Lemma 2.2.11 zufolge läßt sich jeder Snack s = (U, {L_{1}, …, L_{k}}) aus den Erzeugern u_{1}, …, u_{n} von U und l_{i1}, …, l_{im_{i}} von L_{i} (i = 1, … k) darstellen. Wenn es den geforderten Homomorphismus f^{+} gibt, muß daher gelten

f^{+}(s) = f^{+}(({|u_{1}|} ⊓ … ⊓ {|u_{n}|} ⊓ (∅, ∅)) ∪
({|l_{11}|} ⊓ … ⊓ {|l_{1m_{1}}|}) ∪ … ∪ ({|l_{k1}|} ⊓ … ⊓ {|l_{km_{k}}|}))
= (f^{+}({|u_{1}|}) ⊓ … ⊓ f^{+}({|u_{n}|}) ⊓ f^{+}((∅, ∅))) ∪

(f^{+}({|l_{11}|}) ⊓ … ⊓ f^{+}({|l_{1m_{1}}|})) ∪ … ∪ (f^{+}({|l_{k1}|}) ⊓ … ⊓ f^{+}({|l_{km_{k}}|}))

= (f(u_{1}) ⊓ … ⊓ f(u_{n}) ⊓ e) ∪
(f(l_{11}) ⊓ … ⊓ f(l_{1m_{1}})) ∪ … ∪ (f(l_{k1}) ⊓ … ⊓ f(l_{km_{k}})).

Dabei ist schon berücksichtigt, daß f^{+}((∅, ∅)) = e sein muß. Man kann annehmen, daß {u_{1}, …, u_{n}} und {l_{i1}, …, l_{im_{i}}} (i = 1, …, k) bezüglich ≤ sowie {L_{1}, …, L_{k}} bezüglich ⊆ Antiketten sind, um zu einer kanonischen Darstellung zu gelangen. Wegen der Lemmata 2.2.13 und 2.2.14 hängt die obige Darstellung jedoch nicht von dieser Annahme ab.

Wir haben gezeigt, daß f^{+}, falls es existiert, eindeutig bestimmt ist. Wegen der Existenz der kanonischen Darstellung der Snacks können wir die obige Gleichung auch als Definition von f^{+} lesen. Nun bleibt noch nachzuweisen, daß hierdurch ein Snackalgebra-Homomorphismus gegeben ist. Daß f^{+}((∅, ∅)) = e ist, erwähnten wir bereits oben. Es bleibt zu zeigen, daß f^{+} die Operationen ∪ und ⊓ bewahrt.

Es seien also s = (↑{u_{1}, …, u_{n}}, {↑{l_{i1}, …, l_{im_{i}}} | i = 1, …, k}) und ŝ = (↑{û_{1}, …, ûn̂}, {↑{l̂_{j1}, …, l̂_{jm̂_{j}}} | j = 1, …, k̂}) Snacks auf D.

Mit den Abkürzungen

a = f(u_{1}) ⊓ … ⊓ f(u_{n})
b_{i} = f(l_{i1}) ⊓ … ⊓ f(l_{im_{i}})
c = f(û_{1}) ⊓ … ⊓ f(ûn̂)
d_{j} = f(l̂_{j1}) ⊓ … ⊓ f(l̂_{jm̂_{j}})

bekommen wir

f^{+}(s) ∪ f^{+}(ŝ) = (e ⊓ a) ∪ ( ⋃ ; −_{i=1}^{k} b_{i}) ∪ (e ⊓ c) ∪ ( ⋃ ; −_{j=1}^{k̂} d_{j})
= (e ⊓ (a ∪ c)) ∪ ( ⋃ ; −_{i=1}^{k} b_{i}) ∪ ( ⋃ ; −_{j=1}^{k̂} d_{j})
= (e ⊓ a ⊓ c) ∪ ( ⋃ ; −_{i=1}^{k} b_{i}) ∪ ( ⋃ ; −_{j=1}^{k̂} d_{j}) (nach Lemma 2.2.12)
= f^{+}(s ∪ ŝ),

wobei sich der letzte Schritt mit Lemma 2.2.14 ergibt. Also bewahrt f^{+} die Operation ∪. Für die Operation ⊓ haben wir:

f^{+}(s) ⊓ f^{+}(ŝ) = ((e ⊓ a ∪ ⋃ ; −_{i=1}^{k} b_{i}) ⊓ ((e ⊓ c ∪ ⋃ ; −_{j=1}^{k̂} d_{j})
= (e ⊓ a ⊓ c) ∪ (e ⊓ a ⊓ ⋃ ; −_{j=1}^{k̂} d_{j}) ∪ ( ⋃ ; −_{i=1}^{k} b_{i} ⊓ e ⊓ c) ∪ ( ⋃ ; −_{i=1}^{k} b_{i} ⊓ ⋃ ; −_{j=1}^{k̂} d_{j}).

Mit Lemma 2.2.12 und Lemma 2.2.14 können wir vereinfachen:

(e ⊓ a ⊓ c) ∪ (e ⊓ a ⊓ ⋃ ; −_{j=1}^{k̂} d_{j}) = (e ⊓ a ⊓ c) ∪ (e ⊓ a ⊓ ⨅_{j=1}^{k̂} d_{j})

= e ⊓ ((a ⊓ c) ∪ (a ⊓ ⨅_{j=1}^{k̂} d_{j}))

= e ⊓ a ⊓ c ⊓ ⨅_{j=1}^{k̂} d_{j}
= e ⊓ a ⊓ c.

Analog ergibt sich

(e ⊓ a ⊓ c) ∪ ( ⋃ ; −_{i=1}^{k} b_{i} ⊓ e ⊓ c) = (e ⊓ a ⊓ c).

Damit läßt sich f^{+}(s) ⊓ f^{+}(ŝ) folgendermaßen umformen:

f^{+}(s) ⊓ f^{+}(ŝ) = (e ⊓ a ⊓ c) ∪ ( ⋃ ; −_{i=1}^{k} b_{i} ⊓ ⋃ ; −_{j=1}^{k̂} d_{j})
= (e ⊓ a ⊓ c) ∪ ⋃ ; −_{i=1}^{k} ⋃ ; −_{j=1}^{k̂}(b_{i} ⊓ d_{j}).

Unter Verwendung von Lemma 2.2.12 und Lemma 2.2.14 erkennt man, daß dies gerade f^{+}(s ⊓ ŝ) ist.

Eine auf den kompakten Elementen eines Bereichs definierte monotone Funktion kann stets eindeutig zu einer Scott-stetigen Funktion auf dem Bereich fortgesetzt werden. Sind D und E Bereiche, und ist f : KD → E monoton, so ist diese Fortsetzung gegeben durch

f̂: D → E,  f̂(x) = ^{⋁ ↑}f(↓x ∩ KD).

So läßt sich {| · |} : KD → S(D) zunächst zu einer Funktion nach idl(S(D)) abändern, indem man das von (↑k, {↑k}) erzeugte Hauptideal als Funktionswert von k angibt. Eine Scott-stetige Funktion {| · |}_{D}: D → P^{S}D erhält man durch

\{|x|\}_{D} := \begin{matrix}⋃ & ↑ \\ k∈↓x∩KD \end{matrix} ↓(↑k, \{↑k\}).

Entsprechend definiert man die Scott-stetige Funktion ∪_{idl}:

∪_{idl} : P^{S}D × P^{S}D → P^{S}D
x ∪_{idl} y := ^{⋃ ↑}{↓(k_{x} ∪ k_{y}) | k_{x}, k_{y} ∈ S(D), k_{x} ∈ x, k_{y} ∈ y}

Analog kann man ⊓_{idl} definieren. Da dies jedoch das Infimum bezüglich der Ordnung ⊑ auf S(D) ist, hat man ⊓_{idl} = ∩, d. h. dies ist gerade der Durchschnitt zweier Ideale.

Damit ist P^{S}D ein Bereich mit zwei Scott-stetigen Halbverbandsoperationen ∪_{idl} und ⊓_{idl}, für die die Beziehungen (S0), (S1) und (S2) aus der Definition der Snackalgebren gelten, dabei ist das Hauptideal ↓(∅, ∅) neutral bezüglich ∪_{idl}. Da die Definitionen von ∪_{idl} und ⊓_{idl} keinen Gebrauch von der speziellen Struktur der Snacks machen, läßt sich dies auf beliebige Snackalgebren übertragen, es ist dann ↓e neutral bezüglich ∪_{idl}.

Definition 2.2.16 Eine stetige Snackalgebra ist eine Snackalgebra (D, ∪ , ⊓, e), für die D ein Bereich und ∪ und ⊓ Scott-stetig sind. Von den Homomorphismen zwischen stetigen Snackalgebren verlangen wir nun auch Scott-Stetigkeit.

Mit den bisherigen Ergebnissen ergibt sich auch die Darstellung des Snack-Po-tenzbereichs eines Bereichs als freie Algebra:

Satz 2.2.17 Es sei D ein Bereich. Der Snack-Potenzbereich P^{S}D ist die von D frei erzeugte stetige Snackalgebra, d. h. für jede stetige Snackalgebra A und jede stetige Funktion f: D → A gibt es einen eindeutig bestimmten stetigen Snackalgebra-Homo-morphismus f^{+}: P^{S}D → A, für den gilt f^{+} ∘ {| · |}_{idl} = f.

Beweis: Es sei f_{0} die Einschränkung von f auf KD. Satz 2.2.15 liefert uns ein eindeutig bestimmtes f_{0}^{+}: S(D) → A mit f_{0}^{+} ∘ {| · |} = f_{0}. Wir spalten f_{0}^{+} auf in die Einbettung i: S(D) → P^{S}D, die jedem Snack das durch ihn erzeugte Hauptideal zuweist, und den Snackalgebra-Homomorphismus (f^{+})_{0}: KP^{S}D → A, welcher jedem solchen Hauptideal den Funktionswert seines Erzeugers unter f_{0}^{+} zuweist. Natürlich ist (f^{+})_{0} eindeutig bestimmt, und es gilt für alle k ∈ KD:

f_{0}(k) = f_{0}^{+}({|k|}) = (f^{+})_{0} ∘ i({|k|}) = (f^{+})_{0}({|k|}_{D}) .

Für die eindeutig bestimmte Fortsetzung von (f^{+})_{0} zu einem stetigen Snackalgebra-Homomorphismus f^{+}: P^{S}D → A gilt damit f = f^{+} ∘ {| · |}_{idl}, so daß f^{+} der gesuchte Homomorphismus ist.

2.3 Das Snack-Potenzlokal

Mit dem Snack-Potenzbereich haben wir einen Bereich zur Modellierung mengenwertiger Datentypen gefunden. Um seine Eignung für das bereichstheoretische Datenbankmodell zu prüfen, könnte man nun dazu übergehen, eine auf Bereichen aufbauende Typstruktur und Operationen für Datenbanken zu definieren. Da die Objekte der Datenbank, auf die sich die Operationen beziehen, immer vom Mengentyp, also Snacks, sein werden, ist eine einfachere Darstellung der Snack-Konstruktion jedoch wünschenswert. Wir gewinnen solch eine Darstellung auf dem von Abramsky [Abr91b] vorgezeichneten Weg. Er beschreibt Datenelemente (eines Bereiches) durch die Eigenschaften, die sie erfüllen. Die Menge dieser Eigenschaften hat die mathematische Struktur eines Prälokals.

Definition 2.3.1 Ein kohärentes algebraisches Prälokal A ist eine prägeordnete Algebra mit zwei binären Operationen ∨ und ∧, zwei Konstanten 0 und 1 und einstelligen Prädikaten E und T auf A derart, daß a∨b ein Supremum und a∧b ein Infimum für {a, b} und 0 ein kleinstes und 1 ein größtes Element ist. Die Präordnung auf A wird mit ≲ bezeichnet, die dazugehörige Äquivalenzrelation mit ≈. Das Prädikat E(a) ist genau dann erfüllt, wenn a kein kleinstes Element ist, das Prädikat T(a) genau dann, wenn a kein größtes Element ist. Schließlich muß jedes Element von A endliches Supremum ∨-primer Elemente sein.

Ein Scott-Prälokal hat zusätzlich die Eigenschaft, daß das Infimum einer endlichen Menge ∨-primer Elemente wieder ∨-prim oder äquivalent zu 0 ist.

Es erscheint einsichtig, daß es auf der Menge der Eigenschaften die Konjunktion ∨ und die Disjunktion ∧ geben soll. Auch die Formeln 0 für die nie erfüllte Eigenschaft und 1 für die immer erfüllte Eigenschaft überraschen nicht. Hervorzuheben ist allerdings, daß die Menge der Eigenschaften nicht geordnet, sondern nur prägeordnet ist, d. h. es fehlt die Antisymmetrie. Dies erklärt sich dadurch, daß wir im weiteren nicht immer die Menge der Eigenschaften selbst betrachten werden, sondern die Menge der logischen Formeln, welche die Eigenschaften beschreiben. Für eine Eigenschaft mag es aber viele syntaktisch verschiedene sie beschreibende Formeln geben. Als Beispiel sei die nie erfüllte Eigenschaft genannt, die durch 0, aber auch durch die Formeln 0∧a, 0∧(a∨b), … beschrieben wird. Diese Formeln sind als äquivalent zu betrachten, so daß wir eine prägeordnete Menge haben, wobei a ≲ b bedeutet ”a impliziert b“. Vor dem Hintergrund fehlender Antisymmetrie wird auch klar, daß man nicht von ”dem“ Supremum etc. sondern nur von ”einem“ Supremum etc. sprechen kann.

Die Prädikate E und T werden später beim Typaufbau für Prälokale benötigt. Dieser soll als rein syntaktische Konstruktion durchgeführt werden, so daß die entsprechenden Eigenschaften durch Mittel der Syntax verfügbar gemacht werden müssen. Es sei darauf hingewiesen, daß in [Abr91b] ein anderes Prädikat C in die Definition aufgenommen wurde, das genau für die ∨-primen Elemente erfüllt ist. Abramsky benötigt dieses Prädikat für die Konstruktion des Funktionentyps, den wir nicht verwenden. Statt des Prädikats C genügt für unsere Zwecke das Prädikat E, das sich mit Hilfe von C ausdrücken ließe und das für die Existenz eines Elementes mit der gegebenen Eigenschaft steht. Von Abramsky übernehmen wir das Prädikat T, dessen Bezeichnung von Abramskys Anwendung herrührt, wo es die Terminierung eines Prozesses ausdrückt. Die übrigen Teile der Definition 2.3.1 erklären sich aus der Struktur der betrachteten Eigenschaften. Als Eigenschaften für die Elemente eines Bereiches werden dessen kompakt-offenen Teilmengen herangezogen. Ein Element erfüllt die durch eine derartige Menge gegebene Eigenschaft, wenn es Element der Menge ist. Die Menge KΩ(D) der kompakt-offenen Mengen eines Bereiches D mit den Operationen ∪ und ∩ und den Konstanten ∅ und D hat gerade die Struktur eines Prälokals; seine Elemente sind durch die Teilmengenrelation geordnet. Daß jedes Element eines Prälokals das Supremum endlich vieler ∨-primer Elemente ist, entspricht der Eigenschaft kompakt-offener Mengen, die Vereinigung endlich vieler solcher oberer Mengen zu sein, die von genau einem kompakten Element erzeugt sind. Das sind in KΩ(D) gerade die ∨-primen Elemente. In Bereichen ist zudem der Schnitt zweier solcher Mengen vom Supremum der erzeugenden kompakten Elemente erzeugt, falls dieses Supremum existiert, andernfalls ist der Schnitt leer. Dies führt zu der zusätzlichen Bedingung für Scott-Prälokale.

Die folgende Definition präzisiert, in welchem Sinne Bereiche durch Prälokale beschrieben werden:

Definition 2.3.2 Es seien A und B Prälokale. Eine Funktion Φ: A → B ist ein Prä-Isomorphismus, wenn Φ surjektiv, ordnungserhaltend und ordnungsreflektierend ist. Ist A ein Scott-Prälokal und D ein Bereich und gibt es einen Prä-Isomorphismus ⟦·⟧: A → KΩ(D), so nennen wir A eine lokalische Beschreibung von D durch ⟦·⟧.

Mit der Feststellung, daß A eine lokalische Beschreibung von D ist, wird ausgedrückt, daß A und KΩ(D), der Verband der kompakt-offenen Teilmengen von D, im wesentlichen übereinstimmen. Allerdings bleibt festzuhalten, daß die Übereinstimmung nicht so weit geht, daß beide Strukturen isomorph sind. Das Prälokal ist nur prägeordnet, während KΩ(D) durch ⊆ sogar geordnet ist. Erst eine Faktorisierung von A bezüglich der durch die Präordnung gegebenen Äquivalenzrelation ergibt eine zu KΩ(D) isomorphe Struktur.

Die Bedeutung der Beschreibung von Elementen durch (Beschreibungen) kompakt-offene(r) Mengen ergibt sich aus der Stone-Dualität, denn es läßt sich nicht nur aus einem Bereich D mit KΩ(D) ein Scott-Prälokal gewinnen. Vielmehr erhält man aus jedem Scott-Prälokal A mit dem Spektrum spec(A), d. h. der Menge der primen Filter von A (geordnet durch ⊆), einen Bereich, und es gilt für alle Bereiche D:

spec(KΩ(D)) ≅ D .

Wir können hier nicht auf die Details der Theorie eingehen und verweisen dazu auf [Abr91b, AJ95, Vic89, Joh82, GHK^{+}80].

Im folgenden geht es darum, eine lokalische Beschreibung des Snack-Potenzberei-ches eines Bereiches D zu gewinnen. In [Abr91b, AJ95] ist die generelle Vorgehensweise für das Erzeugen lokalischer Darstellungen solcher Bereiche dargelegt, die aus anderen Bereichen durch Bereichskonstruktionen hervorgehen. Stets nimmt man an, daß für die Ausgangsbereiche lokalische Beschreibungen gegeben sind. Deren Elemente korrespondieren zu kompakt-offenen Mengen der Ausgangsbereiche. Wenn man angeben kann, wie aus den kompakt-offenen Mengen der Ausgangsbereiche solche der konstruierten Bereiche entstehen, so läßt sich das auf die korrespondierenden syntaktischen Darstellungen der kompakt-offenen Mengen, also auf die Prälokale, übertragen. Nun wird man in der Regel nicht alle kompakt-offenen Mengen des konstruierten Bereiches in direkter Weise aus den kompakt-offenen Mengen der Ausgangsbereiche gewinnen können. Ziel ist es dann, zumindest so viele zu erhalten, daß sich die übrigen aus ihnen durch Schnitte und Vereinigungen erzeugen lassen. Auf der abstrakteren Ebene der Prälokale heißt dies, es ist eine Menge von Erzeugern gesucht derart, daß sich jedes Element der angestrebten lokalischen Beschreibung als Term aus Erzeugern, den Verknüpfungen ∧ und ∨ und den Konstanten 0 und 1 ergibt. Die Menge dieser Terme trägt zunächst noch keine Struktur; die Eigenschaften eines Prälokals müssen erst noch durch Axiome und Regeln erzwungen werden.

Das Auffinden geeigneter Erzeuger und der richtigen Axiome und Regeln ist die eigentliche Aufgabe bei der Suche nach einer lokalischen Beschreibung. Für die Snack-Potenzkonstruktion sind das Plotkin- [Abr91b] und das Mixed-Potenzlokal [Gun92] gute Vorbilder. Beide gewinnen aus jedem Element a einer lokalischen Beschreibung eines Bereiches D zwei Erzeuger □a und ♢a des entsprechenden Potenzlokals. Hierin kommt zum Ausdruck, daß im Potenzbereich Teilmengen von D in zweierlei Interpretationen verwendet werden, die durch die Ordnungen ≤^{♯} und ≤^{♭} gegeben sind. Jedes der Symbole □ und ♢ bezieht sich auf eine dieser Interpretationsweisen: □ drückt die ≤^{♯}-Interpretation aus, ♢ die ≤^{♭}-Interpretation. Der Unterschied zwischen beiden Potenzlokalen tritt in den Axiomen und Regeln (und natürlich der Interpretationsfunktion ⟦·⟧) zutage. Je allgemeiner die Potenzkonstruktion ist (d. h. je ”komplizierter“ der Potenzbereich ist), desto einfacher wird die lokalische Darstellung. Damit genügt es für das Snack-Potenzlokal im wesentlichen, die Axiome und Regeln des Plotkinoder des Mixed-Potenzlokals geeignet abzuschwächen.

Man erhält dann

Definition 2.3.3 Das Snack-Potenzlokal^{3} P^{S}(A) eines Scott-Prälokals A ist definiert als die Termalgebra vom Typ (∧, ∨, 0, 1) über der Erzeugendenmenge

G_{P} = {□a | a ∈ A} ∪ {♢a | a ∈ A} .

Präordnung, E- und T-Prädikat werden durch Axiome und Regeln definiert, von denen wir zuerst die angeben, die sich auf die Erzeuger beziehen: Axiome

(□ − ∧) □(⋀_{i∈I} a_{i}) ≈ ⋀_{i∈I} □a_{i} (I endlich),
(♢ − 0)  ♢(0) ≈ 0,
(♢ − ∧)  □a ∧ ♢b ≲ ♢(a ∧ b),
(P − E − □) E(□a).

Regeln

(P − ≲)  Wenn a ≲ b, dann □a ≲ □b, ♢a ≲ ♢b,
(P − E − ♢) Wenn E(a), dann E(♢a),
(P − T − □) Wenn T(a), dann T(□a),
(P − T − ♢) Wenn E(a), dann T(♢a).

Hinzu kommen Axiome und Regeln, die die Struktur eines Prälokals erzwingen; sie hängen nicht von den Erzeugern ab, sondern verwenden Elemente des Potenzlokals:

(pr) \{ \begin{matrix}φ ≲ φ, \\ Wenn φ ≲ ψ und ψ ≲ χ, dann φ ≲ χ, \\ Wenn φ ≲ ψ und ψ ≲ φ, dann φ ≈ ψ, \\ Wenn φ ≈ ψ, dann φ ≲ ψ, ψ ≲ φ, \end{matrix}

(sup) \{ \begin{matrix}0 ≲ φ, \\ Wenn φ ≲ χ und ψ ≲ χ, dann φ ∨ ψ ≲ χ, \\ φ ≲ φ ∨ ψ und ψ ≲ φ ∨ ψ, \end{matrix}

3Man beachte, daß das Symbol P^{S} dadurch in zweierlei Verwendungen auftritt: Zur Konstruktion des Snack-Potenzbereiches und des Snack-Potenzlokals. Welche der beiden Bedeutungen gemeint ist, wird durch das jeweilige Argument von P^{S} klar.

(inf) \{ \begin{matrix}φ ≲ 1, \\ Wenn φ ≲ ψ und φ ≲ χ, dann φ ≲ ψ ∧ χ, \\ φ ∧ ψ ≲ φ und φ ∧ ψ ≲ ψ, \end{matrix}
(dist) φ ∧ (ψ ∨ χ) ≈ (φ ∧ ψ) ∨ (φ ∧ χ),
(t)  \{ \begin{matrix}Wenn T(φ) und ψ ≲ φ, dann T(ψ), \\ T(φ_{1}), …, T(φ_{n}), dann T(⋁_{i=1}^{n} φ_{i}), \end{matrix}
(e)  Wenn E(φ) und φ ≲ ψ, dann E(ψ).

Definition 2.3.4 Das Prälokal A sei eine lokalische Beschreibung des Scott-Be-reichs D durch ⟦·⟧_{A}. Die Interpretationsfunktion ⟦·⟧: P^{S}(A) → KΩ(P^{S}(D)) für das Snack-Potenzlokal definieren wir auf den Erzeugern durch

⟦□a⟧ = {s ∈ P^{S}(D) | ∃(U, L) ∈ s. U ⊆ ⟦a⟧_{A}} ,
⟦♢a⟧ = {s ∈ P^{S}(D) | ∃(U, L) ∈ s. ∃L ∈ L. L ⊆ ⟦a⟧_{A}} ;

sie wird auf P^{S}(A) zu einem Verbandshomomorphismus fortgesetzt.

Die Behauptung ist, daß P^{S}(A) eine lokalische Beschreibung des Snack-Potenzbe-reiches P^{S}(D) durch ⟦·⟧ ist, falls A eine lokalische Beschreibung von D vermöge ⟦·⟧_{A} ist. Der Beweis hiervon gliedert sich in eine Reihe von Schritten wie sie in [AJ95] angeführt sind. Manche davon hängen nicht von der konkret betrachteten Konstruktion ab und können im Detail [AJ95] entnommen werden. Wir werden hier nur diejenigen Schritte ausführlich vollziehen, die von der betrachteten Konstruktion abhängen.

Wir beginnen mit:

Lemma 2.3.5 Die Interpretationsfunktion ⟦·⟧ bildet Elemente von P^{S}(A) auf kompakt-offene Teilmengen von P^{S}(D) ab.

Beweis: Der Beweis wird durch Induktion über den Aufbau der Terme geführt.

Die kompakt-offenen Teilmengen eines Bereiches sind diejenigen oberen Mengen, die von endlich vielen kompakten Elementen des Bereiches erzeugt werden. Damit sieht man direkt, daß ⟦0⟧ = ∅ und ⟦1⟧ = P^{S}(D) kompakt-offen sind.

Für die Interpretation der Erzeuer ♢a (a ≉ 0) und □a kann man sogar zeigen, daß sie von der Form ↑k für kompakte k ∈ P^{S}(D) sind.

Zunächst betrachten wir einen Erzeuger der Form □a. Der kleinste Snack (U, L) mit U ⊆ ⟦a⟧_{A} ist (⟦a⟧_{A}, ∅). Da ⟦a⟧_{A} nach Voraussetzung eine kompakt-offene Menge ist, ist dies in der Tat ein Snack. Jedes Ideal in ⟦□a⟧ muß diesen Snack enthalten, und das kleinste solche Ideal ist ↓(⟦a⟧_{A}, ∅). Dies ist ein kompaktes Element in P^{S}(D). Jedes größere Ideal enthält diesen Snack natürlich auch, also ist ⟦□a⟧ = ↑_{P^{S}(D)}(↓(⟦a⟧_{A}, ∅)).

Für Erzeuger der Form ♢a mit a ≉ 0 ist der kleinste Snack (U, L), in dem es eine Menge L ∈ L mit L ⊆ ⟦a⟧_{A} gibt, durch (D, {⟦a⟧_{A}}) gegeben. Wie oben ergibt sich ⟦♢a⟧ = ↑_{P^{S}(D)}(↓(D, {⟦a⟧_{A}})), was wieder eine einelementig erzeugte kompakt-offene Menge ist. Ist a ≈ 0, so ist ⟦♢a⟧ kompakt-offen, denn ⟦♢a⟧ = ⟦♢0⟧ = ⟦0⟧ = ∅.

Da in einem Bereich Vereinigung und Schnitt kompakt-offener Mengen kompakt offen sind, folgt schließlich, daß mit ⟦φ⟧ und ⟦ψ⟧ auch ⟦φ ∧ ψ⟧ = ⟦φ⟧ ∩ ⟦ψ⟧ und ⟦φ ∨ ψ⟧ = ⟦φ⟧ ∪ ⟦ψ⟧ kompakt-offen sind.

Als nächstes beweisen wir, daß aus den angegebenen Axiomen und Regeln durch Anwendung von ⟦·⟧ wahre Aussagen über kompakt-offene Teilmengen von P^{S}(D) entstehen, d. h. daß die Axiome und Regeln korrekt bezüglich ⟦·⟧ sind.

Für die Axiome und Regeln, in denen nicht Erzeuger des Potenzlokals, sondern allgemeine Formeln verwendet werden, ist dies offensichtlich, da die Symbole ≲, ∧, ∨ zu den mengentheoretischen Symbolen ⊆, ∩, ∪ werden, für die die angegebenen Beziehungen erfüllt sind. Lediglich zum Axiom (dist) sei hier noch ein Wort gesagt: In der Definition eines Prälokals ist die Distributivität nicht explizit verlangt. Sie ergibt sich jedoch daraus, daß jedes Element Supremum endlich vieler ∨-primer Elemente ist. Diese Eigenschaft ist für das Potenzlokal nicht durch ein Axiom sichergestellt. Daher verlangen wir die Distributivität ausdrücklich, und unter ihrer Verwendung werden wir die Erzeugung durch ∨-prime Elemente beweisen können.

Wir wenden uns nun dem Beweis der Korrektheit der für das Potenzlokal spezifischen Axiome und Regeln zu und beginnen mit der Regel (P − ≲). Ist a ≲ b im Prälokal A, so gilt ⟦a⟧_{A} ⊆ ⟦b⟧_{A}, da ⟦·⟧_{A} ein Prä-Isomorphismus ist. Ist nun s ∈ ⟦□a⟧, so gibt es einen Snack (U, L) ∈ s mit U ⊆ ⟦a⟧_{A} ⊆ ⟦b⟧_{A}, weshalb s ∈ ⟦□b⟧ ist. Auf die gleiche Weise erhalten wir ⟦♢a⟧ ⊆ ⟦♢b⟧. Ist nämlich s ∈ ⟦♢a⟧, so gibt es einen Snack (U, L) ∈ s mit einem L ∈ L derart, daß L ⊆ ⟦a⟧_{A} ⊆ ⟦b⟧_{A}, also s ∈ ⟦♢b⟧.

Die Richtung ⟦□(⋀_{i∈I} a_{i})⟧ ⊆ ⟦⋀_{i∈I} □a_{i}⟧ des Axioms (□ − ∧) folgt aus der Korrektheit von (P − ≲). Um die andere Richtung zu zeigen, sei s ∈ ⟦⋀_{i∈I} □a_{i}⟧ = ⋂_{i∈I}⟦□a_{i}⟧. Dann gibt es für jedes i ∈ I einen Snack (U^{i}, L^{i}) ∈ s mit U^{i} ⊆ ⟦a_{i}⟧_{A}. Da s als Ideal gerichtet ist, haben diese (U^{i}, L^{i}) ein Supremum (U, L) ∈ s, wobei U = ⋂_{i∈I} U^{i} gilt. Nun ist ⋂_{i∈I} U^{i} ⊆ ⋂_{i∈I}⟦a_{i}⟧_{A} = ⟦⋀_{i∈I} a_{i}⟧_{A}, weshalb s ∈ ⟦□ ⋀_{i∈I} a_{i}⟧ gilt.

Das Axiom (♢ − 0) ist korrekt, denn die Interpretation ⟦♢0⟧ = {s ∈ P^{S}(D) | ∃(U, L) ∈ s. ∃L ∈ L. L ⊆ ∅} muß leer sein, da die Mengen L der zweiten Komponente eines Snacks nicht leer sein können.

Nun zu (♢ − ∧): Ist s ∈ ⟦□a ∧ ♢b⟧, so gibt es ein (U, L) ∈ s mit U ⊆ ⟦a⟧_{A} und einem L ∈ L, für das L ⊆ ⟦b⟧_{A} gilt. Da L ⊆ U ist, haben wir L ⊆ ⟦a⟧_{A} ∩ ⟦b⟧_{A} = ⟦a ∧ b⟧_{A}, also s ∈ ⟦♢(a ∧ b)⟧.

Oben sahen wir schon, daß ⟦□a⟧ = ↑_{P^{S}(D)}(↓(⟦a⟧_{A}, ∅)) ist. Dies ist nicht leer, weshalb (P − E − □) korrekt ist. Ist ⟦a⟧_{A} ≠ D, d. h. gilt T(a), dann ist ↑_{P^{S}(D)}(↓(⟦a⟧_{A}, ∅)) auch von P^{S}(D) verschieden, d. h. es gilt T(□a). Folglich ist auch (P − T − □) korrekt.

Auch ⟦♢a⟧ konnten wir explizit angeben. Für a ≉ 0, d. h. bei Gültigkeit von E(A), ist ⟦♢a⟧ = ↑_{P^{S}(D)}(↓(D, {⟦a⟧_{A}})), was sowohl von ∅ als auch von P^{S}(D) verschieden ist. Somit folgt die Korrektheit von (P − E − ♢) und (P − T − ♢).

Damit ist gezeigt:

Lemma 2.3.6 Die Axiome und Regeln für das Snack-Potenzlokal sind korrekt bezüglich der Interpretationsfunktion ⟦·⟧.

Wir sind oben schon darauf eingegangen, weshalb wir im Gegensatz zu Abramsky kein eigenes Prädikat für ∨-prime Elemente eingeführt haben. Um eine Darstellung eines Elements aus ∨-primen Elementen angeben zu können, werden wir dennoch im folgenden von gewissen Elementen der Termalgebra nachweisen, daß sie ∨-prim sind.

Lemma 2.3.7 Es seien a, b_{1}, …, b_{n} ∈ A (n ∈ ℕ_{0}) so, daß 0 ≉ b_{i} ≲ a für alle i ∈ {1, …, n}. Dann ist das Element

(⋆) □ a ∧ ⋀_{i=1}^{n} ♢b_{i}

∨-prim im Snack-Potenzlokal P^{S}(A).

Der Beweis dieses Lemmas gliedert sich in mehrere Schritte:

Proposition 2.3.8 Das Kriterium aus Lemma 2.3.7 ist korrekt, d. h. das Bild eines Elements der Form (⋆) unter ⟦·⟧ ist koprim im Verband KΩP^{S}(D) der kompaktoffenen Teilmengen von P^{S}(D).

Beweis: Wir wissen bereits, wie die Erzeuger □a und ♢a durch ⟦·⟧ interpretiert werden; diese Interpretationen sind ∨-prim in KΩP^{S}(D), d. h. sie werden von einem Hauptideal von Snacks erzeugt. Das Supremum der diese Hauptideale erzeugenden Snacks erzeugt ein Hauptideal, das seinerseits die Interpretation des Ausdrucks (⋆) erzeugt:

⟦□a ∧ ⋀_{i=1}^{n} ♢b_{i}⟧ = ⟦□a⟧ ∩ ⋂_{i=1}^{n}⟦♢b_{i}⟧
= ↑_{P^{S}(D)}(↓(⟦a⟧_{A}, ∅)) ∩ ⋂_{i∈I} ↑_{P^{S}(D)}(↓(D, {⟦b_{i}⟧_{A}}))
= ↑_{P^{S}(D)}(↓((⟦a⟧_{A}, ∅) ⊔ ⨆_{i∈I}(D, {⟦b_{i}⟧_{A}})))
= ↑_{P^{S}(D)}(↓(⟦a⟧_{A}, {⟦b_{i}⟧_{A} | i = 1, …, n})).

Offensichtlich ist dies ∨-prim in KΩP^{S}(D), so daß die Korrektheit unseres Kriteriums gezeigt ist.

Proposition 2.3.9 Es seien φ, ψ ∈ P^{S}(A) von der Form (⋆). Gilt ⟦φ⟧ ⊆ ⟦ψ⟧, so auch φ ≲ ψ.

Beweis: Es ist

φ = □a ∧ ⋀_{i∈I} ♢b_{i} (0 ≉ b_{i} ≲ a für alle i ∈ I),
ψ = □c ∧ ⋀_{j∈J} ♢d_{j}  (0 ≉ d_{j} ≲ c für alle j ∈ J).

Es ist ⟦φ⟧ = ↑_{P^{S}(D)}(↓(⟦a⟧_{A}, {⟦b_{i}⟧_{A} | i ∈ I})) und ⟦ψ⟧ = ↑_{P^{S}(D)}(↓(⟦c⟧_{A}, {⟦d_{j}⟧_{A} | j ∈ J})), wie wir oben gesehen haben. Wegen ⟦φ⟧ ⊆ ⟦ψ⟧ ist der Snack, der ⟦φ⟧ erzeugt, größer als der, welcher ⟦ψ⟧ erzeugt. Also ist ⟦a⟧_{A} ⊆ ⟦c⟧_{A}, und für jedes j ∈ J gibt es ein i_{j} ∈ I mit ⟦d_{j}⟧_{A} ⊇ ⟦b_{i_{j}}⟧_{A}. Die Interpretationsfunktion ⟦·⟧_{A} ist ordnungsreflektierend; folglich ist a ≲ c und d_{j} ≳ b_{i_{j}} für alle j ∈ J. Unter Verwendung der Monotonie von □ und ♢ bekommen wir schließlich

φ = □a ∧ ⋀_{i∈I} ♢b_{i} ≲ □a ∧ ⋀_{j∈J} ♢b_{i_{j}} ≲ □c ∧ ⋀_{j∈J} ♢d_{j} = ψ.

Proposition 2.3.10 Es sei A ein Scott-Prälokal. Dann ist jedes Element x ∈ P^{S}(A) das Supremum endlich vieler Elemente der Form (⋆).

Beweis: Zunächst bemerken wir, daß die Äquivalenz

(D) □ a ∧ ♢b ≈ □a ∧ ♢(a ∧ b)

aus Axiom (♢ − ∧) und der Monotonie von □ und ♢ folgt.

Ist nun ein x ∈ P^{S}(A) gegeben, so formen wir x mit Hilfe des Distributivgesetzes in eine äquivalente (endliche) Disjunktion endlicher Konjunktionen um. Eventuell vorkommende Konstanten 0 und 1 schreiben wir unter Verwendung von (♢ − 0) und (□ − ∧) als ♢0 bzw. □1. Damit sind die Konjunktionen aus Erzeugern aufgebaut und von der Form

⋀_{i∈I} □a_{i} ∧ ⋀_{j∈J} ♢b_{j} (I, J endlich).

Dies läßt sich weiter vereinfachen. Mit Hilfe von (□ − ∧) fassen wir alle □-Erzeuger zu einem Term □a zusammen. Wegen der Beziehung (D) können wir zusätzlich annehmen, daß b_{j} ≲ a für alle j ∈ J erfüllt ist. Damit gelangen wir zu einem Ausdruck

□a ∧ ⋀_{j∈J} ♢b_{j} ,

der schon von der Form (⋆) ist, sofern b_{j} ≉ 0 für alle j ∈ J. Ist ein b_{j} äquivalent zu 0, so ist wegen (♢ − 0) die ganze Konjunktion äquivalent zu 0 und kann aus der betrachteten Disjunktion von Konjunktionen entfernt werden. Übrig bleibt eine (evtl. leere) endliche Disjunktion von Elementen der geforderten Gestalt, die äquivalent zu x ist.

Damit können wir den Beweis von Lemma 2.3.7 formulieren:

Beweis: [Von Lemma 2.3.7] Ist φ von der Form (⋆) und ⋁_{i∈I} ψ_{i} ≳ φ in P^{S}(A), so läßt sich die Situation mit ⟦·⟧ zu den kompakt-offenen Teilmengen von P^{S}(D) transportieren, d. h. ⋃_{i∈I}⟦ψ_{i}⟧ ≳ ⟦φ⟧. Wegen Proposition 2.3.10 können wir annehmen, daß auch die ψ_{i} von der Form (⋆) sind, und wegen der Korrektheit des Kriteriums (⋆) (Proposition 2.3.8) sind die jeweiligen Bilder unter ⟦·⟧ ∨-prime kompakt offene Mengen. So gibt es ein i_{0} ∈ I mit ⟦ψ_{i_{0}}⟧ ⊇ ⟦φ⟧. Mit Proposition 2.3.9 folgt dann ψ_{i_{0}} ≳ φ.

Als nächstes zeigen wir, daß jedes ∨-prime Element im Verband KΩP^{S}(D) der kompakt-offenen Teilmengen von P^{S}(D) die Interpretation eines ∨-primen Elements der Form (⋆) ist.

Lemma 2.3.11 Zu jedem ∨-primen Element V ∈ KΩP^{S}(D) gibt es ein φ ∈ P^{S}(A) von der Form (⋆) mit ⟦φ⟧ = V.

Beweis: Als ∨-primes Element in KΩP^{S}(D) wird V von einem Ideal erzeugt, das seinerseits von einem einzigen Snack (U, {L_{1}, …, L_{k}}) erzeugt wird. Da A eine lokalische Beschreibung von D ist und U, L_{1}, …, L_{k} kompakt-offene Teilmengen von D sind, gibt es Elemente a, a_{1}, …, a_{k} ∈ A mit ⟦a⟧_{A} = U und ⟦a_{i}⟧_{A} = L_{i} für i = 1, …, k. Ferner ist jedes L_{i} (i = 1, …, k) eine nichtleere Teilmenge von U, d. h. 0 ≉ a_{i} ≲ a für i = 1, …, k. Die Formel □a∧⋀_{i=1}^{k} ♢a_{i} hat die geforderte Form und die Interpretation ↑_{P^{S}(D)}↓(U, {L_{1}, …, L_{k}}) = V.

Auf eine allgemeine, nicht von unserer Konstruktion abhängige Weise kann nun gezeigt werden, daß ⟦·⟧ ein Prä-Isomorphismus ist. In [AJ95] sind diese Schritte durchgeführt, weshalb wir sie hier nur kurz angeben wollen. Unter Verwendung von Lemma 2.3.10 und Lemma 2.3.9 zeigt man, daß ⟦·⟧ ordnungsreflektierend ist. Mit Lemma 2.3.11 folgt dann die Surjektivität von ⟦·⟧. Daß das Potenzlokal tatsächlich ein Scott-Prälokal ist, folgt aus der Tatsache, daß ⟦·⟧ ordnungserhaltend und -reflektie-rend ist und daß KΩP^{S}(D) selbst ein Scott-Prälokal ist. Damit ergibt sich schließlich, daß ⟦·⟧ ein Prä-Isomorphismus ist.

Somit haben wir:

Satz 2.3.12 Ist das Scott-Prälokal A eine lokalische Beschreibung des Scott-Berei-ches D, so ist das Snack-Potenzlokal P^{S}(A) eine lokalische Beschreibung des Snack-Potenzbereiches P^{S}(D).

Die Stone-Dualität zwischen Bereichen und Scott-Prälokalen liefert daraus:

Korollar 2.3.13 Für jedes Scott-Prälokal ist

P^{S}(specA) ≅ spec(P^{S}(A)).

Diese Isomorphie erlaubt es uns, wahlweise in der Sprache der Bereiche oder in der der Prälokale über Approximationen von Mengen zu sprechen. Tatsächlich erscheint es naheliegender die logische Sprache zu verwenden: Selbst als wir Snacks in der Bereichssprache beschrieben, trennten wir die Bedeutung der Komponenten der Snacks. Um partiell beschriebene Relationen in einem Datenbanksystem anzugeben, könnte man nun Relationen mit partiellen Einträgen zusätzlich mit einer Kennung □ oder ♢ versehen. Die Approximation einer Menge besteht dann aus mehreren solchermaßen markierten Relationen, die man in der logischen Betrachtung konjunktiv verknüpft denkt.

Zudem mag die hier gewonnene Logik als Fragment in eine ausdrucksstärkere Logik eingehen, mit der — im Sinne einer Verallgemeinerung des Relationenkalküls für Relationale Datenbanken — Anfragen an ein Datenbanksystem gestellt werden können.

46 KAPITEL 2. DIE SNACK-POTENZKONSTRUKTION

Ein Typsystem für Datenbanken

In der Informatik besteht seit langem der Wunsch, daß die Typen der Datenbanken und Programmiersprachen dieselben sein sollen, damit durch Befehle einer Programmiersprache direkt auf Objekte der Datenbank zugegriffen werde kann. Im zweiten Abschnitt dieses Kapitels werden wir eine Typsystem vorstellen, daß in der Tat auch das einer Programmiersprache sein könnte. Es wird aber um eine Struktur angereichert sein, die für die Anwendung in Datenbanken spezifisch ist und die in einer reinen Programmiersprache nicht gebraucht wird, nämlich eine Subtyprelation. Jedem Typ ist eine Wertemenge für die Objekte dieses Typs zugeordnet. In den Datenbankoperationen sind oft aber gar nicht diese Werte selbst von Interesse, sondern nur gewisse Teilinformationen der durch die Werte gegebenen Gesamtinformation. Die Subtypen eines Typs korrespondieren zu den abfragbaren Teilstücken der Gesamtinformation und sind natürlich ihrerseits Typen. Diese Zusatzstruktur rechtfertigt es, von Typen für Datenbanken zu sprechen, auch wenn man sich die Typen selbst auch in einer Programmiersprache vorstellen kann.

So wie wir im vorangegangenen Kapitel die Snack-Potenzkonstruktion zur Interpretation mengenwertiger Typen sowohl für Bereiche als auch für Prälokale angegeben haben, wollen wir im weiteren für Datenbanktypen stets diese zwei Arten der Interpretation vorsehen. Der erste Abschnitt dieses Kapitels befaßt sich damit, wie wir auf der Ebenen der Bereiche und der Prälokale Entsprechungen für eine Subtyprelation finden, insbesondere dann, wenn wir einen Mengenkonstruktor durch die Snack-Konstruktion interpretieren wollen. Im zweiten Abschnitt geben wir ein konkretes Typsystem an, bei dem wir, von nur einem — sehr einfachen — Grundtyp ausgehend, unter Verwendung einiger Typkonstruktoren ein reichhaltiges Sortiment von Typen gewinnen. Für diese Typen geben wir eine logische und eine bereichstheoretische Interpretation an, die durch die Stone-Dualität miteinander verbunden sind. Im dritten Abschnitt führen wir für dieses Typsystem eine Subtyprelation ein und zeigen, daß sie durch die im ersten Abschnitt für Bereiche und Prälokale vorgestellten Unterstrukturen interpretiert wird.

3.1 Unterstrukturen

Im relationalen Datenbankmodell lassen sich die Unterstrukturen einfach angeben. Zu jeder Relation gehört eine Menge von Attributnamen, das Schema der Relation. Die Elemente der Relation sind Tupel, deren Struktur durch das Schema gegeben ist: Zu jedem der Attribute enthalten sie einen Wert aus der dem Attribut zugeordneten Wertemenge, d. h. sie sind Elemente des Produkts dieser Wertemengen, und die Menge möglicher Werte einer Relation ist gerade dieses Produkt. Jedes Subschema, d. h. jede Teilmenge des Schemas einer Relation, spezifiziert eine Unterstruktur hiervon, nämlich das Produkt der Wertemengen, die den im Subschema enthaltenen Attributen zugeordnet sind. Der Übergang von der Wertemenge eines Schemas zu der eines Subschemas kann demnach durch die Projektion auf den Faktor eines kartesischen Produktes erfolgen, und in der Tat sind derartige Projektionen wesentlicher Bestandteil aller relationalen Datenbankabfragesprachen. Wie wir in Abschnitt 1.2 beschrieben, erlauben Buneman et al. in [BJO91], die Tupelidee aufgebend, beliebige Bereiche als Wertemengen für Datenbankobjekte. Damit mußten auch neue Unterstrukturen für die Projektion von Datenbankobjekten gefunden werden. Hierzu schlugen sie die später [JLP92] Semi-Faktoren genannten Teilmengen eines Bereichs vor:

Definition 3.1.1 Ein stabiler Unterbereich A eines Bereichs D ist eine untere Teilmenge von D, die unter allen existierenden Suprema abgeschlossen ist. Die Projektion p_{A} auf A ist für alle x ∈ D definiert durch

p_{A}(x) = ⋁{y ∈ A | y ≤ x} .

Ein stabiler Unterbereich A heißt Semi-Faktor, falls für alle x ∈ D und y ∈ A mit p_{A}(x) ≤ y die Menge {x, y} beschränkt ist.

Der Bereich D ist stets ein Semi-Faktor von sich selbst, und man sieht sofort, daß solche stabilen Unterbereiche A eines Bereichs D, für deren Elemente a ausnahmslos D_{max} ⊆ ↑a gilt, stets Semi-Faktoren sind. Denn ihre Elemente haben mit jedem Element von D eine gemeinsame obere Schranke, so daß die Bedingung für Semi-Faktoren trivialerweise erfüllt ist. Diese Semi-Faktoren nennen wir die trivialen Semi-Faktoren, da sie entweder vollständige oder gar keine Information über maximale Elemente bieten, die auf sie projiziert werden.

Wollen wir eine Subtyprelation durch Semi-Faktoren interpretieren, so ist es wünschenswert, daß Semi-Faktoren von denjenigen Bereichskonstruktionen respektiert werden, mit denen wir die verwendeten Typkonstruktoren modellieren, d. h. daß Semi-Faktoren in den Grundbereichen mit Hilfe der Typkonstruktion in Semi-Faktoren der konstruierten Bereiche übergehen. Daß man Semi-Faktoren einer disjunkten Summe oder eines Produkts von Bereichen als Summe bzw. Produkte von Semi-Faktoren der Ausgangsbereiche erhält, wurde in [BJO91] gezeigt. Mit der Interpretation mengenwertiger Typen durch den Snack-Potenzbereich sind Semi-Faktoren jedoch nicht verträglich. Dies zeigt der folgende Satz, dessen Beweis im Anhang angegeben wird.

Satz 3.1.2 Der Snack-Potenzbereich eines jeden Bereichs hat nur triviale Semi-Faktoren.

Damit erzeugen insbesondere die Snacks, die aus Elementen eines Semi-Faktors aufgebaut sind, keinen Semi-Faktor im Snack-Potenzbereich, was, informell formuliert, gerade die Verträglichkeit von Substruktur und Mengentyp-Konstruktor bedeuten würde.

Semi-Faktoren scheiden damit zur Interpretation von Subtypen aus. Eine leichte Veränderung der Definition rettet die Situation: Wir verlangen nicht mehr, daß die Substrukturen untere Mengen sind. Zudem verzichten wir darauf, daß die Substruktur eine Teilmenge des betrachteten Bereichs ist. Es wird genügen, wenn Substruktur und Ausgangsbereich durch ein Einbettungs-Projektionspaar miteinander verbunden sind. Damit ist die Projektion auf die Unterstruktur bereits in der Definition gegeben. Zugleich entspricht dies der Beobachtung, daß die Wertemenge eines Subtyps streng genommen keine Teilmenge der Wertemenge des Obertyps ist, aber durch eine Einbettung als solche verstanden werden kann.

Definition 3.1.3 Ein Bereich D ist ein starker Unterbereich eines Bereichs E, falls es ein Einbettungs-Projektionspaar e: D ⇋ E:p derart gibt, daß für alle x ∈ E und y ∈ D mit p(x) ≤ y die Menge {x, e(y)} in E beschränkt ist.

Tatsächlich harmoniert diese Definition einer Unterstruktur mit der Snack-Po-tenzkonstruktion. Um dies zu zeigen, nutzen wir die Stone-Dualität aus. Hierfür definieren wir zunächst Unterstrukturen für Prälokale.

Definition 3.1.4 Es seien A und B Scott-Prälokale. Wir nennen A ein Sub-Prälokal von B (in Zeichen A ⊴ B), wenn die folgenden Bedingungen erfüllt sind:

1. A ist bezüglich ∨, ∧, 0 und 1 eine Unteralgebra von B,

2. die Präordnung auf A ist die Einschränkung der Präordnung von B auf A,

3. T_{A} = A ∩ T_{B},

4. E_{A} = A ∩ E_{B}.

Definition 3.1.5 Ein Sub-Prälokal A eines Scott-Prälokals B ist ein starkes Sub-Prälokal von B (in Zeichen A ⊴_{s} B), falls für alle a ∈ A und b ∈ B mit a ∧ b ≈ 0_{B} ein a′ ∈ A derart existiert, daß a′ ≳ b und a ∧ a′ ≈ 0_{B}.

Die Definition eines Sub-Prälokals stellt sicher, daß die durch das größere Prälokal gegebene Logik mit der des kleineren Prälokals insofern harmoniert, als die logischen Operationen auf den schon im kleineren Prälokal vorhandenen Formeln durch das größere Prälokal nicht umdefiniert werden. Mit der Definition des starken Sub-Prälo-kals kommt ein weiterer Aspekt hinzu: Durch das größere Prälokal ist eine konservative Erweiterung der Logik des Sub-Prälokals gegeben; die Bedingung aus der Definition kann man so lesen, daß es einen Widerspruch zwischen Formeln der kleineren und der erweiterten Logik nur dann gibt, wenn der Widerspruch schon zwischen (allgemeineren) Aussagen der kleineren Logik besteht.

Die Begriffe ”starker Unterbereich“ und ”starkes Sub-Prälokal“ übersetzen sich beim Übergang zwischen Bereichen und Prälokalen (mittels KΩ und spec) ineinander. Bevor wir dies präzisieren, stellen wir einige vorbereitende Betrachtungen an.

Im weiteren bezeichne κ_{D} die durch die Obermengenrelation geordnete Menge der kompakten oberen Teilmengen eines Bereichs D. Nach Proposition 4.2.15 in [AJ95] gilt:

Proposition 3.1.6 Für jeden Bereich D ist κ_{D} ein stetiger Verband, in dem A ∈ κ_{D} genau dann weit unterhalb von B ∈ κ_{D} liegt, wenn es eine Scott-offene Menge O ⊆ D gibt mit B ⊆ O ⊆ A.

Proposition 3.1.7 Aus einer stetigen Funktion f zwischen Bereichen D und E gewinnt man eine stetige Funktion f^{∗} zwischen κ_{D} und κ_{E}, indem man f^{∗}(W) := ↑f(W) für jede kompakte obere Teilmenge W von D setzt.

Beweis: Die Abbildung f^{∗} ist wohldefiniert, denn stetige Bilder und obere Abschlüsse kompakter Mengen sind kompakt.

Beim Nachweis der Stetigkeit von f^{∗} beachte man, daß κ_{D} und κ_{E} durch umgekehrte Inklusion geordnet sind. Es ist daher zu zeigen, daß f^{∗} gefilterte Schnitte kompakter oberer Mengen bewahrt.

Es sei also {W_{i}}_{i∈I} eine gefilterte Familie kompakter oberer Teilmengen von D und W = ⋂_{i∈I} W_{i}. Natürlich gilt f^{∗}(W) ⊆ ⋂_{i∈I} f^{∗}(W_{i}). Um die umgekehrte Inklusion zu zeigen, nehmen wir an, daß es ein x ∈ ⋂_{i∈I} f^{∗}(W_{i}) \ f^{∗}(W) gibt. Dann gibt es eine offene Teilmenge O von E, die f^{∗}(W) umfaßt, aber das Element x nicht enthält. Die Menge f^{−1}(O) ist offen in D und enthält ⋂_{i∈I} W_{i}. Nach dem Hofmann-Mislove Theorem gibt es dann ein i_{0} ∈ I mit W_{i_{0}} ⊆ f^{−1}(O). Nun ist aber x ∈ f^{∗}(W_{i_{0}}) ⊆ f^{∗}(e^{−1}(O)) ⊆ O, im Widerspruch zur obigen Annahme. Dies zeigt die Stetigkeit von f^{∗}.

Aus einem Einbettungs-Projektionspaar zwischen Bereichen gewinnt man ein Einbettungs-Projektionspaar zwischen den Verbänden ihrer kompakten oberen Teilmengen:

Proposition 3.1.8 Es sei e: D ⇋ E:p ein Einbettungs-Projektionspaar zwischen Bereichen. Dann bilden e^{∗} und p^{∗} ein Einbettungs-Projektionspaar zwischen den Verbänden der kompakten oberen Teilmengen κ_{D} und κ_{E}.^{1}

Beweis: Es ist p^{∗} ∘ e^{∗} = id: Dazu sei W ∈ κ_{D}. Ist w ∈ W, so ist wegen w ≥ pe(w) offenbar w ∈ p^{∗} ∘ e^{∗}(W). Ist umgekehrt w ∈ p^{∗} ∘ e^{∗}(W), so gibt es ein u ∈ e^{∗}(W) mit w=p(u). Nun liegt u über dem Bild eines Elementes w′ ∈ W unter e. Damit haben wir w = p(u) ≥ pe(w′) = w′. Da W eine obere Menge ist, folgt w ∈ W.

Es ist e^{∗} ∘ p^{∗} ≤ id: Dazu sei V ∈ κ_{E} und v ∈ V. Es ist ep(v) ≤ v und ep(v) ∈ e^{∗} ∘ p^{∗}(V). Letzteres ist eine obere Menge, also folgt v ∈ e^{∗} ∘ p^{∗}(V).

Lemma 3.1.9 Es sei e: D ⇋ E:p ein Einbettungs-Projektionspaar zwischen Bereichen. Dann gibt es zu jeder kompakten oberen Teilmenge W von D und jeder kompakt-offenen Teilmenge V ⊆ E, die e^{∗}(W) enthält, eine kompakt-offene Menge W′ ⊆ D mit e^{∗}(W) ⊆ e^{∗}(W′) ⊆ V.

Beweis: Aus e^{∗}(W) ⊆ V folgt zunächst W ⊆ e^{−1}(V). Die kompakte obere Menge W ist der gefilterte Schnitt ihrer kompakt-offenen Umgebungen. Die offene Menge e^{−1}(V) enthält diesen Schnitt. Mit dem Hofmann-Mislove Theorem folgt, daß bereits eine dieser Umgebungen in e^{−1}(V) enthalten ist. Wir nennen diese Menge W′. Es ist also W ⊆ W′ ⊆ e^{−1}(V). Wenden wir hierauf die Funktion e^{∗} an, so ergibt sich wie gewünscht e^{∗}(W) ⊆ e^{∗}(W′) ⊆ V.

1Wobei p^{∗}(V) = p(V); da p obere Mengen auf obere Mengen abbildet, erübrigt es sich, den oberen Abschluß ↑p(V) explizit zu bilden.

Ist D ein starker Unterbereich von E, so können wir natürlich nicht erwarten, daß KΩ(D) ein Sub-Prälokal von KΩ(E) ist, denn die kompakt-offenen Teilmengen von D werden in aller Regel keine kompakt-offenen Teilmengen von E sein. Da D in E durch eine Abbildung e eingebettet werden kann und Einbettungen Kompaktheit bewahren, ist für jede kompakt-offene Menge U ⊆ D mit e^{∗}(U) = ↑e(U) eine von endlich vielen kompakten Elementen erzeugte obere Menge, also eine kompakt-offene Menge in E gegeben. Betrachten wir die Projektion aus dem Einbettungs-Projektionspaar e: D ⇋ E:p, so haben wir e^{∗}(U) = p^{−1}(U); denn ist x ∈ p^{−1}(U), so gilt p(x) ∈ U, und wegen x ≥ ep(x) ist x ∈ e^{∗}(U). Ist umgekehrt x ∈ e^{∗}(U), so gibt es ein u ∈ U mit x ≥ e(u), was p(x) ≥ pe(u) = u impliziert. Da U eine obere Menge ist, folgt p(x) ∈ U, d. h. x ∈ p^{−1}(U). Die durch ⊆ geordnete Menge p^{−1}(KΩ(D)) = {e^{∗}(U) | U ∈ KΩ(D)} ist isomorph zu KΩ(D), und sie ist ein Sub-Prälokal von KΩ(E). Wir können zeigen, daß dies ein starkes Sub-Prälokal ist und formulieren dies so:

Lemma 3.1.10 Wenn D vermöge des Einbettungs-Projektionspaars e: D ⇋ E:p ein starker Unterbereich von E ist, so ist KΩ(D) bis auf Isomorphie ein starkes Sub-Prälokal von KΩ(E).

Beweis: Wir haben schon angegeben, daß das Prälokal KΩ(D) isomorph ist zu p^{−1}(KΩ(D)) = {e^{∗}(U) | U ∈ KΩ(D)} und daß dies ein Sub-Prälokal von KΩ(E) ist.

Nun nehmen wir an, daß U ∈ p^{−1}(KΩD) und V ∈ KΩE so sind, daß U ∩ V = ∅. Wir müssen eine Menge U′ ∈ p^{−1}(KΩD) finden, für die U′ ⊇ V und U ∩ U′ = ∅ gilt.

Hierzu gehen wir von e^{∗}p^{∗}(V) aus. Dies ist eine kompakte, aber nicht notwendig offene Obermenge von V. Mit F bezeichnen wir die Menge aller kompakt-offenen Obermengen von e^{∗}p^{∗}(V), und wir setzen F′ := {F ∩ U | F ∈ F}. Dies ist eine gefilterte Menge kompakt-offener Mengen. Nach dem Hofmann-Mislove Theorem [HM81, KP94] ist ⋂ F′ ≠ ∅, falls jeder der Schnitte F ∩ U nichtleer ist.

Wäre dies der Fall, so hätten wir e^{∗}p^{∗}(V) ∩ U = ⋂ F ∩ U = ⋂ F′ ≠ ∅, und es gäbe Erzeuger x von U und y von V, für die {x, ep(y)} beschränkt wäre. Mit x und ep(y) wäre auch ihr Supremum x ∨ ep(y) in e(D), da e(D) unter existierenden Suprema abgeschlossen ist. Wir hätten ep(y) ≤ x ∨ ep(y) und p(y) = pep(y) ≤ p(x ∨ ep(y)) in D. Da D ein starker Unterbereich von E ist, folgte hieraus die Beschränktheit von {y, x ∨ ep(y)}, denn ep(x ∨ ep(y)) = x ∨ ep(y) wegen x ∨ ep(y) ∈ e(D). Nun ist aber x ≤ x ∨ ep(y), so daß wir die Beschränktheit von {x, y} folgern könnten, d. h. U ∩ V ≠ ∅, im Widerspruch zur Wahl von U und V.

Folglich gibt es eine kompakt-offene Obermenge W von e^{∗}p^{∗}(V) mit W ∩ U = ∅. Diese Menge W braucht nicht in p^{−1}(KΩD) sein. Lemma 3.1.9 garantiert schließlich die Existenz einer Menge U′ ∈ p^{−1}(KΩD) mit W ⊇ U′ ⊇ e^{∗}p^{∗}(V), d. h. U′ ∩ U = ∅ und U′ ⊇ e^{∗}p^{∗}(V) ⊇ V. Dies vollendet den Beweis.

Um zu zeigen, daß starke Sub-Prälokale durch den Funktor spec in starke Unterbereiche übersetzt werden, benötigen wir das ”Prime Filter Theorem“:

Lemma 3.1.11 Ist I ein Ideal in einem distributiven Verband und F ein Filter, der unter den von I disjunkten Filtern maximal ist, so ist F prim.

Nun können wir zeigen:

Lemma 3.1.12 Ist A ein starkes Sub-Prälokal von B, so ist spec(A) ein starker Unterbereich von spec(B).

Beweis: Das Einbettungs-Projektionspaar ist gegeben durch e: specA → specB, e(G) = ↑_{B}G und p: specB → specA, p(F) = F ∩ A, wobei F und G prime Filter in B bzw. A sind (siehe hierzu [AJ95], Proposition 7.3.6). Um die Bedingung für starke Unterbereiche nachzuweisen, sei p(F) ≤ G, d. h. F ∩ A ⊆ G. Wir müssen zeigen, daß F und ↑_{B}G beschränkt sind, also daß es einen primen Filter in B gibt, der diese beiden umfaßt. Die Menge F ∧ ↑_{B}G := {b ∧ a | b ∈ F, a ∈ ↑_{B}G} ist ein Filter, der F und ↑_{B}G enthält, muß aber nicht prim sein. Ist 0 ∉ F ∧↑_{B}G , so können wir jedoch die Existenz eines solchen primen Filters zeigen. Wir betrachten dann die Menge der Filter in B, die F ∧ ↑_{B}G umfassen, aber nicht die 0 enthalten. Nach dem Lemma von Zorn gibt es einen maximalen Filter mit dieser Eigenschaft, und nach dem Satz über prime Filter (Lemma 3.1.11) ist dieser prim.

Es bleibt uns also noch, 0 ∉ F ∧ ↑_{B}G zu zeigen. Wäre 0 Element dieses Filters, so gäbe es Elemente b ∈ F und a ∈ G mit a ∧ b ≈ 0. Nun ist A ein starkes Sub-Prälokal von B, weshalb wir ein a_{b} ≳ b in A finden könnten mit a_{b} ∧ a ≈ 0. Dann wäre aber a_{b} ∈ F ∩ A ⊆ G und folglich 0 ≈ a ∧ a_{b} ∈ G. Als primer Filter enthält G jedoch nicht die 0, so daß dies nicht sein kann.

Wir zeigen nun, daß die Snack-Potenzkonstruktion starke Sub-Prälokale respektiert. Dabei verwenden wir folgende Beobachtung:

Lemma 3.1.13 Es sei A ein Scott-Prälokal. Im Snack-Potenzlokal von A gilt □a ∧ ⋀_{i=1}^{n} ♢b_{i} ≈ 0 genau dann, wenn es ein i_{0} ∈ {1, …, n} gibt mit a ∧ b_{i_{0}} ≈ 0_{A}.

Beweis: Man sieht leicht, daß die Bedingung hinreichend ist. Ist nämlich a∧b_{i_{0}} ≈ 0_{A} für ein i_{0} ∈ {1, …, n}, so hat man

□a ∧ ⋀_{i=1}^{n} ♢b_{i} ≲ □a ∧ ♢b_{i_{0}} ≲ ♢(a ∧ b_{i_{0}}) ≈ ♢0 ≈ 0 .

Um die Notwendigkeit der Bedingung einzusehen, sei □a ∧ ⋀_{i=1}^{n} ♢b_{i} ≈ 0. Nun ist P^{S}(A) eine lokalische Beschreibung von P^{S}spec(A), d. h. es gibt einen Prä-Isomorph-ismus ⟦·⟧: P^{S}(A) → KΩP^{S}spec(A). Wenden wir ihn auf die Situation an, so ergibt sich

∅ = ⟦□a ∧ ⋀_{i=1}^{n} ♢b_{i}⟧ = ⟦□a⟧ ∩ ⋂_{i=1}^{n}⟦♢b_{i}⟧ .

Die Interpretation von □a ist durch ↑_{P^{S}(specA)}↓(⟦a⟧_{A}, ∅), die Interpretation von ♢b_{i} durch ↑_{P^{S}(specA)}↓(specA, {⟦b_{i}⟧_{A}}) (i = 1, …, n) gegeben, wobei wir den Prä-Isomorphismus ⟦·⟧_{A}: A → KΩspec(A) haben, weil A eine lokalische Beschreibung von spec(A) ist. Der Schnitt dieser Interpretationen ist ↑_{P^{S}(specA)}↓(⟦a⟧_{A}, {⟦a⟧_{A} ∩ ⟦b_{i}⟧_{A} | i = 1, …, n}), falls der erzeugende Ausdruck hierin ein korrekt gebildeter Snack ist^{2}. Dies ist genau dann der Fall, wenn ⟦a⟧_{A} ∩ ⟦b_{i}⟧_{A} ≠ ∅ für alle i ∈ {1, …, n} ist. In diesem Fall haben wir also eine nichtleere Interpretation von □a ∧ ⋀_{i=1}^{n} ♢b_{i}. Nur dann, wenn ⟦a⟧_{A} ∩ ⟦b_{i_{0}}⟧_{A} = ∅ für ein i_{0} ∈ {1, …, n} ist, sind die Snacks (⟦a⟧_{A}, ∅) und (specA, {⟦b_{i}⟧_{A}}) (i = 1, …, n) nicht beschränkt, so daß sich eine leere Interpretation ergibt. Das heißt aber ⟦a⟧_{A} ∩ ⟦b_{i_{0}}⟧_{A} = ∅ und, da ⟦·⟧ ordnungsreflektierend ist, a ∧ b_{i_{0}} ≈ 0.

Nützlich ist auch folgendes Lemma, mit dem wir die Eigenschaft, durch die starke Sub-Prälokale definiert sind, von Elementen auf Suprema von Elementen ausdehnen können.

Lemma 3.1.14 Es sei A ein Sub-Prälokal von B und für die Elemente a ≈ a_{1} ∨ … ∨ a_{m} ∈ A und b ≈ b_{1} ∨ … ∨ b_{n} ∈ B gelte a ∧ b ≈ 0. Wenn es für alle 1 ≤ i ≤ m und 1 ≤ j ≤ n ein a^{(i,j)} ∈ A mit a^{(i,j)} ≳ b_{j} und a_{i} ∧ a^{(i,j)} ≈ 0 gibt, dann existiert ein a^{b} ∈ A mit a^{b} ≳ b und a ∧ a^{b} ≈ 0.

2Daß wir in seiner zweiten Komponente streng genommen eine Antikette bezüglich ⊆ zu bilden haben, ist für die Argumentation unerheblich.

Beweis: Wir setzen a^{b} := ⋀_{k=1}^{m} ⋁_{j=1}^{n} a^{(k,j)}. Natürlich ist a^{b} ∈ A, denn dies ist für alle a^{(k,j)} der Fall. Außerdem gilt ⋁_{j=1}^{n} a^{(k,j)} ≳ b_{1} ∨ … ∨ b_{n} ≈ b für alle k ∈ {1, …, m}, also a^{b} ≳ b. Schließlich ist

a ∧ a^{b} = ( ⋁_{i=1}^{m} a_{i}) ∧ ( ⋀_{k=1}^{m} ⋁_{j=1}^{n} a^{(k,j)})
≈ ⋁_{i=1}^{m}(a_{i} ∧ ⋀_{k=1}^{m} ⋁_{j=1}^{n} a^{(k,j)})
≲ ⋁_{i=1}^{m}(a_{i} ∧ ⋁_{j=1}^{n} a^{(i,j)})
≈ ⋁_{i=1}^{m} ⋁_{j=1}^{n}(a_{i} ∧ a^{(i,j)})
≈ 0,

also a ∧ a^{b} ≈ 0.

Satz 3.1.15 Ist A ein starkes Sub-Prälokal des Scott-Prälokals B, dann gilt die gleiche Beziehung zwischen P^{S}(A) und P^{S}(B).

Beweis: Oben sagten wir schon, daß die Snack-Potenzkonstruktion bezüglich der Sub-Prälokalrelation monoton ist, was sich nach der in [AJ95] in allgemeiner Form dargestellten Vorgehensweise ergibt.

Wir müssen zeigen, daß die Bedingung für starke Sub-Prälokale erfüllt ist. Dazu seien a ∈ P^{S}(A), b ∈ P^{S}(B) so, daß a ∧ b ≈ 0. Unter Verwendung der Distributivität können wir sowohl a als auch b als Disjunktion von Konjunktionen a_{i} (i = 1, …, n) bzw. b_{j} (j = 1, …, m) von Erzeugern der jeweiligen Potenzlokale schreiben. Wegen Lemma 3.1.14 genügt es, für jedes Paar (i, j) (i = 1, …, n; j = 1, …, m) ein Element a_{i,j} ≳ b_{j} in P^{S}(A) so finden, daß a_{i} ∧ a_{i,j} ≈ 0 gilt.

Hierzu formen wir mit Hilfe des Distributivitätsgesetzes den Ausdruck a ∧ b zu einer Disjunktion von Konjunktionen a_{i} ∧ b_{j} um. Mit a ∧ b ist auch jede dieser Konjunktionen äquivalent zu 0. Wegen (□ − ∧) können wir annehmen, daß a_{i} und b_{j} je einen □-Erzeuger und endlich viele ♢-Erzeuger haben. Die □-Erzeuger bezeichnen wir mit □â bzw. □b̂. Wegen Lemma 3.1.13 wissen wir, daß es unter den ♢-Erzeugern von a_{i} oder b_{j} ein ♢ĉ gibt mit â ∧ b̂ ∧ ĉ ≈ 0. Nun verwenden wir, daß A ein starkes Sub-Prälokal von B ist. Wenn ♢ĉ eine Teilformel von a_{i} ist, so erhalten wir daraus ein Element ā ≳ b̂ in A mit â∧ĉ∧ā ≈ 0. Wie im Beweis von Lemma 3.1.13 gesehen, folgt damit □â∧♢ĉ∧□ā ≈ 0. Da □â∧♢ĉ ≳ a_{i} und □ā ≳ b_{j}, können wir a_{i,j} := □ā setzen.

Ist dagegen ♢ĉ eine Teilformel von b_{j}, so gibt es ein Element ā ≳ b ∧ c in P^{S}(A) mit â ∧ ā ≈ 0. Es folgt dann □â ∧ ♢ā ≈ 0. Da □â ≳ a_{i} und ♢ā ≳ ♢(b̂∧ ĉ) ≳ □b̂∧ ♢ĉ ≳ b_{j}, können wir dann a_{i,j} := ♢ā setzen. Damit sind die Elemente a_{i,j} gefunden, was den Beweis vollendet.

Zum Abschluß dieses Abschnitts erhalten wir aus dem vorangegangenen Satz, daß die Snack-Potenzkonstruktion mit starken Unterbereichen verträglich ist:

Korollar 3.1.16 Ist D ein starker Unterbereich des Bereiches E, so gilt die gleiche Beziehung zwischen den Snack-Potenzbereichen P^{S}(D) und P^{S}(E).

Beweis: Wenn D ein starker Unterbereich von E ist, dann ist Lemma 3.1.10 zufolge das Prälokal KΩ(D) ein starkes Sub-Prälokal von KΩ(E). Wegen Satz 3.1.15 ist P^{S}(KΩ(D)) ein starkes Sub-Prälokal von P^{S}(KΩ(E)). Nun verwenden wir Lemma 3.1.12, womit wir schließen können, daß spec(P^{S}(KΩD)) ein starker Unterbereich von spec(P^{S}(KΩE)) ist. Mit Hilfe von Korollar 2.3.13 ergibt sich, daß P^{S}(spec(KΩD)) ein starker Unterbereich von P^{S}(spec(KΩE)) ist. Da spec(KΩD) isomorph zu D ist (und entsprechendes für E gilt), können wir schließlich folgern, daß P^{S}D ein starker Unterbereich von P^{S}E ist.

3.2 Typen und ihre Interpretation

Mit den starken Unterbereichen und Sub-Prälokalen des vorigen Abschnitts haben wir noch nicht auf ein konkretes Typsystem abgezielt. Sie reihen sich noch gut in Bunemans [BJO91] Ansatz ein, beliebige Bereiche als Wertemengen für Datenbanken zuzulassen. Tatsächlich wird man so radikal aber höchstens bei der Auswahl von Grundtypen vorgehen wollen. Bei jeder Implementierung wird man aus ihnen mit Typkonstruktoren weitere Typen herleiten, deren Struktur nicht mehr ganz so beliebig, sondern von den Konstruktoren abhängig ist. Wir verzichten auf eine umfangreiche Sammlung von Grundtypen und verwenden sogar nur einen einzigen, nämlich 1. Die sonst üblichen konstruieren wir daraus mit Hilfe der Typkonstruktoren.

Den Aufbau unserer Typausdrücke gibt folgende Grammatik an:

σ ::= 1 | σ × τ | σ ⊕ τ | σ_{⊥} | P^{S}σ | t | rec t.σ ,

wobei σ und τ für Typausdrücke stehen und t eine Typvariable ist.

Die Typausdrücke werden üblicherweise in der Kategorie der Bereiche interpretiert. Dann wird 1 durch den einelementigen Bereich, × durch das kartesische Produkt und ⊕ durch die verklebte Summe interpretiert. Das Hinzufügen eines neuen kleinsten Elements (Lift) zu einem Bereich wird durch ()_{⊥} ausgedrückt, und P^{S} wird als Mengenkonstruktor verstanden, interpretiert durch den Snack-Potenzbereich. Mit rec t.σ können schließlich rekursive Typen gebildet werden, wozu auch die Typvariable t benötigt wird. Ein rekursiver Typ rec t.σ wird durch die initiale Lösung der Bereichsgleichung t = σ interpretiert.

Die verklebte Summe wird in erster Linie verwendet, um Grundtypen wie den Wahrheitswertebereich bool oder die ganzen Zahlen int zu konstruieren:

bool := (1)_{⊥} ⊕ (1)_{⊥} und int := rec t.(1)_{⊥} ⊕ t.

Um Verbundtypen mit Variantteil zu bilden, verwenden wir ⊕ wie bei der Konstruktion von bool nur in Verbindung mit ()_{⊥}. Die Konstruktion wird dann durch die disjunkte Summe von Bereichen interpretiert, und wir fügen sie als abgeleitete Konstruktion hinzu:

σ + τ := (σ)_{⊥} ⊕ (τ)_{⊥}.

Mit diesem Typaufbau erhalten wir die Typsysteme einer ganzen Reihe von Datenbankmodellen als Spezialfälle. Der Typ einer Relation mit n Attributen des Relationenmodells schreibt sich in unserer Darstellung als

P^{S}((σ_{1} × σ_{2}) × … × σ_{n}) ,

wobei σ_{1}, …, σ_{n} die Typen der jeweiligen Attribute sind. Genestete Relationen [SS86] erhält man durch die auf die Konstruktoren × und P^{S} eingeschränkte Grammatik. Baumartige Grundtypen im Sinne Zaniolos [Zan84] lassen sich schließlich unter Verwendung der Summenkonstruktoren aufbauen.

An die Seite der Interpretationen der Typen durch Bereiche wollen wir nun noch die Interpretation in der Kategorie der Prälokale stellen. Damit erhalten wir eine Logik für Datenbankobjekte, die es uns erlaubt, Typkonstruktoren durch die Eigenschaften der konstruierten Objekte zu beschreiben. Die logische Interpretation des Konstruktors P^{S} geschieht durch das Snack-Potenzlokal, das im vorangegangenen Kapitel vorgestellt wurde. Die lokalischen Interpretationen für die anderen Typkonstruktoren finden sich in [Abr91b, AJ95].

Notation: Die Interpretation der Typen durch Bereiche bezeichnen wir mit ⟦·⟧_{D}, die durch Prälokale durch ⟦·⟧_{L}.

Durch die Stone-Dualität stehen die beiden Interpretationen miteinander in Beziehung:

Satz 3.2.1 Ist σ ein geschlossener Typausdruck, so ist

spec(⟦σ⟧_{L}) ≅ ⟦σ⟧_{D} .

Der Beweis geschieht durch Induktion über den Typaufbau. Die Verankerung ist trivial. Den Induktionsschritt für die Snack-Potenzkonstruktion haben wir im letzten Kapitel durchgeführt. Für die anderen Konstruktionen müßten wir dieselben Schritte wie dort durchführen. Da das Ergebnis für diese Konstruktionen aber schon von [Abr91a] bekannt ist und dort auch die wesentlichen Beweisschritte explizit durchgeführt werden, beschränken wir uns hier darauf, die jeweiligen Prälokale ohne Beweis der Stone-Dualität durch Erzeuger, Axiome und Regeln anzugeben. Dabei geben wir stets nur die Axiome und Regeln an, die spezifisch für die Konstruktion sind. Hinzu treten die allgemein benötigten Regeln und Axiome, die wir schon beim Snack-Potenzlokal angaben.

Konstruktion  Erzeuger
1  keine

spezifische Axiome und Regeln keine

Konstruktion  Erzeuger
A × B  {a_{l} | a ∈ A} ∪ {b_{r} | b ∈ B}

spezifische Axiome und Regeln

Wenn a ≲ a′, dann a_{l} ≲ a′_{l}  b ≲ b′, dann b_{r} ≲ b′_{r}
(a ∧ a′)_{l} ≈ a_{l} ∧ a′_{l}  (b ∧ b′)_{r} ≈ b_{r} ∧ b′_{r}
(a ∨ a′)_{l} ≈ a_{l} ∨ a′_{l}  (b ∨ b′)_{r} ≈ b_{r} ∨ b′_{r}
0_{l} ≈ 0_{r} ≈ 0  1_{l} ≈ 1_{r} ≈ 1
Wenn T(a), dann T(a_{l})  Wenn T(b), dann T(b_{r})
Wenn E(a), dann E(a_{l})  Wenn E(b), dann E(b_{r})

Konstruktion  Erzeuger
A ⊕ B  {a ⊕ f | a ∈ A} ∪ {f ⊕ b | b ∈ B},
wobei f ∉ A ∪ B

spezifische Axiome und Regeln

Wenn a ≲ a′, dann a ⊕ f ≲ a′ ⊕ f Wenn b ≲ b′, dann f ⊕ b ≲ f ⊕ b′
(a ∧ a′) ⊕ f ≈ (a ⊕ f) ∧ (a′ ⊕ f)  f ⊕ (b ∧ b′) ≈ (f ⊕ b) ∧ (f ⊕ b′)
(a ∨ a′) ⊕ f ≈ (a ⊕ f) ∨ (a′ ⊕ f)  f ⊕ (b ∨ b′) ≈ (f ⊕ b) ∨ (f ⊕ b′)
0 ⊕ f ≈ f ⊕ 0 ≈ 0  1 ⊕ f ≈ f ⊕ 1 ≈ 1
Wenn T(a), dann T(a ⊕ f)  Wenn T(b), dann T(f ⊕ b)

Wenn T(a) und T(b), dann (a ⊕ f) ∧ (f ⊕ b) ≈ 0

Wenn E(a), dann E(a ⊕ f)  Wenn E(b), dann E(f ⊕ b)
Konstruktion  Erzeuger
A_{⊥}  {a_{⊥} | a ∈ A}

spezifische Axiome und Regeln Wenn a ≲ a′, dann a_{⊥} ≲ a′_{⊥}

(a ∧ a′)_{⊥} ≈ a_{⊥} ∧ a′_{⊥}  (a ∨ a′)_{⊥} ≈ a_{⊥} ∨ a′_{⊥}

0_{⊥} ≈ 0 T(a_{⊥}) Wenn E(a), dann E(a_{⊥})

Für rekursive Ausdrücke gibt es keine Axiome oder Regeln, da das Prälokal für einen rekursiven Typ gerade die Vereinigung der Prälokale für die Approximationen an diesen Typ ist. Auf eine ausführliche Erläuterung der Interpretation rekursiver Ausdrücke durch Prälokale verzichten wir hier jedoch; es sei dafür auf [AJ95], Kapitel 7.3.5 verwiesen.

Im nächsten Abschnitt werden wir bei der Definition der Subtyp-Beziehung die separierte Summe verwenden, ohne dabei auf ihre Definition durch die verklebte Summe zurückgreifen zu wollen. Daher geben wir auch hierfür die lokalische Konstruktion an. Mit den Abkürzungen

a + f = a_{⊥} ⊕ f und f + b = f ⊕ b_{⊥}

erhalten wir:

Konstruktion  Erzeuger
A + B  {a + f | a ∈ A} ∪ {f + b | b ∈ B}
wobei f ∉ A ∪ B

spezifische Axiome und Regeln

Wenn a ≲ a′, dann a + f ≲ a′ + f Wenn b ≲ b′, dann f + b ≲ f + b′
(a ∧ a′) + f ≈ (a + f) ∧ (a′ + f)  f + (b ∧ b′) ≈ (f + b) ∧ (f + b′)
(a ∨ a′) + f ≈ (a + f) ∨ (a′ + f)  f + (b ∨ b′) ≈ (f + b) ∨ (f + b′)

0 + f ≈ f + 0 ≈ 0

T(a + f)  T(f + b)

(a + f) ∧ (f + b) ≈ 0

Wenn E(a), dann E(a + f)  Wenn E(b), dann E(f + b)

3.3 Subtypen

Nachdem wir in Abschnitt 3.1 starke Unterbereiche und Sub-Prälokale als Unterstrukturen eingeführt haben, ohne uns schon auf bestimmte Typen zu beziehen, geben wir nun Subtypen für die gerade definierte Typstruktur an und zeigen, daß Subtypen lokalisch durch starke Sub-Prälokale interpretiert werden. Mit den Ergebnissen aus Abschnitt 3.1 folgern wir unter Verwendung der Stone-Dualität, daß die Subtypen auf der Seite der Bereiche durch starke Unterbereiche interpretiert werden.

Hier zeigt sich, daß die Begriffe des starken Unterbereichs und Sub-Prälokals allgemeiner sind als der des Subtyps, denn wir zeigen nur, daß Subtypen durch diese Begriffe interpretiert werden. Die zusammengesetzten Bereiche, die in unserem Zusammenhang betrachtet werden, können jedoch durchaus mehr starke Unterbereiche haben als diejenigen, die zu Subtypen korrespondieren. Dies gilt insbesondere für die verklebte Summe von Bereichen. Um starke Unterbereiche einer verklebten Summe zu finden, ist es nötig, einen genaueren Einblick in die Struktur der beteiligten Bereiche zu haben. Dies ist mit Hilfe der hier betrachteten Typstruktur nur möglich, wenn die beteiligten Bereiche durch ()_{⊥} erzeugt werden, so daß wir nur für die abgeleitete Konstruktion + und nicht für ⊕ Regeln für die Subtyprelation angeben. Einzelheiten über starke Unterbereiche verklebter Summen (die zudem nach unten abgeschlossen, also Semi-Faktoren sind) finden sich in [Puh90].

Unsere Subtyprelation ≤_{s} wird induktiv durch folgende Axiome und Regeln definiert:

Axiome: 1 ≤_{s} σ
σ ≤_{s} σ
σ ≤_{s} σ × τ
τ ≤_{s} σ × τ
Regeln: Wenn σ ≤_{s} τ und τ ≤_{s} υ, dann σ ≤_{s} υ.
Wenn σ ≤_{s} τ, dann σ_{⊥} ≤_{s} τ_{⊥}.
Wenn σ_{1} ≤_{s} σ_{2} und τ_{1} ≤_{s} τ_{2}, dann σ_{1} × τ_{1} ≤_{s} σ_{2} × τ_{2}.
Wenn σ_{1} ≤_{s} σ_{2} und τ_{1} ≤_{s} τ_{2}, dann σ_{1} + τ_{1} ≤_{s} σ_{2} + τ_{2}.
Wenn σ ≤_{s} τ, dann P^{S}σ ≤_{s} P^{S}τ.
Wenn σ ≤_{s} τ[t := rec t.τ], dann σ ≤_{s} rec t.τ.

Wir behaupten, daß die Subtyprelation unter den Interpretationen ⟦·⟧_{D} und ⟦·⟧_{L} in die starke Unterbereich- bzw. die starke Sub-Prälokalrelation übersetzt wird.

Satz 3.3.1 Ist σ ein Subtyp von τ, so ist ⟦σ⟧_{L} bis auf Isomorphie ein starkes Sub-Prälokal von ⟦τ⟧_{L}.

Beweis: Wir führen den Beweis durch Induktion. Die Verankerung ist in den Fällen 1 ≤_{s} σ und σ ≤_{s} σ trivial.

Von den beiden symmetrischen Fällen σ ≤_{s} σ × τ und τ ≤_{s} σ × τ führen wir den ersten aus. Natürlich ist ⟦σ⟧_{L} isomorph zu einem Sub-Prälokal von ⟦σ × τ⟧_{L}, der Isomorphismus ist durch die Abbildung (·)_{l} gegeben, die jedem a ∈ ⟦σ⟧_{L} das Element a_{l} ∈ ⟦σ × τ⟧_{L} zuordnet. Wir zeigen, daß das Sub-Prälokal (⟦σ⟧_{L})_{l} von ⟦σ × τ⟧_{L} stark ist. Dazu sei a ∈ ⟦σ⟧_{L}, x ∈ ⟦σ × τ⟧_{L} und a_{l} ∧ x ≈ 0. Wir müssen ein a^{x} ∈ ⟦σ⟧_{L} finden mit a^{x}_{l} ≳ x und a ∧ a^{x} ≈ 0.

Jedes Element von ⟦σ × τ⟧_{L} läßt sich als Disjunktion von Konjuktionen der speziellen Form s_{l} ∧ t_{r} mit s ∈ ⟦σ⟧_{L} und t ∈ ⟦τ⟧_{L} schreiben. Es ist also

a_{l} ∧ x ≈ a_{l} ∧ ⋁_{i=1}^{n}(s_{l}^{i} ∧ t_{r}^{i}) ≈ 0.

Wegen Lemma 3.1.14 reicht es nun, für jedes i ∈ {1, …, n} ein x^{i} ∈ ⟦σ⟧_{L} zu finden mit x^{i} ≳ s_{l}^{i} ∧ t_{r}^{i} und a_{l} ∧ x_{l}^{i} ≈ 0. Für jedes solche i ist (a ∧ s^{i})_{l} ∧ t_{r}^{i} ≈ 0, was nach den Axiomen und Regeln für das Produkt nur sein kann, wenn a ∧ s^{i} ≈ 0 oder t^{i} ≈ 0 ist. Im ersten Fall können wir x^{i} := s^{i}, im zweiten x^{i} := 0 setzen.

Wir kommen nun zum Induktionsschritt, wobei wir den trivialen Fall der Transitivitätsregel überspringen. In allen anderen Fällen ist es klar, daß die entsprechenden Prälokale die Sub-Prälokalrelation erfüllen, wobei wir hier auf den Zusatz ”bis auf Isomorphie“ sogar verzichten können. Wir müssen also stets nur die Bedingung für starke Sub-Prälokale nachweisen.

Wir beginnen mit σ ≤_{s} τ ⇒ σ_{⊥} ≤_{s} τ_{⊥}. Es seien a ∈ ⟦σ_{⊥}⟧_{L}, b ∈ ⟦τ_{⊥}⟧_{L} derart, daß a ∧ b ≈ 0. Wir müssen ein a^{b} ≳ a mit a^{b} ∈ A finden, für das a ∧ a^{b} ≈ 0. Wenn a ≈ 1, dann gilt b ≈ 0 und wir können a^{b} := b wählen. Ist b ≈ 1, so folgt a ≈ 0, und wieder setzen wir a^{b} := b. Andernfalls gibt es a′ ∈ ⟦σ⟧_{L}, b′ ∈ ⟦τ⟧_{L} mit a = a′_{⊥} und b = b′_{⊥}. Dann haben wir a ∧ b = a′_{⊥} ∧ b′_{⊥} ≈ (a′ ∧ b′)_{⊥} ≈ 0. Nun kann x_{⊥} ≈ 0 (x ∈ A) nur gelten, wenn x ≈ 0 ist, denn 0_{⊥} ≈ 0 ist die einzige Regel, derzufolge ein Element zu 0 äquivalent sein kann. Also folgt a′ ∧ b′ ≈ 0. Da ⟦σ⟧_{L} nach Voraussetzung ein starkes Sub-Prälokal von ⟦τ⟧_{L} ist, finden wir ein (a′)^{b′} ∈ ⟦σ⟧_{L} mit (a′)^{b′} ≳ b′ und a′ ∧ (a′)^{b′} ≈ 0. Dann ist a^{b} := ((a′)^{b′})_{⊥} das gesuchte Element von ⟦σ_{⊥}⟧_{L}.

Als nächstes betrachten wir σ_{1}×τ_{1} ≤_{s} σ_{2}×τ_{2}. Wir nehmen an, daß ⟦σ_{1}⟧_{L} und ⟦τ_{1}⟧_{L} starke Sub-Prälokale von ⟦σ_{2}⟧_{L} bzw. ⟦τ_{2}⟧_{L} sind. Sei nun a ∈ ⟦σ_{1} × τ_{1}⟧_{L}, b ∈ ⟦σ_{2} × τ_{2}⟧_{L} und a ∧ b ≈ 0. Sowohl a als auch b kann man als Disjunktion von Konjunktionen schreiben, die folgendermaßen aus Erzeugern aufgebaut sind:

a ≈ ⋁_{i=1}^{m}(s_{l}^{i} ∧ t_{r}^{i}),  s^{i} ∈ ⟦σ_{1}⟧_{L}, t^{i} ∈ ⟦τ_{1}⟧_{L}, i = 1, …, m ,
b ≈ ⋁_{j=1}^{n}(u_{l}^{j} ∧ v_{r}^{j}),  u^{j} ∈ ⟦σ_{2}⟧_{L}, v^{j} ∈ ⟦τ_{2}⟧_{L}, j = 1, …, n .

Gemäß Lemma 3.1.14 genügt es, Elemente b^{(i,j)} ≳ u_{l}^{j} ∧ v_{r}^{j} in ⟦σ_{1} × τ_{1}⟧_{L} zu finden, für die s_{l}^{i} ∧ t_{r}^{i} ∧ b^{(i,j)} ≈ 0 gilt (i = 1, …, m; j = 1, …, n). Für diese i und j haben wir

(s_{l}^{i} ∧ u_{l}^{j}) ∧ (t_{r}^{i} ∧ v_{r}^{j}) ≈ 0.

Den Regeln für das Produkt zufolge kann dies nur der Fall sein, wenn s_{l}^{i} ∧ u_{l}^{j} ≈ 0 oder t_{r}^{i} ∧ v_{r}^{j} ≈ 0. Da ⟦σ_{1}⟧_{L} ⊴_{s} ⟦σ_{2}⟧_{L} und ⟦τ_{1}⟧_{L} ⊴_{s} ⟦τ_{2}⟧_{L}, gibt es im ersten Fall ein (u^{j})^{s^{i}} ≳ u^{j} in ⟦σ_{1}⟧_{L} mit s^{j} ∧ (u^{j})^{s^{i}} ≈ 0 und im zweiten Fall ein (v^{j})^{t^{i}} ≳ v^{j} in ⟦τ_{1}⟧_{L} mit t^{i} ∧ (v^{j})^{t^{i}} ≈ 0. Im ersten Fall ist b^{(i,j)} := ((u^{j})^{s^{i}})_{l}, im zweiten b^{(i,j)} := ((v^{j})^{t^{i}})_{r} das gesuchte Element.

Nun behandeln wir σ_{1} +τ_{1} ≤_{s} σ_{2} +τ_{2}. Wieder nehmen wir an, daß ⟦σ_{1}⟧_{L} ⊴_{s} ⟦σ_{2}⟧_{L} und ⟦τ_{1}⟧_{L} ⊴_{s} ⟦τ_{2}⟧_{L}. Ist a ∈ ⟦σ_{1} + τ_{1}⟧_{L}, b ∈ ⟦σ_{2} + τ_{2}⟧_{L} mit a ∧ b ≈ 0, so betrachten wir zunächst den Fall, daß a ≈ 1 oder b ≈ 1 gilt. Dann ist b ≈ 0 bzw. a ≈ 0, und in beiden Fällen ist b ∈ ⟦σ_{1} + τ_{1}⟧_{L}, so daß man nichts zeigen muß. Andernfalls stellen wir a und b wieder als Disjunktion von Konjuntionen der Form s + f ∧ f + t dar. Der Beweis kann dann auf die gleiche Art wie für das Produkt vollendet werden.

Der Fall des Mengenkonstruktors P^{S} ist mit Satz 3.1.15 bereits gezeigt.

Schließlich kommen wir zu den rekursiven Typen. Hier ist jedoch nichts zu zeigen, da τ[t := rec t.τ] und rec t.τ durch dasselbe Prälokal interpretiert werden.

Satz 3.3.2 Ist σ ein Subtyp von τ, so ist ⟦σ⟧_{D} ein starker Unterbereich von ⟦τ⟧_{D}.

64 KAPITEL 3. EIN TYPSYSTEM FÜR DATENBANKEN

Nesten und Entnesten — Übergänge zwischen genesteten Relationen

Mit unserem Typsystem aus Kapitel 3 und der Interpretation der Typen durch Bereiche (statt Mengen) und Prälokale haben wir das relationale Datenbankmodell, aber auch Erweiterungen dieses Modells, etwa durch genestete Relationen [SS86], verallgemeinert. Dabei haben wir uns bisher auf die Datentypen konzentriert und die Datenbankoperationen außer acht gelassen. Die Leistungsfähigkeit einer Datenbank hängt jedoch auch von der Ausdrucksstärke der Operationen ab, mit denen die Anfragen an die Datenbank gestellt werden. Im relationalen Modell kommt man mit wenigen Operationen aus und kann dennoch sehr viele der in der Praxis vorkommenden Anfragen direkt formulieren. So bezieht man sich bei den Erweiterungen des relationalen Modells üblicherweise auf dessen Ausdrucksmöglichkeiten mit dem Bestreben, die dort möglichen Operationen zur Verfügung zu stellen, hinsichtlich der erweiterten Möglichkeiten aber zusätzliche oder bessere Anfrageoperationen zu verwirklichen. Als wichtige relationale Operation sprachen wir schon die Projektion an. Bei uns ist es stets möglich, von einem Typ σ auf einen Suptyp von σ zu projizieren. Daß die Projektion die am leichtesten auf das bereichstheoretische Modell übertragbare relationale Operation ist, wurde schon in [BJO91] festgestellt, wo auch die mathematischen Grundlagen dafür erörtert wurden. Wir gehen hier nicht weiter auf die Projektion ein; und auch die anderen relationalen Operationen, deren Übertragung auf das bereichstheoretische Modell noch nicht gelöst ist, sind nicht Gegenstand dieser Arbeit. Vielmehr wenden wir uns der Frage zu, auf welche Weise der Übergang zwischen genesteten Relationen unterschiedlicher Nestungstiefe vollzogen werden kann.

In Abschnitt 4.1 stellen wir dazu die Operationen nest (ν) und unnest (μ) der Schekschen Algebra für genestete Relationen vor, in Abschnitt 4.2 definieren wir solche Operationen für das bereichstheoretische Modell und zeigen, daß hier nest und unnest ein Einbettungs-Projektionspaar bilden, was für die Schekschen Operationen nicht gilt.

4.1 Nesten und Entnesten genesteter Relationen

In [JS82] rücken Jaeschke und Schek von dem Prinzip relationaler Datenbanken ab, daß die Wertemengen, die einzelnen Attributen einer Relation zugeordnet sind, selbst keine weitere Struktur aufweisen dürfen; sie lassen als Einträge für ein Attribut wiederum Relationen zu. Es kommen also Relationen innerhalb von Relationen vor, und dies darf wiederholt geschehen. Man erhält so ineinander geschachtelte Relationen, sogenannte ”genestete Relationen“. Für jede Attributmenge lassen sich unterschiedliche Typen genesteter Relationen angeben, die diese Attribute verwenden und sich nur dadurch unterscheiden, daß gewisse Attribute in verschiedener Schachtelungstiefe auftauchen. Der Übergang zwischen solchen Relationen erfolgt mit den in [JS82] vorgestellten Operationen ν (nest) und μ (unnest).

Um das Prinzip zu erläutern, kann man sich auf zwei Attribute A und B beschränken. Alle Effekte, die bei den Operationen ν und μ auftreten, erkennt man schon beim Wechsel zwischen Relationen der Typen {A × B} und {A × {B}}. Dabei stehen die Mengenklammern für das Bilden einer Relation, d. h. {A × B} ist der Typ einer Relation mit den zwei Attributen A und B, und {A × {B}} der einer Relation mit den zwei Attributen A und {B}. Das zweite Attribut ist hier also selbst relationenwertig, und diese Relationen haben nur das eine Attribut B.

Tatsächlich können wir das Wort ”Relation“, das hier im Sinne von ”Datenbankrelation“ steht, auch im mathematischen Sinne als Relation lesen, wenn wir uns auf endliche Relationen einschränken. Dazu interpretieren wir die Attribute A und B als Bezeichnungen zweier Mengen. Die Objekte vom Typ {A × B} sind dann endliche Teilmengen von A × B, und die Objekte vom Typ {A × {B}} sind endliche Teilmengen des Produkts von A und der Menge der endlichen Teilmengen von B. Die Übergange zwischen beiden Typen durch die Funktionen ν und μ sind folgendermaßen definiert, wobei π_{A} die Projektion von A × B auf A bezeichnet und wir Paare in spitzen Klammern schreiben:

ν : {A × B} → {A × {B}}
ν(R) := {⟨a, b̂⟩ | a ∈ π_{A}(R) und b̂ = {b ∈ B | ⟨a, b⟩ ∈ R}}

und

μ : {A × {B}} → {A × B}
μ(S) := {⟨a, b⟩ | ∃⟨a, b̂⟩ ∈ S. b ∈ b̂}.

Den Übergang ν : {A × B} → {A × {B}} kann man sich so vorstellen, daß zu jedem A-Wert nun die Menge der ihm zugeordneten B-Werte gespeichert wird.

Der Übergang μ : {A × {B}} → {A × B} macht dies rückgängig, indem die Paare aus einem A-Wert und einer Menge von B-Werten so in Paare aus A- und B-Werten aufgelöst werden, daß der A-Wert zu jedem Element der Menge der ihm zugeordneten B-Werte wiederholt wird. Tatsächlich gilt stets μ ∘ ν = id [JS82]. Die Umkehrung ν ∘ μ = id gilt allerdings nicht. Dies ist auch nicht überraschend, denn in einer genesteten Relation vom Typ {A × {B}} kann dasselbe Element a ∈ A zusammen mit unterschiedlichen Teilmengen von B vorkommen. Dazu betrachten wir eine Beispielrelation R:

R : A  {B}
a_{1}  \begin{matrix}b_{1} \\ b_{2} \end{matrix}
a_{1}  \begin{matrix}b_{2} \\ b_{3} \end{matrix}
a_{2}  ∅

Entnestet man diese Relation, so erhält man

μ(R) : A  B
a_{1}  b_{1}
a_{1}  b_{2}
a_{1}  b_{3}

Die Information, auf welche Weise a_{1} mit Teilmengen von B verbunden war, aber auch die Information über das Element a_{2}, dem die leere Menge zugeordnet war, ist nun verloren. Durch erneutes Nesten läßt sich diese Information nicht zurückgewinnen:

\begin{aligned}νμ(R) : & A & \{B\} \\ & a_{1} & \begin{matrix}b_{1} \\ b_{2} \\ b_{3} \end{matrix} \end{aligned}

Nun ist es nicht erstaunlich, daß beim Anwenden mancher Datenbankoperationen Information verlorengeht; die relationale Projektion ist sogar dafür vorgesehen, Information auszublenden. Im Fall von ν ∘ μ haben wir aber den Effekt, daß die inneren Relationen größer werden (wenn sie nicht verschwinden) und die äußere Relation Tupel verliert. Würde man das Modell genesteter Relationen mit einer Informationsordnung versehen, die die Relationen auf allen Schachtelungsebenen mit der gleichen Semantik versieht, so wäre daher im allgemeinen ν ∘ μ ≤ id, was der Idee des eventuellen Verlierens von Information entspräche, nicht gegeben. Statt dessen wären Fälle konstruierbar, in denen allein durch das Ausführen von Datenbankoperationen Information gewissermaßen aus dem Nichts hinzugewonnen würde. Stellt die in der Datenbank gespeicherte Information in irgendeinem Sinne ein korrektes Bild der Wirklichkeit dar, so darf so etwas aber nicht passieren, denn die ”hinzugewonnene“ Information wird im allgemeinen zu einer inkorrekten Beschreibung der Wirklichkeit führen.

Auch Variationen der Operationen ν und μ, wie sie in [Sch88] vorgeschlagen werden, verbessern diese Situation nicht.

Das zugrundeliegende Problem ist die unklare Semantik von Datenbankrelationen. Für Relationen, die im Snack-Potenzbereich interpretiert werden, können wir dagegen Funktionen nest und unnest angeben, die diesen Nachteil nicht aufweisen, sondern für die nest ∘ unnest ≤ id und unnest ∘ nest = id gelten. Die beiden Funktionen bilden damit ein Einbettungs-Projektionspaar, und wir können die Situation so verstehen, daß bei der Komposition, in der Information verlorengeht, der Informationsverlust so gering wie möglich ist.

Wir stellen diese Funktionen im nächsten Abschnitt vor.

4.2 Nesten und Entnesten für Bereichsdatenbanken

Unser Typsystem aus Kapitel 3 erlaubt es, die im letzten Abschnitt betrachteten genesteten Relationen in die Sprache der bereichstheoretischen Datenbanken zu übersetzen. Zur Tupelbildung haben wir das Produkt × und zur Bildung mengenwertiger Typen den Konstruktor P^{S}. Hat das Attribut A aus dem vorigen Abschnitt den Typ σ und das Attribut B den Typ τ, so schreibt sich der Typ der nicht genesteten Relation aus dem vorigen Abschnitt nun als P^{S}(σ × τ). Der Typ der genesteten Relation ist P^{S}(σ × P^{S}(τ)).

Zum Übergang zwischen beiden Typen definieren wir nun die Funktionen nest und unnest für die Interpretationen der Typen durch Bereiche. Dazu sei ⟦σ⟧_{D} = A und ⟦τ⟧_{D} = B, so daß wir in den Bezeichnungen die Analogie zum vorigen Abschnitt wahren. Die Funktionen nest und unnest müssen damit die Bereiche P^{S}(A × B) und P^{S}(A × P^{S}(B)) miteinander verbinden. Es genügt aber, die Funktionen auf den kompakten Elementen der Bereiche zu definieren. Zudem werden die Funktionen so sein, daß Bilder kompakter Elemente kompakt sind. Ohne darauf genauer einzugehen, sei gesagt, daß der Grund hierfür ist, daß die Objekte, die in einer Datenbank verarbeitet werden, immer durch kompakte Elemente eines Bereichs interpretiert werden. Da Datenbankoperationen aus im Rechner dargestellten Objekten wieder solche erzeugen sollen, ergibt sich die genannte Bedingung an die Funktionen. Beachtet man noch, daß die Menge S(A × B) der Snacks auf A × B isomorph zu K(P^{S}(A × B)) und S(A × P^{S}(B)) isomorph zu K(P^{S}(A × P^{S}(B)) ist, so reduziert sich die Aufgabe darauf, Funktionen

nest : S(A × B) → S(A × P^{S}(B))
und unnest : S(A × P^{S}(B)) → S(A × B)

zu definieren. Nun bestehen die Snacks auf einem Bereich aus kompakt-offenen Mengen, also Mengen, die durch kompakte Elemente eines Bereichs erzeugt werden. Die Bestandteile der Snacks auf A × P^{S}(B) sind also durch Paare erzeugt, deren erste Komponente ein kompaktes Element in A und deren zweite Komponente ein kompaktes Element in P^{S}(B) ist. Die kompakten Elemente in P^{S}(B) sind Hauptideale in S(B). Statt mit den Hauptidealen können wir mit den erzeugenden Snacks auf B rechnen: Die Ordnung ⊆ zwischen Hauptidealen übersetzt sich in die Ordnung ⊑ zwischen den erzeugenden Snacks. Das Supremum (Infimum) zweier Hauptideale ist das Hauptideal, das vom Supremum (Infimum) der erzeugenden Snacks erzeugt wird. Es bedeutet daher keine Einschränkung, wenn wir die Hauptideale in P^{S}(B) durch die erzeugenden Snacks ersetzen, um die Komplexität der Formeln in diesem Kapitel in einem erträglichen Rahmen zu halten.

Zum Zwecke der Abkürzung bezeichnen wir in diesem Kapitel Ausdrücke, die aus den Snacks auf P^{S}(B) dadurch entstehen, daß wir anstelle der Hauptideale von S(B) die erzeugenden Snacks auf B verwenden, als Snacks auf A × S(B). Das geschieht, obwohl S(B) und damit A × S(B) im allgemeinen kein Bereich ist und die Ausdrücke im strengen Sinne keine Snacks sind. Die aus S(A × P^{S}(B)) auf diese Weise entstehende geordnete Menge bezeichnen wir mit S(A × S(B)).

Wir werden in diesem Kapitel also Funktionen

nest : S(A × B) → S(A × S(B))
und unnest : S(A × S(B)) → S(A × B)

definieren. Danach werden wir zeigen, daß nest ∘ unnest ≤ id und unnest ∘ nest = id gilt, d. h. daß durch die beiden Funktionen ein Einbettungs-Projektionspaar gegeben ist.

Für den Rest dieses Kapitels vereinbaren wir nun noch einige Bezeichnungen. Stets seien A und B Bereiche und π_{1}: A × B → A und π_{2}: A × B → B die Projektionen von A × B auf A bzw. B. Paare aus A × B und A × S(B) schreiben wir wie im ersten Abschnitt dieses Kapitels in spitzen Klammern: ⟨a, b⟩. Snacks hingegen (die ja auch Paare sind) schreiben wir in runden Klammern: (U, L); und für jeden Snack (U, L) wird mit fst(U, L) seine erste Komponente U und mit snd(U, L) seine zweite Komponente L ausgewählt.

4.2.1 Die Funktion Nest

Die Funktion nest wird auf Snacks auf A × B angewendet. Diese sind aus Mengen U und L (L ∈ L) aufgebaut, die jeweils Teilmengen von A × B sind. Wir fassen diese Teilmengen als zweistellige Relationen auf und verwenden für Elemente a ∈ A und Relationen R ⊆ A × B die für Relationen übliche Notation

[a]R := {b | ⟨a, b⟩ ∈ R} .

Definition 4.2.1 Die Funktion nest ist gegeben durch

nest : S(A × B) → S(A × S(B))
nest(U, {L_{1}, …, L_{k}})
:= (↑{⟨a, ([a]U, ∅)⟩ | a ∈ A},
{↑{⟨c, ([c]U, {[c]L_{i}})⟩ | c ∈ π_{1}(L_{i})} | i = 1, …, k}) .

Man sieht nicht sofort, daß das Ergebnis von nest ein korrekt gebildeter Ausdruck in S(A × S(B)) ist, d. h. daß die einzelnen Mengen durch endlich viele kompakte Elemente erzeugt sind. Zur Vorbereitung des Beweises hiervon zeigen wir zunächst:

Proposition 4.2.2 Ist U ⊆ A × B eine obere Menge und a ∈ A, so ist [a]U eine obere Menge in B.

Proposition 4.2.3 Ist a ≤ a′ in A und U ⊆ A × B eine obere Menge, so gilt [a]U ⊆ [a′]U.

Beweis: Ist ⟨a, b⟩ in U, so auch ⟨a′, b⟩, denn U ist ein obere Menge.

Proposition 4.2.4 Ist U offen in A × B, so ist [a]U offen in B.

Beweis: Ein gerichtetes Supremum ^{⋁ ↑}_{i∈I} b_{i} liegt genau dann in [a]U, wenn das Supremum ^{⋁ ↑}_{i∈I}⟨a, b_{i}⟩ in U liegt.

Proposition 4.2.5 Es sei a ∈ A und {U_{i}}_{i∈I} eine Familie von Teilmengen von A × B. Dann gilt

[a](⋃_{i∈I} U_{i}) = ⋃_{i∈I}([a]U_{i}) und [a](⋂_{i∈I} U_{i}) = ⋂_{i∈I}([a]U_{i}) .

Proposition 4.2.6 Für jedes Element a ∈ A und jede endlich erzeugte obere Teilmenge U ⊆ A × B ist M := [a]U eine endlich erzeugte obere Menge in B. Ist U von {⟨a_{1}, b_{1}⟩, …, ⟨a_{n}, b_{n}⟩} erzeugt, so gilt M = ↑{b_{i} | a ≥ a_{i}, i ∈ {1, …, n}}.

Beweis: Ist ⟨a, b⟩ ∈ U, so gibt es ein i ∈ {1, …, n} mit ⟨a, b⟩ ≥ ⟨a_{i}, b_{i}⟩. Damit ist M = {b | ⟨a, b⟩ ∈ U} ⊆ ↑{b_{i} | a ≥ a_{i}, i ∈ {1, …, n}}. Natürlich ist für alle i mit a ≥ a_{i} das Element b_{i} in M enthalten. Von Lemma 4.2.2 wissen wir, daß M eine obere Menge ist, so daß ingesamt die gewünschte Gleichheit folgt.

Proposition 4.2.7 Ist U ⊆ A × B eine kompakte obere Menge und a ∈ A, so ist [a]U eine kompakte obere Menge in B.

Beweis: Nach dem Hofmann-Mislove Theorem ist U der gefilterte Durchschnitt seiner offenen Umgebungen O_{i} (i ∈ I). Nun ist [a]U = [a](⋂_{i∈I} O_{i}) = ⋂_{i∈I}([a]O_{i}), was wiederum ein gefilterter Schnitt offener Mengen ist, also eine kompakte obere Menge.

Proposition 4.2.8 Ist U ⊆ A×B eine endlich erzeugte obere Menge, so gibt es nur endlich viele verschiedene Mengen [a]U. Ist M die Menge der Erzeuger von U und {a_{1}, …, a_{n}} = π_{1}(M), so sind diese durch die Mengen gegeben, die zu Suprema von Teilmengen von {a_{1}, …, a_{n}} in Relation stehen.

Beweis: Es sei a ∈ A und ǎ := ⋁{a_{i} | a_{i} ≤ a, i ∈ {1, …, n}}. Es ist ǎ ≤ a, also [ǎ]U ⊆ [a]U nach Proposition 4.2.3. Ist b ∈ [a]U, d. h. ⟨a, b⟩ ∈ U, so gibt es ein ⟨a_{i}, b_{i}⟩ ∈ M, welches unter ⟨a, b⟩ liegt. Dann ist ⟨ǎ, b⟩ ≥ ⟨a_{i}, b⟩ ≥ ⟨a_{i}, b_{i}⟩, also ⟨ǎ, b⟩ ∈ U, was insgesamt [ǎ]U = [a]U zeigt.

Proposition 4.2.9 Sind L, L′ ⊆ A × B, und gibt es ein ⟨a, b⟩ ∈ L \ L′, so gilt

[a]L ⊈ [a]L′ .

Proposition 4.2.10 Sind L, L′ kompakt-offene Mengen in A × B mit L ⊈ L′, so gibt es ein a ∈ π_{1}(L) derart, daß für alle a′ ≤ a gilt [a]L ⊈ [a′]L′.

Beweis: Es gibt ein ⟨a, b⟩ ∈ Ł \ L′. Da L′ eine obere Menge ist, kann für a′ ≤ a das Paar ⟨a′, b⟩ nicht zu L′ gehören. Folglich ist b ∈ [a]L \ [a′]L′.

Proposition 4.2.11 Es seien L und L′ kompakt-offene Teilmengen von A × B, die bezüglich ⊆ nicht vergleichbar und in der kompakt-offenen Menge U ⊆ A×B enthalten sind. Dann sind

↑{⟨c, ([c]U, {[c]L})⟩ | c ∈ π_{1}(L)} (1)

und

↑{⟨c, ([c]U, {[c]L′})⟩ | c ∈ π_{1}(L′)} (2)

in A × S(B) bezüglich ⊆ unvergleichbar.

Beweis: Nach Proposition 4.2.8 gibt es ein ĉ ∈ π_{1}(L) mit [ĉ]L ⊈ [c′]L′ für alle c′ ≤ ĉ. Damit kann es in (2) kein Element geben, welches kleiner oder gleich ⟨ĉ, ([ĉ]U, {[ĉ]L})⟩ ist. Also gilt (1) ⊈ (2). Aus der Symmetrie der Situation ergibt sich die Behauptung.

Lemma 4.2.12 Die Funktion nest liefert für jeden Snack (U, {L_{1}, …, L_{k}}) auf A×B einen Snack auf A × S(B).

Beweis: Mit Hilfe der Propositionen 4.2.4 und 4.2.7 erkennt man, daß die Mengen [a]U für alle a ∈ A (und damit auch für a ∈ π_{1}(L_{i}), i = 1, …, k) und [c]L_{i} für alle c ∈ π_{1}(L_{i}) (i = 1, …, k) kompakt-offen sind. Natürlich gilt wegen ∅ ≠ L_{i} ⊆ U für i = 1, …, k auch ∅ ≠ [c]L_{i} ⊆ [c]U für c ∈ π_{1}(L_{i}). Da die Snacks auf der inneren Ebene eine leere oder einelementige zweite Komponente haben, braucht man nicht nachprüfen, ob die Elemente der zweiten Komponente eine Antikette bilden. Es folgt damit, daß die Snacks auf der inneren Ebene korrekt aufgebaut sind.

Daß auf der äußeren Ebene nicht alle a ∈ A bzw. c ∈ π_{1}(L_{i}) zur Erzeugung benötigt werden, sondern jeweils endlich viele Elemente von A bzw. π_{1}(L_{i}) genügen, folgt direkt mit Proposition 4.2.8. Daß diese kompakt sind, besagt Proposition 4.2.7.

Daß die Mengen in der zweiten Komponente von nest(U, {L_{1}, …, L_{k}}) nicht leer und in der ersten Komponente enthalten sind, ist leicht zu sehen. Sie sind nicht leer, da die Mengen L_{i} (i = 1, …, k) nicht leer sind, und sie sind in der ersten Komponente enthalten, weil π_{1}(L_{i}) ⊆ A und ⟨c, ([c](U), ∅)⟩ ≤ ⟨c, ([c]U, {[c]L_{i}})⟩ für alle i = 1, …, k und c ∈ π_{1}(L_{i}) gilt.

Schließlich zeigt Proposition 4.2.11, daß die zweite Komponente des Ergebnisses von nest eine Antikette ist.

Insgesamt zeigt dies, daß nest korrekt aufgebaute Snacks auf A × S(B) liefert.

Lemma 4.2.13 Die Funktion nest ist monoton.

Beweis: Es seien (U, L) und (U′, L′) Snacks auf A × B mit (U, L) ⊑ (U′, L′). Für jedes a ∈ A ist [a]U ⊇ [a]U′. Damit folgt fst(nest(U, L)) ⊇ fst(nest(U′, L′)). Ist nun L ∈ L, so gibt es ein L′ ∈ L′ mit L′ ⊆ L, und es gilt für jedes c ∈ π_{1}(L′) die Beziehung

([c]U, {[c]L}) ⊑ ([c]U′, {[c]L′}) .

Ferner ist π_{1}(L) ⊇ π_{1}(L′), also c ∈ π_{1}(L) für jedes c ∈ π_{1}(L′). Damit schließt man, daß

↑{⟨c, ([c]U, {[c]L})⟩ | c ∈ π_{1}(L)} ⊇ ↑{⟨c, ([c]U′, {[c]L′})⟩ | c ∈ π_{1}(L′)} .

Somit hat man zu jeder Menge in snd(nest(U, L)) eine in ihr enthaltenen Menge in snd(nest(U′, L′)) gefunden. Insgesamt ist damit nest(U, L) ⊑ nest(U′, L′) gezeigt.

4.2.2 Die Funktion Unnest

Während zum Nesten einer Relation die ganze Relation vorliegen muß, kann man beim Entnesten schrittweise vorgehen, indem man jede Zeile für sich entnestet. Enthält die ursprüngliche Zeile einen Wert a aus der Menge A und eine Menge von B-Werten, so entsteht dadurch die Relation der Paare ⟨a, b⟩, für die b einer dieser B-Werte ist. Die gesamte Relation wird entnestet, indem man diese Teilergebnisse vereinigt.

In ähnlicher Weise können wir auch die Funktion unnest für Bereichsdatenbanken definieren. Anstelle gleich einen Snack auf A×S(B) zu entnesten, ordnen wir zunächst einem Element in K(A) × S(B) einen Snack auf A × B zu. In [BTBW92] wird auf ähnliche Weise eine Funktion Unnest für den Fall definiert, daß die Objekte des mengenwertigen Typs endliche Teilmengen des Grundtyps sind. In Anlehnung an die dort verwendete Paarbildungsfunktion (pairwith) bezeichnen wir die folgende Funktion mit pw:

Definition 4.2.14 Es sei ⟨a, (U, {L_{1}, …, L_{k}})⟩ ∈ KA × S(B). Dann definieren wir

pw(⟨a, (U, {L_{1}, …, L_{k}})⟩) := (↑a × U, {↑a × L_{1}, … ↑a × L_{k}}) .

Proposition 4.2.15 Die Funktion pw bildet Paare aus KA × S(B) auf Snacks auf A × B ab und ist monoton.

Beweis: Da a ∈ KA ist, ist ↑a kompakt-offen in A. Die Produkte von ↑a mit den kompakt-offenen Mengen U, L_{1}, …, L_{k} aus B sind kompakt-offen in A × B. Die Gültigkeit der übrigen Bedingungen für Snacks auf A × B ergeben sich leicht daraus, daß (U, {L_{1}, …, L_{k}) ein Snack auf B ist.

Die Monotonie von pw ist ebenfalls leicht einzusehen.

Nun liefert uns die Charakterisierung des Snack-Potenzbereichs als freie Algebra (Satz 2.2.15) einen Snackalgebra-Homomorphismus pw^{+}: S(A × S(B)) → S(A × B), den wir unnest nennen:

Definition 4.2.16 Die Funktion unnest ist die durch Satz 2.2.15 gegebene eindeutig bestimmte Fortsetzung von pw zu einem Snackalgebra-Homomorphismus von S(A × S(B)) nach SA × B, d. h. es ist

unnest(↑{⟨a_{1}, B_{1}⟩, …, ⟨a_{n}, B_{n}⟩}, {↑{⟨c_{i1}, D_{i1}⟩, …, ⟨c_{im_{i}}, D_{im_{i}}⟩} | i = 1, …, k})

= (pw(⟨a_{1}, B_{1}⟩) ⊓ … ⊓ pw(⟨a_{n}, B_{n}⟩) ⊓ (∅, ∅))

∪ ⋃ ; −_{i=1}^{k} (pw(⟨c_{i1}, D_{i1}⟩) ⊓ … ⊓ pw(⟨c_{im_{i}}, D_{im_{i}}⟩))

Möchte man einen konkret gegebenen Snack entnesten, so ist es nützlich eine geschlossene Darstellung für unnest zu haben:

Lemma 4.2.17 Für die Funktion unnest gilt

unnest(↑{⟨a_{1}, B_{1}⟩, …, ⟨a_{n}, B_{n}⟩}, {↑{⟨c_{i1}, D_{i1}⟩, …, ⟨c_{im_{i}}, D_{im_{i}}⟩} | i = 1, …, k})

= ( ⋃_{j=1}^{n}(↑a_{j} × fstB_{j}), MIN^{⊆} ⋃_{i=1}^{k}{ ⋃_{j=1}^{m_{i}}(↑c_{ij} × ℓ(j)) | ℓ: {1, …, m_{i}} ⟶^{⊙} ⋃_{j=1}^{m_{i}} sndD_{ij}}),

wobei ℓ: {1, …, m_{i}} ⟶^{⊙} ⋃_{j=1}^{m_{i}} sndD_{ij} besage, daß ℓ eine Auswahlfunktion ist, d. h. ℓ(j) ∈ sndD_{ij}.

Beweis: Es ist

(pw(⟨a_{1}, B_{1}⟩) ⊓ … ⊓ pw(⟨a_{n}, B_{n}⟩) ⊓ (∅, ∅))

∪ ⋃ ; −_{i=1}^{k} (pw(⟨c_{i1}, D_{i1}⟩) ⊓ … ⊓ pw(⟨c_{im_{i}}, D_{im_{i}}⟩))

= ( ⋃_{j=1}^{n}(↑a_{j} × fstB_{j}), ∅) ∪ ⋃ ; −_{i=1}^{k} ( ⋃_{j=1}^{m_{i}}(↑c_{ij} × fstD_{ij}),

MIN^{⊆}{ ⋃_{j=1}^{m_{i}}(↑c_{ij} × ℓ(j)) | ℓ: {1, …, m_{i}} ⟶^{⊙} ⋃_{j=1}^{m_{i}} sndD_{ij}})

= ( ⋃_{j=1}^{n}(↑a_{j} × fstB_{j}), MIN^{⊆} ⋃_{i=1}^{k}{ ⋃_{j=1}^{m_{i}}(↑c_{ij} × ℓ(j)) | ℓ: {1, …, m_{i}} ⟶^{⊙} ⋃_{j=1}^{m_{i}} sndD_{ij}}) ,

wobei der letzte Schritt gilt, weil ⋃_{j=1}^{m_{i}}(↑c_{ij} × fstD_{ij}) ⊆ ⋃_{j=1}^{n}(↑a_{j} × fstB_{j}) für i = 1, …, k ist.

4.2.3 Das Einbettungs-Projektionspaar

Lemma 4.2.18 Für die Funktionen nest und unnest aus den Definitionen 4.2.1 und 4.2.16 gilt unnest ∘ nest = id.

Beweis: Es sei (U, {L_{1}, …, L_{k}}) ∈ S(A × B). Dann ist

unnest(nest(U, {L_{1}, …, L_{k}}))
= unnest(↑{⟨a, ([a]U, ∅)⟩ | a ∈ A},
{↑{⟨c, ([c]U, [c]L_{i}})⟩ | c ∈ π_{1}(L_{i})} | i = 1, …, k}).

Beim Entnesten können wir die beiden Komponenten des (äußeren) Snacks getrennt betrachten. Wir beginnen mit der ersten Komponente. Aus Proposition 4.2.8 wissen wir, daß es eine endliche Teilmenge Ǎ von A gibt mit

↑{⟨a, ([a]U, ∅)⟩ | a ∈ A} = ↑{⟨a, ([a]U, ∅)⟩ | a ∈ Ǎ}

und daß es zu jedem a ∈ A ein ǎ ∈ Ǎ mit ǎ ≤ a und [a]U ⊆ [ǎ]U gibt. Damit wird die erste Komponente des zu entnestenden Snacks unter unnest zu

⋃_{a∈Ǎ} (↑a × [a]U) = ⋃_{a∈A} (↑a × [a]U) ⊇ ⋃_{a∈A} ({a} × [a]U) = U.

Da U eine obere Menge ist, sieht man andererseits sofort, daß auch die umgekehrte Inklusion gilt.

Wie für die erste Komponente finden wir für die i-te (i = 1, …, k) Menge der zweiten Komponente eine endliche Menge Č_{i}, die zudem erzeugende Teilmenge von π_{1}(L_{i}) ist, derart, daß diese i-te Menge von den Ausdrücken ⟨c, ([c]U, {[c]L_{i}})⟩ mit c ∈ Č_{i} erzeugt wird. Man beachte, daß die zweiten Komponenten der Snacks hierin einelementig sind. Daher gibt es jeweils nur eine Auswahlfunktion und die Menge wird unter unnest zu

{ ⋃_{c∈Č_{i}}(↑c × [c]L_{i})} .

Daß diese einzige Menge der zweiten Komponente gleich L_{i} ist, schließt man in Analogie zur obigen Argumentation für die erste Komponente.

Die zweite Komponente des Ergebnisses unter unnest ist also MIN^{⊆}({L_{1}, …, L_{k}}). Dies ist gleich {L_{1}, …, L_{k}}, da die Mengen L_{1}, …, L_{k} eine Antikette bezüglich ⊆ bilden.

Damit ergibt sich die Behauptung.

Zur Vorbereitung des nächsten Ergebnisses zeigen wir:

Proposition 4.2.19 Es seien U_{1}, …, U_{n} Teilmengen von B und a_{1}, …, a_{n} Elemente von A. Ferner sei c ≥ a_{i} und V ⊆ U_{i} für ein i ∈ {1, …, n}. Dann gilt

[c]( ⋃_{j=1}^{n}(↑a_{j} × U_{j})) ⊇ V .

Beweis: Es ist

[c]( ⋃_{j=1}^{n}(↑a_{j} × U_{j})) ⊇ [c](↑a_{i} × U_{i}) = U_{i} ⊇ V .

Lemma 4.2.20 Für die Funktionen nest und unnest gilt

nest ∘ unnest ≤ id .

Beweis: Wir wenden nest ∘ unnest auf ein Element von S(A × SB)) an und führen für dabei entstehende Teilterme Abkürzungen ein. Es ist

nest(unnest(↑{⟨a_{1}, B_{1}⟩, …, ⟨a_{n}, B_{n}⟩}, {↑{⟨c_{i1}, D_{i1}⟩, …, ⟨c_{i_{mi}}, D_{i_{mi}}⟩} | i = 1, …, k}))

= nest(\underbrace{⋃_{j=1}^{n}(↑a_{j} × fstB_{j})}_{U}, MIN^{⊆}(\underbrace{⋃_{i=1}^{k}\{⋃_{l=1}^{m_{i}}(↑c_{il} × ℓ(l)) | ℓ: \{1, …, m_{i}\} ⟶^{⊙} ⋃_{l=1}^{m_{i}} sndD_{il}\}}_{L})) .

Der Beweis gliedert sich nun in mehrere Schritte. Schritt 1: Wir zeigen fst(nest(U, MIN^{⊆}(L))) ⊇ ↑{⟨a_{1}, B_{1}⟩, …, ⟨a_{n}, B_{n}⟩}.

Es ist fst(nest(U, L)) = ↑{⟨a, [a]U), ∅)⟩ | a ∈ A}, und so genügt es, für i = 1, …, n die Gültigkeit der Beziehung

([a_{i}]U, ∅) ⊑ B_{i}

nachzuweisen. Für die zweite Komponente der Snacks ist nichts zu zeigen, da diese für den links stehenden Snack leer ist. Es ist also noch

[a_{i}]( ⋃_{j=1}^{n}(↑a_{j} × fstB_{j})) ⊇ fst(B_{i})

zu zeigen. Dies folgt direkt mit Proposition 4.2.19. Schritt 2: Für jedes Element M ∈ snd(nest(U, MIN^{⊆}(L))) ist ein i ∈ {1, …, k} zu finden mit M ⊇ ↑{⟨c_{i1}, D_{i1}⟩, …, ⟨c_{im_{i}}, D_{im_{i}}⟩}. Dies bedeutet, daß für jedes L_{•} ∈ MIN^{⊆}(L) ein i ∈ {1, …, k} zu finden ist mit

↑{⟨c, ([c]U, {[c]L_{•}})⟩ | c ∈ π_{1}(L_{•})}
⊇ ↑{⟨c_{i1}, D_{i1}⟩, …, ⟨c_{im_{i}}, D_{im_{i}}⟩} . (∗)

Wir beschränken uns nicht auf die Elemente von L, die bezüglich ⊆ minimal sind, sondern zeigen, daß es für alle L_{•} ∈ L ein solches i gibt.

Für jedes L_{•} ∈ L gibt es einen natürlichen Kandidaten für das gesuchte i ∈ {1, …, k}. Es ist nämlich L die Vereinigung gewisser Mengen, die durch einen Parameter zwischen 1 und k unterschieden werden. Der Parameter der Teilmenge von L, zu der L_{•} gehört, ist die gesuchte Zahl zwischen 1 und k.

Sei also i ∈ {1, …, k} so gewählt, daß

L_{•} ∈ {⋃_{l=1}^{m_{i}}(↑c_{il} × ℓ(l)) | ℓ: {1, …, m_{i}} ⟶^{⊙} ⋃_{l=1}^{m_{i}} sndD_{il}} ,

und sei ℓ_{•}: {1, …, m_{i}} ⟶^{⊙} ⋃_{l=1}^{m_{i}} sndD_{il} so, daß L_{•} = ⋃_{l=1}^{m_{i}}(↑c_{il} × ℓ_{•}(l)).

Um (∗) zu zeigen, weisen wir zunächst nach, daß c_{ij} ∈ π_{1}(L_{•}) für alle j ∈ {1, …, m_{i}} gilt.

Für alle j ∈ {1, …, m_{i}} ist

π_{1}(L_{•}) = π_{1}(⋃_{l=1}^{m_{i}} ↑c_{il} × ℓ_{•}(l)) ⊇ π_{1}(↑c_{ij} × ℓ_{•}(l)) .

Wegen ℓ_{•}(j) ≠ ∅ folgt nun c_{ij} ∈ π_{1}(↑c_{ij} ×ℓ_{•}(j)) und insgesamt c_{ij} ∈ π_{1}(L_{•}). Damit brauchen wir, um (∗) nachzuweisen, nur noch zu zeigen, daß für alle j ∈ {1, …, m_{i}} gilt

([c_{ij}]U), {[c_{ij}]L_{•})}) ⊑ D_{ij} .

Dies betrachten wir für beide Komponenten der Snacks wieder getrennt. \underline{Schritt 2a}: Zeige: [c_{ij}]U) ⊇ fst(D_{ij}). Zu ⟨c_{ij}, D_{ij}⟩ gibt es ein ⟨ǎ, B̌⟩ ∈ {⟨a_{1}, B_{1}⟩, …, ⟨a_{n}, B_{n}⟩} mit ⟨ǎ, B̌⟩ ≤ ⟨c_{ij}, D_{ij}⟩,

da die erste Komponente eines Snacks stets alle Elemente seiner zweiten Komponente umfaßt. Das heißt insbesondere ǎ ≤ c_{ij} und fstD_{ij} ⊆ fstB̌. Damit erfüllen fst(B_{1}), …, fst(B_{n}), a_{1}, …, a_{n}, c_{ij} und fst(D_{ij}) die Voraussetzungen der Proposition 4.2.19, so daß die gewünschte Beziehung folgt.

\underline{Schritt 2b}: Es ist zu zeigen, daß es ein L_{D} ∈ snd(D_{ij}) gibt mit

[c_{ij}]L_{•}) ⊇ L_{D} .

Nun ist

L_{•} = ⋃_{l=1}^{m_{i}}(↑c_{il} × ℓ_{•}(l)) ,

wobei ℓ_{•}(l) ∈ snd(D_{il}) für jedes l ∈ {1, …, m_{i}} gilt. Wählen wir L_{D} = ℓ_{•}(j), so folgt die gewünschte Beziehung direkt mit Proposition 4.2.19.

Damit ist Schritt 2 und auch der gesamte Beweis vollendet.

Damit bilden nest und unnest ein Einbettungs-Projektionspaar. In der auf Seite 34 geschilderten Weise gewinnt man aus diesen beiden monotonen Funktionen nun stetige Funktionen

nest_{idl} : P^{S}(A × B) → P^{S}(A × P^{S}(B))
und unnest_{idl} : P^{S}(A × P^{S}(B)) → P^{S}(A × B).

Mit Lemma 4.2.18 und Lemma 4.2.20 ergibt sich direkt:

Satz 4.2.21 Die Abbildungen nest_{idl} und unnest_{idl} bilden ein Einbettungs-Projek-tionspaar stetiger Funktionen.

Anhang A

Semifaktoren im Snack-Potenzbereich

Im folgenden beweisen wir Satz 3.1.2 aus Kapitel 3, der hier zu Erinnerung wiederholt sei:

Satz 3.1.2: Der Snack-Potenzbereich eines jeden Scott-Bereichs hat nur triviale Semi-Faktoren.

Zur Erinnerung sei auch wiederholt, daß jeder Bereich ein trivialer Semi-Faktor von sich selbst ist und daß wir ferner die Semi-Faktoren A eines Bereichs D trivial nennen, für die ↑a ⊇ D_{max} für alle a ∈ A gilt.

Zunächst stellen wir einige Aussagen zusammen, die für die weiteren Beweisschritte nützlich sind.

Proposition A.1 Es sei D ein Bereich und s ∈ P^{S}(D) derart, daß es einen Snack (U, L) ∈ s mit L ≠ ∅ gibt. Dann gibt es zu jedem (U′, L′) ∈ s ein (U′′, L′′) ∈ s mit (U′, L′) ⊑ (U′′, L′′) und L′′ ≠ ∅.

Beweis: Zu (U, L) ∈ s und (U′, L′) ∈ s existiert eine obere Schranke (U′′, L′′) ∈ s, denn s ist ein Ideal und daher gerichtet. Wegen (U′′, L′′) ⊒ (U, L) und L ≠ ∅ ist L′′ ≠ ∅.

Von [BJO91] wissen wir:

Proposition A.2 Bei der Projektion auf einen Semifaktor gehen maximale Elemente eines Bereichs in maximale Elemente des Semifaktors über.

Proposition A.3 Ist D ein Bereich und ↓x ein Semifaktor für ein x ∈ D, so ist der Semifaktor trivial.

Beweis: Nach Proposition A.2 ist p_{↓x}(y) = x für alle y ∈ D_{max}. Mithin ist y ≥ x und ↑x′ ⊇ ↑x ⊇ D_{max} für alle x′ ∈ ↓x.

Der Beweis des Satzes 3.1.2 erfolgt nun mit Hilfe der Lemmata A.4, A.5 und A.6 folgendermaßen: Es sei D ein Bereich. Das von dem Snack (∅, ∅) erzeugte Hauptideal in der Menge der Snacks auf D ist ein maximales Element im Snack-Potenzbereich P^{S}(D) (vgl. Satz 2.2.7). In Lemma A.4 zeigen wir, daß dies ein Element jedes nichttrivialen Semifaktors von P^{S}(D) sein muß. Anschließend weisen wir in Lemma A.5 nach, daß jeder Semi-Faktor, der dieses Element enthält, auch gewisse weitere maximale Elemente des Snack-Potenzbereichs enthält, nämlich diejenigen, die einelementige Teilmengen von D_{max} approximieren. Daraus schließen wir in Lemma A.6, daß ein solcher Semi-Faktor alle maximalen Elemente von P^{S}(D) enthält, also trivial ist, woraus letztlich folgt, daß alle Semi-Faktoren eines Snack-Potenzbereichs trivial sind.

Lemma A.4 Es sei D ein Bereich. Jeder nichttriviale Semifaktor F in P^{S}(D) enthält das Ideal ↓(∅, ∅).

Beweis: Wegen Proposition A.3 hat jeder nichttriviale Semifaktor in P^{S}(D) wenigstens zwei maximale Elemente. Diese können nicht beide kleiner als ↓(∅, ∅) sein, denn je zwei maximale Elemente eines Semifaktors sind unbeschränkt. Es gibt in F also ein maximales Element s ⊈ ↓(∅, ∅). Es sei t die Teilmenge von s, die alle (U, L) aus s mit L ≠ ∅ enthält. Die Menge t ist eine obere Teilmenge von s und mit Proposition A.1 folgt ↓t = s.

Nun konstruieren wir ein Element s′ ∈ P^{S}(D), das kleiner als s, aber unvergleichbar mit p_{F} (↓(∅, ∅)) ist. Falls p_{F} (↓(∅, ∅)) ≠ ↓(∅, ∅), so werden wir für {s′, p_{F} (↓(∅, ∅))} eine obere Schranke angeben können. Es existiert dann das Supremum x und dieses liegt in F. Das steht im Widerspruch zur Maximalität von p_{F} (↓(∅, ∅)) in F, die uns die Maximalität von ↓(∅, ∅) in P^{S}(D) (vgl. Satz 2.2.7) und Proposition A.2 liefern. Die folgende Abbildung illustriert die Lage der zu konstruierenden Elemente innerhalb des Snack-Potenzbereiches:

↓(∅, ∅) F p_{F} (↓(∅, ∅)) s s′  x

Im folgenden nutzen wir aus, daß die zweite Komponente aller in p_{F} (↓(∅, ∅)) enthaltener Snacks leer ist. Wir definieren t′ := {(U ∪ V, {U ∪ V }) | (U, L) ∈ t, (V, ∅) ∈ p_{F} (↓(∅, ∅))}. Da U ≠ ∅ für alle (U, L) ∈ t gilt, ist hierin stets U ∪ V ≠ ∅, so daß dies eine Menge von Snacks ist. Es ist ↓t′ ⊆ ↓t = s, denn für jedes (U, L) ∈ t und (V, ∅) ∈ p_{F} (↓(∅, ∅)) ist zum einen U ∪ V ⊇ U; wegen L ≠ ∅ und U ⊇ L für alle L ∈ L gibt es zum anderen zu U ∪ V ein L ∈ L mit U ∪ V ⊇ L, so daß (U ∪ V, {U ∪ V }) ⊑ (U, L) für alle (U, L) ∈ t und (V, ∅) ∈ p_{F} (↓(∅, ∅)) gilt. Es ist t eine obere Teilmenge der gerichteten Menge s, demnach ist t gerichtet. Da p_{F} (↓(∅, ∅)) als Ideal auch gerichtet ist, ergibt sich hieraus leicht die Gerichtetheit von t′, so daß s′ := ↓t′ ein Ideal, d. h. ein Element von P^{S}(D) ist.

Falls p_{F} (↓(∅, ∅)) ≠ ↓(∅, ∅) wäre, so enthielte P^{S}(D) die Menge {(V, {V }) | (V, ∅) ∈ p_{F} (↓(∅, ∅))} als Element; man sieht leicht, daß dies eine obere Schranke für s′ und p_{F} (↓(∅, ∅)) wäre. Diese beiden Elemente von P^{S}(D) müßten dann ein Supremum x haben. Da F unter existierenden Suprema abgeschlossen ist, wäre x ∈ F. Nun ist s′ ⊈ p_{F} (↓(∅, ∅)), denn s′ enthält Snacks mit nichtleerer zweiter Komponente. Daher müßte x echt größer als p_{F} (↓(∅, ∅)) sein, im Widerspruch zur Maximalität von p_{F} (↓(∅, ∅)) in F. Also ist p_{F} (↓(∅, ∅)) = ↓(∅, ∅), d. h. ↓(∅, ∅) ∈ F, wie behauptet.

Abschließend sei noch darauf eingegangen, wieso der obige Widerspruch im Fall p_{F} (↓(∅, ∅)) = ↓(∅, ∅) nicht zustande kommt. In diesem Fall wäre nämlich unter den betrachteten (V, {V }) auch das Paar (∅, {∅}), welches kein Snack ist, da die zweite Komponente die leere Menge enthält (und nicht etwa die leere Menge ist). So entstünde dort kein Element des Snack-Potenzbereichs, weshalb die darauf folgende Argumentation in diesem Falle nicht durchgeführt werden kann.

Lemma A.5 Ist ↓(∅, ∅) in einem Semifaktor F des Snack-Potenzbereichs eines Bereichs D enthalten, so ist für jedes x ∈ D_{max} auch die Menge sn({x}) der {x} approximierenden Snacks in F enthalten.

Beweis: Wir sahen bereits (vgl. Seite 24), daß sn({x}) ∈ P^{S}(D) ist. Satz 2.2.7 zeigt zudem, daß dies ein maximales Element in P^{S}(D) ist.

Die Projektion p_{F} (sn({x})) ist größer als {(U, ∅) | (U, L) ∈ sn({x})} und enthält mindestens einen Snack, dessen zweite Komponente nicht leer ist. Andernfalls wäre p_{F} (sn({x}) ⊆ ↓(∅, ∅), und sn({x}) und ↓(∅, ∅) müßten wegen der charakterisierenden Eigenschaft der Semi-Faktoren beschränkt sein, im Widerspruch zur Maximalität dieser Elemente.

Ist (U, L) ∈ sn({x}), so ist nach dem oben Gesagten (U, ∅) ∈ p_{F} (sn({x})), und wegen Proposition A.1 finden wir ein (U′, L′) ∈ sn({x}) mit (U′, L′) ⊒ (U, ∅) und L′ ≠ ∅. Der kleinste Snack mit nichtleerer zweiter Komponente, der oberhalb von (U, ∅) liegt, ist (U, {U}). Folglich ist (U, {U}) ∈ p_{F} (sn({x}).

Wir betrachten nun die Menge derjenigen Erzeuger der Mengen L ∈ L, die unterhalb von x liegen. Dies ist eine endliche Menge kompakter Elemente, deren Supremum k wiederum kleiner oder gleich x und kompakt ist. Es ist (↑k, {↑k}) ∈ sn({x}) und — wegen der vorangegangenen Argumentation — (↑k, {↑k}) ∈ p_{F} (sn({x})). Da k ∈ U und k ∈ L für alle L ∈ L gilt, ist (↑k, {↑k}) ⊒ (U, L), so daß auch (U, L) ∈ p_{F} (sn({x})) ist. Damit erhalten wir p_{F} (sn({x})) = sn({x}), also sn({x}) ∈ F.

Lemma A.6 Ist ↓(∅, ∅) in einem Semifaktor F des Snack-Potenzbereichs eines Bereichs D enthalten, so ist F = P^{S}(D).

Beweis: Es genügt, zu zeigen, daß alle maximalen Elemente von P^{S}(D) in F enthalten sind. Diese sind nach Satz 2.2.7 genau die Mengen sn(X) der Snacks, die den Schnitt X einer Scott-kompakten Teilmenge von D mit D_{max} approximieren.

Es sei also X eine solche Teilmenge von D_{max} und (U, L) ∈ sn(X). Für jedes x ∈ X ist S_{(U,x)} := ↓{(U, {U ∩ ↑k}) | k ∈ ↓x ∩ KD} ein Ideal in S(D), und es ist S_{(U,x)} ⊆ sn({x}). Da sn({x}) nach Lemma A.5 in F enthalten ist, folgt auch S_{(U,x)} ∈ F. Ist L = {L_{1}, …, L_{n}}, so findet man zu jedem i ∈ {1, …, n} ein x_{i} ∈ X ∩ L_{i}. Die Menge S_{(U;x_{1},...,x_{n})} := ↓{(U, {U∩↑k_{1}, …, U∩↑k_{n}}) | k_{i} ∈ ↓x_{i}∩KD, i = 1, …, n} ist in P^{S}(D), und sie ist das Supremum der Mengen S_{(U,x_{1})}, …, S_{(U,x_{n})}. Da F unter existierenden Suprema abgeschlossen ist, folgt S_{(U;x_{1},...,x_{n})} ∈ F. Nun ist ↓(U, L) ⊆ S_{(U;x_{1},...,x_{n})}, weshalb auch ↓(U, L) ∈ F ist.

Dies gilt für alle (U, L) ∈ sn(X). Die Ideale ↓(U, L) mit (U, L) ∈ sn(X) bilden ein gerichtetes System in P^{S}(D), dessen Supremum gerade sn(X) ist. Da alle Elemente dieses gerichteten Systems in F liegen und F unter existierenden Suprema abgeschlossen ist, folgt sn(X) ∈ F.

Damit erhalten wir den Beweis des Hauptergebnisses dieses Abschnitts: Beweis von Satz 3.1.2 Nach Lemma A.4 enthalten alle nichttrivialen Semifaktoren das Ideal ↓(∅, ∅). Die Semifaktoren, die dieses Ideal enthalten, sind nach Lemma A.6 jedoch gleich dem Snack-Potenzbereich selbst, also trivial.

84 ANHANG A. SEMIFAKTOREN IM SNACK-POTENZBEREICH

Literaturverzeichnis

[Abr91a] S. Abramsky. A domain equation for bisimulation. Information and Computation, 92:161–218, 1991.

[Abr91b] S. Abramsky. Domain theory in logical form. Annals of Pure and Applied Logic, 51:1–77, 1991.

[AJ95] S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 3. Clarendon Press, 1995.

[BDW88] P. Buneman, S. Davidson, and A. Watters. A semantics for complex objects and approximate queries. In Principles of Database Systems. ACM, 1988.

[BJO91] P. Buneman, A. Jung, and A. Ohori. Using powerdomains to generalize relational databases. Theoretical Computer Science, 91:23–55, 1991.

[BTBW92] V. Breazu-Tannen, P. Buneman, and L. Wong. Naturally embedded query languages. In J. Biskup and R. Hull, editors, Database Theory - ICDT’92, volume 646 of Lecture Notes in Computer Science, pages 140–154. Springer Verlag, 1992.

[GHK^{+}80] G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. Mislove, and D. S. Scott. A Compendium of Continuous Lattices. Springer Verlag, 1980.

[Gun92] C. Gunter. The mixed power domain. Theoretical Computer Science, 103:311–334, 1992.

[Hec90] R. Heckmann. Power Domain Constructions. Dissertation, Universität des Saarlandes, 1990.

[HM81] K. H. Hofmann and M. Mislove. Local compactness and continuous lattices. In B. Banaschewski and R.-E. Hoffmann, editors, Continuous Lattices, Proceedings Bremen 1979, volume 871 of Lecture Notes in Mathematics, pages 209–248. Springer Verlag, 1981.

[HP79] M. C. B. Hennessy and G. D. Plotkin. Full abstraction for a simple parallel programming language. In J. Beçvar, editor, Mathematical Foundations of Computer Science, volume 74 of Lecture Notes in Computer Science. Springer Verlag, 1979.

[JLP92] A. Jung, L. Libkin, and H. Puhlmann. Decomposition of domains. In S. Brookes, M. Main, A. Melton, M. Mislove, and D. Schmidt, editors, Mathematical Foundations of Programming Semantics, volume 598 of Lecture Notes in Computer Science, pages 235–258. Springer Verlag, 1992.

[Joh82] P. T. Johnstone. Stone Spaces, volume 3 of Cambridge Studies in Advanced Mathematics. Cambridge University Press, Cambridge, 1982.

[JP95] A. Jung and H. Puhlmann. Types, logic, and semantics for nested databases. Electronic Notes in Theoretical Computer Science, (1), 1995. Proceedings of the 11th Conference on Mathematical Foundations of Programming Semantics.

[JS82] G. Jaeschke and H.-J. Schek. Remarks on the algebra of non first normal form relations. In Proceedings of the ACM SIGACT/SIGMOD Symposium on Principles of DBS, 1982.

[KP94] K. Keimel and J. Paseka. A direct proof of the Hofmann-Mislove theorem. Proceedings of the AMS, 120:301–303, 1994.

[Nga92] Teow-Hin Ngair. Convex Spaces as an Order-theoretic Basis for Problem Solving. PhD thesis, Department of Computer and Information Science, University of Pennsylvania, July 1992.

[Pło67] J. Płonka. On distributive quasi-lattices. Fundamenta Mathematicae, 60:191–200, 1967.

[Plo76] G. D. Plotkin. A powerdomain construction. SIAM Journal on Computing, 5:452–487, 1976.

[Plo81] G. D. Plotkin. Post-graduate lecture notes in advanced domain theory (incorporating the “Pisa Notes”). Dept. of Computer Science, Univ. of Edinburgh, 1981.

[Puh90] H. Puhlmann. Verallgemeinerung relationaler Schemata in Datenbanken mit Informationsordnung, 1990. Diplomarbeit, Technische Hochschule Darmstadt, 78 pp.

[Puh91] H. Puhlmann. A Semantics for Generalized Database Relations. Master’s thesis, Imperial College of Science, Technology and Medicine, London, 1991.

[Puh93] H. Puhlmann. The snack powerdomain for database semantics. In A. M. Borzyszkowski and S. Sokołowski, editors, Mathematical Foundations of Computer Science, volume 711 of Lecture Notes in Computer Science, pages 650–659, 1993.

[Rom80] A. Romanowska. On bisemilattices with one distributive law. Algebra Universalis, 10:36–47, 1980.

[Sch88] M. H. Scholl. Das Modell geschachtelter Relationen. Dissertation, Fachbereich Informatik, Technische Hochschule Darmstadt, 1988.

[Sco70] D. S. Scott. Outline of a mathematical theory of computation. In 4th Annual Princeton Conference on Information Sciences and Systems, pages 169–176, 1970.

[Sco81] D. S. Scott. Lectures on a mathematical theory of computation. Monograph PRG-19, Oxford University Computing Laboratory, Oxford, 1981.

[Sco82] D. S. Scott. Domains for denotational semantics. In M. Nielson and E. M. Schmidt, editors, International Colloquium on Automata, Languages and Programs, volume 140 of Lecture Notes in Computer Science, pages 577– 613. Springer Verlag, 1982.

[Smy78] M. B. Smyth. Powerdomains. Journal of Computer and Systems Sciences, 16:23–36, 1978.

[SS86] H.-J. Schek and M. Scholl. The relational model with relation-valued attributes. Information Systems, 11:137–147, 1986.

[Vic89] S. J. Vickers. Topology Via Logic. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

[Zan84] C. Zaniolo. Database relation with null values. Journal of Computer and System Sciences, 28:142–166, 1984.

Lebenslauf

Name: Hermann Puhlmann Geboren am 22.04.64 in Frankfurt am Main

1970–1974 Besuch der Albert-Schweitzer-Schule (Grundschule), Neu-Isenburg, 1974–1976 Besuch der Schule am Buchenbusch (Förderstufe), Neu-Isenburg, 1976–1983 Besuch des Goethe-Gymnasiums, Neu-Isenburg, 1983 Reifeprüfung, 1983–1984 Grundwehr- und Zivildienst, 1984–1990 Studium der Fächer Mathematik und Informatik an der Technischen

Hochschule Darmstadt, 1990 Diplom in den Fächern Mathematik und Informatik, 1990–1991 Studium der ”Foundations of Advanced Information Technology“ am

Imperial College of Science and Technology, London, abgeschlossen mit dem ”Diploma of the Imperial College“ und dem ”Master of Science“ der University of London.

seit November 1991 Wissenschaftlicher Mitarbeiter am Fachbereich Mathematik der Technischen Hochschule Darmstadt.