3.3 Grundbegriffe der Termersetzung

3.3.1 Termersetzung erster Stufe

Unter einem Baum oder auch Termstruktur verstehen wir hier eine präfixabgeschlosse, endliche Teilmenge B von N^{∗}. D.h., ist n_{1}.n_{2}. . . . .n_{k} in B mit k ≥ 1, so ist auch n_{1}.n_{2}. . . . .n_{k−1} in B sowie alle n_{1}.n_{2}. . . . .n_{k−1}.j mit j < n_{k}. Ein Term t über F, wobei F eine Menge von Funktionssymbolen, ist eine Abbildung t : B → F, wobei B ein Baum. Die Knoten in B nennen wir auch die Positionen in t. Wir sagen, daß f an Position p in t vorkommt, wenn t(p) = f gilt. Ist p eine Position in t, so bezeichnet t/p den Subterm von t an p, d.h. den Term t′ mit der Struktur bestehend aus den Positionen q in N^{∗}, für die p.q eine Position in t ist, mit der Markierung t′(q) = t(p.q). Sind s und t Terme und ist p eine Position in t, so bezeichne t[s]_{p} den Baum, der durch Ersetzung des Subterms an p in t durch s entsteht. Als lineare Notation für Terme verwenden wir die Präfixnotation, d.h. schreiben f(t_{1}, …, t_{n}) für einen Term, bei dem f an der Wurzel ϵ vorkommt, und der die Subterme t_{1}, …, t_{m} (an ϵ) besitzt. Oft verwenden wir auch Infix oder Postfixnotation für Funktionssymbole, für die dies die übliche Schreibweise darstellt. Wir schreiben also beispielsweise a + b für den Term +(a, b).

Terme, in denen nur Funktionssymbole vorkommen, heißen auch Grundterme oder variablenfreie Terme. Zusätzlich zu diesen betrachten wir auch Terme mit (getypten) Variablen. Sei also X eine Menge von getypten Variablen der Form x : τ, die disjunkt zu F ist. Dann ist ein Term über X und F einfach ein Tern über X ∪ F, in dem Variablen nur an Blattpositionen vorkommen dürfen.

Wohlgetypte Terme ergeben sich aus folgendem Typinferenzsystem:

\overline{x : τ}  falls x : τ in X

\frac{t_{1} : τ_{1} … t_{n} : τ_{n}}{f(t_{1}, …, t_{n}) : τ_{0}} falls f : τ_{1} ∗ … ∗ τ_{n} → τ_{0} in F, n ≥ 0

Ein Term t heißt daher wohlgetypt, wenn t : τ für einen Typ τ in obigem Inferenzsystem ableitbar ist. In diesem Fall heißt τ ein Typ von t. Im Kontext von Typpolymorphismus braucht es zur Typinferenz weitere Regeln, auf die wir später noch zurückkommen werden.

Nachfolgend bezeichnte T_{F,X} bzw. T_{F} die Menge der Terme mit bzw. ohne Variablen über F und X. Eine Substitution ist eine Abbildung σ : X → T_{F,X}. Die Anwendung einer Substitution σ auf einen Term t, bezeichnet mit σ(t) oder mit tσ, liefert den Term t[s_{1}]_{p_{1}}[s_{2}]_{p_{2}} … [s_{k}]_{p_{k}}, wenn die p_{i} genau die Variablenpositionen in t sind, und wenn t(p_{i}) = X_{i} mit σ(X_{i}) = s_{i} gilt. Die Anwendung ersetzt also alle Auftreten von Variablen durch die gemäß σ zugeordneten Terme.

Substitutionen sind Grundlage für die Formalisierung von Mustertest auf Termen und von Termersetzung. Sind s und t Terme und ist p eine Position in t, so sagen wir, daß das Muster s auf t an p paßt, wenn es eine Anpaßsubstitution σ gibt, so daß t/p = sσ. Paßt s, so ist die Anpaßsubstitution auf den Variablen in t/p eindeutig festgelegt.

Eine Termersetzungsregel ist ein Paar von Termen l und r, geschrieben l → r. Die Regel paßt auf t an p, wenn ihre linke Seite l auf t an p paßt. Ist σ die zugehörige Anpaßsubstitution, so nennen wir t′ = t[rσ]_{p} das Resultat der Anwendung der Regel. In diesem Fall schreiben wir auch t →_{p,l→r,σ} t′. Wir sprechen auch von der Reduktion von t zu t′, und t/p heißt der Redex dieses Reduktionsschrittes. Wir lassen den Subskript weg, wenn die jeweiligen Größen irrelevant oder aus dem Kontext bekannt sind. Ein Termersetzungssystem R ist eine Menge von Termersetzungsregeln. Wir schreiben t →_{R} t′, wenn t′ aus t durch Anwendung einer Regel aus R auf t entsteht. Mit →_{R}^{+} bzw. →_{R}^{∗} bezeichnen wir die transitive bzw. transitive und reflexive Hülle dieser durch R definierten Ersetzungsrelation →_{R}. Wir sagen, daß ein Term irreduzibel ist bzgl. R, wenn für keinen Term t′ →_{R} t′ gilt. t′ heißt eine Normalform von t bzgl. R, wenn t →_{R}^{∗} t′ und wenn t′ irredizibel ist.

