Wir waren stehen geblieben bei der Frage nach Normalformen im Fall der
Prädikatenlogik und hatten zuerst festgestellt, das ist die hier
vorgezeigte Folie,
dass wir in der Lage sind, die sämtlichen Quantoren, die in einer
Formel vorkommen, ganz nach vorne zu ziehen und damit die sogenannte
Pränex in Normalform herzustellen.
Die Methodik, mit der das gemacht wird, sahen wir auf der
vorangehenden Folie, bei der wir feststellten, du kannst also ein NOT,
was vor einem Quantor steht, nach hinten bringen.
Du kannst das ODER nach hinten bringen und du kannst genauso das UND
nach hinten bringen und damit können wir also sämtliche Teile einer
Formel, die nichts mit Quantoren zu tun hat, hinter die
Quantorenzeichen bringen.
Das, was notwendig ist dabei, ist möglicherweise Umbenennung von
Variablen, weil hier jeweils die Bedingung dabei stand, dass die
Variable, die wir nach vorne schieben wollen mit ihrem Quantor, nicht
frei vorkommen darf in dem Teil, über den wir wegschieben.
Damit ist also geklärt, dass wir, wie in diesem Beispiel vorgezeigt,
irgendeine solche Formel hernehmen können und schrittweise zunächst
einmal feststellen können, dieses NICHT kann ersetzt werden durch ein
Existenzquantor.
Dabei rutscht das NICHT nach hinten.
Außerdem ist es zweckmäßig, das X bei der Gelegenheit umzubinden, weil
X da vorne noch mal vorkommt, weshalb ich es hier jetzt Z genannt
habe.
Und anschließend haben wir es nur noch mit ODERS und UNDS zu tun und
können die ganze Geschichte also nach vorne ziehen und haben dann zum
Schluss die drei Quantoren vorne stehen und hintendran eine
Quantorenfreie Formel und das heißt, bereits die Normalform
herstellen.
Also eigentliche Aktion, sich überlegen, dass man bei dem NOT die
Quantoren vertauschen muss und dass man aufpassen muss, dass man also
nicht denselben Bezeichner für zwei verschiedene Zwecke benutzt.
Und da muss man einfach umbenennen.
Die Quantoren bleiben dabei in der Reihenfolge, in der sie in der
ursprünglichen Formel standen.
Also da stand für alle X, es existiert Y.
Für alle X, das für alle X, hier hatten wir durch existiert Z ersetzt
und die Reihenfolge bleibt erhalten.
Vertauschung von Reihenfolgen von Quantoren kommt bei dieser
Transformation nicht vor.
Und wir hatten ja auch bereits gesehen, an dieser Stelle, dass diese
Geschichte mit Vertauschung von Quantoren Schwierigkeiten machen wird.
Ich muss das vielleicht nochmal ganz deutlich hinmalen.
Das ist nicht äquivalent zur
Stetigkeitsdefinition, die ich hier hingeschrieben hatte, nur deshalb,
weil ich also die Quantoren miteinander vertauscht hatte.
Ist die nächste Frage dementsprechend, können wir das ganze Ding nicht
noch ein zweiter standardisieren und zum Beispiel verlangen, am Anfang
müssen alle Altquantoren kommen, dann dürfen Existenzquantoren kommen
und danach die Quantorenfreie Formel.
Also die ganze Geschichte noch sortieren.
Das funktioniert leider nicht.
Das Einzige, was funktioniert an dieser Stelle, ist, man kann die
Existenzquantoren komplett rausschmeißen.
Dann bleiben nur die Altquantoren stehen und das ist also dieser Satz
hier, zu jeder prädikatischen logischen Formel F gibt es eine Formel
G, die nur noch die Altquantoren enthält, die auch in F vorkamen.
G' ist Quantorenfrei, wir haben also pränexe Normalform und haben
sämtliche Existenzquantoren rausgeworfen.
Allerdings ist die Transformation, die dieses G herstellt, nun keine
syntaktische Transformation mehr.
Ich kann also nicht sagen, ersetze doch bitte schön diese und jene
Teilformel durch eine bestimmte andere Teilformel.
Und daher, weil es keine syntaktische Transformation ist, kann ich
auch nur noch fordern, dass F genau dann erfüllbar ist, wenn G
erfüllbar ist.
Sprich, ich kann sämantische Äquivalenz herstellen, aber ich kann
keine syntaktische Äquivalenz herstellen.
Diese Transformation, die das leistet, wurde von einem Herrn Skolem
erfunden und heißt daher Skolem-Form.
Von F, die Herstellung der Transformation, wird im Jargon als
Skolemisieren bezeichnet.
Das heißt also, G ist die sogenannte Skolemisierte
Fassung von F.
Und um uns klarzumachen, was da für eine Grundidee zugrunde liegt,
schauen wir uns nochmal unsere Stetigkeitsdefinition an, die wir hier
hingeschrieben hatten.
Die heißt ja also, für alle Epsilon größer als 0 existiert ein Delta
größer als 0.
Nun, wenn ich etwas weiß über die Funktion F, dann kann ich das Delta
ausrechnen, wenn das Epsilon gegeben ist.
Wenn ich zum Beispiel also weiß,
dass F von X eine lineare Funktion ist, A X plus B, dann weiß ich
sofort, welches Delta das Ganze tut,
nämlich dann wähle ich Delta gleich Epsilon durch A und dann rechnet
sich sofort aus, dass in der Tat für dieses Delta aus der Gleichung X
minus Y kleiner als Delta das Gewünschte folgt.
Denn was haben wir denn hier?
Wir haben hier hingeschrieben, Epsilon durch A, dann würde also hier
stehen, X minus Epsilon kleiner als Epsilon dividiert durch A.
Kann ich mit A durchmultiplizieren, dann bekomme ich A X minus A Y,
muss kleiner als Delta sein, damit F von X minus F von Y kleiner als
Delta ist.
Nun, da drüben steht genau dieselbe Formel, A X minus A Y.
Also das ist das größte Delta, was ich wählen kann.
Und ich lerne, ich kann also das Delta wählen, wenn ich das Epsilon
kenne.
Und dann ist das Delta eine Funktion von Epsilon.
Diese Idee lässt sich generalisieren und das ist genau der Inhalt der
Skolemisierung.
Man bestimmt solche Skolem-Funktionen, die sagen, wenn du hast eine
Formel für alle X1 bis für alle Xn und dann einen Existenzquantor Y,
dann kannst du das transformieren in die Form, die Allquantoren
bleiben stehen.
Und jetzt nehmen wir die Formel, die hinten dran kommt und setzen in
der Formel, die hinten dran kommt, eine Funktion ein, man nennt sie
eine Skolem-Funktion, die abhängt von all den Variablen, die vorne
dran allquantifiziert sind.
Vorhin war es das eine Epsilon, jetzt generalisiere ich das und sage,
da stehen also beliebige solche Funktionen, Sk von X1 bis Xn.
Und diese Funktion setzt sich an all den Stellen ein, wo das Y in
meiner Formel kommt und lässt das Existiert Y weg.
Das habe ich hier am Beispiel vorgeführt.
Da kommen zwei Existenzquantoren vor.
Das Existiert V kommt nachdem für alle U.
Infolgedessen muss ich für V eine Skolem-Funktion wählen, die von U
abhängt.
Das Existiert Y kommt nach für alle U und für alle X.
Also muss ich für Y eine Skolem-Funktion wählen, die von beiden
Variablen U und X abhängt.
Und das Ergebnis sehen Sie hier unten.
Hier hatte ich halt so ursprünglich das einfache Prädikat P von U, V,
X und Y.
Und jetzt schreibe ich hin U.
Das V ersetzt sich durch seine Skolem-Funktion, die hat U als
Argument.
X lasse ich stehen und Y ersetzt sich durch die Skolem-Funktion, die
von U und X abhängt.
Wie die Skolem-Funktion im Einzelnen aussieht, das weiß ich nicht.
Das hängt außerdem von dem P ab.
Haben wir gerade am Beispiel gesehen.
Unsere Ersetzung für Delta ging ja auch noch davon ab, dass wir
wussten, dass F von X eine lineare Funktion ist.
Wenn ich da F von X gleich X² gewählt hätte, wäre die ganze Geschichte
anders gelaufen.
Das heißt also, das ist eine rein formale Transformation, bei der ich
noch nicht gesagt habe, wie die Funktion aussieht.
Und das ist ja auch verständlich.
Die ursprüngliche Formel sagte, es existiert ein V.
Und ich habe mich bequem zurückgelegt und habe gesagt, ja, es
existiert eine Skolem-Funktion.
Ich habe aber weder ursprünglich gesagt, wie das V berechnet wird,
noch sage ich jetzt, wie die Skolem-Funktion aussieht.
Das ist eine rein formale Transformation, die aber den Zweck erfüllt,
eine Formel herzustellen, bei der nur noch i-Quantoren vorkommen.
Und wir merken uns aus der ganzen Geschichte in Feuchte dessen, man
kann zunächst eine Normalform herstellen, und dann kann man, wenn man
will, auch noch die Existenzquantoren in semantisch gleichwertiger
Weise beseitigen.
Die für alle Quantoren kann man nicht beseitigen, die bleiben immer
stehen.
Also ist die Grundformel, mit der wir es immer zu tun haben, eine
prädikatenlogische Formel, die mit einer Reihe von a-Quantoren
beginnt.
Die Existenzquantoren könnten wir rausschmeißen können, aber die a
-Quantoren können wir nicht rausschmeißen.
Gibt es Fragen dazu?
Wenn nein, dann spezialisieren wir uns jetzt mit dem Ziel,
herauszufinden, wie logisches Programmieren funktioniert.
Dazu muss ich anfangen in der Logik bei einem Herrn Herbrand.
Der ist, wie Sie den Daten entnehmen, nur 27 Jahre alt geworden.
Er stürzte beim Bergsteigen in den Alpen ab.
Er hatte aber eine ganze Reihe ganz toller Ideen, weshalb es auch
heute noch einen Satz und verschiedene Dinge gibt, die nach ihm
benannt sind.
Die Grundidee, die hier vorkommt, ist die folgende.
Wir haben also gesehen, die Logiker haben da ein Alphabet.
Das besteht aus einer Menge von Prädikaten, einer Menge von
Funktionen.
Damit kann ich Terme definieren.
Und dann bilden sie bei Interpretation dieses Alphabet in eine
Struktur ab.
Und dazu brauchen sie eine Belegung.
Die Interpretation habe ich hier hingeschrieben.
Und hier steht also die Belegung der Struktur A.
Wenn ich mir aber jetzt anschaue, wie die Regeln sind für diese
Interpretation.
Da muss ich also zurück auf Folie 38.
Da stehen die alle.
Und mich jetzt erinnere, was die Homomorphie-Bedingung zwischen Term
-Algebren war.
Das hatten wir in Kapitel 3.
Dann stelle ich sofort fest, was hier aufgeschrieben ist, ist im
Prinzip eine Spezialisierung der Homomorphie-Bedingung.
Das heißt, ich habe eigentlich einen Homomorphismus vorliegen.
Und wenn ich also einen Homomorphismus vorliegen habe, von irgendeinem
Alphabet in eine solche Struktur.
Dann weise ich, der induziert insbesondere einen Homomorphismus der
Term -Algebra, die dem Alphabet zugrunde lag, in das Universum, auf
das ich meine Interpretation abbilde.
Und dann kommt dieser Homomorphie-Satz der Algebra, der sagt, wenn du
eine solche Abbildung hast, von deiner Term-Algebra T in diese
Struktur A, dann kannst du die faktorisieren.
Du kannst zunächst einmal bilden, T-Potient davon über eine
Äquivalenzrelation.
Und dann hast du von da einen Isomorphismus oder Endomorphismus nach A
hinein.
Das war der Inhalt des Homomorphie-Satzes.
Was sagt denn hier diese Äquivalenzrelation?
Die Äquivalenzrelation sagt, wenn es irgendwelche Gleichheiten gibt,
Aktionen, die bereits in T gelten, dann legen wir die verschiedenen
Terme T zusammen, die hier unter der Äquivalenzrelation gleich werden
und dann bekommen wir die Algebra-Potient von T nach dieser
Äquivalenzrelation heraus.
So war die ganze Geschichte definiert.
Jetzt schaue ich doch mal nach und stelle fest, in den Formeln, in
denen irgendwelche Terme vorkommen, da gibt es gar keine Äquivalenz
auf der Term-Ebene.
Die Terme sind alle verschieden.
Jubel.
Wir können das ganze Ding vereinfachen.
Na, wo ist mein Rotstift?
Ja, hier.
Wir stellen fest, dass dieser Teil gestrichen werden kann.
Da ist gar nichts, was gleichzusetzen ist.
Und infolgedessen haben wir also jetzt diese Art von Abbildung.
Und ja, was ist denn die Termalgebra, von der die Rede ist?
Die Termalgebra enthält all die Funktionen, die in unserer
ursprünglichen Formelmenge vorkommen.
Mehr enthält sie nicht.
Andere brauchen wir nicht.
Und infolgedessen geben wir dieser speziellen Termalgebra jetzt einen
Namen.
Wir betrachten das sogenannte Herbrand-Universum und das ist die
initiale Grundtermalgebra über den sämtlichen Funktionen, die in
unseren Formeln vorkommen.
Das ist also eine Einschränkung.
Irgendwelche Operationen, die zwar vielleicht ursprünglich mal
definiert waren, die aber in meinen speziellen Formeln nicht benutzt
werden, die lassen wir weg.
Und das führt uns zum Herbrand-Universum.
Das ist also eine ganz gewöhnliche initiale Grundtermalgebra.
Damit die vernünftig definiert werden kann, ist es allerdings
notwendig, dass mindestens eine Konstante vorkommt.
Das muss in unseren Formeln unter Umständen nicht der Fall sein.
Und infolgedessen nehme ich sicherheitshalber zu Sigma f noch ein
nullstelliges Funktionssymbol dazu, wenn kein solches vorkommt.
Ein Beispiel, wenn also meine Formel etwa lautet, für alle x gilt p
von x oder q von f von x,y Wobei y hier jetzt eine freie Variable ist.
Wie sieht dann das Herbrand-Universum aus?
Und ich kann es aufzählen.
Ich sehe das als Termin hier vorkommen x.
Das ist offensichtlich eine Konstante, nullstellig.
Und außerdem kommt vor f von x,y.
Da ist das y offensichtlich auch eine solche nullstellige Funktion.
Und infolgedessen kann ich jetzt anfangen das Herbrand-Universum
aufzuschreiben.
Es besteht aus x, es besteht aus y.
Dann kommt f von... und jetzt kann ich also beliebige Terme, die ich
schon habe, einsetzen.
Also f von x,x.
f von x,y.
f von y,y.
Ja, jetzt habe ich noch einige Terme dazugekriegt.
Die kann ich auch wieder als Argumente von f gebrauchen.
Also geht die ganze Geschichte weiter mit f von x,x.
Das zweite brauche ich noch nicht ersetzen.
Kann ich aber auch noch, ich kann also auch noch hinschreiben, f von x
,x und f von y,y und so weiter.
Die ganze Geschichte geht endlos weiter, weil ich das f beliebig oft
iterieren kann.
Ja.
Diese endlose Iteration, die ganze Zeit die Terme, die wir schon
gehabt haben, die wir da schon angefangen haben, hinzuschreiben,
nochmals als Argumente einzusetzen, das liefert mir mein Herbrand
-Universum.
Ja, und für den Fall jetzt, dass meine Formel f keine freien Variablen
aufweist, man nennt das eine geschlossene Formel, kann ich eine
Herbrand -Interpretation herleiten.
Und das ist eine Interpretation, die sagt, ich bewerte entsprechend
der Isomorphie, die ich hier habe, alle Terme, die ich hier habe,
genauso, wie ich sie bewerten würde in meiner Struktur A.
Und für den Fall, dass diese Struktur A mit dieser variablen Belächung
die Formel erfüllt, kann ich dann feststellen, wegen dieser
Isomorphie, die wir hier haben, erfüllt die Herbrand-Interpretation
ebenfalls diese Formel.
Und der Schlussstrich der ganzen Geschichte lautete, statt der
unzählig vielen Möglichkeiten, irgendwelche Strukturen A zu
betrachten, die möglicherweise F erfüllen, kann ich mich darauf
beschränken zu sagen, wir schauen doch bloß mal dieses Herbrand
-Universum an und fragen, ob wir irgendeine Interpretation finden
können im Herbrand-Universum.
Wenn es die gibt, dann haben wir die Formel erfüllbar.
Wenn es die aber nicht gibt, dann kann auch keine andere
Interpretation existieren.
Das heißt, wir können unser gesamtes Augenmerk darauf richten, gibt es
diese Herbrand-Interpretation, und wenn es die nicht gibt, dann geht
gar nichts.
Das führt zu dem Satz von Herbrand, wenn eine Formel ohne freie
Variable kein Herbrand-Modell besitzt, also keine bildliche Herbrand
-Interpretation, dann gibt es überhaupt keine Möglichkeit, diese
Formel zu erfüllen.
Und das heißt, dann ist die ganze Formel unerfüllbar.
Beschränkung auf das Herbrand-Universum.
Und das Herbrand-Universum, ich wiederhole das, ist die gewöhnliche
freie Termalgebra ohne Variable, die entsteht, wenn ich mich nur
konzentriere auf die Terme, die in meiner Formel vorkommen.
Nochmal zurück zu meiner hier rot geschriebenen Formel.
Die ist für diesen Zweck nicht geeignet.
Warum?
Was für einen Fehler hat die?
Bezogen auf den Satz von Herbrand.
Die enthält Y als freie Variable und ich habe verlangt, dass das Ding
geschlossen ist.
Keine freien Variablen enthält.
Ich kann also das Herbrand-Universum konstruieren für diese Formel,
aber die Herbrand-Interpretation ist nur definiert, wenn keine freien
Variablen vorkämen.
Das heißt also, für diesen Zweck müsste ich auch noch davor
geschrieben haben für alle Y, dann ginge es.
Dann wäre auch das Y noch geschlossen.
So, diesen Satz von Herbrand, der sagt, konzentriere dich auf das
Herbrand -Universum und wenn eine geschlossene Formel da nicht
erfüllbar ist, dann ist sie überhaupt nicht erfüllbar, den wendet man
jetzt im logischen Programmieren an.
Und die Idee dazu hatte 1951 ein norwegischer Logiker namens Horn.
Und der hat sich zunächst auf ganz spezielle Prädikaten, logische
Formeln konzentriert.
Er hat nämlich gesagt, wir betrachten zunächst mal eine Menge von
atomaren Formeln.
Atomare Formeln sind also, wie wir wissen, entweder Konstante, 0 oder
1, oder einfache Prädikate.
Und jetzt definiert er sogenannte Klauseln, die nach ihm benannt
werden und daher Hornklauseln heißen.
Und die sind alle von der Bauart aus der Konjunktion mehrerer atomarer
Formeln.
Folgt eine andere atomare Formel.
Und wenn ich das umschreibe unter Kenntnis, was der Implikationsfall
bedeutet, dann heißt das, diese Hornklauseln sind alle Disjunktionen,
bei denen eine, aber nur eine der Operanten kein Negationszeichen
trägt.
Alle anderen sind negiert.
Und von den Hornklauseln kann ich jetzt drei verschiedene Fassungen
unterscheiden.
Nämlich erstmal das, was intuitiv verständlich ist.
Das Ganze ist eine Implikation, aus P1 bis Pm folgt Q.
Und diese Implikation liegt dann vor, wenn also M größer gleich 1 ist,
mindestens eine Voraussetzung brauche ich.
Wenn M gleich 0 ist, dann steht da nur, es folgt Q, ohne
Voraussetzung.
Und das heißt Q ist allgemeingültig.
Das nennen wir ein Faktum.
Ja, und wenn das Q fehlt, dann haben wir nur Voraussetzungen.
Und das ist eine Frage, ob jetzt diese Voraussetzungen gelten.
Daher, wenn Q fehlt, dann soll die M natürlich größer gleich 1 sein,
denn sonst haben wir überhaupt nichts dastehen.
Und dann nennen wir das ganze Ding eine Anfrage.
Mit diesen Hornklauseln hatte jetzt Anfang der 60er Jahre ein
Engländer namens Robert Kowalski folgende Idee, die wirklich verquer
klingt.
Wenn ich solch eine Hornformel habe und beweisen will, dass irgendeine
Anfrage erfüllbar ist.
Das heißt, es soll gelten, aus der Hornformel H folgt meine Formel G.
Mit geeigneter Variablenbelegung.
Die Formeln können ja auch noch Variablen belegen.
Dann ist das gleichwertig mit der Aussage, dass die Negation dieser
Implikation unerfüllbar ist.
Ist ja klar.
Ich habe eine Ausnahme gefunden, wenn ich die Implikation finden kann.
Schön, und jetzt blätter ich zurück zu meinem Satz von Herrn Brand und
stelle fest, er macht eine Aussage über Unerfüllbarkeit.
Alles ist einqualifiziert.
Und ich kann feststellen, die Negation nicht gilt H folgt G, die ist
unerfüllbar, genau dann, wenn sie über dem Herbrand-Universum
unerfüllbar ist.
Also kann ich jetzt anfangen, über dem Herbrand-Universum zu rechnen
und muss über dem Herbrand-Universum versuchen, herauszufinden, ob in
der Tat, es gilt nicht H impliziert G, oder anders geschrieben, es
gilt H und nicht G, ob diese Formel unerfüllbar ist.
Ja, und wie beweise ich das?
Ich versuche durch systematische Maßnahmen ein Gegenbeispiel zu
konstruieren.
Wenn mir das gelingt, dann habe ich die Unerfüllbarkeit widerlegt.
Wenn es mir nicht gelingt, dann ist die ganze Geschichte
offensichtlich unerfüllbar.
Und dann weiß ich also, die Implikation gilt nicht, in der Form, in
der sie dasteht.
Damit ich jetzt die ganze Geschichte hinbekommen kann, brauche ich
noch eine weitere Voraussetzung.
Wir haben ja gesehen, der Satz von Herbrand setzt voraus, dass keine
freien Variablen vorkommen.
Also muss ich alle Variablen allquantifizieren.
Und das heißt also, ich muss eine solche Hornklausel so
interpretieren.
Für alle freien Variablen, die in P1 bis Pm und Q vorkommen, gilt
diese Implikation.
Allquantifikation über sämtliche Variablen, die vorkommen.
Und dann überlege ich mir, Gegenbeispiele verlangen, dass ich eine
einzelne Belegung habe.
Und die tolle Idee, die der Herr Kowalski jetzt hatte, lautete, dieses
Gegenbeispiel, das berechne ich mit Hilfe von Unifikation.
Versuche herauszufinden, ob ich die Voraussetzungen erfüllen kann,
indem ich die Variablen, die darin vorkommen, spezialisiere auf Werte,
sodass die Anfrage passt.
Diese Idee hat dann ein Franzose, Professor in Marseille à la
Colmarois, aufgegriffen und hat gesagt, das ist mir aber zu allgemein,
was du gesagt hast, lieber Robert.
Wir brauchen das spezieller, damit das deterministisch durchgeht,
während du mir so einen allgemeinen, logischen Kalkül vorgeführt hast,
der ist praktisch nicht brauchbar.
Und jetzt hat er genau die Idee von Herrn Kowalski genommen und hat
die ganze Geschichte deterministisch gemacht, mit folgenden Maßnahmen.
Erste Maßnahme, er hat gesagt, die Reihenfolge, in der du deine
Hornklausel hinschreibst, die ist für mich interessant, die werde ich
beachten und ich arbeite nur dann vernünftig weiter, wenn die erste
Hornklausel, die passt, auch tatsächlich das Ergebnis liefert.
Was heißt hier die passt?
Ja, bitte blättern Sie zurück an die Definition in Kapitel 3 von
Unifikation und dann sehen Sie, da habe ich definiert, was es passt
heißt.
Nämlich, es gibt die Substitution, dass linke und rechte Seite gleich
werden.
Ja, und wir unifizieren also die Anfrage G mit dem Kopf, dem Q, der
ersten geeigneten Hornklausel.
Wenn die also von dieser Form ist, P1 bis Pm impliziert Q, dann heißt
unifizieren ja, bestimme eine Substitution, sodass Q Sigma gleich ist
G Sigma der Anfrage.
Und da wir ja noch nicht wissen, ob die Voraussetzungen stimmen, haben
wir jetzt folgende Situation, wir wissen, G wird in der
Spezialisierung, die durch die Substitution Sigma gegeben ist,
erfüllt, unter der Voraussetzung, dass P1 bis Pm mit der
Spezialisierung, die durch Sigma vorgegeben ist, erfüllbar sind.
Also, aus der einzelnen Anfrage G wird jetzt eine Anfrage, eine Liste
von Anfragen, die besteht aus P1 Sigma bis Pm Sigma.
Und Sigma ist also die durch die bisherigen Unifikationen definierte
Variablen -Substitution.
Ja, jetzt könnte ich dann als nächstes hergehen und sagen, würfeln wir
doch, welche dieser Anfragen P1 Sigma bis Pm Sigma wir als nächstes
bearbeiten.
Das wäre wiederhin deterministisch und auch das hat Herr Kolmarower
deterministisch gemacht.
Er hat gesagt, die letzte der Liste zugefügte Anfrage wird immer als
erstes bearbeitet.
Das ist in diesem Fall das P1, also er fügt die Dinge in umgekehrter
Reihenfolge dazu, dass Pm als letztes, dass P1 als erstes.
Reihenfolge, die sich dann ergibt, ist also P1 Sigma, P2 Sigma und so
weiter.
Ja, für den Fall, dass das nicht funktioniert, weil sich eine der
Voraussetzungen nicht erfüllen lässt.
Ja, dann haben wir unter Umständen ja noch weitere Hornklauseln
vorrätig.
Diese hier, die hat es nicht getan, dann nehmen wir die nächste.
Das ist der nächste Schritt.
Wenn sich die so nicht erfüllen lässt, dann suche ich die nächste
passende Hornklausel.
Und für den Fall, dass es überhaupt keine gibt, mit denen man
weiterkommt, dann melde ich Misserfolg.
Und der Misserfolg lautet, ich habe mit diesem Verfahren nicht
feststellen können, dass die Aussage aus den vorgegebenen
Hornklauseln, folgt meiner Anfrage G, erfüllbar ist.
Das muss man sich ganz genau merken, was die Aussage ist.
Ich habe nicht feststellen können, dass das erfüllbar ist.
Und das heißen wir, die Anfrage ist fehlgeschlagen.
Aus dem Fehlschlagen der Anfrage kann folgen, in der Tat, die Anfrage
war falsch.
Es geht nicht.
Es kann aber auch folgen, durch diese Vereinfachungen, die hier
vorgenommen worden sind, bezüglich Reihenfolge, haben wir eine ganz
wichtige Möglichkeit verpasst.
Und es wäre schon gegangen, aber wir haben leider Gottes den Weg nicht
gefunden.
Und daher arrangiert dieses Fehlschlagen im Englischen unter der
Überschrift Negation by Failure.
Ich kann nur feststellen, es ist fehlgeschlagen, aber ich kann nicht
entscheiden, ob diese Antwort Nein heißt, oder ich war nur zu dumm.
Beide Möglichkeiten sind gegeben.
Frage.
Er fragt, wieso man die Methode verwendet, wenn sie nicht sicher ist.
Die Antwort lautet, an der Antwort Nein bin ich nicht interessiert.
Ich bin an der Antwort Ja interessiert.
Und wenn ich die Antwort Ja bekomme, dann bekomme ich das
Gegenbeispiel heraus.
Und das war eigentlich das, was wir haben wollten.
Sprich also, die ganze Konstruktion beruht auf der Voraussetzung, wir
sind nur an der positiven Antwort interessiert und bekommen dann unser
Beispiel.
Und für den Fall, dass es nicht gegangen ist, sagen wir nur Schade,
das Verfahren hat nicht funktioniert.
Und es hängt jetzt vom Programmierer ab, dafür zu sorgen, dass die
Antwort Schade nicht kommt in Fällen, in denen sie eigentlich falsch
gewesen wäre.
Das kann man durch Tricks im Prolog Programmieren beeinflussen.
Ich erinnere daran, was unser Ziel war.
Wir wollten nachweisen, dass aus den Hornklauseln H die Anfrage G
folgt.
Und dazu haben wir uns überlegt, dass wir nachweisen, dass H und nicht
G unerfüllbar ist.
Und die Antwort Nein heißt, ist unerfüllbar nach meiner Kenntnis.
Und wenn Ihre Kenntnisse nicht ausreichen, um eine bessere Antwort zu
geben, dann ist es eben für Sie unerfüllbar.
Aber das ist keine absolute Aussage.
Das ist die Grundidee des Verfahrens.
Und das kann man jetzt als Programmiersprache besichtigen.
Sie können das als Modul auch mit Ihrem Haskell-Interpretierer durch
Xen.
Der Herr Gelhausen hat Ihnen bereits vorgeführt, wie die ganzen
Geschichten dann geschrieben werden als Programm.
Die Hornklausel dreht man um.
Man schreibt das Q zuerst.
Statt im Implikationspfeil schreibt man ein Doppelpunkt Minus.
Und schreibt dann anschließend die Voraussetzungen P1 bis Pm mit Komma
getrennt hin.
Das Komma bedeutet also das Umzeichen an dieser Stelle.
Das Faktum, ja da ist da hinten nichts.
Das schreibt man nur einfach mit U.
Und alle solchen Formeln werden mit einem Punkt abgeschlossen.
Und eine Anfrage, ja da steht vor dem Doppelpunkt Minus nichts.
Das signalisieren wir dadurch, dass wir ein Fragezeichen vorne
hinschreiben.
Das ist also reine Syntax.
Und hier ist ein Beispiel.
Wie ich dieses Verfahren jetzt dazu benutzen kann, um in einfachen
Fällen formal zu differenzieren.
Was ich tun möchte ist, ich möchte hinschreiben eine Formel.
Dann die Variable X, nach der ich differenzieren will.
Und dann möchte ich herausbekommen das Ergebnis.
Und weil ich das jetzt mit logischem Programmieren mache, ist die
Antwort die ich bekommen will.
Diff ist ein Prädikat und liefert mir als erstes mal die Antwort ja
oder nein.
Die Antwort ja heißt, ich konnte die Formel differenzieren.
Und wenn ich die Formel differenzieren konnte, dann gebe ich dir auch
an, mit welcher Variablenbelegung ich das machen kann.
Und insbesondere, wenn du mir jetzt eine Anfrage stellst, bei dem als
Ergebnis eine Variable steht, dann spezialisier ich die ganze
Geschichte und sag dir, was das Ergebnis ist.
Und für den Fall, dass ich nicht differenzieren konnte, gebe ich dir
die Antwort nein.
Dann gebe ich aber auch nichts an.
Begründung gibt es nicht.
Die Aussage lautet nur, ich konnte nicht.
Und das sehen Sie also jetzt zunächst mal am Ergebnis.
Wenn ich hinschreibe, differenziere die Formel x mal x, einen Term,
nach der Variablen x, dann ist e, in Prolog heißt Großbuchstabe immer,
das ist eine Variable, Kleinbuchstaben sind Konstante, dann soll das
Ergebnis e sein.
Und dann liefert mir mein Prolog-System zurück, ja, dieses Prädikat
diff stimmt, vorausgesetzt, dass du für die Variable e einsetzt, x mal
1 plus 1 mal x.
Ja, in der Tat, 2x ist ja das, was wir erwarten wollten.
Dass er das so umständlich schreibt, darüber rede ich gleich noch.
Also er spezialisiert Variable, das ist das Ergebnis der Substitution.
Und auf die Art und Weise differenziere ich mit Hilfe eines Prädikats
diff.
Und wenn ich ihm aber vorgebe, die lineare Funktion a mal x plus b,
hat er mir auch ein Ergebnis zu liefern und sagt, das ist a mal 1 plus
0.
Wenn ich ihm aber frage, kannst du auch x Quadrat differenzieren, dann
sagt er no.
Anfrage fehlgeschlagen.
Und der Grund liegt daran, dass in meinem Programm, wie wir jetzt
gleich sehen werden, zwar die vier Grundrechenarten vorkommen, aber
potenzieren kommt nicht vor.
Ich habe ihm also nichts beigebracht, wie man umgehen sollte, wenn
potenziert wird.
Das ist der Fehler.
Aber das ist der Fehler meines Programms.
Das ist nicht der Fehler meiner Anfrage.
Und daraufhin reagiert er mit der Antwort no.
Ja, und wie schreibe ich jetzt meine Formeln hin?
Ich lasse mal die ersten zwei Zeilen aus.
Wenn ich eine Summe von zwei Operanten differenzieren will, nach
irgendeiner Variablen x, dann kommt es nicht darauf an, wie die
Operanten aussehen und es kommt auch nicht darauf an, was die Variable
ist, nach der ich differenzieren will.
Infolgedessen schreibe ich für den ersten und den zweiten Operanten,
genauso wie für die Variable, nach der ich differenzieren will, eine
Prologvariable, eine logische Variable hin.
Großbuchstaben sind Variablen.
Ich kenne nämlich das Ergebnis.
Das Ergebnis heißt, leite u ab und zähle dazu die Ableitung von v, du
und dv.
Jetzt muss ich aber noch hinschreiben, das gilt natürlich nur unter
der Voraussetzung, dass du tatsächlich die Ableitung von u war und die
v tatsächlich die Ableitung von v war.
Infolgedessen habe ich eine Implikation, die sagt, dieses Ergebnis
kriegst du heraus unter der Voraussetzung, dass du das Ergebnis ist
des Ableitens von u nach x und analog für v.
Das können wir natürlich mit Subtraktion genauso machen und mit
Multiplikation ebenfalls.
Da haben wir eine etwas kompliziertere Formel und für die Division
ganz genauso.
Und was hier steht in dieser Spalte, das sind also die Regeln, die Sie
wohl kennen über Differenzieren.
Und die Voraussetzungen sind immer gleich.
Du hast die Ableitung deiner einzelnen Operanten richtig berechnet.
Ja, jetzt brauchen wir noch die Elementarfälle.
Der Elementarfall ist zunächst einmal, wenn du x nach x ableitest,
dann bekommst du 1 heraus.
Und der zweite Elementarfall ist, wenn du versuchst, eine Konstante
abzuleiten, dann sollst du 0 rauskriegen.
Also schreiben wir das doch auch noch hin.
Diff xx liefert uns die 1 als Ergebnis.
Und Diff Konstante nach x liefert uns die 0 als Ergebnis.
Jetzt muss ich nur noch spezifizieren und C ist tatsächlich eine
Konstante.
Ich weiß nicht welche, aber es ist eine Konstante.
Dazu gibt es jetzt in Prolog eine ganze Reihe vorgefertigter
Prädikate.
Eines dieser vorgefertigten Prädikate heißt Atomic.
Und heißt, dieses C ist ein Term, der keine weiteren Operanten
enthält.
Also f von T1 bis Tn kannst du dafür nicht einsetzen.
Sondern nur einen einfachen Term, der damit tatsächlich eine Konstante
darstellt.
Und ich habe zur Verständlichkeit jetzt noch dahinter geschrieben, und
diese Konstante kann nicht x sein.
Das ist in Wahrheit überflüssig, denn ich habe vorher schon
geschrieben, x wird nach 1 abgeleitet.
Und da das System ja, wie wir gerade gelernt haben, die Formeln von
oben nach unten nimmt, würde es beim Versuch x zu differenzieren,
sofort auf die erste Formel stoßen und gar nicht bis zur zweiten
vordringen.
Also ist diese Bedingung in Wahrheit überflüssig, weil wir gar nicht
bis zu der Stelle kommen, wo wir versuchen, das auf c gleich x
anzuwenden.
Und damit können wir diese Anfrage formulieren.
Ist das Grundprinzip klar?
Das Beispiel ist zugleich das elementarste Beispiel für das, was die
künstlich intelligenten Leute ein Expertensystem nennen.
Ein Expertensystem ist eine Sammlung von Regeln, die sagen, wenn du
den und den Fall vorliegen hast, dann tue doch bitte schön das und
das.
Verallgemeinerung, falls du einen Fall vorliegen hast, der nicht ganz
mit den Fällen zusammenpasst, die ich dir vorgegeben habe, dann führe
eine Metrik ein, eine Abstandsmessung, die dir erlaubt zu sagen, ja,
aber der Fall, der mir vorliegt, der ist ähnlich zu dem Fall.
Also will ich die Regel anwenden, aber ich will was Ähnliches
herausbekommen, nicht exakt das, was die Regel sagt.
Also wenn ich eine Mutter auf eine Schraube drehen will, dann lautet
eine Regel, nimm die Mutter in die Hand und dreh sie immer rechts
herum.
Ist bei uns so üblich.
Es gibt eine zweite Regel, die lautet, das Gewinde könnte leider
Gottes ein Linksgewinde sein, dann müsste es ja andersherum drehen.
Wenn ich jetzt eine Schraube samt Mutter in die Hand bekomme, bei der
ich nicht genau hinschaue, ob das ein Links- oder Rechtsgewinde ist,
versuche ich zuerst die eine Regel, dann die andere Regel.
Eine von denen wird funktionieren, aber die Mutter passt nicht auf die
Schraube.
Und das ist die Frage, welchen der Fälle ist eigentlich der
vorgegebene Fall am Ähnlichsten.
Um das Beispiel fortzusetzen, Sie können das jetzt ausweiten und
können sagen, mir gefällt aber dieses Ergebnis A mal 1 plus 0 nicht.
Ich möchte als Ableitung von A X plus B doch bitte schön nur A
herausbekommen.
Das kann ich Ihnen liefern.
Dann brauche ich also jetzt wesentlich mehr Regeln, nämlich alle
diejenigen, die hier blau noch dazu geschrieben worden sind.
Das sind alle Spezialfälle, die sagen, wenn du differenzieren willst,
sollst du die Summe aus einer Konstante und einem Term, dann kannst du
die Konstante auslassen, weil du schon weißt, dass das 0 ist.
Und 0 plus Ableitung von U ist Ableitung von U, wissen wir auch.
Also kommt bei der Gelegenheit D heraus, wenn D die Ableitung von U
ist.
Und ob du die Konstante vorne hinschreibst oder hinten hinschreibst,
das ist mir gleichgültig.
Das heißt, die Anwendung dieser Regel, differenziere U plus C, das ist
das, was in diesem Beispiel hier unten diese 0 beseitigt.
Spezialfall.
Ja und bei der Multiplikation kann ich es genauso machen, wenn ich
eine Ableitung habe eines Produkts, bei dem eine der Faktoren eine
Konstante ist, dann brauche ich mich um die Ableitung dieser
Konstanten nicht zu kümmern.
Die Sache geht auch einfacher.
Das brauche ich Ihnen, glaube ich, jetzt nicht auf Detail erklären.
Und damit bekomme ich also hier das Ergebnis A heraus.
Beim Differenzieren des Produkts x mal x bekomme ich immer noch diesen
öden Ausdruck x mal 1 zurück.
Nach meinen Regeln kann ich nicht ändern.
Könnte ich jetzt die Frage stellen und können wir das ganze Thema denn
nicht in zwei Teile zerlegen?
Das eine ist differenzieren und das zweite ist das Ergebnis nehmen und
vereinfachen.
Das habe ich auf der nächsten Folie vorgeführt.
Der erste Teil von hier bis hier ist mein Differenzierprogramm, so wie
ich es ursprünglich hatte.
Da ist jetzt also kein Spezialfall mehr drin.
Aber das Ergebnis steht jetzt nicht mehr an der Stelle, wo es
ursprünglich stand.
Da stand an der Stelle dU plus dV.
Sondern da steht jetzt eine Variable E.
Und die ganze Geschichte gilt unter der Voraussetzung, dass dU die
Ableitung von U ist und dV die Ableitung von V ist.
Und dass außerdem das E die Vereinfachung von dU plus dV ist.
Ich führe ein neues Prädikat ein, einfach, welches dann erfüllt ist,
wenn der zweite Parameter eine Vereinfachung des ersten Parameters
darstellt.
Ja, das mache ich in all diesen Fällen.
Und jetzt fange ich an zu erklären, wie Vereinfachung funktioniert.
Ja, die Vereinfachung von 0 plus U ist natürlich ganz offensichtlich
U.
Aber U könnte ja unter Umständen weiter vereinfacht werden.
Also schreibe ich da nicht hin, das ist schon das Endergebnis.
Sondern ich schreibe hin, vereinfache doch bitte U weiter und liefere
mir das als Endergebnis.
Das mache ich natürlich auch für U plus 0.
Wenn ich U mal 1 habe, dann kann ich das mal 1 weglassen.
Und wenn da noch ein plus V dabei steht, dann spielt das überhaupt
keine Rolle.
Das kann ich mit 1 mal U ganz genauso machen.
Wenn der Faktor 0 sein sollte, dann kann ich das U weglassen, dann
kommt nur das V heraus.
Ja, und solche Regeln kann ich natürlich noch in jeder Menge angeben.
Daher die Punkte.
Wenn ich jetzt frage, und wie ist denn ein Fach für eine solche Summe
U und V mit unbekannten U und V definiert?
Ja, da musst du das U vereinfachen und musst du das V vereinfachen.
Und musst dann als Ergebnis zurückliefern die Vereinfachung der Summe
von U1 und U2, wenn das die Vereinfachungen von U und V sind.
Nur wenn ich das so hingeschrieben hätte, dann hätte ich an der Stelle
eine Endlosschleife produziert.
Dann hätte der nämlich gesagt, ja, du hast mir gerade vorgegeben, dass
deine Summe die Bauart X plus Y hat.
X kann ich nicht weiter vereinfachen, also Ergebnis X.
Y kann ich nicht weiter vereinfachen, also Ergebnis Y.
Und jetzt verlangst du von mir, dass ich aufrufen soll, Vereinfachung
von X plus Y mit Ergebnis E.
Das ist genau der Aufruf, den ich gerade fabriziert habe.
Ich muss also verhindern, dass diese Vereinfachung sich selbst nochmal
aufruft, ohne irgendetwas geändert zu haben.
Und das, was sich geändert haben muss, ist also entweder die
Vereinfachung von U muss tatsächlich zu einer Vereinfachung geführt
haben, oder analog die Vereinfachung von V muss zu einer Vereinfachung
geführt haben.
Ich habe hier nur den Fall hingeschrieben, die Vereinfachung von U
muss zu einer Vereinfachung geführt haben.
Und das heißt also, U ist verschieden von U1.
Ich brauche noch eine analoge Regel, die genauso aussieht wie diese,
bei der aber hier drin steht NOT V gleich V1.
Ja, und wenn gar nichts zu vereinfachen geht, dann habe ich ganz am
Ende die Regel, du darfst U nehmen und darfst mir das Ergebnis
ausspucken.
Ich mache gar nichts.
Das ist ein Faktum.
Und das ist die allerletzte Regel, die ich hinschreibe, denn das ist
diejenige Regel, die nur dann anzuwenden ist, wenn wirklich nichts zu
machen ist.
Dann spuckt das Ergebnis aus.
Und wenn ich jetzt differenziere mit meinem vorigen Beispiel, dann
bekomme ich tatsächlich heraus, das ist X plus X.
Und wenn Sie Lust haben, dann dürfen Sie sich überlegen, wie könnten
Sie diese Regelmenge noch so erweitern, dass er zweimal X rausbringt.
Sie sehen also, mit dieser Art von Programming kann man spielen.
Und sie sind ungeheuer einfach.
Es ist die einfachste Form, eine deduktive Datenbank zu formulieren.
Man muss sich jeweils überlegen, wie verhindere ich, wie Sie hier an
diesem Beispiel gesehen haben, wie verhindere ich, dass das Programm
in Endlosschleife geht und dieselbe Anfrage nochmal stellt, die es
schon gestellt hat und noch nicht endgültig beantworten konnte.
Das führt zur Endlosschleife.
Prolog wird in der Praxis für viele solche Abfragesysteme eingesetzt.
Und zwar in der Hauptsache deshalb, weil die Regeln so einfach
hinzuschreiben sind.
In dem Augenblick allerdings, wo ein Prolog-Programm groß wird, 500
oder 1.000 Seile, braucht es eine extrem gute Dokumentation, um noch
zu verstehen, was dieses Programm tut.
Das heißt also, eine sehr lobenswerte Programmiersprache für kleine
Programme und dann leistet sie offensichtlich Erstaunliches.
In einer halben Seite hätten Sie in keiner imperativen
Programmiersprache ein Differenzierprogramm geschrieben.
Gleich gar keines, was Vereinfachungen kann.
Aber wenn Sie große Programme schreiben wollen, dann müssen Sie
vorsichtig sein mit Prolog.
Ausblick zum Schluss dazu.
Viele der Abfragestellungen, die man mit Prolog formalisieren kann,
kann man in Wahrheit auch mit SQL, also mit Abfragesprachen für
Relationale Datenbanken formalisieren.
Das ist dann meistens die wesentlich effizientere Lösung.
Allerdings sehr viel schwieriger zu begreifen.
Also Effizienz und leichte Lesbarkeit kommen nicht immer zusammen.
Gibt es noch Fragen dazu?
Das ist eine gute Frage.
Sie sehen, auf der Folie schreibt man Ergebnisse hin, die man im Kopf
gerechnet hat.
Und dann passieren solche Fehler.
Wenn es keine weiteren Fragen gibt...
Hier oben steht, wenn du X nach X differenzierst, dann lautet das
Ergebnis 1.
Ist das richtig?
Und das steht da.
Es steht nicht da, X wird durch 1 ersetzt.
Und die nächste Regel sagt, wenn du eine Konstante nach X
differenzierst, dann kommt 0 heraus.
Also bedenken Sie immer, Diff ist keine Aufforderung, differenziere,
sondern ist ein Prädikat.
Was sagt, zwischen der Formel, die du differenzieren willst, und der
Variablen, die du differenzieren willst, und dem Ergebnis, herrscht
die Beziehung Diff XX1.
Das ist ein Prädikat.
Wenn Sie es imperative auffassen und sagen, differenziere die Formel
nach X mit einem Resultat, dann sind Sie gelegentlich fehlgeleitet.
Logisches Programmieren heißt, wir versuchen herauszufinden, ob
Prädikate wahr sind.
Und wenn sie wahr sind, dann liefern wir euch ein Ergebnis.
Sie werden abgesehen von den Übungen, die Sie jetzt machen, vom Prolog
zunächst einmal verschont bleiben, aber im Hauptstudium kann Ihnen das
ganz plötzlich wieder begegnen.
Und insbesondere kann Prolog all den Informationswirten wieder
begegnen, die hier drinnen sitzen.
Denn das ist eine sehr beliebte Sprache unter den Leuten, die sich
nicht in die Details der Imperativprogrammierung stürzen wollen.
Und kommt dazu sehr häufig auf Anwendungsebene vor, bei Leuten, die
Java oder C oder sonst was gar nicht beherrschen.
Damit bin ich mit dem Kapitel Logik fertig.
Bevor ich jetzt so unter dem nächsten Kapitel übergehe, muss ich noch
eine Korrektur anbringen.
Die Qualitätskontrolle hat versagt.
Es stellt sich heraus, dass, das ist meines Wissens die Folie 70 in
Kapitel 2,
eine falsche Definition von fundiert enthielt.
Die korrekte Definition habe ich hier rot hingeschrieben.
Der Rest der Folie bleibt erhalten.
Im Buch steht es richtig, aber auf der Folie stand es falsch.
Also jede nicht kläre Teilmenge von x enthält mindestens ein minimales
Element.
Und damit kann ich dann also meinen Beweis, dass fundiert und arthing
die selbe Eigenschaft sind, über den sich einige Leute beschwert
haben, korrekt führen.
Wenn nämlich vorgegeben ist, dass die Halbordnung u kleiner gleich
arthing ist, sprich also jede absteigende Kette bricht ab, dann
behaupte ich, dass u auch fundiert ist mit seiner Halbordnung.
Und das beweise ich durch Widerspruch.
Ich nehme an, dass es irgendeine Teilmenge x gäbe, in der kein
minimales Element vorliegt.
Und jetzt konstruiere ich eine absteigende Kette.
Und wenn kein minimales Element vorliegt, dann müsste diese
absteigende Kette endlos weiter konstruierbar sein.
Denn sobald sie abbricht, hätte ich ja ein minimales Element.
Ja, sie muss aber abbrechen.
Weil ich ja voraussetze, dass u arthing sei.
Und damit habe ich dann also ein minimales Element gefunden, im
Gegensatz zu meiner Annahme, dass es kein minimales Element gäbe.
Also zu korrigieren ist die Definition von fundiert auf der Folie und
ich wiederhole, im Buch steht es richtig.
Das ist irgendwann mal durch Nachlässigkeit falsch auf die Folie
gekommen, mangelhafte Qualitätskontrolle nennt man das.
Gibt es dazu noch Fragen?
Richtig.
Er fragt, kann es den Fall geben, dass da mehrere minimale Elemente
existieren?
Ja, ganz einfaches Beispiel.
Ich betrachte u als eine Menge, die nur zwei Elemente hat, a und b.
Und die sind unvergleichbar, das heißt die Ordnungsrelation habe ich
gar nicht definiert.
Dann ist sowohl a minimal, als auch b minimal.
Jede Kette bricht ab nach einem Element, es gibt kein zweites.
Also bereits in ganz elementaren Fällen funktioniert das.
Noch Fragen?
Wenn
nein, dann sind wir mit Kapitel 4 fertig und kommen zu unserem
nächsten Kapitel.
Funktionales Programmieren.
Gleich geht der Programmierkurs los, aber nur gleich.
Als allererstes habe ich vor dem Programmierkurs noch ein Stückchen
Theorie gesetzt.
Theorie von 1936.
Die ihn illustrieren soll, wie die einfachste Programmiersprache
aussieht, die wir uns überhaupt vorstellen können, die aber alles
leistet.
Das ist der Lambda-Kalkül, erfunden von einem Herrn namens Church.
Und unser Thema ist also zunächst der Lambda-Kalkül.
Bevor wir dazu übergehen, aber die Grundideen schlagwortartig
erläutert.
Wir haben zuerst begonnen mit Simitui-Systemen, das waren
Textersetzungssysteme.
Und fanden dann, dass für praktische Ausführung es zweckmäßig wäre,
die ganze Geschichte deterministisch zu machen.
Und das hat zu Markov-Algorithmen geführt.
Dann haben wir in Kapitel 3 Termersetzungssysteme fabriziert.
Und haben genauso wie beim logischen Programmieren gerade gesehen,
Termersetzungssysteme sind vielleicht schön, aber praktisch
unhandlich.
Wir möchten das ganze Ding gerne deterministisch machen.
Und funktionale Programmiersprachen tun genau das.
Sie sind Termersetzungssysteme, aber deterministisch gemacht.
Und die Methoden sind immer die gleichen, die wir schon bei Markov
-Algorithmen kennen.
Schreib doch bitte deine Regeln in einer bestimmten Reihenfolge an.
Und ich garantiere dir, dass die Regeln angewandt werden, indem ich
eine nach der anderen von oben nach unten probiere.
Und die erste anwendbare Regel nehme ich.
Gleiche Geschichte wie bei Markov-Algorithmen.
Damit wir sehen, wie die ganze Geschichte sich einordnet.
Wir möchten eigentlich Programme schreiben.
Genauer gesagt, wir möchten keine Programme schreiben.
Das ist öde.
Das, was wir eigentlich gerne möchten, ist, wir möchten Probleme
lösen.
Die Probleme müssen uns aber so vorgegeben sein, dass wir auf dem
Rechner etwas damit anfangen können.
Und das heißt, es muss eine Spezifikation vorliegen, die hinterher
mechanisch interpretiert werden kann.
Also ich kann mir nicht hier einen Roboter hinstellen und dem den
Befehl geben, bitte schön, verlass diesen Hörsaal.
Der wird da durch die geschlossene Glastür da rauslaufen.
Oder er wird hier versuchen, gegen die Wand zu laufen, in der
Hoffnung, dass man die Wand beiseite schieben kann.
Das ist also keine vernünftige Spezifikation.
Wir müssen also offensichtlich, wenn wir programmieren wollen, und
programmieren heißt jetzt nur, die Spezifikation so vorgeben, dass sie
ausführbar wird.
Eine Spezifikation haben, die tatsächlich auf Rechnern ausführbar ist.
Und sowas nennen wir ein Programm.
Solche Aufgabenspezifikationen können sehr abstrakt scheinen.
Also es gibt zum Beispiel Systeme wie Mabel oder Mathematica, denen
können Sie eine Formel vorlegen, wie Sie sie als Schulaufgabe gehabt
haben.
Ich integriere irgendeine Funktion und er spuckt Ihnen in der Tat das
Integral raus.
Das macht er mit Ihren sämtlichen Schulaufgaben.
Das reicht ihm als Spezifikation vollkommen aus.
Und insoweit ist die Angabe einer solchen Mathematikaufgabe bereits
eine Spezifikation.
Weitere Einzelheiten brauche ich nicht.
So ähnlich funktionieren die Abfragesprachen für Relationale
Datenbanken oder die Abfragesprache ABAP4, die SAP in seinen Systemen
verwendet und die man so landläufig unter Journalisten als Sprachen
der vierten Generation bezeichnet.
Eine Definition, was eine Sprache der vierten Generation ist, kann ich
Ihnen nicht geben.
Ich habe sie nie gelesen.
Es wäre eine freie Erfindung, wenn ich das sagen würde.
Es ist nur ein Schlagwort, was sich wunderschön macht, wenn man das in
die Computerwoche schreibt oder in eine ähnliche Zeitschrift.
Logische Programmiersprachen, wir haben das gerade am Beispiel des
Differenzierens gesehen.
Ich habe die Elementarbeispiele angegeben, wie differenziert wird.
Und daraus kann mein System Gesamtlösungen zusammensetzen.
Wie die Zusammensetzung funktioniert, habe ich nicht hingeschrieben.
Wenn ich das in einer landläufigen Programmiersprache hingeschrieben
hätte, wäre das drei, vier, fünf Seiten lang geworden.
Und ich hätte viele Einzelheiten angeben müssen, die ich im Produkt
nicht spezifiziert habe.
Genauso funktionale Programmiersprachen erlauben mir, Programme zu
spezifizieren, Aufgaben zu spezifizieren.
Indem ich sage, da rechne doch bitte die folgende Funktion aus.
Aber ich spezifiziere nicht, in welcher Reihenfolge die verschiedenen
Funktionsanwendungen, die ich habe, nun angewandt werden sollen.
Wobei unter Funktion sowohl etwas zu verstehen ist, was ich in der
Form f von x und y schreibe, als auch irgendeine Addition a plus 2,
das ist auch eine Funktionsaufrufe.
Die Imperativen Sprachen, das ist die weit verbreitete Klasse, bemüht
sich da um sehr viel größere Genauigkeit.
Und sagt, ja, wenn du irgendetwas berechnen willst auf diesem
komischen Rechner, dieser Rechner hat durch seine Speicherbelegung,
die sich über den Zeit ändert, einen Zustand.
Und das, was du beschreiben musst, sind die Zustandsübergänge des
Rechners.
Das tue ich in keinem der anderen Beispiele.
Also Sprachen der vierten Generation, logische Programmiersprachen,
funktionale Programmiersprachen, die beschäftigen sich nicht mit
Zustandsübergänge.
Das geschieht ausschließlich bei Imperativen Programmiersprachen.
Und objektorientierte Programmiersprachen sind quasi ein Spezialfall
der Imperativen Programmiersprachen, bei denen ich nur ein anderes
Modell zugrunde lege, nämlich das Modell kooperierender Objekte.
In Wahrheit stellt sich heraus, keines dieser verschiedenen Paradigmen
kommt in absoluter Reihenkultur vor.
Also wenn Sie eine kommerzielle Implementierung vom Prolog haben, dann
können Sie darin rechnen und haben Zustand bezogen auf die Rechnung.
Viele funktionale Programmiersprachen erlauben Ihnen irgendwo eine
Hintertür, durch die Sie ebenfalls rechnen können und plötzlich
zustandsorientiert arbeiten können.
Umgekehrt, viele imperative und objektorientierte Sprachen formulieren
einen Teil ihrer Aufgaben in einer Weise, wie Sie eigentlich in
funktionalen Sprachen erwartet hätten.
Also keines der Modelle, was wir im Laufe des Studiums kennenlernen,
kommt wirklich in Reihenkultur vor, sondern wir haben immer
irgendwelche Mixturen.
Gehen wir jetzt über zu funktionalem Programmieren.
Die Grundidee ist zu schreiben, wir haben eine Folge von
Funktionsdefinitionen.
Funktionsname f, 0 oder mehrere Parameter ist gleich Funktionsruf und
dazu ein Aufruf a und den werten wir auf.
Und natürlich könnte unter den Argumenten für f ebenfalls weitere
Funktionsaufrufe stehen.
Und die übliche Schreibweise ist, wir schreiben dann hin,
Funktionsname, erster Parameter, Zwischenraum, zweiter Parameter,
Zwischenraum und so weiter.
Die Klammern lassen wir weg, wir schreiben auch keine Komma.
Das ist eine syntaktische Regel, die hat inhaltlich nichts zu tun.
Und wie interpretieren wir das?
Nun wir interpretieren das so, dass da steht, du hast Funktionsname
und die ganzen Parameter als linke Seite einer Teilersetzungsregel.
Der Funktionsrumpf, das was du eigentlich tun sollst, ist die rechte
Seite.
Und Funktionsaufruf heißt, ersetze die linke Seite durch die rechte
Seite.
Und das war's.
Wenn Sie nun eine Funktion definiert haben, fx ist gleich x plus 1.
Und Sie kommen an mit einem Aufruf f a plus b.
Dann ist das erste was wir feststellen, a plus b ist nicht x.
Woher sollen wir wissen, dass dieser Funktionsaufruf gebrauchsfähig
ist?
Nun, da machen wir jetzt Gebrauch von unseren Regeln über
Substitutionen und sagen, eine solche Ersetzung ist dann anwendbar,
wenn es eine Substitution Sigma so gibt, dass f mit der Substitution
Sigma angewandt auf die Parameter, gerade den Aufruf liefert.
Ja, das funktioniert.
Wenn ich die Substitution nehme, Sigma heißt, ersetze x durch a plus
b, dann sieht plötzlich der Aufruf und die Funktionsdefinition gleich
aus.
Und dann weiß ich auch, welchen Funktionsrumpf ich brauche.
Du musst auch im Funktionsruf das x durch a plus b ersetzen.
Also Ergebnis ist dann a plus b plus 1.
Und das ist die Standardinterpretation, die wir ergeben können mit
unseren Kenntnissen über Textersetzungssysteme.
Und damit können wir Funktionales Programmieren komplett begreifen.
Mehr Regeln haben wir nicht.
Wir können stattdessen auch alles über Textersetzung vergessen und
können den Lambda-Kalkül, den wir gleich lernen, zu benutzen
versuchen.
Und dann haben wir die Regeln des Lambda-Kalküls und die ganze
Geschichte funktioniert auch so.
Es stellt sich in der Praxis heraus, dass man beide Arten der
Interpretation beherrschen muss, weil einmal die einfacher ist und
einmal die einfacher.
Und man schreibt also Programme und versteht den Ablauf von Programmen
natürlich mit den Regeln am besten, die jeweils am einfachsten sind.
Beide Verfahren beschreiben also den selben Vorgang.
Das zweite Verfahren, die Benutzung des Lambda-Kalküls, führt zu etwas
sehr Merkwürdigem, was wir aber in der Informatik an vielen Stellen
brauchen, nämlich zu der Auffassung, Funktionsaufrufe liefern als
Ergebnis nicht Zahlen wie 1 oder 2 oder sonst irgendetwas, sondern
liefern als Ergebnis Widerfunktionen.
Und es stellt sich heraus, dass im Lambda-Kalkül diese Auffassung so
weit fabriziert worden ist, dass man damit also auch mit Zahlen
rechnen kann und mit allen möglichen Dingen rechnen kann, obwohl die
Funktionen immer nur Widerfunktionen als Ergebnis liefern.
Der größte Vorzug funktionalen Programmierens ist, die ganze
Geschichte ist nebenwirkungsfrei.
Sie brauchen weder zu Ihrem Arzt gehen noch zum Apotheker, die Sache
ist garantiert nebenwirkungsfrei.
Imperatives Programmieren hat hier furchtbare Schwierigkeiten, denn
dort ändern Sie den Zustand des Rechners ab und eine einzelne
Anweisung wie Rechne mal i plus 1 aus, können die ungeahnten
Nebenwirkungen entfalten auf den Rest Ihres Rechensystems.
Also ich brauche aus i plus einen Funktionsaufruf machen, der sagt,
ja, liefere doch bitte schon die Zahl 3 zurück, aber vorher lösche den
ganzen Speicher.
Und das kann man programmieren.
Solche Nebenwirkungen können hier nicht auftreten und das ist der
größte Vorteil auch im Verständnis, wie Funktionales Programmieren
funktioniert oder wie Programmieren überhaupt funktioniert.
Dazu kommen wir also zum Lambda-Kalkül.
Erfunden ist das von dem Herrn Church.
Den Herrn Church haben wir jetzt schon zweimal kennengelernt.
Wo haben wir den schon kennengelernt?
Also zuerst haben wir ihn kennengelernt als den Autor der sogenannten
Churchen -These, die da sagt, egal welche Art von Berechnungsschema du
vorgibst, der Begriff Berechenbarkeit ist immer der gleiche.
Und das, was er hier entwickelt hat, ist sozusagen seine eigene
Illustration gewesen.
Ich gebe den Lambda-Kalkül an, das ist ein völlig anderes Verfahren,
niemand hat es bisher gehabt und siehe da, es leistet dasselbe wie
alle anderen Berechnungsverfahren, die wir bisher hatten.
So, und wo kam der Herr Church noch vor?
Der kam jetzt gerade in der Prädikatenlogik vor.
Da gab es einen Satz, der sagte, und es gibt kein universelles
algorithmisches Verfahren, um festzustellen, ob aus gegebener
Voraussetzung eine gegebene Aussage ableitbar ist.
Das stammt auch von dem Herrn Church.
Er hat sich also an mehreren Stellen um die Grundlagen verdient
gemacht.
Und hier hat er uns also jetzt mit einer Programmiersprache beglückt.
Veröffentlicht wurde das Ganze 1941, bei der er gesagt hat, und wir
fassen alles als Terme auf, auch Programme sind Terme, und sogar
Funktionen werden als Terme angefasst.
Und dazu brauchen wir natürlich dann eine Definition einer
Termalgebra, und die Termalgebra im Fall des Lambda-Kalküls benennen
wir mit den Buchstaben Groß-Lambda, das ist also nicht irgendeine
komische Hieroglyphe, sondern das ist Großes-Lambda.
Und in dieser Termalgebra gibt es zunächst mal Variablen, und jede
Variable ist ein Term.
Na, das hatten wir schon.
Dann gibt es aber was Neues, und das nannte Herr Church eine Lambda
-Abstraktion, und das ist eine Funktionsdefinition.
Die hat die Form Lambda-V.F.
Dabei ist V eine Variable, und F ist ein Term.
Und wenn ich als so einen Term F, den ich schon kenne, vorgebe, und
eine Variable V, darf ich hinschreiben, Lambda-V.F, und das ist wieder
ein Term.
Und die anschauliche Bedeutung ist, Lambda-V.F ist eine Funktion mit
Rumpf F und Parameter V.
Und wenn Sie fragen, wie heißt denn diese Funktion, hat die einen
Namen?
Dann lautet die Antwort, nein, sie hat bisher keinen Namen.
Sie ist namenlos.
Das heißt also, du kannst hinterher, das ist die Aussicht, Programme
hinschreiben, bei denen Funktionen, Funktionsdefinitionen einfach
irgendwo mittendrin stehen, ohne dass sie irgendeinen Namen bekommen
haben.
Das ist sehr erwünscht, insbesondere wenn ich Funktionen als Ergebnis
herausbringen will.
Denn dann rechne ich die Funktionen erst aus, und dann haben sie
natürlich keinen Namen.
Dritte Art, einen Term hinzuschreiben.
Ich kann hinschreiben, zwei Terme in Klammern.
Und das wird so interpretiert, wende doch bitte F1 auf F2 an, das
heißt F1 sollte eine Funktionsdefinition sein, dann ist F2 ein
Argument, und wir wenden die Funktionsdefinition auf das Argument F2
an.
Auf einer der nächsten Folien steht dann auch, wie das zu
interpretieren ist, wenn ich also jetzt hinschreibe zum Beispiel,
Lambda V Punkt mit irgendeiner Formel F, soll angewandt werden auf
eine Formel G, dann habe ich hier eine Funktionsdefinition, und hier
habe ich ein Argument, und was erwarten wir denn, was rauskommt?
Es soll herauskommen, F angewandt auf G, und G soll dabei eingesetzt
werden für V.
Also muss das Ergebnis wohl sein, F, und darauf angewandt die
Substitution, ersetze in F überall V durch G.
Das ist das Ergebnis.
Das sind die Methoden, mit denen ich also Terme definieren kann.
Ich kann Variable hinschreiben, ich kann Funktionsdefinitionen
hinschreiben, ich kann hinschreiben, wie eine Funktionsanwendung
aussieht, und mehr Regeln gibt es nicht.
Ende.
Zur Schreibweise.
Sehr häufig ist es notwendig, dass wir solche Lambda-Ausdrücke
klammern, oder überhaupt Formeln klammern.
Klammern können Sie freizügig einführen.
Das ist notwendig, damit man unterscheiden kann, wenn eine Funktion
beispielsweise mehrere Argumente hat.
Zweitens, das ist natürlich unbefriedigend, dass man überhaupt keine
Funktion benennen kann.
Also führen wir jetzt eine Schreibweise ein.
Wenn es zu Variable ist, gleich Formel schreibst, dann kannst du damit
diesem Term F einen Namen geben.
Und das machen wir insbesondere dann, wenn F eine Lambda-Abstraktion
ist.
Und dann hat die Funktion plötzlich einen Namen gekriegt.
Und jetzt kann ich definieren, wie in diesem Lambda-Kalkül ein
komplettes Programm aussieht.
Das ist eine Folge von solchen Funktionsdefinitionen, wie ich sie hier
eingefügt habe.
Und ganz am Ende folgt dann ein Funktionsaufruf F.
Und das Ergebnis des Programms ist, rechne F aus unter
Berücksichtigung dieser ganzen Funktionsaufrufe.
Das ist die ganze Geschichte.
Und dabei habe ich jetzt Bindungsregeln zu berücksichtigen.
Zunächst einmal, wenn ich in meinem Programm schreibe, V ist gleich F,
dann heißt das permanent, egal wo es vorkommt, soll V die Bedeutung
haben der Funktion F.
Und das ist, wenn wir uns jetzt anschauen, was wir über freie und
gebundene Variable gelernt haben, offensichtlich eine
Variablenbindung, ebenso wie wir sie mit einem Alquandorkennen gelernt
haben.
Wir schreiben es zwar nicht hin mit einem Alquando oder so, aber
gemeint ist eigentlich, in allen Fällen, in denen V noch vorkommt,
soll V diese Funktion bedeuten.
Das heißt, so eine Bindung oder Belegung von V mit dem Term F, die im
gesamten Programm gültig ist.
Die Lambda-Ausdrücke machen so ähnliche Sachen.
Wenn ich Lambda-V hinschreibe, dann ist das eine Bindung von V, die
kommt aber jetzt nur auf die Formel G.
Das heißt also, bezogen auf die Bindungsregeln, ist irgendeine
Schreibweise von der Bauart für alle X, G und Lambda, X, G.
Das ist bezogen auf die Bindungsregeln völlig identisch aufzufassen.
Innerhalb von G soll X immer diesen Parameter bedeuten, den wir an
dieser Stelle eingefallen haben.
Das V kann natürlich auch noch frei vorkommen, ohne eine solche
Bindung, also weder durch Variablendefinition noch durch einen solchen
Lambda -Ausdruck.
Dann nennen wir es frei.
Wir haben auch wieder wie in der Logik die Situation, dass ein
Bezeichner X sowohl frei als auch gebunden vorkommen kann.
Also gleiche Geschichte.
Und irgendeine Formel F, die keine freien Variablen enthält, so etwas
nennen wir eine geschlossene Formel.
Und wie bei Prolog verlangen wir, und im logischen Programmieren,
verlangen wir, dass grundsätzlich alle Variablen, die in unseren
Programmen vorkommen, gebunden sind.
Sprich, es muss entweder für irgendeinen Bezeichner X eine
Funktionsdefinition geben, oder X muss Parameter einer Funktion sein,
aber die Idee da einfach hinzuschreiben, Buchstabe X, und zu hoffen,
dass irgendjemand schon wüsste, was X bedeutet, die gibt es nicht.
Also alle in einem Programm vorkommenden Variablen müssen gebunden
sein, Programme sind geschlossen, und hier haben Sie ein Beispiel, was
Sie vergleichen können jetzt mit unserer Definition von frei und
gebunden im Fall von der Logik.
Und Sie sehen, die Regeln sind exakt die gleichen, Sie müssen nichts
Neues hinzunehmen.
Ja, wie sieht also dann die Geschichte aus, wenn ich solch eine
Funktion definiert habe, V, mit einem Term T, dann heißt das, du
kannst überall da, wo V steht, das T einsetzen, denn das hat die
gleiche Bedeutung, und das heißt also, V angewandt auf G, liefert das
Gleiche mit T auf G, und das bedeutet, dass du also diese Substitution
hast, wenn da was los ist, ersetze V durch G, das habe ich Ihnen
vorhin handschriftlich schon auf der Folie erläutert, und als
einfachstes Beispiel einer solchen Lambda-Funktion, die Funktion
Lambda V mit Rumpf V, ja, wenn ich da den Parameter einsetze für V,
dann liefert mir das Ergebnis das als Parameter zurück, das heißt,
wenn das meine Funktion F ist, und ich wende sie auf T an, dann
liefert mir die immer T zurück, und das ist offensichtlich, dass also
diese Funktion die Identitätsfunktion ist.
Liefere das Argument als Ergebnis zurück.
Damit kommen wir zu der nächsten Folie und letzten Folie für heute,
mit der wir auch nächstes Mal wieder anfangen müssen, nämlich, auf der
Folie steht alles, was man über den Lambda-Kalkül wissen muss, um zu
wissen, wie irgendetwas ausgeführt wird.
Es gibt nur drei Regeln im Lambda-Kalkül.
Die erste Regel lautet, du darfst Variable umbenennen,
du darfst also eine Substitution anwenden auf irgendeinen Term, der
sagt, ersetze V durch V' und das wird dann an allen Stellen
durchgeführt.
Zweite Feststellung, wenn du eine Lambda-Abstraktion hast, Lambda VT,
und dahinter dann ein Argument T', dann ist das die normale
Funktionsanwendung und dann kommt heraus das Ergebnis der
Funktionsrumpf T mit V überall ersetzt durch T'.
Und die dritte Idee lautet, wenn du eine Lambda-Abstraktion hast, bei
dem das V nicht frei in T vorkommt, dann hat das V offensichtlich in
diesem Rumpf keine Bedeutung und dann kannst du einfach das T ohne
weitere Substitutionen hinschreiben als Ergebnis.
Diese drei Ausführungsregeln heißen aus mir unbekannten Gründen,
Alpha, Beta und Eta-Konversion, die Welt versucht vergeblich
herauszufinden, wieso Herr Church auf diese Idee kam, das so zu
nennen, aber er hat es nicht genannt.
Und selbstverständlich, diese Ausführungsregeln sind immer nur
zulässig, wenn dabei keine freien Variablen aus Versehen gebunden
werden.
Gleiche Regeln wie in der Logik.
Soviel für heute.