Next: Sortenbedingungen Up: Integration von Sortenals ausgezeichnete Previous: Einleitung

Sorten als First-Class Citizens

In RELFUN werden Sorten als un"are Pr"adikate aufgefa"st, die auf besondere Weise definiert und benutzt werden.

Um ein Pr"adikat als Sorte zu benutzen, wird einfach eine Variante seines Namen verwendet; es gibt also keine getrennte Deklaration der Sorten. Um die Sorten (-namen) von Konstanten (kein Pr"afix) und Variablen (,,_``-Pr"afix bzw. gro"ser Anfangsbuchstabe) unterscheiden zu k"onnen, zeichnet man Sorten mit einem neuen Pr"afixzeichen (,,$``) aus.

Defaultm"a"sig sind Variablen in RELFUN nicht typisiert; jetzt k"onnen sie durch einen ,,:``-Infix getypt werden, also in ihrem Wertebereich eingeschr"ankt werden.

X : $dog
Die Variable X kann nur noch Werte der Sorte $dog annehmen.

Eine Sorte $s subsumiert eine Sorte $s, wenn die Sorte $s alle Individuen der Sorte $s (und evtl. zus"atzliche Individuen) enth"alt. Mit anderen Worten, die Sorte $s ist spezieller als die Sorte $s. "Uber diese Subsumtionsrelation kann man die Sorten in Beziehung zueinander setzen und erh"alt so eine Taxonomie. Es erscheint nat"urlich, diese Taxonomie mittels Hornregeln, f"ur die entsprechenden Pr"adikate, zu definieren.
veb(X) :- dog(X)
wobei die Pr"adikate veb (als Abk"urzung von vertebrate) und dog die Sorten $veb und $dog beschreiben. Die Regel dr"uckt dann aus, da"s $dog eine direkte Untersorte von $veb ist.

Allerdings sind so die subsumtionsbeschreibenden Regeln f"ur taxonomische Pr"adikate nicht mehr unterscheidbar von DATALOG-Regeln mit einer Pr"amisse f"ur gew"ohnliche un"are Pr"adikate. Dies ist f"ur die (effiziente) Verwaltung der Sorten jedoch notwendig (siehe Kapitel ). Um eine Unterscheidung zu erreichen, kann man das Wissen partionieren, d.h. die taxonomischen Regeln in eine gesonderte Partition auslagern (hier: zur bisherigen operatorbase mit dem Behauptungswissen gibt es eine sortbase mit Sortenwissen) und/oder statt mit Hornregeln durch ein ausgezeichnetes ,,second-order`` Pr"adikat (hier: subsumes) beschreiben (siehe Abbildung ).
subsumes(veb, dog).
Man beachte, da"s $dog als Untersorte von $veb definiert wird.

Gleich welche Notation man w"ahlt, wird in der ausgezeichneten Partition bzw. innerhalb des ausgezeichneten second-order Pr"adikates auf die textuelle Unterscheidung ($-Pr"afix) von Konstanten und Sorten verzichtet. Man kann vereinbaren, da"s alle un"aren Pr"adikate der Sortenpartition bzw. die Argumente der subsumes-Klauseln f"ur die sp"atere Verwendung mit einem $-Pr"afix gedacht sind.

In der Hornnotation k"onnen Sorten sowohl intensional als auch extensional benutzt werden. Intensionaler Gebrauch von Sorten soll hier bedeuten, da"s Sorten als geschlossene L"osungen geliefert werden (X is $dog bindet X an $dog; genauso pet(X), falls das Behauptungswissen pet(Y: $dog) gespeichert ist). Unter extensionalem Gebrauch wird hier das Aufz"ahlen der Individuen des Sortenpr"adikats verstanden (dog(X) bindet X an fido und lassy, falls das Sortenwissen dog(fido) und dog(lassy) gespeichert wurde). F"uhrt man ein spezielles second-order Pr"adikat subsumes zur Beschreibung der Sortenbeziehungen ein, erreicht man zwar eine Abgrenzung zum Behauptungswissen, gleichzeitig wird aber der Gebrauch von Sorten i.a. auf intensionale Art beschr"ankt.

W"unschenswert ist es jedoch, Sorten sowohl intensional als auch extensional nutzen zu k"onnen (siehe Abbildung ).

Eine zweite M"oglichkeit der Abgrenzung besteht in der Strukturierung des Wissens mittels Partitionierung. Die Einteilung des Wissens in Partitionen ergibt sich aus dem inhaltlichen Zusammenhang. So erh"alt man eine Partition mit Behauptungswissen operatorbase und eine Partition mit dem zus"atzlichen ,,Sortenwissen`` sortbase. Dabei k"onnen die operatorbase und die sortbase noch weiter untergliedert sein. Die sortbase k"onnte noch in Taxonomisches-/ und Instantiierungs- (KL-ONE: assertionales) Wissen unterteilt werden. Da sich die Notation des Taxonomisches-/ und Instantiierungs-Wissens eindeutig unterscheidet (Instantiierungen: un"are Fakten; Taxonomien: bin"are Fakten [subsumes-Notation] oder un"are DATALOG-Regeln mit einer Pr"amisse), ist diese weitere Partitionierung zum Zweck der Trennung verschiedenartigen Wissens nicht n"otig. Bei dem Partitionskonzept ist zu beachten, da"s Wissen auf keinen Fall "uberschrieben werden darf, also die verschiedenen Partitionen disjunkt sein m"ussen. Dies wird durch die Voraussetzung, da"s gleichnamige Pr"adikate nur in einer Partition definiert werden d"urfen, sichergestellt (siehe Abbildung ).

Man beachte, da"s durch eine Unterscheidung in verschiedenartiges Wissen der Benutzer stets wissen mu"s, was als Sortenwissen und was als Behauptungswissen definiert wurde. Au"serdem ergibt sich, bei der Erstellung der Wissensbasis, die Frage, welche un"aren DATALOG-Pr"adikate "uberhaupt taxonomisch wertvoll sind, d.h berechtigt sind als Sorte modelliert zu werden[NG94]. Hier bedeutet das, welches Wissen geh"ort in die sortbase bzw. mu"s mit subsumes-Fakten beschrieben werden.


Die Individuen einer Sorte werden explizit aufgez"ahlt. Dies geschieht durch un"are Fakten:

dog(lassy)
Das Individuum lassy wird der Sorte $dog zugewiesen.

Dabei werden Individuen von Sorten an ihre "ubergeordneten Sorten weitergereicht:
veb(lassy).
Mit obiger Instanzenzuweisung mu"s das Individuum lassy nicht mehr explizit f"ur die Sorte $veb angegeben werden, da lassy bereits als Individuum von $dog definiert wurde und $dog eine Untersorte von $mammal und diese wiederum eine Untersorte von $veb ist (siehe Abbildung ).

Eine Sorte repr"asentiert alle Individuen ihrer Untersorten und zus"atzlich noch die Individuen, die direkt f"ur diese Sorte definiert wurden.

Man beachte, da"s die Sorten hier extensional (durch Aufz"ahlen der Individuen) beschrieben werden. Potentiell unendlichen Sorten k"onnen also nicht beschreiben werden.