3.3.2 Funktionsauswertung als Termersetzung

Funktionsdefinitionen in SML definieren Termersetzungsregeln, mit denen Applikationen reduziert werden können. Betrachten wir beispielsweise die Funktion

fun append(nil,l) = l
  | append(hd::tl,l) = hd :: append(tl,l)

von oben. Sie definiert die beiden Termersetzungsregeln

append (nil,l)    -> l
append (hd::tl,l) -> hd :: append(tl,l)

vorstellen. In F haben wir hierbei alle Konstanten von den Typen int, real, string, und bool, die Konstruktoren für Listen und Verbunde, alle vordefinierten Funktionen, den Applikationsoperator apply, den wir nicht explizit hinschreiben, sowie die Konstante append. Variablen sind l, hd und tl. Im Zusammenhang mit Funktionen höherer Ordnung wird es noch essentiell sein zu beachten, daß ein ML-Ausdruck von der Form append (hd::tl,l) einen Term bezeichnet, den man in strenger Präfixnotation eigentlich als

apply(append, ”, ”(:: (hd, tl), l))

schreiben müßte. In der Tat erzeugt die Auswertung einer Funktionsdefinition wie die von append eine Bindung

        append ≡ (fn (nil,l) => l | (hd::tl) => hd :: append(tl,l))

die explizit macht, daß man append eine Variable von funktionalem Typ ist. Diese Bindung verwendet eine erweiterte Notation von λ-Ausdrücken mit musterorientierten Regeln. Wir werden diesen Punkt weiter unten noch vertiefen. Jetzt, wo wir zunächst keine Funktionen höherer Ordnung betrachten wollen, können wir append auch als eine 2-stellige Funktion auffassen und den Applikationsoperator apply vergessen.

Im Falle von append ist beispielsweise folgende Reduktionsfolge möglich:

   append(1::nil,2::3::nil)
-> 1::append(nil,2::3::nil)
-> 1::2::3::nil

Im ersten Schritt wurde die erste Regel, im zweiten Schritt die zweite Regel angewendet, und zwar jeweils an der Wurzel des Terms. Folgendes Beispiel ist etwas komplizierter, indem die definierte Funktion append mehrfach vorkommt.

   append(1::nil,append(2::nil,2::3::nil))
-> append(1::nil,2::append(nil,2::3::nil))
-> append(1::nil,2::2::3::nil)
-> 1::append(nil,2::2::3::nil)
-> 1::2::2::3::nil

Im Prinzip wäre auch folgende Reduktionsfolge möglich gewesen:

   append(1::nil,append(2::nil,2::3::nil))
-> 1::append(nil,append(2::nil,2::3::nil))
-> 1::append(nil,2::append(nil,2::3::nil))
-> 1::append(nil,2::2::3::nil)
-> 1::2::2::3::nil

Wir sehen, daß das Ergebnis das Gleiche ist, unabhängig von der Reduktionsstrategie. In SML ist die zweite Reduktionsfolge nicht erlaubt. SML-Reduktion erfolgt nach der Strategie “innerste Redexe zuerst“. Der erste Schritt in der zweiten Reduktionsfolge wäre daher in SML nicht erlaubt, da es ein weiter innen liegendes Auftreten von append gibt, welches ebenfalls reduzierbar ist. Die Argumente einer Funktion müssen daher zuerst zu Konstruktortermen normalisiert werden, bevor irgendeine Regel der jeweiligen Funktionsdefinition angewendet wird. Unter einem Konstuktorterm verstehen wir einen Term, in dem nur Konstruktoren (die Konstanten der Typen int, real, string, und bool sowie die Konstruktoren für Verbunde und Listen) vorkommen dürfen. Wir werden später sehen, daß der ML-Programmierer weitere Konstruktoren deklarieren darf, also nicht notwendig alle rekursiven, strukturierten Daten als Listen kodieren muß.

Halten wir fest: Das Ergebnis value(e) der Auswertung eines SML-Ausdrucks e ist die Normalform, die sich durch Reduktion von e mit der Strategie “innerste Redexe zuerst“ ergibt. Gibt es keine Normalform weil die Reduktion nicht terminiert, so ist die Auswertung undefiniert. Konsequenz dieser Reduktionsstrategie ist die Striktheit aller benutzerdefinierten Funktionen f. Es gilt

value(f(e_{1}, …, e_{n})) = value(f(value(e_{1}), …, value(e_{n})))  (1)

und als Konsequenz ist value(f(e_{1}, …, e_{n})) undefiniert, sofern eines der value(e_{i}) undefiniert ist. Ausdrücke mit funktionalem Typ, if-Ausdrücke, usw. sind speziellen Reduktionsstrategien unterworfen. Erstere werden nicht reduziert. Bei letzteren wird erst die Bedingung reduziert und dann, je nach Ergebnis, der then- oder der else-Ausdruck. Es gilt daher

value(if true then e_{1} else e_{2}) = value(e_{1})  (2)
value(if false then e_{1} else e_{2}) = value(e_{2})  (3)

Es bleibt noch anzumerken, daß die SML-Semantik garantiert, daß Normalformen, sofern sie existieren, immer eindeutig bestimmt sind, die Reduktionsrelation ist konfluent. Dazu gehört, daß die Regeln geordnet sind, so daß, wenn mehr als eine regel anwendbar ist, immer die erste anwendbare Regel verwendet wird. Aus diesem Grunde gilt, wenn l → r eine Regel ist,

value(t[lσ]_{p}) = value(t[rσ]_{p})  (4)

für jeden Term und jede Position p in t, die nach der vorgenannten Reduktionsstrategie mit Regel l → r unter Substitution σ reduziert werden darf.

3.3.3 β-Reduktion

Wir wollen nun noch erklären, wie allgemeine Applikationen von Funktionen auf ihr Argument reduziert werden, wenn also die Applikation nicht gerade die Form (f e′) hat, wobei f der Name einer Funktion ist. Allgemein kann f ja ein beliebiger Ausdruck von funktionalem Typ sein. Durch die strenge Typisierung von SML wird sichergestellt, daß sich als Ergebnis der Reduktion von f entweder eine Variable von funktionalem Typ oder ein λ-Ausdruck ergibt. Im ersten Fall ist dann außerdem sichergestellt, daß die Variable an einen λ-Ausdruck gebunden ist, der eindeutig aus der zugehörigen Funktions- oder Wertedeklaration hervorgeht.

Die einfachste Form eines λ-Ausdrucks in SML ist

                              (fn x => e) ,

wobei x eine Variable und e ein beliebiger Ausdruck ist. Eine Applikation, nachdem beide Operanden f und e reduziert sind, und sich für f ein λ-Ausdruck dieser Form ergeben hat, wird dann in folgender Weise β-reduziert:

(fn x => e) e′ ⟶ e[e′/x]

wobei e[e′/x] aus e durch Substitution von e′ für alle freien Auftreten von x in e entsteht. Der Substitutionsbegriff ist in diesem Kontext komplexer als wir ihn für Konstruktorterme und Muster kennengelernt haben. Es gibt im wesentlichen zwei Komplikationen:

Es werden nur freie Auftreten von x in e reduziert. Ein Auftreten von x in einem Ausdruck e ist frei, wenn es nicht ein Auftreten in einem Teilausdruck der Form (fn x => ẽ) von e ist. Ein solches Auftreten heißt gebunden. Enthält e also innere λ-Ausdrücke, die x binden, so wird x in deren Rümpfen nicht ersetzt:

           (fn x => (x (fn x => x))) e′ ⟶ (e′ (fn x => e))

Desweiteren ist immer vorausgesetzt, daß bei der Substitution keine freie Variable in e′ nach Einsetzung für x gebunden wird. Gegebenenfalls muß man sonst gebundene Variablen in e umbenennen. Also, nicht gemeint ist etwa

             (fn x => (fn y => y x)) y ⟶ (fn y => y y) ,

sondern stattdessen

             (fn x => (fn y => y x)) y ⟶ (fn y′ => y′ y) ,

wobei wir zuerst im innernen λ-Ausdruck y in y′ umbenannt haben, um den Variablenkonflikt zu vermeiden. Die Bindungen der freien Variablen in e′ verändern sich also nicht, sondern bleiben so, wie es dem statischen Auftreten von (f e′) in einem größeren Ausdruck oder Programm entspricht.

In SML ist die allgemeine Form von Funktionsdefinitionen und von λ-Ausdrücken komplexer. So erzeugt die Auswertung von fun f x y => e die Bindung f ≡ (fn x=> (fn y => e)),^{1} was aber keiner Erweiterung des Konzeptes der β-Reduktion bedarf.

Anstelle einer Variablen x kann auch allgemeiner ein Muster M stehen. Dann haben wir als allgemeinere Form der β-Reduktion die Regel

(fn M => e) e′ ⟶ e[e′_{1}/x_{1}, …, e′_{n}/x_{n}]