Sorten werden in RELFUN auf nat"urliche Weise integriert, was bedeutet, da"s sie genauso wie ,,gew"ohnliche`` Terme verwendet werden. Sie k"onnen also an

Um Sorten als solche First-Class Citizens[Bol94], d.h. vollwertige Sprachobjekte, einzubauen, mu"s die Unifikation zu einer ordnungssortierten Unifikation erweitert werden. Die Sorteninformation soll w"ahrend der Unifikation benutzt werden [BBDV91].

Unifikation von Sorten (o.B.d.A wird Sorte als 2. Term benutzt):

Bei der Unifikation einer freien Variablen mit einer Sorte wird die Variable in ihrem Wertebereich eingeschr"ankt, d.h. getypt. Ist die Variable bereits gebunden, verh"alt sich die Unifikation entsprechend dem Inhalt der Variable. Unifiziert man zwei Sorten, wird von allen gemeinsamen Untersorten (common lower bounds) die allgemeinste/ gr"o"ste Untersorte (GLB - greatest lower bound, Infimum) zum Ergebnis der Unifikation.

X is $mammal, X is $carnivore
Die Variable X wird zun"achst an die Sorte $mammal und mit der zweiten Zuweisung an die Sorte $carnivore gebunden. Hier m"ussen die Sorten $mammal und $carnivore unifiziert werden. Das Ergebnis der Unifikation ist der GLB $cat dieser Sorten.

Man kann endliche Sorten als benannte endliche Dom"anen verstehen. Wird also eine endliche Dom"ane mit einer (endlichen) Sorte unifiziert, wird der Schnitt zwischen der endlichen Dom"ane und der Sorte gebildet. Als Resultat erh"alt man eine neue endliche Dom"ane mit denjenigen Elementen der urspr"unglichen Dom"ane, die gleichzeitig auch Individuen der Sorte sind. In dem Spezialfall einer Konstanten (einelementige endliche Dom"ane) ist die Unifikation nur erfolgreich, wenn die Konstante ein Individuum der Sorte ist.

X is $dog, X is dom[fido, fifi, lassy
] unifiziert mit X = dom[fido, lassy].
X is $dog, X is fido
unifiziert mit X = fido.

Die Unifikation einer endlichen Exklusion (,,negierte`` endliche Dom"ane) [Bol94] mit einer potentiell unendlichen Sorte st"o"st auf gro"se Implementationsprobleme, trotzdem m"u"ste man bei endlichen Sorten eine solche Unifikation erlauben. Nat"urlich sollen sich unendliche und endliche Sorten gleich verhalten; deshalb mu"s hier auf die Unifikation von endlichen Sorten mit Exklusionen verzichtet werden.



Next: Sortenbedingungen Up: Integration von Sortenals ausgezeichnete Previous: Einleitung


Harold Boley & Victoria Hall (hall@dfki.uni-kl.de)