1Man beachte, daß in SML der wesentliche Unterschied zwischen einer val-Deklaration und einer fun-Deklaration der ist, daß erstere (leider?) nicht rekursiv ist, d.h. die rechte Seite e in val x = e in der alten Umgebung ausgewertet wird. Bei Funktions- (und datatype-) Definitionen ist dies anders. In fun f x = e ist die neue Bindung f ≡ (fn x => e) bereits in e sichtbar. Damit ist nur, wenn f in e nicht frei auftritt, fun f x = e mit val f = (fn x=> (fn y => e)) äquivalent.

wenn x_{i} die in M auftretenden Variablen sind und unter Substitution

σ = [x_{1} ↦ e′_{1}, …, x_{n} ↦ e′_{n}]

das Muster M auf die Normalform von e′ paßt, d.h. Mσ = value(e′) gilt. Entsprechend wird bei mehr als einem Muster die Applikation so reduziert, daß die erste passende Alternative j ausgewählt wird:

(fn M_{1} => e_{1} | … | M_{k} => e_{k}) e′ ⟶ e_{j}[e′_{1}/x_{1}, …, e′_{n}/x_{n}] .

Merke:

• Ausdrücke von funktionalem Typ werden nur soweit reduziert, bis sich ein λ-Ausdruck ergibt. Ergibt sich eine Funktionsvariable, so wird der an sie gebundene λ-Ausdruck eingesetzt.

• Die diversen, komplexen Formen von Funktionsdefinitionen in SML erzeugen Bindungen von (Funktions-)Variablen an λ-Ausdrücke nach SML-Bauart (Übung!).

• Applikationen mit einem λ-Ausdruck als Funktion werden β-reduziert, wobei die gebundenen Variablen durch die (Komponenten des) aktuellen Parameter(s) ersetzt werden.

• Bei diesen Substitutionen muß darauf geachtet werden, daß keine Namenskonflikte vorliegen, die aus einer freien Variablen eine gebundene machen könnten. Andernfalls müssen gebundene Variablen geeignet umbenannt werden.

• Die Bindungen von freien Variablen werden nicht verändert.

• Diese Konzept der Reduktion von Applikationen ist eine echte Verallgemeinerung des in Abschnitt 3.3.2 besprochenen Konzepts von Termersetzung erster Stufe. Dort haben wir für die Funktionen erster Stufe die Schritte von Applikation einer Funktionsvariablen über zugehörigen λ-Ausdruck zu Reduktionsregeln für die Applikation vereinfacht dergestellt unter Auslassung der λ-Ausdrücke. Wann immer Funktionen als Daten auftreten, ist diese vereinfachte Sicht nicht mehr angebracht.

Kommen wir abschließend zu einem Beispiel, was die erhöhte Mächtigkeit des erweiterten Reduktionsbegriffs illustriert:

Sei map eine Funktion, welche Funktionen auf Listen elementweise fortsetzt, und wie folgt definiert ist:

fun map _nil = nil
  | map f (x::l) = (f x)::(map f l)

Sei weiter

fun plus x y = x+y:int;

Dann ist

val mapsucc = map (plus 1);

eine Funktion vom Typ int list → int list, welches die Elemente seiner Argumentlisten um 1 erhöht:

- mapsucc [1,2]

[2,3]

Die angegeben Definitionen erzeugen folgene Menge von Bindungen:

   map ≡ (fn f => (fn nil => nil | (hd::tl) => (f hd) :: (map f tl)))
  plus ≡ (fn x => (fn y => x + y))
mapsuc ≡ map (plus 1)

In dieser Umgebung reduzieren wir daher beispielsweise (wobei wir ≡ schreiben, wenn Bindungen eingesetzt werden):

mapsucc [2]
≡ (map (plus 1)) [2]
≡ (map ((fn x=>(fn y=>x + y)) 1)) [2]
→ (map (fn y=>1 + y)) [2]
≡ ((fn f=>(fn nil=>nil | (hd::tl)=>(f hd)::(map f tl))) (fn y=>1 + y)) [2]
→ (fn nil=>nil | (hd::tl)=>((fn y=>1 + y) hd)::(map (fn y=>1 + y) tl) [2]
→ ((fn y=>1 + y) 2)::(map (fn y=>1 + y) nil)
→ (1 + 2)::(map (fn y=>1 + y) nil)
→ 3::(map (fn y=>1 + y) nil)
≡ 3::(((fn f=>(fn nil=>nil | (hd::tl)=>(f hd)::(map f tl))) (fn y=>1 + y)) nil)
→ 3::((fn nil=>nil | (hd::tl)=>((fn y=>1 + y) hd)::(map (fn y=>1 + y) tl)) nil)
→ 3::nil

= [3]