Transcript
¨ Ubersetzerbau Algebraic Compiler Construction Peter Padawitz, TU Dortmund, Germany Webseite zur LV: fldit-www.cs.uni-dortmund.de/ueb.html Thursday 24th March, 2016 00:33 1
Inhalt
Mit ∗ markierte Abschnitte bzw. Kapitel werden zur Zeit in der LV nicht behandelt. Zur Navigation auf Titel, nicht auf Seitenzahlen klicken! 1 Einleitung 2 Algebraische Modellierung - Mengen und Typen - Signaturen - 2.9 Konstruktive Signaturen - 2.10 Destruktive Signaturen - 2.11 Algebren - 2.12 Terme und Coterme - 2.13 Beispiele - 2.14 Die Algebren Bool und Regword (BS) - 2.15 Die Algebren Beh(X, Y ), Pow (X), Lang(X) und Bro(BS) - 2.16 Die Erreichbarkeitsfunktion - 2.17 Termfaltung und Zustandsentfaltung - 2.21 * Compiler fu¨r regul¨are Ausdru¨cke - 2.22 * Minimale Automaten
7 14 14 30 31 34 38 44 49 56 57 61 62 74 77 2
- 2.25 * Baumautomaten 3 * Rechnen mit Algebren - Unteralgebren - Kongruenzen und Quotienten - Automatenminimierung durch Quotientenbildung - Transitionsmonoid und syntaktische Kongruenz - 3.6 Termsubstitution - Term¨aquivalenz und Normalformen - 3.10 Normalformen regul¨arer Ausdru¨cke - 3.11 Die Brzozowski-Gleichungen - 3.12 Optimierter Brzozowski-Automat - 3.13 Erkenner regul¨arer Sprachen sind endlich 4 Kontextfreie Grammatiken (CFGs) - Nicht-linksrekursive CFGs - Abstrakte Syntax - Wort- und Ableitungsbaumalgebra - Modelle der Ausdru¨cke von JavaLight 5 Parser und Compiler fu¨r CFGs - 5.1 Funktoren und Monaden - Compilermonaden - Monadenbasierte Parser und Compiler
80 82 83 87 91 92 94 96 101 102 104 106 109 114 117 126 131 136 138 150 152 3
6 LL-Compiler 7 LR-Compiler 8 Haskell: Typen und Funktionen 9 Haskell: Listen 10 Haskell: Datentypen und Typklassen 11 Algebren in Haskell - 11.1 Beispiele - 11.2 Datentyp der JavaLight-Algebren - 11.3 Die Termalgebra von JavaLight - 11.4 Die Wortalgebra von JavaLight - 11.5 Das Zustandsmodell von JavaLight - 11.6 * Die Ableitungsbaumalgebra von JavaLight ¨ 12 Attributierte Ubersetzung - 12.1 * Bin¨ardarstellung rationaler Zahlen - 12.2 * Strings mit Hoch- und Tiefstellungen ¨ - 12.3 * Ubersetzung regul¨arer Ausdru¨cke in erkennende Automaten - 12.4 * Darstellung von Termen als hierarchische Listen - 12.5 Eine kellerbasierte Zielsprache fu¨r JavaLight 13 JavaLight+ = JavaLight + I/O + Deklarationen + Prozeduren - 13.1 Assemblersprache mit I/O und Kelleradressierung - 13.2 Grammatik und abstrakte Syntax von JavaLight+
157 177 205 215 226 240 241 246 247 248 250 253 256 257 259 261 267 270 276 276 283 4
14 15 16
17
18
19
- 13.3 JavaLight+-Algebra javaStackP * Mehrp¨assige Compiler Funktoren und Monaden in Haskell Monadische Compiler - 16.1 Compilerkombinatoren - 16.2 Monadische Scanner - 16.3 Monadische LL-Compiler - 16.4 Generischer JavaLight-Compiler - 16.5 Korrektheit des JavaLight-Compilers - 16.6 Generischer XMLstore-Compiler * Induktion, Coinduktion und rekursive Gleichungen - Induktion - Induktive L¨osungen - Coinduktion - Coinduktive L¨osungen - 17.11 Cotermbasierte Erkenner regul¨arer Sprachen * Iterative Gleichungen - 18.2 Das iterative Gleichungssystem einer CFG - 18.5 Von Erkennern regul¨arer Sprachen zu Erkennern kontextfreier Sprachen * Interpretation in stetigen Algebren - 19.1 Schleifensemantik
287 310 318 327 331 333 335 338 340 344 346 346 348 353 360 376 378 379 384 394 399 5
- 19.2 Semantik der Assemblersprache StackCom ∗ - Erweiterte Σ-B¨aume - Cosignaturen und ihre Algebren Literatur Index
401 408 415
6
1 Einleitung
Die Folien dienen dem Vor- (!) und Nacharbeiten der Vorlesung, k¨onnen und sollen aber deren regelma¨ßigen Besuch nicht ersetzen! Interne Links (einschließlich der Seitenzahlen im Index) sind an ihrer dunkelroten F¨arbung, externe Links (u.a. zu Wikipedia) an ihrer magenta-F¨arbung erkennbar. Dunkelrot gef¨arbt ist auch das jeweils erste Vorkommen einer Notation. Fettgedruckt ist ein Begriff in der Regel nur an der Stelle, an der er definiert wird. Jede Kapitelu¨berschrift und jede Seitenzahl in der rechten unteren Ecke einer Folie ist mit dem Inhaltsverzeichnis verlinkt. Namen von Haskell-Modulen wie Java.hs sind mit den jeweiligen Programmdateien verknu¨pft. Ein Scanner (Programm zur lexikalischen Analyse) fasst Zeichen zu Symbolen zusammen, u¨bersetzt also eine Zeichenfolge in eine Symbolfolge. Bezu¨glich der Grammatik, die der nachfolgenden Syntaxanalyse zugrundeliegt, heißen die Symbole auch Terminale. Man muss unterscheiden zwischen Symbolen, die Komponenten von Operatoren sind (if, then, =, etc.), und Symbolen wie 5 oder True, die der Scanner einer Basismenge (Int, Float, Bool, Identifier, etc.) zuordnet. In der Grammatik kommt ein solches Symbol nicht vor, jedoch der Namen der Basismenge, der es angeh¨ort. 7
Ein Parser (Programm zur Syntaxanalyse) u¨bersetzt eine Symbolfolge in einen Syn¨ taxbaum, der den fu¨r ihre Ubersetzung in eine Zielsprache notwendigen Teil ihrer Bedeutung (Semantik) wiedergibt. Der Parser scheitert, wenn die Symbolfolge in diesem Sinne bedeutungslos ist. Er orientiert sich dabei an einer (kontextfreien) Grammatik, die korrekte von bedeutungslosen Symbolfolgen trennt und damit die Quellsprache definiert. Ein Compiler (Programm zur semantischen Analyse und Codeerzeugung) u¨bersetzt ein Programm einer Quellsprache in ein semantisch ¨aquivalentes Programm einer Zielsprache. Ein Interpreter • wertet einen Ausdruck in Abh¨angigkeit von einer Belegung seiner Variablen aus bzw. • fu¨hrt eine Prozedur in Abh¨angigkeit von einer Belegung ihrer Parameter aus. Letzteres ist ein Spezialfall von Ersterem. Deshalb werden wir einen Interpreter stets als die Faltung von Termen (Ausdru¨cken, die aus Funktionssymbolen einer Signatur bestehen) in einer Algebra (Interpretation der Signatur) modellieren.
8
Auch Scanner, Parser und Interpreter sind Compiler, insofern sie Objekte von einer Repr¨asentation in eine andere u ¨bersetzen. Die Zielrepr¨asentation eines Interpreters ist i.d.R. eine Funktion, die Eingabedaten verarbeitet. Daher liegt es nahe, alle o.g. Programme nach denjenigen Prinzipien zu entwerfen, die bei Compilern im engeren Sinne Anwendung finden. Die Entwicklung dieser Prinzipien und ihrer formalen Grundlagen wurzelt in der mathematischen Logik und dort vor allem in der Theorie formaler Sprachen und der Universellen Algebra, deren Anwendung im Compilerbau in dieser LV eine zentra¨ le Rolle spielen wird. Die Aufgabe, Ubersetzer zu schreiben, hat auch entscheidend die Weiterentwicklung von Programmiersprachen, insbesondere der logischen und funktionalen, vorangetrieben. Insbesondere Konzepte der universellen Algebra und der funktionalen Programmierung im ¨ Ubersetzerbau erlauben es, bei Entwurf und Implementierung von Scannern, Parsern, Compilern und Interpretern a¨hnliche Methoden einzusetzen. So ist z.B. ein wie oben definierter Interpreter gleichzeitig ein Compiler, der den Ausdruck oder die Prozedur in eine Funktion u¨bersetzt, die eine Belegung auf einen Wert des Ausdrucks bzw. eine vom Aufruf der Prozedur erzeugte Zustandsfolge abbildet.
9
Der algebraische Ansatz kla¨rt nicht nur die Bezu¨ge zwischen den oben genannten Programmen, sondern auch eine Reihe weiterer in der Compilerbauliteratur meist sehr speziell definierter und daher im Kern vager Begriffe wie attributierter Grammatiken und mehrp¨assiger Compilation. Mehr Beachtung als die nicht wirklich essentielle Trennung zwischen Scanner, Parser, Compiler und Interpreter verdienen die Ans¨atze, Compiler generisch (neu-informatisch: agil) zu entwerfen, so dass sie mit verschiedenen Quellsprachen und - wichtiger noch - mehreren Zielsprachen instanziiert werden k¨onnen. Es handelt sich dann im Kern um einen Parser, der keine Symbol-, sondern Zeichenfolgen verarbeitet und ohne den klassischen Umweg u¨ber Syntaxb¨aume gleich die gewu¨nschten Zielobjekte/programme aufbaut. Sein front end kann mit verschiedenen Scannern verknu¨pft werden, die mehr oder weniger detaillerte Symbolund Basistypinformation erzeugen, w¨ahrend sein back end mit verschiedenen Interpretationen ein und derselben - u¨blicherweise als kontextfreie Grammatik eingegebenen - Signatur instanziiert werden kann, die verschiedenen Zielsprachen entsprechen. Die beiden folgenden Grafiken skizzieren die Struktur des algebraischen Ansatzes und seine Auswirkung auf die Generizit¨at der Programme. Auf die Details wird in den darauffolgenden Kapiteln eingegangen. Dabei wird die jeweilige Funktionalita¨t der o.g. Programme in mathematisch pr¨azise Definitionen gefasst, auf denen Entwurfsregeln aufbauen, deren Befolgung automatisch zu korrekten Compilern, Interpretern, etc. fu¨hren.
10
Erkenner
Programmeigenschaften Σ(G)-Formeln
Bool
Σ(G)-Algebren Quellsprache L(G)
Verifizierer Unparser
konkrete Syntax Grammatik G
abstrakte Syntax Signatur Σ(G)
Syntaxbäume Termalgebra TΣ(G)
Optimierer allgemein: Termfaltung
Parser
Quellsprache L(G)
Unparser
Compiler
Ableitungsbäume Abl(G)
optimierte Syntaxbäume
Zielsprache
Von konkreter u ¨ber abstrakte Syntax zu Algebren
11
Menge Faltung kontextfreie Sprache
Parser
Termalgebra
Faltung
Menge
Faltung Menge Algebra
kontextfreie Sprache
Parser
Termalgebra
generische Faltung
Algebra
Algebra Algebra
kontextfreie Sprache
generischer Compiler
Algebra
Algebra
Der Weg zum generischen Compiler 12
fact =1; while x > 1 {fact = fact*x; x = x-1;} Eingabewort (Element der JavaLight-Algebra javaWord) parse
fold
Seq Assign fact
Embed
Sum
Prod EmbedI
Loop
NilS
NilP
1
EmbedC
Block
EmbedL
Seq
Atom Sum Prod Var
>
Sum
NilS
NilP
x
Assign
Prod EmbedI
fact
NilS
NilP
1
Sum
Prod Var fact
Embed Assign
NilS
x
Prodsect *
Var x
NilP
Sum
Prod Var x
Syntaxbaum (Element der JavaLight-Algebra javaTerm)
NilP
Sumsect -
Prod
EmbedI
NilS
NilP
1
fold
fold
Zustandstransitionsfunktion (Element der JavaLight-Algebra javaState) Assemblerprogramm (Element der JavaLight-Algebra javaStack)
13
2 Algebraische Modellierung
Mengen und Typen ∅ bezeichnet die leere Menge, 1 die Menge {} und 2 die Menge {0, 1}. 0 und 1 stehen hier in der Regel fu¨r die Wahrheitswerte false und true. Fu¨r alle n > 1, [n] =def {1, . . . , n}. Wir setzen voraus, dass die Definitionen einer Potenzmenge, bin¨ aren Relation bzw. (partiellen oder totalen) Funktion sowie der Vereinigung, des Durchschnitts, des Komplements, der Disjunktheit und der M¨ achtigkeit (Kardinalit¨ at) von Mengen bekannt sind. λ-Abstraktionen zur anonymen Definition und die (sequentielle) Komposition mehrerer Funktionen sollten ebenfalls bekannt sein. Fu¨r jede Menge A bezeichnet |A| die Kardinalit¨at von A, P(A) die Potenzmenge von A und idA : A → A die durch idA(a) = a fu¨r alle a ∈ A definierte Identit¨ at auf A. Fu¨r jede Teilmenge B von A bezeichnet incB : B → A die durch incB (b) = b fu¨r alle b ∈ B definierte Inklusion. Fu¨r alle Mengen A, B bezeichnen A → B und B A die Menge der totalen und A (→ B die Menge der partiellen Funktionen von A nach B. def (f ) bezeichnet den Definitionsbereich einer partiellen Funktion f : A (→ B. 14
Mehrsortige Mengen und Funktionen Sei S eine Menge. Eine S-sortige oder S-indizierte Menge ist ein Tupel A = (As)s∈S von Mengen. Manchmal schreiben wir A auch fu¨r die Vereinigung der Mengen As u¨ber alle s ∈ S. Seien A1, . . . , An S-sortige Mengen. Eine S-sortige Teilmenge von A1 × · · · × An ist eine S-sorted Menge R = (Rs)s∈S mit Rs ⊆ A1,s × . . . × An,s fu¨r alle s ∈ S. Seien A = (As)s∈S und B = (Bs)s∈S S-sortige Mengen. Eine S-sortige Funktion f : A → B ist eine S-sortige Menge (fs)s∈S derart, dass fu¨r alle s ∈ S, fs eine Funktion von As nach Bs ist. Sei I eine Menge. Das kartesische Produkt (der Komponenten) einer I-sortigen Menge A = (Ai)i∈I ist wie folgt definiert: [ Xi∈I Ai = {f : I → Ai | ∀ i ∈ I : f (i) ∈ Ai}. i∈I
Xi∈I Ai aus der einzigen Funktion von ∅ nach i∈I Ai. Gibt es eine Menge A mit Ai = A fu¨r alle i ∈ I, dann stimmt Xi∈I Ai offenbar mit AI
Im Fall I = ∅ besteht
S
u¨berein. Im Fall I = [n] fu¨r ein n > 1 schreibt man auch A1 × · · · × An anstelle von An anstelle von AI .
Xi∈I Ai und 15
Sei I eine Menge. Die disjunkte Vereinigung (der Komponenten) einer I-sortigen Menge A = (Ai)i∈I ist wie folgt definiert: ] [ Ai = (Ai × {i}). i∈I
i∈I
Die disjunkte Vereinigung des leeren Mengentupels wird definiert als die leere Menge. U Gibt es eine Menge A mit Ai = A fu¨r alle i ∈ I, dann stimmt i∈I Ai offenbar mit A × I u¨berein. U Im Fall I = [n] fu¨r ein n > 1 schreibt man auch A1 + · · · + An anstelle von i∈I Ai. Der Plusoperator + und der Sternoperator ∗ bilden jede Menge A, die das leere Wort nicht enth¨alt, auf die Menge der (nichtleeren) W¨ orter oder Listen u ¨ ber A ab: S n A+ =def n>0 A , 1 =def {}, A∗ =def 1 ∪ A+. Die Folge der Komponenten eines Elements von A+ wird manchmal (z.B. in Haskell) nicht wie oben mit runden, sondern mit eckigen Klammern eingeschlossen oder (wie in der Theorie formaler Sprachen) zusammen mit den Kommas ganz weggelassen. Teilmengen von A∗ werden auch Sprachen u ¨ ber A genannt. 16
Die Konkatenationen · : A∗ × A∗ → A∗ und · : P(A∗) × P(A∗) → P(A∗) sind wie folgt induktiv definiert: Fu¨r alle s, v = (a1, . . . , am), w = (b1, . . . , bn) ∈ A∗ und B, C ⊆ A∗, · w = w, v · = v, v · w = (a1, . . . , am, b1, . . . , bn), B · C = {v · w | v ∈ B, w ∈ C}. Fu¨r alle w ∈ A+ bezeichnet head(w) das erste Element von w und tail(w) die Restliste, d.h. es gilt w = head(w) · tail(w). |w| bezeichnet die L¨ ange eines Wortes w, d.h. die Anzahl seiner Elemente.
17
L ⊆ A∗ heißt pr¨ afixabgeschlossen, wenn fu¨r alle w ∈ A∗ und a ∈ A aus wa ∈ L w ∈ L folgt. Eine partielle Funktion f : A∗ (→ B mit pr¨afixabgeschlossenem Definitionsbereich heißt deterministischer Baum. f ist wohlfundiert (a: e), wenn es n ∈ N gibt mit |w| ≤ n fu¨r alle w ∈ def (t). Anschaulich gesprochen ist f wohlfundiert, wenn f endliche Tiefe hat, wenn also alle von der Wurzel ausgehenden Pfade endlich sind. Tatsa¨chlich kann man sich f als (m¨oglicherweise unendlichen) Baum tf mit Kantenmarkierungen aus A und Knotenmarkierungen aus B vorstellen, der keine zwei Kanten mit derselben Quelle, aber verschiedener Markierung besitzt. f () ∈ B ist die Markierung der Wurzel von tf und jeder von der Wurzel ausgehende Pfad p endet in einem Knoten, der mit f (w) markiert ist, wobei w ∈ A+ die Folge der Markierungen der Kanten von p ist. Demnach kann ein deterministischer Baum als eine Art Record notiert werden: tf = f (){x → tλw.f (xw) | x ∈ def (t) ∩ A}. Die Menge aller deterministischer B¨aume von A∗ nach B wird mit dtr(A, B) bezeichnet, die Menge der wohlfundierten darunter mit wdtr(A, B).
18
Fu¨r alle Mengen A, B, Funktionen f : A → B, C ⊆ A, D ⊆ B und n > 0, ∆nA =def {(a1, . . . , an) ∈ An | ∀ 1 ≤ i < n : ai = ai+1} Diagonale von A f (C) =def {f (a) | a ∈ C}
Bild von C unter f
= P(f )(C) (siehe Mengenfunktor) img(f ) =def f (A) f −1(D) =def {a ∈ A | f (a) ∈ D}
Urbild von D unter f
ker(f ) =def {(a, a0) ∈ A × A | f (a) = f (a0)}
Kern von f
graph(f ) =def {(a, f (a)) ∈ A × B | a ∈ A} f |C : C
→ B
c 7→ f (c) f [b/a] : A → B
Graph von f Einschr¨ ankung von f auf C Update von f
c 7→ if c = a then b else f (c) χ : P(A) → χ(C) C
7→ λa.if a ∈ C then 1 else 0
charakteristische Funktion von C
19
f ist surjektiv ⇔def img(f ) = B f ist injektiv ⇔def ker(f ) = ∆2A f ist bijektiv ⇔def ∃ g : B → A : g ◦ f = idA ∧ f ◦ g = idB A und B heißen isomorph, geschrieben: A ∼ = B, wenn es eine bijektive Funktion von A nach B gibt. Aufgabe Zeigen Sie: P(A) ∼ = 2A . Aufgabe Zeigen Sie: P(A × B) ∼ = P(B)A.
o
Aufgabe Zeigen Sie: f : A → B ist bijektiv ⇔ f ist injektiv und surjektiv.
o
o
Aufgabe Zeigen Sie: Ist f : A → B bijektiv, dann gibt es genau eine (u¨blicherweise mit f −1 bezeichnete) Funktion g : B → A mit g ◦ f = idA und f ◦ g = idB . o
20
Produkte und Summen als universelle Konstruktionen Sei I eine nichtleere Menge und A eine I-sortige Menge. Das kartesische Produkt und die disjunkte Vereinigung eines Mengentupels A haben bestimmte universelle Eigenschaften, d.h. erstens, dass alle Mengen, die diese Eigenschaften haben, isomorph sind und zweitens, dass jede Menge, die zu einer anderen Menge, die diese Eigenschaften hat, isomorph ist, selbst diese Eigenschaften hat. Jede Menge, die die universellen Eigenschaften des kartesischen Produkts bzw. der disjunkten Vereinigung von A hat, nennt man Produkt bzw. Summe von A: Sei A = (Ai)i∈I ein Mengentupel, P eine Menge und π = (πi : P → Ai)i∈I ein Funktionstupel. Das Paar (P, π) heißt Produkt von A, wenn es fu¨r alle Tupel f = (fi : B → Ai)i∈I genau eine Funktion g : B → P gibt derart, dass fu¨r alle i ∈ I Folgendes gilt: πi ◦ g = f i
(1)
πi heißt i-te Projektion von P und g Produktextension oder Range-Tuplung von f . g wird mit hfiii∈I und im Fall I = [n], n > 1, auch mit hf1, . . . , fni bezeichnet. Demnach ist im Fall I = ∅ eine Menge P genau dann ein Produkt, wenn es zu jeder Menge B genau eine Funktion von B nach P gibt, wenn also P einelementig ist. 21
Wegen der Eindeutigkeit von Produktextensionen sind zwei Funktionen f, g : B → P genau dann gleich, wenn ihre Produktkomponenten paarweise miteinander u¨bereinstimmen: (∀ i ∈ I : πi ◦ f = πi ◦ g)
⇒
f = g.
(2)
Mit f = λx.a : 1 → P und g = λx.b : 1 → P folgt aus (2), dass zwei Elemente a, b ∈ P genau dann gleich sind, wenn fu ¨ r alle i ∈ I πi(a) = πi(b) gilt. Beweis. (2)
∀ i ∈ I : πi(a) = πi(b) ⇒ ∀ i ∈ I : πi ◦ f = πi ◦ g ⇒ f = g ⇒ a = f () = g() = b. o Aufgabe 2.1 Sei P = Xi∈I Ai (s.o.) und πi(f ) =def f (i) fu¨r alle i ∈ I und f ∈ P . Zeigen Sie, dass (P, (πi)i∈I ) ein Produkt von A ist, wenn die Extension von (fi : B → Ai)i∈I wie folgt definiert wird: • Fu¨r alle b ∈ B und i ∈ I, hfiii∈I (b)(i) =def fi(b).
o
Satz 2.2 (Produkte sind bis auf Isomorphie eindeutig) (i) Seien (P, π) und (P 0, π 0) Produkte von A. Dann sind P und P 0 isomorph. (ii) Sei (P, π) ein Produkt von A, P 0 eine Menge und h : P 0 → P eine bijektive Abbildung. 22
Dann ist (P 0, π 0) mit π 0 = (πi ◦ h)i∈I ebenfalls ein Produkt von A. Beweis von (i). Um die Extensionen auf P ersten von denen auf P 0 zu unterscheiden, wird die schließende Klammer letzterer gestrichelt. Sei h =def hπii0i∈I : P → P 0 und h0 =def hπi0 ii∈I : P 0 → P . Dann gilt (1)
(1)
(1)
(1)
πi ◦ h0 ◦ h = πi ◦ hπi0 ii∈I ◦ hπii0i∈I = πi0 ◦ hπii0i∈I = πi, πi0 ◦ h ◦ h0 = πi0 ◦ hπii0i∈I ◦ hπi0 ii∈I = πi ◦ hπi0 ii∈I = πi0 fu¨r alle i ∈ I, also h0 ◦ h = idP und h ◦ h0 = idP 0 wegen (2). Beweis von (ii). Sei f = (fi : B → Ai)i∈I und g =def h−1 ◦ hfiii∈I : B → P 0. g erfu¨llt (1) mit π 0 anstelle von π: Fu¨r alle i ∈ I, (1)
πi0 ◦ g = πi ◦ h ◦ g = πi ◦ h ◦ h−1 ◦ hfiii∈I = πi ◦ hfiii∈I = fi. g ist eindeutig: Sei g 0 : B → P 0 eine weitere Funktion, die (1) erfu¨llt, fu¨r die also πi0 ◦ g 0 = fi fu¨r alle i ∈ I gilt. Daraus folgt πi ◦ h ◦ g = πi0 ◦ g = fi = πi0 ◦ g 0 = πi ◦ h ◦ g 0, also h ◦ g = h ◦ g 0 wegen (2) und damit g = h−1 ◦ h ◦ g = h−1 ◦ h ◦ g 0 = g 0.
o 23
Sei (P, π) ein Produkt von (Ai)i∈I , (P 0, π 0) ein Produkt von (Bi)i∈I und f = (fi : Ai → Bi)i∈I . Die Funktion Y
fi =def hfi ◦ πii : P → P 0
i∈I
heißt Produkt von f . Daraus folgt πk ◦ (
Y
f i ) = f k ◦ πk
i∈I
fu¨r alle k ∈ I. Sei I eine nichtleere Menge und n > 0. f I =def
Q
i∈I [n]
f,
f1 × · · · × fn =def f .
Aufgabe 2.3 Zeigen Sie, dass im Fall P = Xi∈I Ai und P 0 = Xi∈I Bi (siehe Aufgabe 2.1) fu¨r Q alle f ∈ P ( i∈I fi)(f ) mit λi.fi ◦ f u¨bereinstimmt. o
24
Vom Produkt kommt man zur Summe, indem man alle Funktionspfeile umdreht: Sei A = (Ai)i∈I ein Mengentupel, S eine Menge und ι = (ιi : Ai → S)i∈I ein Funktionstupel. Das Paar (S, ι) heißt Summe oder Coprodukt von A, wenn es fu¨r alle Tupel f = (fi : Ai → B)i∈I genau eine Funktion g : S → B gibt mit g ◦ ιi = fi
(3)
fu¨r alle i ∈ I. ιi heißt i-te Injektion von S und g Summenextension oder Domain-Tuplung von f . g wird mit [fi]i∈I und im Fall I = [n], n > 1, auch mit [f1, . . . , fn] bezeichnet. Demnach ist im Fall I = ∅ eine Menge S genau dann eine Summe, wenn es zu jeder Menge B genau eine Funktion von S nach B gibt, wenn also S die leere Menge ist. Wegen der Eindeutigkeit von Summenextensionen sind zwei Funktionen f, g : S → B genau dann gleich, wenn ihre Summenkomponenten paarweise miteinander u¨bereinstimmen: (∀ i ∈ I : f ◦ ιi = g ◦ ιi)
⇒
f = g.
(4)
Aus (4) folgt, dass fu ¨ r alle a ∈ S genau ein Paar (b, i) mit ιi(b) = a existiert.
25
Beweis. G¨abe es a ∈ S \
S
i∈I ιi (Ai ),
dann wu¨rden f = λx.0 : S → 2 und
g = (λx.if x ∈ S \ {a} then 0 else 1) : S → 2 (4) verletzen, weil fu¨r alle i ∈ I und b ∈ Ai Folgendes gilt: (f ◦ ιi)(b) = f (ιi(b)) = 0 = g(ιi(b)) = (g ◦ ιi)(b). Fu¨r alle i ∈ I und a ∈ Ai sei fi(a) = (a, i). Dann gilt fu¨r alle i, j ∈ I, a ∈ Ai und b ∈ Aj mit ιi(a) = ιj (b): (3)
(a, i) = fi(a) = ([fi]i∈I ◦ ιi)(a) = [fi]i∈I (ιi(a)) = [fi]i∈I (ιj (b)) = ([fi]i∈I ◦ ιj )(b) (3)
= fj (b) = (b, j).
o
Aufgabe 2.4 U Sei S = i∈I Ai (s.o.) und ιi(a) =def (a, i) fu¨r alle i ∈ I und a ∈ Ai. Zeigen Sie, dass (S, (ιi)i∈I ) eine Summe von A ist, wenn die Extension von (fi : Ai → B)i∈I wie folgt definiert wird: Fu¨r alle i ∈ I und a ∈ Ai, [fi]i∈I (a) =def fi(a). o Aufgabe 2.5 S Sei S = i∈I Ai und ιi(a) =def a fu¨r alle i ∈ I und a ∈ Ai. Zeigen Sie, dass (S, (ιi)i∈I ) eine Summe von A ist, falls A aus paarweise disjunkten Mengen besteht. o 26
Aufgabe 2.6 Sei A eine Menge, S = A∗ (s.o.) und ιn(a) =def a fu¨r alle n ∈ N und a = (a1, . . . , an) ∈ An. Zeigen Sie, dass (S, (ιn)n∈N) eine Summe von (An)n∈N ist. o Satz 2.7 (Summen sind bis auf Isomorphie eindeutig) (i) Seien (S, ι) und (S 0, ι0) Summen von A. Dann sind P und P 0 isomorph. (ii) Sei (S, ι) eine Summe von A, S 0 eine Menge und h : S → S 0 eine bijektive Abbildung. Dann ist (S 0, ι0) mit ι0 = (h ◦ ιi)i∈I ebenfalls eine Summe von A. Beweis. Analog zu Satz 2.2. Es mu¨ssen nur alle Funktionspfeile umgedreht werden.
o
Sei (S, ι) eine Summe von (Ai)i∈I , (S 0, ι0) eine Summe von (Bi)i∈I und f = (fi : Ai → Bi)i∈I . Die Funktion a
fi =def [ι0i ◦ fi] : S → S 0
i∈I
heißt Summe von f .
27
Daraus folgt (
a
fi) ◦ ιk = ιk ◦ fk
i∈I
fu¨r alle k ∈ I. Sei n > 0. f + =def f ∗ =def f1 + · · · + fn =def
[n] n∈N f , id1 + f +,
`
`
i∈[n] fi .
U U Aufgabe 2.8 Zeigen Sie, dass im Fall S = i∈I Ai und S 0 = i∈I Bi (siehe Aufgabe 2.4) ` fu¨r alle i ∈ I und a ∈ Ai ( i∈I fi)(a, i) mit (fi(a), i) u¨bereinstimmt. o
28
Typen Sei S eine endliche Menge von – Sorten genannten – Symbolen und I eine Menge nichtleerer Indexmengen, die implizit die Mengen 1, 2 und [n], n > 1, entha¨lt. Die Menge T (S, I) der I-polynomialen Typen u ¨ ber S ist die kleinste Menge von Ausdru¨cken mit folgenden Eigenschaften: • S ∪ I ⊆ T (S, I). ` Q • Fu¨r alle I ∈ I und {ei}i∈I ⊆ T (S, I), i∈I ei, i∈I ei ∈ T (S, I). Q ` Ein Typ der Form i∈I ei bzw. i∈I ei heißt Produkttyp bzw. Summentyp. Fu¨r alle I ∈ I, n > 1 und e, e1, . . . , en ∈ T (S, I) verwenden wir folgende Kurzschreibweisen: Q e1 × · · · × en =def i∈[n] ei , ` e1 + · · · + en =def i∈[n] ei , Q eI =def i∈I e, en =def e[n], e+ =def e +
`
n>1 e +
n
,
e∗ =def 1 + e .
29
Signaturen Eine Signatur Σ = (S, I, F ) besteht aus Mengen S und I wie oben sowie einer endlichen Menge F typisierter Funktionssymbole f : e → e0 mit e, e0 ∈ T (S, I), die u¨blicherweise Operationen genannt werden. dom(f ) = e heißt Domain, ran(f ) = e0 Range von f . f : e → e0 ∈ F heißt Konstruktor bzw. Destruktor, wenn e bzw. e0 zu S geh¨ort. Σ heißt konstruktive bzw. destruktive Signatur, wenn F aus Konstruktoren bzw. Destruktoren besteht und fu¨r alle s ∈ S die Menge aller f ∈ F mit ran(f ) = s bzw. dom(f ) = s implizit zu I geh¨ort. Die komponentenweise Vereinigung zweier Signaturen Σ und Σ0 wird mit Σ ∪ Σ0 bezeichnet. Konstruktoren dienen der Synthese von Elementen einer S-sortigen Menge, Destruktoren liefern Werkzeuge zu ihrer Analyse. Die abstrakte Syntax einer kontextfreien Grammatik (siehe Kapitel 4) ist eine konstruktive Signatur, w¨ahrend Parser, Interpreter und Compiler auf Automatenmodellen beruhen, die destruktive Signaturen interpretieren. 30
Die syntaktische Beschreibung jedes mathematischen Modells, das auf induktiv definierten Mengen basiert, kann als konstruktive Signatur formuliert werden. Solchen Modellen stehen die zustandsorientierten gegenu¨ber, die Objekte nicht anhand ihres Aufbaus, sondern ausschließlich durch Beobachtung ihres Verhaltens voneinander unterscheiden. Dementsprechend werden aus den Operationssymbolen der jeweils zugrundeliegenden destruktiven Signatur keine Objekte, sondern Beobachtungsinstrumente zusammengesetzt. In den folgenden Beispielen steht hinter 1 die Tr¨agermenge der initialen bzw. finalen Algebra der jeweiligen Signatur (siehe 2.11 und 2.17). Unter I listen wir nur die nicht implizit in I enthaltenen (1, 2 und [n]; s.o.) auf. Seien X, Y, X1, . . . , Xn, Y1, . . . , Yn, E1, . . . , En beliebige Mengen und BS eine endliche Menge von Basismengen, die ∅ und 1 enth¨alt. 2.9 Konstruktive Signaturen • Mon 1 Unmarkierte bina¨re Ba¨ume (Monoide sind Mon-Algebren; siehe 2.11.) S = {mon},
I = ∅,
F = { one : 1 → mon, mul : mon × mon → mon }.
31
• Nat 1 N
S = {nat},
I = ∅,
F = { zero : 1 → nat, succ : nat → nat }.
• Lists(X, Y ) 1 X ∗ × I S = {list},
I = {X, Y },
F = { nil : Y → list, cons : X × list → list }.
• List(X) =def Lists(X, 1) 1 X ∗, alternativ: S = {list},
I = {X, N>1},
F = {[. . . ] : X ∗ → list}.
• Bintree(X) 1 bin¨are B¨aume endlicher Tiefe mit Knotenmarkierungen aus X S = {btree},
I = {X},
F = { empty : 1 → btree, bjoin : btree × X × btree → btree }.
32
• Tree(X) 1 B¨aume endlicher Tiefe und endlichen Knotenausgrads mit Knotenmarkierungen aus X S = {tree, trees},
I = {X}, F = { join : X × trees → tree, nil : 1 → trees, cons : tree × trees → trees }.
• Reg(BS) 1 regul¨are Ausdru¨cke u¨ber BS S = { reg }, I = {BS}, F = { par : reg × reg → reg, seq : reg × reg → reg, iter : reg → reg, base : BS → reg }.
(parallele Komposition) (sequentielle Komposition) (Iteration) (Einbettung der Basismengen)
• CCS(Act) 1 Calculus of Communicating Systems (kommunizierende Prozesse) S = { proc }, I = {Act}, F = { pre : Act → proc, cho : proc × proc → proc, par : proc × proc → proc, res : proc × Act → proc, rel : proc × ActAct → proc }.
(prefixing by an action) (choice) (parallelism) (restriction) (relabelling) 33
2.10 Destruktive Signaturen ∗
• DAut(X, Y ) 1 Y X = Verhalten deterministischer Moore-Automaten mit Eingabemenge X und Ausgabemenge Y S = { state }, (Zustandsmenge) I = { X, Y }, (Eingabemenge X und Ausgabemenge Y ) F = { δ : state → stateX , (Transitionsfunktion) β : state → Y }. (Ausgabefunktion) ∗ • Acc(X) =def DAut(X, 2) 1 P(X) ∼ = 2X = Verhalten deterministischer Akzeptoren von Sprachen u¨ber X
• Stream(X ) =def DAut(1, X) 1 X N S = {stream},
I = {X},
F = { head : stream → X, tail : stream → stream },
alternativ: S = {stream},
I = {X, N},
F = {get : stream → X N}.
• coList(X) 1 X ∗ ∪ X N S = {list},
I = {X},
F = {split : list → 1 + X × list}. 34
• Infbintree(X) 1 bin¨are B¨aume unendlicher Tiefe mit Knotenmarkierungen aus X S = {btree},
I = {X},
F = { root : btree → X, left, right : btree → btree }.
• coBintree(X) 1 bin¨are B¨aume beliebiger Tiefe mit Knotenmarkierungen aus X S = {btree},
I = {X},
F = {split : btree → 1 + btree × X × btree}.
• Inftree(X) 1 endlich verzweigende B¨aume unendlicher Tiefe mit Knotenmarkierungen aus X S = {tree},
I = {X, N>1},
F = { root : tree → X, subtrees : tree → tree+ }.
• FBtree(X) 1 endlich verzweigende B¨aume beliebiger Tiefe mit Knotenmarkierungen aus X S = {tree},
I = {X, N>1},
F = { root : tree → X, subtrees : tree → tree∗ }.
35
• coTree(X) 1 beliebig verzweigende B¨aume beliebiger Tiefe mit Knotenmarkierungen aus X S = { tree }, I = {X}, F = { root : tree → X, subtrees : tree → trees, split : trees → 1 + tree × trees }. ∗
• PAut(X, Y ) 1 (1 + Y )X = Verhalten partieller Moore-Automaten S = {state},
I = {X, Y },
F = { δ : state → (1 + state)X , β : state → Y }.
∗
• NAut(X, Y ) 1 (Y ∗)X = Verhalten nichtdeterministischer (bildendlicher) Moore-Automaten S = { state }, I = {X, Y, N>1}, F = { δ : state → (state∗)X , β : state → Y }. • SAut(X) 1 ([0, 1] × Y )∗ = Verhalten stochastischer Automaten ohne Eingabe S = { state }, I = {Y, [0, 1], N>1}, F = { δ : state → ([0, 1] × state)∗, β : state → Y }. 36
• Proctree(Act) 1 Prozessb¨aume, deren Kanten mit Aktionen markiert sind S = { state }, I = {Act, N>1}, F = { δ : tree → (Act × tree)∗ }. +
• Mealy(X, Y ) 1 Y X = Verhalten von Mealy-Automaten S = {state},
I = {X, Y },
F = { δ : state → stateX , β : state → Y X }.
+
Y X ist isomorph zur Menge der kausalen Stromfunktionen f : X ∗ → Y ∗. f heißt kausal, wenn fu¨r alle s, s0 ∈ AN and n ∈ N Folgendes gilt: take(n)(s) = take(n)(s0)
⇒
f (s)(n) = f (s0)(n).
• Class(I) 1 Verhalten von n Methoden einer Objektklasse [17] S = { state }, I = { X1, . . . , Xn, Y1, . . . , Yn, E1, . . . , En }, F = { mi : state → ((state × Yi) + Ei)Xi | 1 ≤ i ≤ n }.
37
Algebren Seien S und I wie oben. Eine T (S, I)-sortige Menge A heißt typvertr¨ aglich, wenn fu¨r alle I ∈ I, AI mit I u¨bereinstimmt und es fu¨r alle {ei}i∈I ⊆ T (S, I) Funktionstupel π = (πi : AQi∈I ei → Aei )i∈I und ι = (ιi : Aei → A`i∈I ei )i∈I gibt derart, dass (AQi∈I ei , π) ein Produkt und (A`i∈I ei , ι) eine Summe von (Aei )i∈I ist. Fu¨r alle e ∈ T (S, I) und a ∈ Ae nennen wir e den Typ von a. Das Typlifting einer S-sortigen Menge A ist Erweiterung von A zu einer typvertr¨aglichen T (S, I)-sortigen Menge, die entsteht, wenn man Indexmengen, Produkte und Summen wie folgt interpretiert: Fu¨r alle I ∈ I und {ei}i∈I ⊆ T (S, I), AI = I, AQi∈I ei = Xi∈I Aei , U A`i∈I ei = i∈I Aei . Aufgabe Sei A typvertr¨aglich. Zeigen Sie, dass fu¨r alle I ∈ I, n > 1 und e, e1, . . . , en ∈ T (S, I) Folgendes gilt: 38
Ae1×···×en Ae1+···+en AeI Aen Ae+ Ae∗
∼ = ∼ = ∼ = ∼ = ∼ = ∼ =
Ae1 × . . . × Aen , Ae1 + · · · + Aen , AIe , Ane, A+ e, A∗e . o
Seien A, B typvertra¨gliche T (S, I)-sortige Mengen. Eine T (S, I)-sortige Funktion h : A → B heißt typvertr¨ aglich, wenn fu¨r alle I ∈ I und {ei}i∈I ⊆ T (S, I) Folgendes gilt: • hI = idI , Q ` • hQi∈I ei = i∈I hei und h`i∈I ei = i∈I hei .
(1) (2)
Das Typlifting einer S-sortigen Funktion h : A → B ist die – ebenfalls mit h bezeichnete – Erweiterung von h zu einer typvertr¨aglichen T (S, I)-sortigen Funktion. Aufgabe Sei h typvertra¨glich. Zeigen Sie, dass fu¨r alle I ∈ I, n > 0 und e, e1, . . . , en ∈ T (S, I) Folgendes gilt: 39
he1×···×en he1+···+en heI hen he+ he∗
= = = = = =
he1 × . . . × hen , he1 + · · · + hen , hIe , [n] he , h+ e, h∗e . o
Sei Σ = (S, I, F ) eine Signatur. Eine Σ-Algebra A = (A, Op) besteht aus einer typvertr¨aglichen T (S, I)-sortigen Menge A und einer F -sortigen Menge Op = (f A : Ae → Ae0 )f :e→e0∈F von Funktionen, den Operationen von A. Fu¨r alle e ∈ T (S, I) heißt Ae Tr¨ agermenge (carrier set) oder Interpretation von e in A. Fu¨r alle f : e → e0 ∈ F heißt f A : Ae → Ae0 Interpretation von f in A. Im Fall |Ae| = 1 schreibt man f A anstelle von f A(a). H¨aufig wird auch die Vereinigung aller Tr¨agermengen von A mit A bezeichnet! AlgΣ bezeichnet die Klasse aller Σ-Algebren. Algebren destruktiver Signaturen werden auch Coalgebren genannt. 40
Seien A, B Σ-Algebren. Das Typlifting einer S-sortigen Funktion h : A → B heißt ΣHomomorphismus, wenn fu¨r alle f : e → e0 ∈ F he0 ◦ f A = f B ◦ he gilt. Ist h bijektiv, dann heißt h Σ-Isomorphismus und A und B sind Σ-isomorph. h induziert die Bildalgebra h(A): • Fu¨r alle e ∈ T (S, I), h(A)e =def he(Ae). • Fu¨r alle f : e → e0 ∈ F und a ∈ Ae, f h(A)(h(a)) =def f B (h(a)). Algebra-Beispiele Die Menge der natu¨rlichen Zahlen ist Tra¨germenge der Nat-Algebra NN = (A, Op = {zeroNN : 1 → N, succNN : N → N}) und auch der List(1)-Algebra NL = (B, Op = {nilNL : 1 → N, consNL : 1 × N → N}), die wie folgt definiert sind:
41
Anat = Blist = N und fu¨r alle n ∈ N, zeroNN succNN (n) nilNL consNL(n)
= = = =
0, n + 1, 0, n + 1.
Die Menge der Wo¨rter u¨ber einer Menge X ist Tra¨germenge der List(X)-Algebra SL(X ) = (A, Op = {nilSL : 1 → X ∗, consSL : X × X ∗ → X ∗}) und auch der Mon-Algebra SM (X ) = (B, Op = {oneSM (X ) : 1 → X ∗, mulSM (X ) : X ∗ × X ∗ → X ∗}), die wie folgt definiert sind: Alist = Bmon = X ∗ und fu¨r alle x ∈ X und v, w ∈ X ∗, nilSL(X ) consSL(X )(x, w) oneSM (X ) mulSM (X )(v, w)
= = = =
, xw, , v · w.
Die Menge X X der Funktionen von X nach X ist Tr¨agermenge der Mon-Algebra FM (X ) = (A, Op = {oneFM (X ) : 1 → X X , mulFM (X ) : X X × X X → X X }), 42
die wie folgt definiert ist: Amon = X X und fu¨r alle f, g : X → X, oneFM (X ) = idX , mulFM (X )(f, g) = g ◦ f. Eine Mon-Algebra A heißt Monoid, wenn mulA assoziativ und oneA ein links- und rechtsneutrales Element bzgl. mulA ist. Demnach sind SM(X) und FM(X) Monoide. Die folgende Stream(Z)-Algebra zo repr¨asentiert die Str¨ome 0, 1, 0, 1, . . . und 1, 0, 1, 0, . . . : zostream headzo(Blink ) tailzo(Blink ) headzo(Blink 0) tailzo(Blink 0)
= = = = =
{Blink , Blink 0}, 0, Blink 0, 1, Blink .
Die folgende Acc(Z)-Algebra eo dient der Erkennung der Parit¨at der Summe von Zahlenfolgen (siehe Beispiel 2.23) und ist wie folgt definiert: eostate δ eo(Esum) δ eo(Osum) β eo
= = = =
{Esum, Osum}, λx.if even(x) then Esum else Osum, λx.if odd(x) then Esum else Osum, λst.if st = esum then 1 else 0.
o 43
2.12 Terme und Coterme Sei Σ = (S, I, F ) eine Signatur, V eine S-sortige Menge, [ [ XΣ =def I ∪ {sel} und YΣ,V =def I ∪ V ∪ {tup}. Im Folgenden verwenden wir die im Abschnitt Mengen und Typen eingefu¨hrte Notation fu¨r deterministische B¨aume. Sei Σ konstruktiv. CTΣ(V ) bezeichnet die gr¨oßte T (S, I)-sortige Menge M von Teilmengen von dtr(XΣ, YΣ,V ) mit folgenden Eigenschaften: • Fu¨r alle I ∈ I, MI = I. (1) • Fu¨r alle s ∈ S und t ∈ Ms geh¨ort t zu Vs (2) oder gibt es c : e → s ∈ F und t0 ∈ Me mit t = c{sel → t0}. (3) • Fu¨r alle I ∈ I, {ei}i∈I ⊆ T (S, I), t ∈ MQi∈I ei und i ∈ I gibt es ti ∈ Mei mit t = tup{i → ti | i ∈ I}. (4) • Fu¨r alle I ∈ I, {ei}i∈I ⊆ T (S, I) und t ∈ M`i∈I ei gibt es i ∈ I und t0 ∈ Mei mit t = i{sel → t0}. (5)
44
(1)
(2/6)
(3/7)
(4)
(5)
Knoten und Kanten eines Σ-Terms. Neben jedem Knoten n steht der Typ von Termen mit Wurzel n. CTΣ(V ) ist typvertra¨glich. Beweis. Fu¨r all I ∈ I und {ei}i∈I ⊆ T (S, I) ist (CTΣ(V )Qi∈I , π) mit πi({tup → ti | i ∈ I}) =def ti und ti ∈ CTΣ(V )ei ein Produkt und (CTΣ(V )`i∈I , ι) mit ιi(t) =def i{sel → t} und t ∈ CTΣ(V )ei eine Summe von (CTΣ(V )i)i∈I . o Die Elemente von CTΣ(V ) heißen Σ-Terme u ¨ ber V . 45
Die Elemente von CTΣ =def CTΣ(∅) heißen Σ-Grundterme. Aufgabe Zeigen Sie, dass TΣ(V ) =def CTΣ(V ) ∩ wdtr(XΣ, YΣ,V ) die kleinste T (S, I)sortige Menge M von Teilmengen von dtr(XΣ, YΣ,V ) mit (1) und folgenden Eigenschaften ist: • Fu¨r alle s ∈ S, Vs ⊆ Ms. (6) • Fu¨r alle c : e → s ∈ F und t ∈ Me geh¨ort c{sel → t} zu Ms. (7) • Fu¨r alle I ∈ I, {ei}i∈I ⊆ T (S, I) und ti ∈ Mei , i ∈ I, geho¨rt tup{i → ti | i ∈ I} zu (8) MQi∈I ei . • Fu¨r alle I ∈ I, {ei}i∈I ⊆ T (S, I), i ∈ I und t ∈ Mei geh¨ort i{sel → t} zu M`i∈I ei . (9) TΣ(V ) und CTΣ(V ) sind die Tr¨agermengen von Σ-Algebren (s.u.). Daru¨berhinaus sind wohlfundierte Σ-Terme Bestandteile von Formeln wie z.B. den in Kapitel 18 iterativen Gleichungen wie (1) in Abschnitt 2.13.
46
Sei Σ destruktiv. DTΣ(V )bezeichnet die gr¨oßte T (S, I)-sortige Menge M von Teilmengen von dtr(XΣ, YΣ,V ) mit (1), (4), (5) und folgender Eigenschaft: • Fu¨r alle s ∈ S und t ∈ Ms gibt es x ∈ Vs und fu¨r alle d : s → e ∈ F gibt es td ∈ Me mit t = x{d → td | d : s → e ∈ F }. (10)
(1)
(10/11)
(4)
(5)
Knoten und Kanten eines Σ-Coterms. Neben jedem Knoten n steht der Typ von Cotermen mit Wurzel n. Die Elemente von DTΣ(V ) heißen Σ-Coterme u ¨ ber V . 47
Die Elemente von DTΣ =def DTΣ(1) heißen Σ-Grundcoterme. Aufgabe Zeigen Sie, dass coTΣ(V ) =def DTΣ(V ) ∩ wdtr(XΣ, YΣ,V ) die kleinste T (S, I)sortige Menge M von Teilmengen von dtr(XΣ, YΣ,V ) mit (1), (8), (9) und folgender Eigenschaft ist: • Fu¨r alle s ∈ S, x ∈ Vs, d : s → e ∈ F und td ∈ Me geh¨ort x{d → td | d : s → e ∈ F } zu Ms. (11) Demgegenu¨ber bezeichnet TΣ(V ) die kleinste T (S, I)-sortige Menge M von Teilmengen von dtr(XΣ, YΣ,V ) mit (1), (8), (9) und folgender Eigenschaft: • Fu¨r alle s ∈ S, d : s → e ∈ F und td ∈ Me geh¨ort {d → td | d : s → e ∈ F } zu Ms. (12) Wie im Fall einer konstruktiven Signatur werden die Elemente von TΣ(V ) (wohlfundierte) Σ-Terme u ¨ ber V genannt. coTΣ(V ) und DTΣ(V ) sind die Tr¨agermengen von Σ-Algebren (s.u.). Im Gegensatz zu Σ-Termen kommen Σ-Coterme in Formeln nicht vor. Stattdessen werden auch im Fall einer destruktiven Signatur nur wohlfundierte Σ-Terme in Formeln verwendet wie z.B. den Gleichungen (2) und (3) von Abschnitt 2.13.
48
Zur Vereinfachung der Wortdarstellung deterministischer Ba¨ume verwenden wir die folgenden Abku¨rzungen: Sei c ∈ YΣ,V und n > 1. c
steht fu¨r
c{sel → },
c(t)
steht fu¨r
c{sel → t},
c(t1, . . . , tn)
steht fu¨r
c{sel → tup{1 → t1, . . . , n → tn}},
c{. . .}
steht fu¨r
c{sel → tup{. . .}},
{. . .}
steht fu¨r
{. . .}.
2.13 Beispiele Sei Σ = Nat (siehe 2.9). CTΣ,nat ist die gr¨oßte Teilmenge M von dtr(XΣ, YΣ,V ) mit folgender Eigenschaft: • Fu¨r alle t ∈ M gilt t = zero oder gibt es u ∈ M mit t = succ(u). TΣ,nat ist die kleinste Teilmenge M von dtr(XΣ, YΣ,V ) mit folgenden Eigenschaften: • zero ∈ M . • Fu¨r alle t ∈ M , succ(t) ∈ M .
49
Sei Σ = List(X) (siehe 2.9). CTΣ,list ist die gr¨oßte Teilmenge M von dtr(XΣ, YΣ,V ) mit folgender Eigenschaft: • Fu¨r alle t ∈ M gilt t = nil oder gibt es x ∈ X und u ∈ M mit t = cons(x, u). TΣ,list ist die kleinste Teilmenge M von dtr(XΣ, YΣ,V ) mit folgenden Eigenschaften: • nil ∈ M . • Fu¨r alle x ∈ X und t ∈ M , cons(x, t) ∈ M . Sei V = {blink, blink 0}. Die folgenden iterativen Gleichungen zwischen List(Z)-Termen u¨ber V haben eine eindeutige L¨osung in CTList(Z) (siehe Kapitel 18): blink = cons(0, blink 0), blink 0 = cons(1, blink).
(1)
Deshalb definiert (1) blink und blink 0 als zwei Elemente von CTList(Z). Als eindeutige L¨osungen iterativer Gleichungen repr¨asentierbare unendliche Terme heißen rational. Sei Σ = Reg(BS) (siehe 2.9). TΣ,reg ist die kleinste Teilmenge M von dtr(XΣ, YΣ,V ) mit folgenden Eigenschaften: • Fu¨r alle t, u ∈ M , par(t, u), seq(t, u) ∈ M . • Fu¨r alle t ∈ M , iter(t) ∈ M . 50
• Fu¨r alle B ∈ BS, base(B) ∈ M . Sei Σ = Stream(X) (siehe 2.10). DTΣ,stream ist die gro¨ßte Teilmenge M von dtr(XΣ, YΣ,V ) mit folgender Eigenschaft: • Fu¨r alle t ∈ M gibt es x ∈ X und t0 ∈ M mit t = {head → x, tail → t0} ∈ M . ε head
tail
0
ε tail
head
1
ε head
2
tail
ε
Stream(N)-Coterm, der den Strom aller natu ¨rlichen Zahlen darstellt
Sei V = {blink, blink 0}. Da zo eine Stream(Z)-Algebra (siehe 2.11) und DTStream(Z) eine finale Stream(Z)-Algebra ist (s.u.), l¨osen die Coterme unfold zo(Blink ) und unfold zo(Blink 0) die folgenden Gleichungen zwischen Stream(Z)-Cotermen u¨ber V eindeutig in blink bzw. blink 0: 51
blink = {head → 0, tail → blink 0}, blink 0 = {head → 1, tail → blink}
(2)
(siehe Kapitel 18). Deshalb definiert (2) blink und blink 0 als zwei Elemente von DTStream(Z). Als eindeutige L¨osungen iterativer Gleichungen repr¨asentierbare unendliche Coterme heißen rational. Sei Σ = Colist(X) (siehe 2.10). DTΣ,list ist die gr¨oßte Teilmenge M von dtr(XΣ, YΣ,V ) mit folgender Eigenschaft: • Fu¨r alle t ∈ M gilt t = {split → 1} oder gibt es x ∈ X und u ∈ M mit t = {split → 2{1 → x, 2 → u}}.
Sei Σ = DAut(X, Y ) (siehe 2.10). DTΣ,state ist die gr¨oßte Teilmenge M von dtr(XΣ, YΣ,V ) mit folgender Eigenschaft: • Fu¨r alle t ∈ M und x ∈ X gibt es tx ∈ M und y ∈ Y mit t = {δ → tup{x → tx | x ∈ X}, β → y}.
52
ε
β
0
δ 1
β
ε
x
y ε
0
tup
x
z
ε
y
δ ε
tup
β
z
δ tup
ε δ
ε
ε
x
1
β
tup
x z
ε
ε
z
ε
y ε
y ε
Acc({x, y, z})-Coterm, der einen Akzeptor der Sprache {w ∈ {x, y, z}∗ | w enth¨alt x oder z} darstellt
Sei V = {esum, osum}. Da eo eine Acc(Z)-Algebra (siehe 2.11) und DTAcc(Z) eine finale Acc(Z)-Algebra ist (s.u.), l¨osen die Coterme unfold eo(Esum) und unfold eo(Osum) die folgenden iterativen Gleichungen zwischen Acc(Z)-Cotermen u¨ber V eindeutig in esum bzw. esum:
53
esum = {δ → tup({x → esum | x ∈ even} ∪ {x → osum | x ∈ odd}), β → 1}, osum = {δ → tup{x → osum | x ∈ even} ∪ {x → esum | x ∈ odd}), β → 0}. even und odd bezeichnen die Mengen der geraden bzw. ungeraden ganzen Zahlen.
(3) o
CTΣ(V ) und DTΣ(V ) sind Σ-Algebren Sei Σ = (S, I, C) eine konstruktive Signatur. CTΣ(V ) wird wie folgt zur Σ-Algebra erweitert: • Fu¨r alle c : e → s ∈ C, t ∈ CTΣ(V )e, cCTΣ(V )(t) =def c{sel → t}. • Fu¨r alle I ∈ I, ti ∈ CTΣ(V )ei , i ∈ I, and k ∈ I, πk (tup{i → ti | i ∈ I}) =def tk . • Fu¨r alle I ∈ I, i ∈ I and t ∈ CTΣ(V )ei , ιi(t) =def i{sel → t}. Sei Σ = (S, I, D) eine destruktive Signatur. DTΣ(V ) wird wie folgt zur Σ-Algebra erweitert: • Fu¨r alle s ∈ S, x ∈ Vs and td ∈ DTΣ(V )e, d : s → e ∈ D, and d0 : s → e0, d0DTΣ(V )(x{d → td | d : s → e ∈ D}) =def td0 . 54
• Fu¨r alle I ∈ I, ti ∈ DTΣ(V )ei , i ∈ I, and k ∈ I, πk (tup{i → ti | i ∈ I}) =def tk . • Fu¨r alle I ∈ I, i ∈ I and t ∈ DTΣ(V )ei , ιi(t) =def i{sel → t}. Die Interpretation von Destruktoren in DTΣ(V ) machen Coterme zu eier Art analytischer Funktionen: Zwei Coterme t, t0 ∈ DTΣ(V )s sind genau dann gleich, wenn die “Anfangswerte” t() und t0() und fu¨r alle d : s → e die “Ableitungen” dDTΣ(V )(t) und dDTΣ(V )(t0) miteinander u¨bereinstimmen. Die atomaren Formeln der Pr¨adikatenlogik sind aus Σ-Termen und Pr¨adikaten (= Relationssymbolen) zusammengesetzt. Prinzipiell kommt man dort mit einer einzigen Sorte aus, muss dann aber die Trennung zwischen mehreren Datenbereichen durch die Einfu¨hrung eines einstelligen Pr¨adikats fu¨r jeden Datenbereich wiedergeben. So entspricht z.B. die Sorte nat der Signatur Nat (siehe 2.9) das Pr¨adikat isNat mit den Axiomen isNat(zero), isNat(x) ⇒ isNat(succ(x)).
(1) (2)
Im Rahmen einer Nat umfassenden Signatur Σ wa¨re ein Σ-Term t genau dann ein NatGrundterm des Typs nat, wenn isNat(t) mit Inferenzregeln der Pr¨adikatenlogik aus (1) und (2) ableitbar ist. 55
2.14 Die Algebren Bool und Regword (BS) (siehe 2.9) Die Menge 2 = {0, 1} ist Tr¨agermenge der Reg(BS)-Algebra Bool : Fu¨r alle x, y ∈ 2 und B ∈ BS \ 1, parBool (x, y) seq Bool (x, y) iterBool (x) baseBool (1) baseBool (B)
= = = = =
max{x, y}, x ∗ y, 1, 1, 0.
Die u¨blichen Wortdarstellungen regul¨arer Ausdru¨cke e wie z.B. aab∗ + c(aN)∗ bilden die Reg(BS)-Algebra Regword (BS): Sei syms(BS) = {+,∗ , (, )} ∪ {B | B ∈ BS}. Im Fall |B| = 1 setzen wir B mit dem einen Element von B gleich. Ob ein Teilausdruck e geklammert werden muss oder nicht, h¨angt von der Priorit¨at des Operationssymbols f ab, zu dessen Domain e geh¨ort. Die Tr¨agermenge von Regword (BS) besteht deshalb aus Funktionen, die, abh¨angig von der Priorit¨at von f , die Wortdarstellung von e mit oder ohne Klammern zuru¨ckgibt: Regword (BS)reg = N → syms(BS)∗. 56
Aus den Priorita¨ten 0,1,2 von par, seq bzw. iter ergeben sich folgende Interpretation der Operationssymbole von Reg(BS): Fu¨r alle f, g : N → syms(BS)∗, B ∈ BS und w ∈ syms(BS)∗, parRegword (BS)(f, g) seq Regword (BS)(f, g) iterRegword (BS)(f ) baseRegword (BS)(B) enclose(True)(w) enclose(False)(w)
= = = = = =
λn.enclose(n > 0)(f (0) + g(0)), λn.enclose(n > 1)(f (1) g(1)), λn.enclose(n > 2)(f (2)∗), λn.B, (w), w.
Ist die Funktion f : N → syms(BS)∗ das Ergebnis der Faltung eines Reg(BS)-Terms t in Regword (BS) (s.u.), dann liefert f (0) eine Wortdarstellung von t, die keine u¨berflu¨ssigen Klammern enth¨alt. Regword(String) ist im Haskell-Modul Compiler.hs durch regWord implementiert.
o
2.15 Die Algebren Beh(X, Y ), Pow (X), Lang(X) und Bro(BS) (siehe 2.10) Seien X und Y Mengen.
57
Funktionen von X ∗ nach Y nennen wir Verhaltensfunktionen (behavior functions). Sie bilden die Tr¨agermenge folgender DAut(X, Y )-Algebra Beh(X, Y ): ∗
Beh(X, Y )state = Y X . Fu¨r alle f : X ∗ → Y , x ∈ X und w ∈ X ∗, δ Beh(X,Y )(f )(x)(w) = f (xw) und β Beh(X,Y )(f ) = f (). Beh(X, 2) ist im Haskell-Modul Compiler.hs durch behFun implementiert. ∗
Eine zu Beh(X, 2)state = 2X bijektive Menge ist die Potenzmenge P(X ∗) (siehe Mengen und Typen). Daraus ergibt sich die Acc(X)-Algebra Pow (X) mit Pow (X)state = P(X ∗). Fu¨r alle L ⊆ X ∗ und x ∈ X, ( δ Pow (X)(L)(x) = {w ∈ X ∗ | xw ∈ L} und β Pow (X)(L) =
1 falls ∈ L, 0 sonst.
58
∗
Aufgabe Zeigen Sie, dass die Funktion χ : P(X ∗) → 2X , die jeder Teilmenge von X ∗ ihre charakteristische Funktion zuordnet (siehe Mengen und Typen), ein Acc(X)-Homomorphismus von Pow (X) nach Beh(X, 2) ist. o Sei BS eine endliche Menge von Basismengen, die ∅ und 1 enth¨alt, und X =
S
BS \ 1.
P(X ∗) ist nicht nur die Tr¨agermenge der Acc(X)-Algebra Pow (X), sondern auch der folgendermaßen definierten Reg(BS)-Algebra Lang(X) der Sprachen u¨ber X: Lang(X)reg = P(X ∗). Fu¨r alle B ∈ BS und L, L0 ⊆ X ∗, parLang(X)(L, L0) seq Lang(X)(L, L0) iterLang(X)(L) baseLang(X)(B)
= = = =
L ∪ L0 , L · L0 , L∗, B.
Anstelle von Lang(X) wird in Compiler.hs die Reg(BS)-Algebra regB mit der Tr¨agermen∗ ge 2X implementiert. Sie macht χ zum Reg(BS)-Homomorphismus. Aufgabe Zeigen Sie, dass χ ein Reg(BS)-Homomorphismus von Lang(X) nach regB ist. o 59
Die Menge der Reg(BS)-Grundterme ist nicht nur eine Tr¨agermenge der Reg(BS)-Algebra TReg(BS), sondern auch der wie folgt definierten Acc(X)-Algebra Bro(BS) (accT in Compiler.hs; siehe [2, 15]), die Brzozowski-Automat genannt wird: Bro(BS)state = TReg(BS),reg . Die Interpretationen von δ und β in Bro(BS) werden induktiv u¨ber dem Aufbau von Reg(BS)-Grundtermen definiert: Fu¨r alle t, u ∈ TReg(BS) und B ∈ BS \ 1, δ Bro(BS)(par(t, u)) = λx.par(δ Bro(BS)(t)(x), δ Bro(BS)(u)(x)), δ Bro(BS)(seq(t, u)) = λx.par(seq(δ Bro(BS)(t)(x), u), if β Bro(BS)(t) = 1 then δ Bro(BS)(u)(x) else reg(∅)), δ Bro(BS)(iter(t)) = λx.seq(δ Bro(BS)(t)(x), iter(t)), δ Bro(BS)(base(1)) = base(∅), δ Bro(BS)(base(B)) = λx.if x ∈ B then base(1) else base(∅), β Bro(BS)(par(t, u)) = max{β Bro(BS)(t), β Bro(BS)(u)}, β Bro(BS)(seq(t, u)) = β Bro(BS)(t) ∗ β Bro(BS)(u), β Bro(BS)(iter(t)) = 1, β Bro(BS)(base(1)) = 1, β Bro(BS)(base(B)) = 0. 60
2.16 Die Erreichbarkeitsfunktion Sei A = (A, Op) eine DAut(X, Y )-Algebra und Z = Astate. Die Erreichbarkeitsfunktion reachA : X ∗ → Z Z von A ist wie folgt induktiv definiert: Fu¨r alle x ∈ X und w ∈ X ∗, reachA() = idA, reachA(xw) = reachA(w) ◦ λa.δ A(a)(x). Der Definitionsbereich X ∗ von reachA ist Tr¨agermenge der Mon-Algebra SM(X), der Wertebereich Z Z ist Tr¨agermenge der Mon-Algebra FM(Z) (siehe 2.11). reachA ist Mon-homomorph: reachA(oneSM (X )) = reachA() = idA = oneFM (Z ). Fu¨r alle x ∈ X und v, w ∈ X ∗, reachA(mulSM (X )(, w)) = reachA(w) = reachA(w) = reachA(w) ◦ idA = reachA(w) ◦ reachA() = mulFM (Z )(reachA(), reachA(w)), reachA(mulSM (X )(xv, w)) = reachA(xvw) = reachA(x(mulSM (X )(v, w))) = reachA(mulSM (X )(v, w)) ◦ λa.δ A(a)(x) ind. hyp.
=
(mulFM (Z )(reachA(v), reachA(w)) ◦ λa.δ A(a)(x) 61
= (reachA(w) ◦ reachA(v)) ◦ λa.δ A(a)(x) = reachA(w) ◦ (reachA(v) ◦ λa.δ A(a)(x)) = reachA(w) ◦ reachA(xv) = mulFM (Z )(reachA(xv), reachA(w)). o 2.17 Termfaltung und Zustandsentfaltung Sei Σ = (S, I, C) eine konstruktive Signatur, A = (A, Op) eine Σ-Algebra, V eine S-sortige Menge von “Variablen” und g : V → A eine – Variablenbelegung (valuation) genannte – S-sortige Funktion. In Abh¨angigkeit von g wertet die wie folgt induktiv definierte T (S, I)-sortige Funktion g ∗ : TΣ(V ) → A, die Extension von g, wohlfundierte Σ-Terme u¨ber V in A aus: • Fu¨r alle • Fu¨r alle • Fu¨r alle • Fu¨r alle ∗ πk (gQ
i∈I
I ∈ I, gI∗ = idI . s ∈ S und x ∈ Vs, gs∗(x) = gs(x). c : e → s ∈ F und t ∈ TΣ(V )e, gs∗(c{sel → t}) = cA(ge∗(t)). I ∈ I und {ei}i∈I ⊆ T (S, I), ti ∈ TΣ(V )ei , i ∈ I, und k ∈ I, ∗ ei ({tup → ti | i ∈ I})) = gek (tk ).
• Fu¨r alle I ∈ I, {ei}i∈I ⊆ T (S, I), k ∈ I und t ∈ TΣ(V )ek , ∗ ∗ g` ei (k{sel → t}) = ιk (gek (t)). i∈I
(1) (2) (3) (4) (5) 62
Satz 2.18 ([32], Theorem FREE) g ∗ ist Σ-homomorph und der einzige Σ-Homomorphismus von TΣ(V ) nach A ist, der (2) erfu¨llt. Offenbar h¨angt die Einschr¨ankung von g ∗ auf Grundterme nicht von g ab. Sie wird Termfaltung genannt und mit fold A bezeichnet. Umgekehrt stimmt g ∗ mit der Termfaltung fold A(g) : TΣ0 → A(g) u¨berein, wobei Σ0 =def (S, I ∪ {Vs | s ∈ S}, C ∪ {vars : Vs → s | s ∈ S}) A(g)
und A(g) ∈ AlgΣ0 definiert ist durch A(g)|Σ = A und vars
= g fu¨r alle s ∈ S.
Aus Satz 2.18 folgt sofort: fold A ist der einzige Σ-Homomorphismus von TΣ nach A.
(6)
Wegen (6) nennt man TΣ eine initiale Σ-Algebra. Wie die Produkt- oder Summeneigenschaft ist auch Initialit¨at eine universelle Eigenschaft (vgl. Satz 2.2 bzw. 2.7): Alle initialen Σ-Algebren sind Σ-isomorph und jede zu einer initialen Σ-Algebra isomorphe Σ-Algebra ist initial. TΣ wird deshalb auch die initiale Σ-Algebra genannt. 63
Z.B. ist neben TNat auch NN eine initiale Nat-Algebra und neben TList(X) auch SL(X ) eine initiale List(X)-Algebra (siehe 2.11). Aufgabe Wie lauten die Isomorphismen von TNat nach NN bzw. von TList(X) nach SL? o Die Faltung fold Lang(X)(t) eines Reg(BS)-Grundterms – also eines regul¨aren Ausdrucks – t in Lang(X) heißt Sprache von t (siehe 2.15). Umgekehrt nennt man L ⊆ X ∗ eine regul¨ are Sprache, wenn L zum Bild von fold Lang(X) geh¨ort. Die Haskell-Funktion foldReg von Compiler.hs implementiert die Faltung fold A : TReg(BS) → A in einer beliebigen Reg(BS)-Algebra A. Aufgabe Zeigen Sie fold Bool = β Bro(BS).
o
Aufgabe Zeigen Sie durch Induktion u¨ber den Aufbau von Reg(BS)-Grundtermen, dass ¨ fu¨r alle t ∈ TReg(BS) die folgende Aquivalenz gilt: ∈ fold Lang(X)(t)
⇔
fold Bool (t) = 1.
o 64
Sei Σ = (S, I, D) eine destruktive Signatur, A = (A, Op) eine Σ-Algebra, V eine S-sortige Menge von “Farben” und g : A → V eine – F¨ arbung (coloring) genannte – S-sortige Funktion. In Abh¨angigkeit von g berechnet die wie folgt definierte T (S, I)-sortige Funktion g # : A → DTΣ(V ), die Coextension von g, zu jedem Zustand a ∈ A das Verhalten von a in Gestalt eines Σ-Coterms u¨ber V : • Fu¨r alle I ∈ I, gI# = idI . • Fu¨r alle s ∈ S und a ∈ As, gs#(a) = gs(a){d → ge#(dA(a)) | d : s → e ∈ D}. • Fu¨r alle I ∈ I, (ei)i∈I ∈ T (S, I) und a ∈ AQi∈I ei , # # gQ ei (a) = tup{i → gei (πi (a)) | i ∈ I}. i∈I
• Fu¨r alle I ∈ I, {ei}i∈I ⊆ T (S, I), k ∈ I und a ∈ Aek , # # g` ei (ιk (a)) = k{sel → gek (a)}. i∈I
(1) (2) (3) (4)
Nicht g # selbst, wohl aber jedes einzelne Bild g #(a) : XΣ∗ (→ YΣ,V von g # ist induktiv definiert. So ist z.B. (2) eine Kurzform fu¨r: 65
falls w = , gs(a) gs#(a)(w) = ge#(dA(a))(w0) falls ∃ d : s → e ∈ D, w0 ∈ XΣ∗ : w = dw0, undefiniert sonst. Satz 2.19 ([32], Theorem COFREE) g # ist Σ-homomorph und der einzige Σ-Homomorphismus von A nach DTΣ(V ) ist, der fu¨r alle a ∈ A g #(a)() = g(a) erfu¨llt. Offenbar h¨angt die Einschr¨ankung von g # auf Grundcoterme nicht von g ab. Sie wird Zustandsentfaltung genannt und mit unfold A bezeichnet. Umgekehrt stimmt g # mit der Zustandsentfaltung unfold A(g) : A(g) → DTΣ0 u¨berein, wobei Σ0 =def (S, I ∪ {Vs | s ∈ S}, D ∪ {vars : s → Vs | s ∈ S}) A(g)
und A(g) ∈ AlgΣ0 definiert ist durch A(g)|Σ = A und vars
= g fu¨r alle s ∈ S.
Aus Satz 2.19 folgt sofort: unfold A ist der einzige Σ-Homomorphismus von A nach DTΣ.
(5)
Wegen (5) nennt man DTΣ eine finale oder terminale Σ-Algebra. 66
Wie Initialita¨t ist auch Finalita¨t eine universelle Eigenschaft: Alle finalen Σ-Algebren sind Σ-isomorph und jede zu einer finalen Σ-Algebra isomorphe Σ-Algebra ist final. DTΣ wird deshalb auch die finale Σ-Algebra genannt. Z.B. ist neben DTStream(X) auch StreamFun(X ) eine finale Stream(X)-Algebra (siehe 17.5), neben DTDAut(X,Y ) auch Beh(X, Y ) eine finale DAut(X, Y )-Algebra und neben DTAcc(X) auch Pow (X) eine finale Acc(X)-Algebra (siehe 2.15). Beispiel 2.20 Sei Σ = DAut(X, Y ). Die Tr¨agermengen von DTΣ und Beh(X, Y ) sind isomorph: Sei L = {(δ, x) | x ∈ X}. DTΣ besteht aus allen Funktionen von L∗ + L∗β nach 1 + Y , die fu¨r alle w ∈ L∗ w auf und wβ auf ein Element von Y abbilden, m.a.W.: DTΣ ∼ = 1
L∗
×Y
L∗ β
∼ = Y
L∗ β
L∗ β ∼ =X ∗
∼ =
∗
YX .
ξ : Beh(X, Y ) → DTΣ bezeichne den entsprechenden DAut(X, Y )-Isomorphismus.
o
Aufgabe Wie lautet der Isomorphismus zwischen DTAcc(X) und Pow (X)?
o
67
Die Acc(X)-Algebra ist DTAcc(X) ist im Haskell-Modul Compiler.hs durch accC implementiert. Coterme kann man als verallgemeinerte Verhaltensfunktionen betrachten. Auch der Realisierungsbegriff von Abschnitt 2.11 l¨asst sich von Beh(X, Y ) auf beliebige destruktive Signaturen u¨bertragen: Fu¨r alle Σ-Algebren, s ∈ S und a ∈ As, (A, a) realisiert t ∈ DTΣ,s ⇔def
unfold A s (a) = t.
Aufgabe Zeigen Sie, dass χ : P(X) → 2X ein Acc(X)-Homomorphismus von Pow (X) nach Beh(X, 2) ist. o Sei A = (A, Op) eine Acc(X)-Algebra. Da Pow (X) final ist, gibt es genau einen Acc(X)Homomorphismus unfoldP A : A → Pow (X).
68
¨ Daraus ergeben sich folgende Aquivalenzen: fold Lang(X) ist Acc(X)-homomorph ⇔ fold Lang(X) = unfoldP Bro(BS) : TReg(BS) → P(X ∗)
(1) (2)
⇔ unfoldP Bro(BS) ist Reg(BS)-homomorph.
(3)
Aufgabe Zeigen Sie (2), indem Sie (1) oder (3) beweisen.
o
(2) folgt auch aus der Form der Gleichungen, die Bro(BS) definieren (siehe Beispiel 17.10). Sei A = (A, Op) eine DAut(X, Y )-Algebra. Da Beh(X, Y ) final ist, gibt es genau einen DAut(X, Y )-Homomorphismus unfoldB A : A → Beh(X, Y ). unfoldB A ordnet jedem Zustand a ∈ Astate eine Verhaltensfunktion zu, die fu¨r jedes Eingabewort w ∈ X ∗ die Ausgabe desjenigen Zustandes zuru¨ckgibt, den A nach Verarbeitung von w erreicht hat: runA (a) βA unfoldB A(a) = X ∗ −→ Astate −→ Y. ∗
A X runA : Astate → AX ¨rter fort: state setzt die Transitionsfunktion δ : Astate → Astate auf Wo 69
Fu¨r alle a ∈ Astate, x ∈ X und w ∈ X ∗, runA(a)() =def a, runA(a)(xw) =def runA(δ A(a)(x))(w).
(4) (5)
runA ist die Erreichbarkeitsfunktion von 2.16 mit vertauschten Argumenten: runA(a)(w) = reachA(w)(a). Außerdem gilt fu¨r alle v, w ∈ X ∗: runA(a)(vw) = runA(runA(a)(v))(w).
(6)
(4) und (6) machen (die dekaskadierte Version von) runA zur Aktion des Monoids X ∗: Fu¨r eine beliebige Zustandsmenge Q und ein beliebiges Monoid M mit Multiplikation ∗ und neutralem Element e heißt eine Funktion (·) : Q × M → Q Aktion von M , wenn fu¨r alle q ∈ Q und m, m0 ∈ M Folgendes gilt: q · e = q, q · (m ∗ m0) = (q · m) · m0.
(7) (8)
Aufgabe Sei h der Isomorphismus von DTDAut(X,Y ) nach Beh(X, Y ). Zeigen Sie: runA = h ◦ id# A.
o
(9) 70
Initiale Automaten Sei a ∈ Astate. Man nennt das Paar (A, a) einen initialen Automaten, der die Verhaltensfunktion unfoldB A(a) : X ∗ → Y realisiert (siehe 2.15). Sei L ⊆ X ∗ und Y = 2. (A, a) erkennt oder akzeptiert L, wenn (A, a) die charakteristische Funktion χ(L) : X ∗ → 2 von L realisiert. ∗
Da χ : P(X ∗) → 2X Acc(X)-homomorph ist (s.o.) und Beh(X, 2) eine finale Acc(X)Algebra, stimmt unfoldB A mit χ ◦ unfoldP A u¨berein. Folglich wird L ⊆ X ∗ genau dann von (A, a) erkannt, wenn L mit unfoldP A(a) u¨bereinstimmt: unfoldP A(a) = L ⇔ χ(unfoldP A(a)) = χ(L) ⇔ unfoldB A(a) = χ(L) ⇔ (A, a) erkennt L. (6) Insbesondere gilt fu¨r jeden regul¨aren Ausdruck t ∈ TReg(BS), dass der initiale Automat (Bro(BS), t) die Sprache von t erkennt: (Bro(BS), t) erkennt fold Lang(X)(t) (6)
(2)
⇔ unfoldP Bro (BS)(t) = fold Lang(X)(t) ⇔ fold Lang(X)(t) = fold Lang(X)(t).
71
Damit erfu¨llt (Bro(BS), t) dieselbe Aufgabe wie der klassische Potenzautomat zur Erkennung der Sprache von t, der u¨ber den Umweg eines nichtdeterministischen Automaten mit ¨ -Uberg ¨angen aus t gebildet wird (siehe Beispiel 12.3). ¨ Ubersicht u¨ber die oben definierten Reg(BS)- bzw. DAut(X, Y )-Algebren und ihre jeweiligen Implementierungen in Compiler.hs:
72
Signatur
Reg(BS)
Acc(X)
TReg(BS) RegT
TReg(BS) regT initial
Bro(BS) accT
P(X ∗)
Lang(X)
Tr¨agermenge
2X
∗
YX
2
Algebra
χ(Lang(X)) regB
Pow (X) final χ(Pow (X)) Beh(X, 2) behFun final Beh(X, Y ) final
∗
N → syms(BS)∗
DAut(X, Y )
Regword (BS) regWord Bool
73
2.21 Compiler fu are Ausdru ¨ r regul¨ ¨ cke Im Folgenden werden wir einen Parser fu¨r die Wortdarstellung eines regul¨aren Ausdrucks t mit dessen Faltung in einer beliebigen Reg(BS)-Algebra A verknu¨pfen und damit ein erstes Beispiel fu¨r einen Compiler erhalten, der die Elemente einer Wortmenge ohne den Umweg u¨ber Reg(BS)-Terme nach A – u¨bersetzt. Werden regul¨are Ausdru¨cke als W¨orter syms(BS) (siehe 2.14) eingelesen, dann muss dem Erkenner fold χ(Lang(X))(t) eine Funktion parseREG : syms(BS)∗ → M (TReg(BS)) vorgeschaltet werden, die jedes korrekte Eingabewort w in einen oder mehrere Reg(BS)Terme t mit fold Regword (BS)(t)(0) = w u¨berfu¨hrt. M ist ein monadischer Funktor (siehe 5.1), der die Ausgabe des Parsers steuert und insbesondere Fehlermeldungen erzeugt, falls w keinem Reg(BS)-Term entspricht. REG steht hier fu¨r eine konkrete Syntax, d.h. eine kontextfreie Grammatik, deren Sprache mit dem Bild von TReg(BS) unter flip(fold Regword (BS))(0) u¨bereinstimmt (siehe Beispiel 4.1). Sei X eine Menge, G eine kontextfreie Grammatik mit abstrakter Syntax Σ und Sprache L ⊆ X ∗. In Kapitel 5 werden wir einen generischen Compiler fu¨r L, der jedes Wort von L in Elemente einer Σ-Algebra A u¨bersetzt, als natu ¨rliche Transformation compileG des konstanten Funktors const(X ∗) nach M M formulieren. 74
parseG ist diejenige Instanz von compileG, die W¨orter von L in Syntaxb¨aume (= ΣT Grundterme) u¨bersetzt: parseG = compileGΣ . Im Fall G = REG, Σ = Reg(BS), X = syms(BS) und M (A) = A+1 fu¨r alle Σ-Algebren A stimmt compileA aren Ausdrucks t G (w) mit der Faltung des durch w dargestellten regul¨ in der Reg(BS)-Algebra A u¨berein: compile
ist nat. Transformation
T
G compileA = M (fold A)(compileGReg(BS) (w)) G (w) = M (fold A)(parseG(w)) = (fold A + id1)(parseG(w)) = (fold A + id1)(parseG(fold Regword (BS)(t)(0))) = (fold A + id1)(t) = fold A(t).
Im Haskell-Modul Compiler.hs ist compileREG durch die Funktion regToAlg implementiert, deren Zahlparameter eine von 8 Zielalgebren ausw¨ahlt.
75
Im folgenden Diagramm sind die wichtigsten Beziehungen zwischen den behandelten Algebren und Homomorphismen zusammengefasst: parseREG 1 + fold Lang(X) 1+χ 1 + Lang(X) 1 + χ(Lang(X)) syms(BS) 1 + TReg(BS) ≺ f f f = = inc = inc inc Regword (BS) π1 ◦ fold +
∪
∪
Bool≺≺
fold
Bool
= β
Bro(BS)
TReg(BS) w w w w w w w w w
fold
Lang(X)
=
Bro(BS) unfold δ Bro(BS) g Bro(BS)X
Bro(BS)
Lang(X) w w w w w w w w w Pow (X) δ Pow (X) g Pow (X)X
∪
χ(Lang(X)) w w w w w w = w w w χ
χ
Beh(X, 2) δ Beh(X,2) g Beh(X, 2)X
76
2.22 Minimale Automaten Wie zeigt man, dass initiale Automaten bestimmte Verhaltensfunktionen realisieren bzw. Sprachen erkennen? Sei A = (A, Op) eine Acc(X)-Algebra, und f : A → P(X ∗). Da Pow (X) eine finale Acc(X)-Algebra ist (s.o.), erkennt fu¨r alle a ∈ Astate der initiale Automat (A, a) genau dann die Sprache f (a), wenn f Acc(X)-homomorph ist. Beispiel 2.23 Sei Pn L = {(x1, . . . , xn) ∈ Z | i=1 xi ist gerade}, P n L0 = {(x1, . . . , xn) ∈ Z∗ | i=1 xi ist ungerade}. ∗
Die Funktion h : eo → Pow (X) (siehe 2.11) mit h(Esum) = L und h(Osum) = L0 ist Acc(Z)-homomorph. Also wird L vom initialen Automaten (eo, Esum) und L0 vom initialen Automaten (eo, Osum) erkannt. o Sei (A, a) ein initialer Automat. Die Elemente der Menge hai =def runA(a)(X ∗) heißen Folgezust¨ ande von a in A. 77
Satz 2.24 Sei A = (A, Op) eine DAut(X, Y )-Algebra. (i) Fu¨r alle a ∈ A ist hai die (Tr¨agermenge der) kleinste(n) DAut(X, Y )-Unteralgebra von A (siehe Kapitel 3), die a enth¨alt. (ii) Fu¨r alle Σ-Homomorphismen h : A → B gilt h(hai) = hh(a)i. (iii) Fu¨r alle f : X ∗ → Y ist (hf i, f ) eine minimale Realisierung von f . Beweis. (i): Wir zeigen zun¨achst durch Induktion u¨ber |w|, dass fu¨r alle a ∈ A, x ∈ X und w ∈ X ∗ Folgendes gilt: runA(a)(wx) = δ A(runA(a)(w))(x). (5)
(7) (4)
runA(a)(x) = runA(a)(x) = runA(δ A(a)(x))() = δ A(a)(x). Fu¨r alle y ∈ X, (5)
runA(a)(ywx) = runA(δ A(a)(y))(wx)
ind. hyp.
=
δ A(runA(δ A(a)(y))(w))(x)
(5)
= δ A(runA(yw))(x)
Wegen (7) gilt δ A(b)(x) ∈ hai fu¨r alle b ∈ hai und x ∈ X. Also ist hai eine Unteralgebra von A. Sei B eine Unteralgebra von A, die a enth¨alt. Durch Induktion u¨ber |w| erh¨alt man aus (4) und (5), dass runA(a)(w) fu¨r alle w ∈ X ∗ zu B geh¨ort. Also ist hai die kleinste Unteralgebra von A, die a enth¨alt. 78
(ii): Da h Σ-homomorph ist, ist h auch mit run vertr¨aglich (s.o.), d.h. fu¨r alle w ∈ X ∗ gilt h(runA(a)(w)) = runB (h(a))(w). Daraus folgt sowohl h(hai) ⊆ hh(a)i als auch hh(a)i ⊆ h(hai). ∗
(iii): Da Beh(X, Y ) final ist, stimmt unfold B Beh(X,Y ) (s.o.) mit der Identit¨at auf Y X u¨berein. Also ist unfold B Beh(X,Y )(f ) = f und damit (hf i, f ) wegen (i) ein initialer Automat, der f realisiert. Sei (A = (A, Op), a) ein initialer Automat, der f realisiert. Wegen (ii) ist h : hai → hunfoldB A(a)i mit h(b) =def unfoldB A(b) fu¨r alle b ∈ hai wohldefiniert und surjektiv. Daraus folgt |hf i| = |hunfoldB A(a)i| ≤ |hai| ≤ |A|. o
79
2.25 Baumautomaten [3, 33, 34, 42] Sei Σ eine konstruktive Signatur und Y eine Menge. Ein (Σ, Y )-Baumautomat (A, out) enth¨alt neben einer Σ-Algebra A = (A, Op) eine S-sortige Funktion out : A → Y . Die Funktion out ◦ fold A : TΣ → Y nennen wir das von (A, out) realisierte Baumverhalten. Wie man leicht sieht, ist die Funktion h : TList(X) → X ∗ nil 7→ cons(x, t) 7→ x · h(t) bijektiv. Folglich verallgemeinert der Begriff eines Baumverhaltens f : TΣ → Y den einer Verhaltensfunktion f : X ∗ → Y . Dementsprechend nennen wir im Fall Y = 2 (S-sortige) Teilmengen von TΣ Baumsprachen und nennen L(A, out) =def χ−1(out ◦ fold A) die vom (Σ, Y )-Baumautomaten (A, out) erkannte Baumsprache und L ⊆ TΣ regul¨ ar, wenn es einen endlichen (!) (Σ, 2)-Baumautomaten (A, out) gibt, der L erkennt, d.h. die Gleichung out ◦ fold A = χ(L) erfu¨llt. Ein initialer Automat (A = (A, Op), a) liefert den (List(X), Y )-Baumautomaten (B, β A)
80
mit Blist = Areg , nilB = a und consB = λ(x, a).δ A(a)(x), der unfoldB A(a) ◦ h realisiert. Umgekehrt liefert ein (List(X), Y )-Baumautomat (B, f ) den initialen Automaten (A, nilB ) mit Areg = Blist, δ A = λa.λx.consB (x, a) und β A = f, der f ◦ fold A ◦ h−1 (im Sinne von 2.17) realisiert. Eine Baumsprache L ⊆ TList(X) ist also genau dann regul¨ar, wenn es einen endlichen initialen Automaten (A, a) gibt, der h(L) erkennt, was wiederum – wegen 3.13 oder 12.3 – genau dann gilt, wenn h(L) – im Sinne von 2.17 – regul¨ar ist. Baumautomaten werden zum Beispiel bei der formalen Behandlung von XML-Dokumenten eingesetzt (siehe Beispiel 4.3).
81
3 Rechnen mit Algebren
In diesem Abschnitt werden die beiden wichtigsten einstelligen Algebratransformationen: die Bildung von Unteralgebren bzw. Quotienten, und ihr Zusammenhang zu Homomorphismen vorgestellt. Unteralgebren und Quotienten modellieren Restriktionen bzw. Abstraktionen eines gegebenen Modells. Beide Konstrukte sind aus der Mengenlehre bekannt. Sie werden hier auf S-sortige Mengen fortgesetzt. Sei Σ = (S, I, F ) eine Signatur, A = (Ae)e∈T (S,I) eine typvertr¨agliche T (S, I)-sortige Menge, n > 0 und Rs ⊆ Ans fu¨r alle s ∈ S. R = (Rs)s∈S wird wie folgt zur T (S, I)-sortigen Relation geliftet: • For all I ∈ I, RI =def ∆nI. • For all I ∈ I and {ei}i∈I ⊆ T (S, I), RQi∈I ei =def {(a1, . . . , an) ∈ AnQ
i∈I ei
| ∀ i ∈ I : (πi(a1), . . . , πi(an)) ∈ Rei },
R`i∈I ei =def {(ιi(a1), . . . , ιi(an)) | (a1, . . . , an) ∈ Rei , i ∈ I} ⊆ An`
i∈I ei
.
82
Lemma LIFT Seien g, h : A → B S-sortige Funktionen und R = (Rs)s∈S und R0 = (Rs0 )s∈S die S-sortigen Relationen mit Rs = {a ∈ As | g(a) = h(a)} und Rs0 = {(g(a), h(a)) | a ∈ As} fu¨r alle s ∈ S. Dann gilt Re = {a ∈ Ae | ge(a) = he(a)} und Re0 = {(ge(a), he(a)) | a ∈ Ae} fu¨r alle e ∈ T (S, I).
o
Unteralgebren Sei Σ = (S, I, F ) eine Signatur und A = (A, Op) eine Σ-Algebra. Eine S-sortige Teilmenge R = (Rs)s∈S von A heißt Σ-Invariante, wenn fu¨r alle f : e → e0 ∈ F und a ∈ Re f A(a) ∈ Re0 gilt. Man nennt R Σ-Invariante, weil die Zugeh¨origkeit von Elementen von A zu R invariant gegenu¨ber der Anwendung von Operationenvon Σ ist. R induziert die Σ-Unteralgebra A|R von A: • Fu¨r alle e ∈ T (S, I), (A|R )e =def Re. • Fu¨r alle f : e → e0 ∈ F und a ∈ Re, f A|R (a) =def f A(a). 83
Beispiel 3.1 S Sei X = BS \ 1. Die Menge fold Lang(X)(TReg(BS)) der regul¨aren Sprachen u¨ber X ist eine Reg(BS)-Invariante von Lang(X). Das folgt allein aus der Vertr¨aglichkeit von fold Lang(X) mit den Operationen von Reg(BS). Fu¨r jede Signatur Σ, jede Σ-Algebra A = (A, Op) und jeden Σ-Homomorphismus h : A → B ist (h(As))s∈S eine Σ-Invariante. Die von ihr induzierte Unteralgebra von A stimmt mit der weiter oben definierten Bildalgebra h(A) u¨berein. Fu¨r jede konstruktive Signatur Σ ist TΣ(V ) eine Σ-Unteralgebra von CTΣ(V ). Fu¨r jede destruktive Signatur Σ ist coTΣ(V ) eine Σ-Unteralgebra von DTΣ(V ).
o
Satz 3.2 (1) Sei B = (B, Op0) eine Unteralgebra von A = (A, Op). Die T (S, I)-sortige Funktion incB = (incBe : Be → Ae)e∈T (S,I) ist Σ-homomorph. (2) (Homomorphiesatz) Sei h : C → A ein Σ-Homomorphismus. h(C) ist eine Unteralgebra von A. h0 : C → h(C) c 7→ h(c) ist ein surjektiver Σ-Homomorphismus. 84
Ist h injektiv, dann ist h0 bijektiv. Alle Σ-Homomorphismen h00 : C → h(C) mit inch(C) ◦ h00 = h stimmen mit h0 u¨berein. h
A
C h0
inch(A)
h(A)
(3) Sei Σ eine konstruktive Signatur und A eine Σ-Algebra. fold A(TΣ) ist die kleinste ΣUnteralgebra von A und TΣ ist die einzige Σ-Unteralgebra von TΣ. Demnach erfu¨llen alle zu TΣ isomorphen Σ-Algebren A das Induktionsprinzip, d.h. eine pra¨dikatenlogische Formel ϕ gilt fu¨r alle Elemente von A, wenn ϕ von allen Elementen einer Σ-Unteralgebra von A erfu¨llt wird. (4) Sei A eine Σ-Algebra und die A die einzige Σ-Unteralgebra von A. Dann gibt es fu¨r alle Σ-Algebren B h¨ochstens einen Σ-Homomorphismus h : A → B. Beweis von (3). Sei B eine Unteralgebra von A. Da TΣ initial und incB Σ-homomorph ist, kommutiert das folgende Diagramm:
85
fold A
A
TΣ
fold
=
B
incB
B
Daraus folgt fu¨r alle t ∈ TΣ, fold A(t) = incB (fold B (t)) = fold B (t) ∈ B. Also ist das Bild von fold A in B enthalten. Sei B eine Unteralgebra von TΣ. Da TΣ initial ist, folgt incB ◦fold B = idTΣ aus (1). Da idTΣ surjektiv ist, ist auch incB surjektiv. Da incB auch injektiv ist, sind B und TΣ isomorph. Also kann B nur mit TΣ u¨bereinstimmen. Beweis von (4). Seien g, h : A → B Σ-Homomorphismen. Dann ist C = {a ∈ A | g(a) = h(a)} eine Σ-Unteralgebra von A: Sei f : e → e0 ∈ F und a ∈ Ae mit ge(a) = he(a). Da g und h Σ-homomorph sind, gilt ge0 (f A(a)) = f B (ge(a)) = f B (he(a)) = he0 (f A(a)). Da g und h S-sortig sind, folgt f A(a) ∈ Ce aus Lemma LIFT. 86
Da A die einzige Σ-Unteralgebra von A ist, stimmt C mit A u¨berein, d.h. fu¨r alle a ∈ A gilt g(a) = h(a). Also ist g = h. o Beispiel 3.3 (siehe Beispiel 3.1) Nach Satz 3.2 (3) ist fold Lang(X)(TReg(BS)) die kleinste Unteralgebra von Lang(X). o Kongruenzen und Quotienten Sei Σ = (S, I, F ) eine Signatur und A = (A, Op) eine Σ-Algebra. Eine S-sortige Teilmenge R = (Rs)s∈S von A2 heißt Σ-Kongruenz, wenn fu¨r alle s ∈ S Rs ¨ eine Aquivalenzrelation ist und fu¨r alle f : e → e0 ∈ F und (a, b) ∈ Re (f A(a), f B (b)) ∈ Re0 gilt. R induziert die Σ-Quotientenalgebra A/R von A: • Fu¨r alle e ∈ T (S, I), (A/R)e =def {[a]R | a ∈ Ae}, wobei [a]R = {b ∈ Ae | (a, b) ∈ Re}. • Fu¨r alle f : e → e0 ∈ F und a ∈ Ae, f A/R ([a]R ) =def [f A(a)]R .
87
Satz 3.4 (ist dual zu Satz 3.2) (1) Sei A eine Σ-Algebra und R eine Σ-Kongruenz auf A. Die natu ¨ rliche Abbildung ¨ natR : A → A/R, die jedes Element a ∈ A auf seine Aquivalenzklasse [a]R abbildet, ist Σ-homomorph. (2) (Homomorphiesatz) Sei h : A → B ein Σ-Homomorphismus und ker(h) ⊆ A2 der Kern von h, d.h. ker(h) = {(a, b) | h(a) = h(b)}. ker(h) ist eine Σ-Kongruenz. h0 : A/ker(h) → B [a]ker(h) 7→ h(a) ist ein injektiver Σ-Homomorphismus. Ist h surjektiv, dann ist h0 bijektiv. Alle Σ-Homomorphismen h00 : A/ker(h) → B mit h00 ◦ nat = h stimmen mit h0 u¨berein. h
B
A
h0
natker(h)
A/ker(h) 88
(3) Sei Σ eine destruktive Signatur, A eine Σ-Algebra und Fin eine finale Σ-Algebra (s.o). Der – Verhaltenskongruenz von A genannte – Kern des eindeutigen Σ-Homomorphismus unfold A : A → Fin ist die gr¨oßte Σ-Kongruenz auf A und die Diagonale von Fin 2 die einzige Σ-Kongruenz R auf Fin. Demnach erfu¨llen alle zu Fin isomorphen Σ-Algebren A das Coinduktionsprinzip: Sei E eine Menge von Σ-Gleichungen t = u zwischen Σ-Termen u¨ber V , die denselben Typ haben. E gilt in A, wenn es eine Σ-Kongruenz R auf A gibt, die fu¨r alle t = u ∈ E und g : V → A das Paar (g ∗(t), g ∗(u)) enth¨alt. (4) Sei B eine Σ-Algebra und die Diagonale von B 2 die einzige Σ-Kongruenz R auf B. Dann gibt es fu¨r alle Σ-Algebren A h¨ochstens einen Σ-Homomorphismus h : A → B. Beweis von (3). Sei R eine Kongruenz auf A. Da Fin final und natR Σ-homomorph ist, kommutiert das folgende Diagramm: unfold A
Fin
A
unfold A/R
natR
A/R 89
Daraus folgt fu¨r alle a, b ∈ A, (a, b) ∈ R ⇒ [a]R = [b]R ⇒ unfold A(a) = unfold A/R ([a]R ) = unfold A/R ([b]R ) = unfold A(b). Also ist R im Kern von unfold A enthalten. Sei R eine Kongruenz auf Fin. Da Fin final ist, folgt unfold Fin/R ◦natR = idFin aus (1). Da idFin injektiv ist, ist auch natR injektiv. Da natR auch surjektiv ist, sind Fin und Fin/R isomorph. Also kann R nur die Diagonale von Fin 2 sein. Beweis von (4). Seien g, h : A → B Σ-Homomorphismen. Dann ist R = {(g(a), h(a)) | a ∈ A} eine Σ-Kongruenz auf B: Sei f : e → e0 ∈ F , a ∈ Ae und (ge(a), he(a)) ∈ Re. Da g und h Σ-homomorph sind, gelten f B (ge(a)) = ge0 (f A(a)) und f B (he(a)) = he0 (f A(a)). Da g und h S-sortig sind, folgt (f B (ge(a)), f B (he(a))) = (ge0 (f A(a)), he0 (f A(a))) ∈ Re0 aus Lemma LIFT. Da ∆2B die einzige Σ-Kongruenz auf B ist, stimmt R mit ∆2B u¨berein, d.h. fu¨r alle a ∈ A gilt g(a) = h(a). Also ist g = h. o
90
Automatenminimierung durch Quotientenbildung Eine minimale Realisierung einer Verhaltensfunktion f : X ∗ → Y erh¨alt man auch als Quotienten eines gegebenen initialen Automaten A: Im Beweis von Satz 2.24 (iii) wurde der DAut(X, Y )-Homomorphismus h : hai → hf i definiert. Wegen der Surjektivit¨at von h ist hai/ker(h) nach Satz 3.4 (2) DAut(X, Y )isomorph zu hf i. Nach Definition von h ist ker(h) = ker(unfold A) ∩ hai2. Nach Satz 3.4 (3) ist ker(unfold A) die gr¨oßte Σ-Kongruenz auf A, also die gr¨oßte bin¨are Relation R auf A, die fu¨r alle a, b ∈ Astate folgende Bedingung erfu¨llt: (a, b) ∈ R
⇒
β A(a) = β A(b) ∧ ∀ w ∈ X ∗ : (δ A(a)(w), δ A(b)(w)) ∈ R.
(1)
Ist Astate endlich, dann l¨asst sich ker(unfold A) schnell und elegant mit dem in Abschnitt 2.3 von [27] und in [31] beschriebene (und in Haskell implementierte) Paull-UngerVerfahren berechnen. Es startet mit R0 = A2state und benutzt die Kontraposition (a, b) 6∈ R
⇐
β A(a) 6= β A(b) ∨ ∀ w ∈ X ∗ : (δ A(a)(w), δ A(b)(w)) 6∈ R
(2)
von (1), um R0 schrittweise auf den Kern von unfold A zu reduzieren.
91
Transitionsmonoid und syntaktische Kongruenz Sei A = (A, Op) eine DAut(X, Y )-Algebra. Das Bild der Mon-homomorphen Erreichbarkeitsfunktion reachA : X ∗ → (Astate → Astate) von A heißt Transitionsmonoid von A. Satz 3.5 (Transitionsmonoide und endliche Automaten) Sei a ∈ Astate und R der Kern von reachhai : X ∗ → (hai → hai). hai ist genau dann ¨ endlich, wenn R endlich viele Aquivalenzklassen hat oder das Transitionsmonoid von hai endlich ist. Beweis. Nach Satz 3.4 (2) ist das Transitionsmonoid von hai Mon-isomorph zum Quotienten X ∗/R. Außerdem ist die Abbildung h : X ∗/R → hai [w]R 7→ δA∗(a)(w) wohldefiniert: Sei (v, w) ∈ R. Dann gilt reachhai(v) = reachhai(w), also insbesondere h([v]R ) = runA(a)(v) = δ hai∗(a)(v) = reachhai(v)(a) = reachhai(w)(a) = δ hai∗(a)(w) = runA(a)(w) = h([w]R ). 92
Da h surjektiv ist, liefert die Komposition h ◦ g mit dem Isomorphismus g : reachhai(X ∗) → X ∗/R eine surjektive Abbildung von reachhai(X ∗) nach hai. Also u¨bertra¨gt sich die Endlichkeit des Transitionsmonoids von hai auf hai selbst. Umgekehrt ist das Transitionsmonoid jedes endlichen Automaten A endlich, weil es eine Teilmenge von Astate → Astate ist. o Sei L ⊆ X ∗. Das Transitionsmonoid von hLi heißt syntaktisches Monoid und der Kern von reachhLi syntaktische Kongruenz von L. Letztere l¨asst sich als Menge aller Paare (v, w) ∈ X ∗ × X ∗ mit uvu0 ∈ L ⇔ uwu0 ∈ L fu¨r alle u, u0 ∈ X ∗ charakterisieren. Satz 3.5 impliziert, dass sie genau dann endlich viele ¨ Aquivalenzklassen hat, wenn L von einem endlichen initialen Automaten (A, a) erkannt wird, was wiederum zur Regularit¨at von L ¨aquivalent ist (siehe 3.13 fu¨r einen direkten Beweis oder Beispiel 12.3 fu¨r den klassischen u¨ber die Konstruktion eines nichtdeterministischen Akzeptors von L). Folglich kann die Nichtregularit¨at einer Sprache L oft gezeigt werden, indem aus der Endlichkeit der Zustandsmenge eines Akzeptors von L ein Widerspruch hergeleitet wird. W¨are z.B. L = {xny n | n ∈ N} regul¨ar, dann g¨abe es einen endlichen Automaten (A, a) mit unfold A(a) = L. 93
Demnach mu¨sste fu¨r alle n ∈ N ein Zustand bn ∈ Areg existieren mit runA(a)(xn) = bn und β A(runA(bn)(y n)) = 1. Da A endlich ist, g¨abe es i, j ∈ N mit i 6= j und bi = bj . Daraus wu¨rde jedoch unfold A(xiy j ) = β A(runA(a)(xiy j )) = β A(runA(runA(a)(xi))(y j )) = β A(runA(bi)(y j )) = β A(runA(bj )(y j )) = 1 folgen, im Widerspruch dazu, dass xiy j nicht zu L geh¨ort. Also ist L nicht regul¨ar. 3.6 Termsubstitution Sei Σ = (S, I, F ) eine Signatur. Belegungen von Variablen durch Σ-Terme heißen Substitutionen und werden u¨blicherweise mit kleinen griechischen Buchstaben bezeichnet. Im Gegensatz zu den Belegungen von Kapitel 2 beschr¨anken wir den Wertebereich von Substitutionen σ : V → TΣ(V ) nicht auf die Tr¨agermenge der Algebra TΣ(V ), also auf Terme ohne λ und ite. Um ungewollte Bindungen von Variablen zu vermeiden, muss die Fortsetzung σ ∗ : TΣ(V ) → TΣ(V ) von σ auf Terme anders als die Auswertung g ∗ : TΣ(V ) → A einer Belegung g : V → A von Kapitel 2 definiert werden: 94
• Fu¨r alle X ∈ ( BS, e ∈ T (S, I), x ∈ VX und t ∈ TΣ(V )e, λx0.σ[x0/x]∗(t) falls x ∈ var(σ(free(t) \ {x})), ∗ σ (λx.t) = λx.σ[x/x]∗(t) sonst. • Fu¨r alle e ∈ T (S, I) t ∈ TΣ(V )2 und u, v ∈ TΣ(V )e, σ ∗(ite(t, u, v)) = ite(σ ∗(t), σ ∗(u), σ ∗(v)). In den restlichen F¨allen ist σ ∗ genauso definiert wie g ∗: • Fu¨r alle x ∈ V , σ ∗(x) = σ(x). • Fu¨r alle x ∈ X ∈ BS, σ ∗(x) = x. • Fu¨r alle n > 1 und t1, . . . , tn ∈ TΣ(V ), σ ∗(t1, . . . , tn) = (σ ∗(t1), . . . , σ ∗(tn)). • Fu¨r alle f : e → e0 ∈ F und t ∈ TΣ(V )e, σ ∗(f t) = f σ ∗(t). • Fu¨r alle X ∈ BS, e ∈ T (S, I), t ∈ TΣ(V )eX und u ∈ TΣ(V )X , σ ∗(t(u)) = σ ∗(t)(σ ∗(u)). σ ∗(t) heißt σ-Instanz von t und Grundinstanz, falls σ alle Variablen von t auf Grundterme abbildet. Man schreibt h¨aufig tσ anstelle von σ ∗(t) sowie {t1/x1, . . . , tn/xn} fu¨r die Substitution σ mit σ(xi) = ti fu¨r alle 1 ≤ i ≤ n und σ(x) = x fu¨r alle x ∈ V \ {x1, . . . , xn}.
95
Satz 3.7 (Auswertung und Substitution) (1) Fu¨r alle Belegungen g : V → A und Σ-Homomorphismen h : A → B gilt: (h ◦ g)∗ = h ◦ g ∗. (2) Fu¨r alle Substitutionen σ, τ : V → TΣ(V ) gilt: (σ ∗ ◦ τ )∗ = σ ∗ ◦ τ ∗. Beweis. (1) Induktion u¨ber den Aufbau von Σ-Termen. (2) folgt aus (1), weil σ ∗ ein ΣHomomorphismus ist. o Term¨ aquivalenz und Normalformen Sei Σ = (S, I, F ) eine konstruktive Signatur. In diesem Abschnitt geht es um Σ-Algebren A, die eine gegebene Menge E von Σ-Gleichungen (s.o.) erfu ¨ llen, d.h. fu¨r die Folgendes gilt: • fu¨r alle t = t0 ∈ E und g : V → A gilt g ∗(t) = g ∗(t0). AlgΣ,E bezeichnet die Klasse aller Σ-Algebren, die E erfu¨llen.
96
Aus Satz 3.7 (1) folgt sofort, dass AlgΣ,E unter Σ-homomorphen Bildern abgeschlossen, d.h. fu¨r alle Σ-Homomorphismen h : A → B gilt: A ∈ AlgΣ,E
⇒
h(A) ∈ AlgΣ,E .
Die Elemente der Menge Inst(E ) =def {(tσ, t0σ) | (t, t0) ∈ E, σ : V → TΣ(V )}
(6)
heißen Instanzen von E. ¨ Die E-Aquivalenz ≡E ist definiert als kleinste Σ-Kongruenz, die Inst(E) enth¨alt. Aufgabe Zeigen Sie, dass der Quotient TΣ(V )/≡E E erfu¨llt.
o
Satz 3.8 Fu¨r alle Belegungen g : V → A in eine Σ-Algebra A, die E erfu¨llt, faktorisiert g ∗ : TΣ(V ) → A durch TΣ(V )/≡E , d.h. es gibt einen Σ-Homomorphismus h : TΣ(V )/≡E → A mit h ◦ nat≡E = g ∗.
97
V
incV
g
TΣ(V ) g
∗
nat≡E
TΣ(V )/≡E
(3) h
g≺ A
Beweis. Da der Kern von g ∗ eine Σ-Kongruenz ist, die Inst(E ) entha¨lt (siehe [29], Satz GLK), ≡E aber die kleinste derartige Relation auf TΣ(V ) ist, ist letztere im Kern von g ∗ enthalten. Folglich ist h : TΣ(V )/≡E → A mit h([t]≡E ) = h(t) fu¨r alle t ∈ TΣ(V ) wohldefiniert. (3) kommutiert, was zusammen mit der Surjektivit¨at und Σ-Homomorphie von nat≡E impliziert, dass auch h Σ-homomorph ist. o Die durch den gestrichelten Pfeil angedeutete Eigenschaft von h, der einzige Σ-Homomorphismus zu sein, der (3) kommutativ macht, folgt ebenfalls aus der Surjektivit¨at und Σ-Homomorphie von nat≡E . Zusammen mit TΣ/≡E ∈ AlgΣ,E impliziert Satz 3.8, dass TΣ/≡E initial in AlgΣ,E ist, dass es also fu¨r alle A ∈ AlgΣ,E genau einen Σ-Homomorphismus h : TΣ/≡E → A gibt.
98
Da g ∗ im Fall V = ∅ mit fold A u¨bereinstimmt, reduziert sich das obige Diagramm zu folgendem:
nat≡E
A
TΣ
fold A
(3)
h
TΣ/≡E
Beispiel 3.9 Sei Σ = Mon, x, y, z ∈ V und E = {mul(one, x) = x, mul(x, one) = x, mul(mul(x, y), z) = mul(x, mul(y, z))}. Die freie Mon-Algebra TMon (V ) ist kein Monoid, wohl aber ihr Quotient TMon (V )/ ≡E . Man nennt ihn das freie Monoid (u¨ber V ). Aufgabe Zeigen Sie, dass das freie Monoid tats¨achlich ein Monoid ist, also E erfu¨llt, und Mon-isomorph zu V ∗ ist. o Bei der Implementierung von Quotienten werden isomorphe Darstellungen bevorzugt, deren ¨ Elemente keine Aquivalenzklassen sind, diese aber eindeutig repr¨asentieren. Z.B. sind die ¨ W¨orter u¨ber V eindeutige Repr¨asentanten der Aquivalenzklassen von TMon (V )/≡E . 99
Bei der Berechnung a¨quivalenter Normalformen beschra¨nkt man sich meist auf die folgende Teilrelation von ≡E , die nur “orientierte” Anwendungen der Gleichungen von E zul¨asst: Die E-Reduktionsrelation →E besteht aus allen Paaren (u{t/x}, u{t0/x}) mit t = t0 ∈ E, u ∈ TΣ(V ) und σ : V → TΣ(V ). +
Die kleinste transitive Relation auf TΣ(V ), die →E enth¨alt, wird mit →E bezeichnet. +
Aufgabe Zeigen Sie, dass →E die kleinste transitive und mit Σ vertr¨agliche Relation auf + TΣ(V ) ist, die Inst(E ) enth¨alt. Folgern Sie daraus, dass →E eine Teilmenge von ≡E ist.o +
Sei t ∈ TΣ(V ). u ∈ TΣ(V ) heißt E-Normalform von t, wenn t →E u gilt und u zu einer vorgegebenen Teilmenge von TΣ(V ) geh¨ort. Eine Funktion reduce : TΣ(V ) → TΣ(V ) heißt E-Reduktionsfunktion, wenn fu¨r alle t ∈ TΣ(V ), reduce(t) eine E-Normalform von t ist. Sei A ∈ AlgΣ,E und g : V → A. Wegen +
→E ⊆ ≡E ⊆ ker(g ∗) (siehe obige Aufgabe und den Beweis von Satz 3.8) gilt g ∗(t) = g ∗(reduce(t)) fu¨r alle 100
t ∈ TΣ(V ), also kurz: g ∗ ◦ reduce = g ∗.
(3)
Allgemeine Methoden zur Berechnung von Normalformen werden in [29], §5.2 behandelt. Beispiel 3.10 Normalformen regul¨ arer Ausdru ¨ cke E bestehe aus folgenden Reg(BS)-Gleichungen: f (f (x, y), z) = f (x, f (y, z)) par(x, y) = par(y, x) seq(x, par(y, z)) = par(seq(x, y), seq(x, z)) seq(par(x, y), z) = par(seq(x, z), seq(y, z)) par(x, x) = x par(mt, x) = x par(x, mt) = x seq(eps, x) = x seq(x, eps) = x seq(mt, x) = mt seq(x, mt) = mt f (ite(x, y, z), z 0) = ite(x, f (y, z 0), f (z, z 0)) f (z 0, ite(x, y, z)) = ite(x, f (z 0, y), f (z 0, z))
(Assoziativita¨t von f ∈ {par, seq}) (Kommutativit¨at von par) (Linksdistributivit¨at von seq u¨ber par) (Rechtsdistributivit¨at von seq u¨ber par) (Idempotenz von par) (Neutralit¨at von mt bzgl. par) (Neutralit¨at von eps bzgl. seq) (Annihilation) (f ∈ {par, seq}) (f ∈ {par, seq})
Demnach entfernt eine E-Reduktionsfunktion mt und Mehrfachkopien von Summanden aus Summen sowie eps aus Produkten, ersetzt alle Produkte, die mt enthalten, durch mt, 101
distribuiert seq u¨ber par und linearisiert geschachtelte Summen und Produkte rechtsassoziativ. Angewendet auf Reg(BS)-Grundterme entspricht sie deren Faltung in der Reg(BS)Algebra regNorm (siehe Compiler.hs). S Sei X = BS. Da Lang(X) E erfu¨llt, gilt (3) fu¨r A = Lang(X). Algebren, die E erfu¨llen, heißen idempotente Semiringe. Da E weder den Sternoperator iter : reg → reg noch die Konstanten B : 1 → reg enth¨alt, brauchen diese in einem Semiring nicht definiert zu sein. Auch die Idempotenz von par ist keine Anforderung an Semiringe. Kleene-Algebren sind Semiringe, auf denen ein Sternoperator definiert ist und die neben E weitere (den Sternoperator betreffende) Gleichungen erfu¨llen. Die Elemente von Beh(X, Y ) (siehe 2.7) heißen formale Potenzreihen, wenn Y ein Semiring ist (siehe [37], Kapitel 9). 3.11 Die Brzozowski-Gleichungen Die folgende Menge BRE von – Brzozowski-Gleichungen genannten – Reg(BS)Gleichungen hat in TReg(BS) genau eine L¨osung, d.h. es gibt genau eine Erweiterung von TReg(BS) zur Acc(X)-Algebra, die BRE erfu¨llt (siehe Beispiel 17.4). In Abschnitt 2.7 wurde diese L¨osung unter dem Namen Bro(BS) eingefu¨hrt. Existenz und Eindeutigkeit folgen aus Satz 17.1 und werden dort aus dem in Satz 3.2 (3) eingefu¨hrten 102
Induktionsprinzip abgeleitet. δ(eps) δ(mt) δ(B) δ(par(t, u)) δ(seq(t, u)) δ(iter(t)) β(eps) β(mt) β(B) β(par(t, u)) β(seq(t, u)) β(iter(t))
= = = = = = = = = = = =
λx.mt λx.mt λx.ite(x ∈ B, eps, mt) λx.par(δ(t)(x), δ(u)(x)) λx.par(seq(δ(t)(x), u), ite(β(t), δ(u)(x), mt)), λx.seq(δ(t)(x), iter(t)) 1 0 0 max{β(t), β(u)} β(t) ∗ β(u) 1
t und u sind hier Variablen der Sorte reg. Nach obiger Lesart definiert BRE Destruktoren (δ und β) auf der Basis von Konstruktoren von Reg(BS). Umgekehrt la¨sst sich BRE auch als Definition der Konstruktoren auf der Basis der Destruktoren δ und β auffassen: Nach Satz 17.7 hat BRE n¨amlich in der finalen Acc(X)-Algebra Pow (X) genau eine coinduktive L¨osung, d.h. es gibt genau eine Erweiterung von Lang(X) zur Reg(BS)-Algebra, die BRE erfu¨llt (siehe Beispiel 17.10). o 103
3.12 Optimierter Brzozowski-Automat Der Erkenner Bro(BS) regul¨arer Sprachen (siehe Abschnitt 2.11) ben¨otigt viel Platz, weil die wiederholten Aufrufe von δ Bro(BS) aus t immer gr¨oßere Ausdru¨cke erzeugen. Um das zu vermeiden, ersetzen wir Bro(BS) durch die Acc(X)-Algebra Norm(BS) (norm in Compiler.hs), die bis auf die Interpretation von δ mit Bro(BS) u¨bereinstimmt. δ Norm(BS) normalisiert die von δ Bro(BS) berechneten Folgezust¨ande mit der in Beispiel 3.10 beschriebenen Reduktionsfunktion reduce : TReg(BS)(V ) → TReg(BS)(V ). Fu¨r alle t ∈ TReg(BS), δ Norm(BS)(t) =def reduce ◦ δ Bro(BS)(t).
(1)
fold Lang(X) ◦ reduce = fold Lang(X).
(2)
Gem¨aß Beispiel 3.10 gilt
104
Es bleibt zu zeigen, dass fu¨r alle t ∈ TReg(BS) die initialen Automaten (Bro(BS), t) und (Norm(BS), t) dieselben Sprachen erkennen, d.h. unfold Norm(BS)(t) = unfold Bro(BS)(t).
(3)
Wir beweisen (3) durch Induktion u¨ber die L¨ange der W¨orter u¨ber X. β Norm(BS)(runNorm(BS)(t)()) = β Norm(BS)(t) = β Bro(BS)(t) = β Bro(BS)(runBro(BS)(t)()). Fu¨r alle x ∈ X und w ∈ X ∗, β Norm(BS)(runNorm(BS)(t)(xw)) = β Norm(BS)(runNorm(BS)(δ Norm(BS)(t)(x))(w)) = unfold Norm(BS)(δ Norm(BS)(t)(x))(w)
ind. hyp.
=
unfold Bro(BS)(δ Norm(BS)(t)(x))(w)
(1)
= unfold Bro(BS)(reduce(δ Bro(BS)(t))(x))(w) = fold Lang(X)(reduce(δ Bro(BS)(t))(x))(w)
(2)
= fold Lang(X)(δ Bro(BS)(t)(x))(w) = unfold Bro(BS)(δ Bro(BS)(t)(x))(w) = β Bro(BS)(runBro(BS)(δ Bro(BS)(t)(x))(w)) = β Bro(BS)(runBro(BS)(t)(xw)).
Also gilt (3): unfold Norm(BS)(t) = {w ∈ X ∗ | β Norm(BS)(runNorm(BS)(t)(w)) = 1} = {w ∈ X ∗ | β Bro(BS)(runBro(BS)(t)(w)) = 1} = unfold Bro(BS)(t).
Im Haskell-Modul Compiler.hs entspricht der Erkenner unfold Norm(BS)(t) dem Aufruf regToAl "" w 4, wobei w die Wortdarstellung von t ist. o 105
3.13 Erkenner regul¨ arer Sprachen sind endlich Aus der Gu¨ltigkeit von BRE in Pow (X) lassen sich die folgenden Gleichungen fu¨r runPow (X) : P(X ∗) → P(X ∗)X
∗
ableiten (siehe 2.9): Fu¨r alle w ∈ X ∗, B ∈ BS und L, L0 ⊆ P(X ∗), ( 1 falls w = , runPow (X)(epsLang(X))(w) = ∅ sonst, runPow (X)(mtLang(X))(w) = ∅, C falls w = , Lang(X) runPow (X)(B )(w) = 1 falls w ∈ C, ∅ sonst, runPow (X)(parLang(X)(L, L0))(w) = runPow (X)(L)(w) ∪ runPow (X)(L0)(w), runPow (X)(seq Lang(X)(L, L0))(w) = {uv | u ∈ runPow (X)(L)(w), v ∈ L0} S ∪ uv=w (if ∈ runPow (X)(L)(u) then runPow (X)(L0)(v) else ∅),
(4) (5) (6) (7)
(8)
106
runPow (X)(iterLang(X)(L))(w) = {uv | u ∈ runPow (X)(L)(w), v ∈ iterPow (X)(L)} S T ∪ u1...unv=w (if ∈ ni=1 runPow (X)(L)(ui) then {uv 0 | u ∈ runPow (X)(L)(v), v 0 ∈ iterPow (X)(L)} else ∅) (9) (siehe z.B. [37], Theorem 10.1). Wir erinnern an Satz 2.24 (iii), aus dem folgt, dass fu¨r alle L ⊆ X ∗ der Unterautomat (hLi, L) von (Pow (X), L) ein minimaler Erkenner von L ist. Ist L die Sprache eines regul¨aren Ausdrucks t, ist also L = fold Lang(X)(t), dann ist hLi = {runPow (X)(fold Lang(X)(t))(w) | w ∈ X ∗}. Daraus folgt durch Induktion u¨ber den Aufbau von t, dass hLi endlich ist: Im Fall t ∈ {eps, mt} ∪ {B | B ∈ BS} besteht hLi wegen (4), (5) und (6) aus zwei, einem bzw. drei Zusta¨nden. Im Fall t = par(t0, t00) folgt |hLi| ≤ |hfold Lang(X)(t0)i| ∗ |hfold Lang(X)(t00)i| aus (7). Im Fall t = seq(t0, t00) folgt |hLi| ≤ |hfold Lang(X)(t0)i| ∗ 2|hfold Im Fall t = iter(t0) folgt |hLi| ≤ 2|hfold
Lang(X) (t0 )i|
Lang(X) (t00 )i|
aus (8).
aus (9). 107
Damit ist ohne den u¨blichen Umweg u¨ber Potenzautomaten (siehe Beispiel 12.3) gezeigt, dass regul¨are Sprachen von endlichen Automaten erkannt werden.
108
4 Kontextfreie Grammatiken (CFGs)
Sie ordnen einer konstruktiven Signatur Σ eine konkrete Syntax und damit eine vom Compiler verstehbare Quellsprache zu, so dass er diese in eine als Σ-Algebra formulierte Zielsprache u¨bersetzen kann. Auch wenn das zu die Quellsprache bereits als konstruktive Signatur Σ und die Zielsprache als Σ-Algebra gegeben sind, ben¨otigt der Compiler eine kontextfreie Grammatik, um Zeichenfolgen in Elemente der Algebra zu u¨bersetzen. Eine kontextfreie Grammatik (CFG) G = (S, BS, R) besteht aus • einer endlichen Menge S von Sorten, die auch Nichtterminale oder Variablen genannt werden, • einer endlichen Menge BS nichtleerer Basismengen, deren Singletons Terminale genannt und mit ihrem jeweiligen einzigen Element gleichgesetzt werden. • einer endlichen Menge R von Regeln s → w mit s ∈ S und w ∈ (S ∪ BS)∗, die auch Produktionen genannt werden. n > 0 Regeln s → w1, . . . , s → wn mit derselben linken Seite s werden oft zu der einen Regel s → w1| . . . |wn zusammengefasst. 109
Beispiel 4.1 Sei BS eine endliche Menge von Basismengen, die ∅ und 1 enth¨alt, syms(BS) wie in 2.14 definiert und R = {reg → reg + reg, reg → reg reg, reg → reg ∗, reg → (reg)} ∪ {reg → B | B ∈ BS}. REG =def ({reg}, syms(BS), R) ist eine CFG.
o
Oft genu¨gt es, bei der Definition einer CFG nur deren Regeln und Basismengen anzugeben. Automatisch bilden dann die Symbole, die auf der linken Seite einer Regel vorkommen, die Menge S der Sorten, w¨ahrend alle anderen W¨orter und Symbole (außer dem senkrechten Strich |; s.o.) auf der rechten Seite einer Regel Terminale oder Namen mehrelementiger Basismengen sind. Beispiel 4.2 Die Regeln der CFG JavaLight fu¨r imperative Programme mit Konditionalen und Schleifen lauten wie folgt:
110
Commands → Command →
Sum Sumsect Prod Prodsect Factor Disjunct Conjunct Literal
→ → → → → → → →
Command Commands | Command {Commands} | String = Sum; | if Disjunct Command else Command | if Disjunct Command | while Disjunct Command Prod Sumsect {+, −} Prod Sumsect | Factor Prodsect {∗, /} Factor Prodsect | Z | String | (Sum) Conjunct || Disjunct | Conjunct Literal && Conjunct | Literal !Literal | Sum Rel Sum | 2 | (Disjunct)
String, {+, −}, {∗, /}, Z, Rel und 2 sind die mehrelementigen Basismengen von JavaLight. String bezeichnet die Menge aller Zeichenfolgen außer den in Regeln von JavaLight vorkommenden Symbolen und W¨ortern außer String. Rel bezeichnet eine Menge nicht n¨aher spezifizierter bin¨arer Relationen auf Z. Ein aus der Sorte Commands ableitbares JavaLight-Programm ist z.B. fact = 1; while x > 1 {fact = fact*x; x = x-1;}
o 111
Beispiel 4.3 XMLstore (siehe [19], Abschnitt 2) Store
→
Orders Order P erson Emails Email Items Item Stock ItemS Suppliers Id
→ → → → → → → → → → →
hstorei hstocki Stock h/stocki h/storei | hstorei Orders hstocki Stock h/stocki h/storei Order Orders | Order horderi hcustomeri P erson h/customeri Items h/orderi hnamei String h/namei | hnamei String h/namei Emails Email Emails | hemaili String h/emaili Item Items | Item hitemi Id hpricei String h/pricei h/itemi ItemS Stock | ItemS hitemi Id hquantityi Z h/quantityi Suppliers h/itemi hsupplieri P erson h/supplieri | Stock hidi String h/idi
112
Die Sprache von XMLstore beschreibt XML-Dokumente wie z.B. das folgende:
John Mitchell [email protected] - I18F 100
- IG8 10 Al Jones [email protected] [email protected]
- J38H 30
- J38H1 10 Richard Bird
- J38H2 20 Mick Taylor
113
Nicht-linksrekursive CFGs Sei G = (S, BS, R) eine CFG und X =
S
BS.
X ist die Menge der Eingabesymbole, die Compiler fu¨r G verarbeiten. Demgegenu¨ber tauchen auf den rechten Seiten der Regeln von G nur (Namen fu¨r) komplette Basismengen auf! Die klassische Definition einer linksrekursiven Grammatik verwendet die (Links-)Ableitungsrelation →G = {(vsw, vαw) | s → α ∈ R, v, w ∈ (S ∪ BS)∗}. +
∗
→G und →G bezeichnen den transitiven bzw. reflexiv-transitiven Abschluss von →G. +
G heißt linksrekursiv, falls es s ∈ S und w ∈ (S ∪ BS)∗ mit s →G sw gibt. Z.B. ist REG linksrekursiv, JavaLight und XMLstore jedoch nicht (siehe Beispiele 4.1-4.3).
114
Linksassoziative Auswertung erzwingt keine Linksrekursion Sind alle Regeln, deren abstrakte Syntax bin¨are Operationen darstellen, dann werden aus diesen Operationen bestehende Syntaxb¨aume rechtsassoziativ ausgewertet. Bei ungeklammerten Ausdru¨cke wie x+y−z−z 0 oder x/y∗z/z 0 fu¨hrt aber nur die linkassoziative Faltung zum gewu¨nschten Ergebnis. Die gegebene Grammatik muss deshalb um Sorten und Regeln erweitert werden, die bewirken, dass aus der linkassoziativen eine semantisch ¨aquivalente rechtsassoziative Faltung wird. Im Fall von JavaLight bewirken das die Sorten Sumsect und Prodsect und deren Regeln. Die Namen der Sorten weisen auf deren Interpretation als Mengen von Sektionen hin, also von Funktionen wie z.B. (∗5) : Z → Z. Angewendet auf eine Zahl x, liefert (∗5) das Fu¨nffache von x. Die linkassoziative Faltung ((x+y)−z)−z 0 bzw. ((x/y)∗z)/z 0 der obigen Ausdru¨cke entspricht daher der – von den Regeln fu¨r Sumsect und Prodsect bewirkten – rechtsassoziativen Faltung ((−z 0) ◦ ((−z) ◦ (+y)))(x) bzw. ((/z 0) ◦ ((∗z) ◦ (/y)))(x). Die Sektionssorten von JavaLight wu¨rden automatisch eingefu¨hrt werden, wenn man die folgende Entrekursivierung auf eine linksrekursive Variante der Grammatik anwendet.
115
Verfahren zur Eliminierung von Linksrekursion Sei G = (S, BS, R) eine CFG und S = {s1, . . . , sn}. Fu¨hre fu¨r alle 1 ≤ i ≤ n die beiden folgenden Schritte in der angegebenen Reihenfolge durch: • Fu¨r alle 1 ≤ j < i und Regelpaare (si → sj v, sj → w) ersetze die Regel si → sj v durch die neue Regel si → wv. • Falls vorhanden, streiche die Regel si → si. • Fu¨r alle Regelpaare (si → siw, si → ev) mit e ∈ (S ∪ BS) \ {si} ersetze die Regel o si → siw durch die drei neuen Regeln si → evs0i, s0i → ws0i und s0i → w. Die Verwendung von jeweils drei Sorten fu¨r arithmetische bzw. Boolesche Ausdru¨cke (Sum, Prod und Factor bzw. Disjunct, Conjunct und Literal ) bewirkt ebenfalls eine bestimmte Auswertungsreihenfolge und zwar diejenige, die sich aus den u¨blichen Priorit¨aten arithmetischer bzw. Boolescher Operationen ergibt.
116
Abstrakte Syntax Sei G = (S, BS, R) eine CFG und Z = {B ∈ BS | |B| = 1} (Terminale von G). Die konstruktive Signatur Σ(G) = (S, BS, F (G)) mit F (G) = {fr : 1 → s | r = (s → w) ∈ R, w ∈ Z ∗} ∪ {fr : e1 × · · · × en → s | r = (s → w0e1w1 . . . enwn) ∈ R, n > 0, w0 . . . wn ∈ Z ∗, e1, . . . , en ∈ S ∪ BS \ Z} heißt abstrakte Syntax von G. Beispiel 4.4 Die Signatur Reg(BS) ist eine Teilsignatur der abstrakten Syntax der CFG REG von Beispiel 4.1. Aufgabe Zu welcher Regel von REG fehlt in Reg(BS) der entsprechende Konstruktor?
o
117
Die Konstruktoren von Σ(G) lassen sich i.d.R. direkt aus den Terminalen von G basteln. So wird manchmal fu¨r den aus der Regel r = (s → w0e1w1 . . . enwn) mit wi ∈ Z ∗ entstandenen Konstruktor fr die (Mixfix-)Darstellung w0 w1 . . . wn gew¨ahlt. So k¨onnte beispielsweise der Konstruktor f : Disjunct × Command × Command fu¨r die JavaLight-Regel Commands → if Disjunct Command else Command (siehe Beispiel 4.2) if else genannt werden. Um Verwechslungen zwischen Terminalen und Konstruktoren vorzubeugen, werden wir hier jedoch keine Terminale als Namen fu¨r Konstruktoren verwenden. Umgekehrt kann jede endlich verzweigende konstruktive Signatur Σ = (S, I, F ) in eine CFG G(Σ) = (S, BS ∪ {(, ), , }, R) mit Σ(G(Σ)) = Σ u¨berfu¨hrt werden, wobei R = {s → f (e1, . . . , en) | f : e1 × · · · × en → s ∈ F }.
Σ(G)-Grundterme werden Syntaxb¨ aume von G genannt. Alle ihre Knoten sind mit Operationssymbolen markiert. 118
Beispiel 4.5 SAB Die Grammatik SAB besteht aus den Sorten S, A, B, den Terminalen a, b und den Regeln r1 = S → aB,
r2 = S → bA,
r3 = S → ,
r4 = A → aS,
r5 = A → bAA,
r6 = B → bS,
r7 = B → aBB.
Demnach lauten die Konstruktoren der abstrakten Syntax von SAB wie folgt: f1 : B → S,
f2 : A → S,
f3 : 1 → S,
f4 : S → A,
f5 : A × A → A,
f6 : S → B,
f7 : B × B → B.
f1 f7 f6
f6
f1
f3
f6
ε
f3 ε
Syntaxbaum des Eingabewortes aababb
Mit markierte Bl¨atter eines Syntaxbaums werden ku¨nftig weglassen. 119
Die folgende SAB-Algebra SABcount berechnet die Anzahl #a(w) bzw. #b(w) der Vorkommen von a bzw. b im Eingabewort w: SABcount S = SABcount A = SABcount B = N2, f1SABcount = f4SABcount = λ(i, j).(i + 1, j), f2SABcount = f6SABcount = λ(i, j).(i, j + 1), f3SABcount
= (0, 0),
f5SABcount
= λ((i, j), (k, l)).(i + k, j + l + 1),
f7SABcount
= λ((i, j), (k, l)).(i + k + 1, j + l).
o
120
Beispiel 4.6 Σ(JavaLight) = (S, I, F ) S = { Commands, Command , Sum, Sumsect, Prod , Prodsect, Factor , Disjunct, Conjunct, Literal } I = { 1, 2, {+, −}, {∗, /}, Z, String, Rel } F = { seq : Command × Commands → Commands, embed : Command → Commands, block : Commands → Command , assign : String × Sum → Command , cond : Disjunct × Command × Command → Command , cond1, loop : Disjunct × Command → Command , sum : Prod × Sumsect → Sum, sumsect : {+, −} × Prod × Sumsect → Sumsect, nilS : 1 → Sumsect, prod : Factor × Prodsect → Prod , prodsect : {∗, /} × Factor × Prodsect → Prodsect, nilP : 1 → Prodsect, embedI : Z → Factor , var : String → Factor , encloseS : Sum → Factor ,
121
disjunct : Conjunct × Disjunct → Disjunct, embedC : Conjunct → Disjunct, conjunct : Literal × Conjunct → Conjunct, embedL : Literal → Conjunct, not : Literal → Literal , atom : Sum × Rel × Sum → Literal , embedB : 2 → Literal , encloseD : Disjunct → Literal }
Z.B. hat das JavaLight-Programm fact = 1; while x > 1 {fact = fact ∗ x; x = x − 1; } folgenden Syntaxbaum:
122
Seq Assign fact
Embed
Sum
Prod EmbedI
Loop
NilS
NilP
1
EmbedC
Block
EmbedL
Seq
Atom Sum Prod Var x
>
Sum
NilS
NilP
Assign
Prod EmbedI 1
fact
NilS
NilP
Sum
Prod Var fact
Embed Assign
NilS
x
Prodsect *
Var x
NilP
Sum
Prod Var x
NilP
Sumsect -
Prod
EmbedI
NilS
NilP
1
javaToAlg "prog" 1 (siehe Java.hs) u¨bersetzt das JavaLight-Programm in der Datei prog in den zugeh¨origen Syntaxbaum und schreibt diesen in die Datei Pix/javaterm.svg. Mit https://cloudconvert.org kann diese schnell in ein anderes Format konvertiert werden. 123
Beispiel 4.7 Σ(XMLstore) = (S , I, ∅, F ) S = = I = F =
{ { { {
Store, Orders, Order, P erson, Emails, Email, Items, Item, Stock, ItemS, Suppliers, Id } 1, String, Id , Z } store : Stock → Store, storeO : Orders × Stock → Store, orders : P erson × Items × Orders → Orders, embedP : P erson × Items → Orders, person : String → P erson, personE : String × Emails → P erson, emails : Email × Emails → Emails, none : 1 → Emails, email : String → Email, items : Id × String × Items → Items, embedI : Id × String → Items, stock : Id × Z × Supplier × Stock → Stock, embedS : Id × Z × Supplier → Stock, supplier : P erson → Suppliers, parts : Stock → Suppliers, id : String → Id } 124
StoreO EmbedP PersonE
Stock EmbedI
John Mitchell Emails
Id 10 Supplier
Id 100 IG8
Email None I18F
[email protected]
EmbedS
PersonE
Id 30 Parts
Al Jones Emails Email
J38H Emails
Id 10 Supplier
[email protected] Email None J38H1
[email protected]
Stock
PersonE
EmbedS Id 20 Supplier
Richard Bird None J38H2
PersonE
Mick Taylor None
Syntaxbaum des XML-Dokumentes von Beispiel 4.3 xmlToAlg "xmldoc" 1 (siehe Compiler.hs) u¨bersetzt das XMLstore-Dokument in der Datei xmldoc in den zugeho¨rigen Syntaxbaum u¨bersetzt und schreibt diesen in die Datei Pix/xmlterm.svg. xmlToAlg "xmldoc" 2 (siehe Compiler.hs) u¨bersetzt xmldoc in eine Listen-ProdukteSummen-Darstellung und schreibt diese in die Datei Pix/xmllist.svg. Fu¨r Beispiel 4.3 sieht sie folgendermaßen aus: 125
() []
[]
() () John Mitchell []
[email protected]
[]
()
()
IG8 10 One
J38H 30 Two
()
Al Jones []
[]
I18F 100
[email protected] [email protected] () J38H1 10 One
() J38H2 20 One
Richard Bird []
Sei G = (S, BS, R) eine CFG, X =
S
Mick Taylor []
BS und Z = {B ∈ BS | |B| = 1}.
Wort- und Ableitungsbaumalgebra Neben TΣ(G) lassen sich auch die Menge der Wo¨rter u¨ber X und die Menge der Ableitungsb¨aume von G zu Σ(G)-Algebren erweitern.
126
Word (G), die Wortalgebra von G • Fu¨r alle s ∈ S, Word (G)s =def X ∗. Word (G)
• Fu¨r alle w ∈ Z ∗ und r = (s → w) ∈ R, fr () =def w. • Fu¨r alle n > 0, w0 . . . wn ∈ Z ∗, e1, . . . , en ∈ S ∪ BS \ Z, r = (s → w0e1w1 . . . enwn) ∈ R und (v1, . . . , vn) ∈ (X ∗)n, frWord (G)(v1, . . . , vn) =def w0v1w1 . . . vnwn. Beispiel 4.8 Nochmal die Regeln von SAB (siehe Beispiel 4.5): r1 = S → aB, r2 = S → bA, r3 = S → , r4 = A → aS r5 = A → bAA, r6 = B → bS, r7 = B → aBB. Alle drei Tr¨agermengen der Wortalgebra Word (SAB) sind durch {a, b}∗ gegeben. Die Konstruktoren von Σ(SAB) werden in Word (SAB) wie folgt interpretiert: Fu¨r alle v, w ∈ {a, b}∗, Word (SAB) Word (SAB) (w) = f4 (w) = aw, f1 Word (SAB) Word (SAB) f2 (w) = f6 (w) = bw, Word (SAB) f3 = , Word (SAB) f5 (v, w) = bvw, Word (SAB) f7 (v, w) = avw. o 127
t ∈ TΣ(G) heißt G-Syntaxbaum fu ¨ r w ∈ X ∗, falls fold Word (G)(t) = w gilt. G ist eindeutig, wenn fold Word (G) injektiv ist. Die Sprache L(G) von G ist die Menge der W¨orter u¨ber X, die sich aus der Faltung eines Syntaxbaums in Word (G) ergeben: L(G) =def fold Word (G)(TΣ(G)).
Z.B. ist L(REG) (siehe 4.1) die Menge aller W¨orter u¨ber syms(BS) (siehe 2.14), die regul¨are Ausdru¨cke u¨ber BS darstellen, formal: L(REG) = {w ∈ syms(BS)∗ | ∃ t ∈ TReg(BS) : fold Regword (BS)(t)(0) = w}. Zwei Grammatiken G und G0 heißen ¨ aquivalent, wenn ihre Sprachen u¨bereinstimmen. Die Theorie formaler Sprachen liefert eine ¨aquivalente Definition von L(G), die die oben definierte Ableitungsrelation →G verwendet: Fu¨r alle s ∈ S, +
L(G)s = {w ∈ BS ∗ | s →G w}. 128
javaToAlg "prog" 2 (siehe Java.hs) u¨bersetzt das JavaLight-Programm in der Datei prog in die Interpretation des zugeh¨origen Syntaxbaums in Word (JavaLight) und schreibt diese in die Datei javasource. Die Inhalte von prog und javasource stimmen also miteinander u¨berein! Abl(G), die Ableitungsbaumalgebra von G Fu¨r alle s ∈ S ist Abl(G) ist das kleinste (S ∪BS)-Tupel von B¨aumen, deren innere Knoten mit Sorten und deren Bl¨atter mit Basismengen markiert sind, und die folgende Eigenschaft haben: • Fu¨r alle B ∈ BS, Abl(G)B = {B}. • Fu¨r alle r = (s → (e1, . . . , en)) ∈ R und (t1, . . . , tn) ∈ Abl(G)e1 × . . . × Abl(G)en , s(t1, . . . , tn) ∈ Abl(G)s. s(t1, . . . , tn) repr¨asentiert den Baum mit Wurzelmarkierung s und maximalen Unterb¨aumen t1, . . . , tn. Abl(G) interpretiert die Konstruktoren von Σ(G) wie folgt: Abl(G)
• Fu¨r alle w ∈ Z ∗ und r = (s → w) ∈ R, fr
() =def s(w). 129
• Fu¨r alle n > 0, w0 . . . wn ∈ Z ∗, e1, . . . , en ∈ S ∪ BS \ Z, r = (s → w0e1w1 . . . enwn) ∈ R und (t1, . . . , tn) ∈ Abl(G)e1 × . . . × Abl(G)en , frAbl(G)(t1, . . . , tn) =def s(w0, t1, w1, . . . , tn, wn). Commands Command
Commands
fact = Sum ;
Command
Prod Sumsect while Disjunct Factor Prodsect
Command
Conjunct
1
Commands
Literal Sum
>
Sum
Prod Sumsect Factor Prodsect x
Command fact = Sum ;
Prod Sumsect Factor Prodsect 1
Commands Command
Prod Sumsect Factor fact
x = Sum ;
Prodsect
Prod
* Factor Prodsect Factor Prodsect x
x
Sumsect - Prod Sumsect Factor Prodsect 1
Ableitungsbaum von fact = 1; while x > 1 {fact = fact*x; x = x-1;}
130
javaToAlg "prog" 3 (siehe Java.hs) u¨bersetzt das JavaLight-Programm in der Datei prog in den zugeh¨origen Ableitungsbaum und schreibt diesen in die Datei Pix/javaderi.svg. Beispiel 4.9 Zwei Modelle der Ausdru ¨ cke von JavaLight Wir interpretieren hier zun¨achst nur die Sorten und Operationen von Σ(JavaLight), die mit Ausdru¨cken zu tun haben, also alle außer Command und Commands. Der erste Modell A = (A, Op) ignoriert daru¨berhinaus Programmvariablen (Strings), d.h. der Konstruktor var : String → Factor bleibt uninterpretiert. ASum = AProd = AFactor = Z ASumsect = AProdsect = Z → Z ADisjunct = AConjunct = ALiteral = 2 embedDA : AConjunct embedLA : ALiteral encloseS A : ASum encloseDA : ADisjunct embedI A : Z embedB A : 2 x
→ → → → → → 7→
ADisjunct AConjunct AFactor ALiteral AFactor ALiteral x 131
sumA : AProd × ASumsect → ASum prodA : AFactor × AProdsect → AProd (x, f ) 7→ f (x) sumsectA : {+, −} × AProd × ASumsect → ASumsect prodsectA : {∗, /} × AFactor × AProdsect → AProdsect (op, x, f ) 7→ λy.f (y op x) nilS A : 1 → ASumsect nilP A : 1 → AProdsect 7→ λx.x disjunctA : AConjunct × ADisjunct → ADisjunct (x, y) 7→ x ∨ y conjunctA : ALiteral × AConjunct → AConjunct (x, y) 7→ x ∧ y notA : ALiteral → ALiteral x 7→ ¬x 132
atomA : ASum × Rel × ASum → ALiteral (x, rel, y) 7→ x rel y Sei Store = String → Z (Menge der Belegungen von Programmvariablen durch ganze Zahlen). Das zweite Modell B = (B, Op) liftet jede Tra¨germenge M ∈ {Z, Z → Z, 2} von A zur Funktionsmenge Store → M : BSum = BProd = BFactor = Store → Z BSumsect = BProdsect = Store → (Z → Z) BDisjunct = BConjunct = BLiteral = Store → 2 B interpretiert embedD, embedL, encloseS und encloseD wie A als Identit¨aten. varB : String → BFactor x 7→ λstore.store(x) Die restlichen Operationen von Σ(JavaLight) werden zustandsabh¨angig gemacht: embedI B : Z → BFactor embedB B : 2 → BLiteral a 7→ λstore.a 133
sumB : BProd × BSumsect → BSum prodB : BFactor × BProdsect → BProd (f, g) 7→ λstore.g(store)(f (store)) sumsectB : {+, −} × BProd × BSumsect → BSumsect prodsectB : {∗, /} × BFactor × AProdsect → BProdsect (op, f, g) 7→ λstore.λx.g(store)(x op f (store)) nilS B : 1 → BSumsect nilP B : 1 → BProdsect 7→ λstore.λx.x disjunctB : BConjunct × BDisjunct → BDisjunct (f, g) 7→ λstore.(f (store) ∨ g(store)) conjunctB : BLiteral × BConjunct → BConjunct (f, g) 7→ λstore.(f (store) ∧ g(store)) notB : BLiteral → BLiteral f 7→ λstore.¬f (store) 134
atomB : BSum × Rel × BSum → BLiteral (f, rel, g) 7→ λstore.(f (store) rel g(store)) In Abschnitt 11.5 wird B als Teil der JavaLight-Algebra javaState in Haskell implementiert.
135
5 Parser und Compiler fu ¨ r CFGs
Sei G = (S, BS, R) eine CFG, X = X u¨bersetzt werden sollen.
S
BS und A eine Σ(G)-Algebra, in die W¨orter u¨ber
In Anlehnung an den klassischen Begriff eines semantisch korrekten Compilers [22, 41] verlangen wir, dass die Semantiken Sem und Mach seiner Quell- bzw. Zielsprache in der durch das folgende Funktionsdiagramm ausgedru¨ckten Weise miteinander zusammenh¨angen: TΣ(G) fold Sem g Sem
fold A
(1)
encode
A evaluate g Mach
Hierbei sind • Sem die ebenfalls als Σ(G)-Algebra gegebene Semantik der Quellsprache L(G), • Mach ein in der Regel unabha¨ngig von Σ(G) definiertes Modell der Zielsprache, meist in Form einer abstrakten Maschine, • evaluate ein Interpreter, der Zielprogramme in der abstrakten Maschine Mach ausfu¨hrt, 136
• encode eine Funktion, die Sem auf Mach abbildet und die gewu¨nschte Arbeitsweise des Compilers auf semantischer Ebene reflektiert. Die Initialit¨at der Termalgebra TΣ(G) erlaubt es uns, den Beweis der Kommutativit¨at von (1) auf die Erweiterung von encode und evaluate zu Σ(G)-Homomorphismen zu reduzieren. Dazu muss zun¨achst Mach zu einer Σ(G)-Algebra gemacht werden, was z.B. bedeuten kann, die elementaren Funktionen der Zielsprache so in einer Signatur Σ0 zusammenzufassen, dass TΣ0 mit A u¨bereinstimmt, jeder Konstruktor von Σ(G) einem Σ0-Term entspricht, Sem eine Σ0-Algebra ist und evaluate Σ0-Terme in Sem faltet. Die Darstellung von Σ(G)Konstruktoren durch Σ0-Terme bestimmt dann m¨oglicherweise eine Definition von encode, die sowohl encode als auch evaluate Σ(G)-homomorph macht. So wurde z.B. in [41] die Korrektheit eines Compilers gezeigt, der imperative Programme in Datenflussgraphen u¨bersetzt. Damit sind alle vier Abbildungen in Diagramm (1), also auch und die beiden Kompositionen evaluate ◦ fold A und encode ◦ fold Mach Σ(G)-homomorph. Da TΣ(G) eine initiale Σ(G)Algebra ist, sind beide Kompositionen gleich. Also kommutiert (1). W¨ahrend fold A Syntaxb¨aume in der Zielsprache auswertet, ordnet fold Word (G) (siehe Kapitel 4) einem Syntaxbaum t das Wort der Quellsprache zu, aus dem ein Parser fu¨r G t berechnen soll.
137
In der Theorie formaler Sprachen ist der Begriff Parser auf Entscheidungsalgorithmen beschr¨ankt, die anstelle von Syntaxb¨aumen lediglich einen Booleschen Wert liefern, der angibt, ob ein Eingabewort zur Sprache der jeweiligen Grammatik geho¨rt oder nicht. Demgegenu¨ber definieren wir einen Parser fu ¨ r G als eine S-sortige Funktion parseG : X ∗ → M (TΣ(G)), die entweder Syntaxba¨ume oder, falls das Eingabewort nicht zur Sprache von G geho¨rt, Fehlermeldungen erzeugt. Welche Syntaxb¨aume bzw. Fehlermeldungen ausgegeben werden sollen, wird durch eine Monade M festgelegt. 5.1 Funktoren und Monaden Funktoren, natu¨rlichen Transformationen und Monaden sind kategorientheoretische Grundbegriffe, die heutzutage jeder Softwaredesigner kennen sollte, da sie sich in den Konstruktionsund Transformationsmustern jedes denkbaren statischen, dynamischen oder hybriden Systemmodells wiederfinden. Die hier ben¨otigten kategorientheoretischen Definitionen lauten wie folgt: Eine Kategorie K besteht aus • einer – ebenfalls mit K bezeichneten – Klasse von K-Objekten, • fu¨r alle A, B ∈ K einer Menge K(A, B) von K-Morphismen, 138
• einer assoziativen Komposition ◦ : K(A, B) × K(B, C) → K(A, C) (f, g) 7−→ g ◦ f, • einer Identit¨ at idA ∈ K(A, A), die bzgl. ◦ neutral ist, d.h. fu¨r alle B ∈ K und f ∈ K(A, B) gilt f ◦ idA = f = idB ◦ f . Im Kontext einer festen Kategorie K schreibt man meist f : A → B anstelle von f ∈ K(A, B). Wir haben hier mit vier Kategorien zu tun: Set, Set2 und SetS , deren Objekte alle Mengen, alle Mengenpaare bzw. alle S-sortigen Mengen und deren Morphismen alle Funktionen, alle Funktionspaare bzw. alle S-sortigen Mengen sind, sowie die Unterkategorie AlgΣ von SetS , deren Objekte alle Σ-Algebren und deren Morphismen alle Σ-Homomorphismen sind. Seien K, L Kategorien. Ein Funktor F : K → L ist eine Funktion, die jedem K-Objekt ein L-Objekt und jedem K-Morphismus f : A → B einen L-Morphismus F (f ) : F (A) → F (B) zuordnet sowie folgende Gleichungen erfu¨llt: • Fu¨r alle K-Objekte A, F (idA) = idF (A),
(2)
• Fu¨r alle K-Morphismen f : A → B and g : B → C, F (g ◦ f ) = F (g) ◦ F (f ).
(3)
139
Zwei Funktoren F : K → L und G : L → M kann man wie andere Funktionen sequentiell zu weiteren Funktoren komponieren: Fu¨r alle K-Objekte und -Morphismen A, (GF )(A) =def G(F (A)). Beispiele Sei B ∈ L. Der konstante Funktor const(B) : K → L ordnet jedem K-Objekt das L-Objekt B zu und jedem K-Morphismus die Identit¨at auf B. Der Identit¨ atsfunktor Id K : K → K ordnet jedem K-Objekt und jedem K-Morphismus sich selbst zu. Der Diagonalfunktor ∆K : K → K2 ordnet jedem K-Objekt A das Objektpaar (A, A) und jedem K-Morphismus f das Morphismenpaar (f, f ) zu. Der Produktfunktor × : Set2 → Set ordnet jedem Mengenpaar (A, B) die Menge A × B und jedem Funktionspaar (f : A → B, g : C → D) die Funktion f × g =def λ(a, c).(f (a), g(c)) zu.
140
Der Listenfunktor Star : Set → Set ordnet jeder Menge A die Menge A∗ der Wo¨rter u¨ber A zu und jeder Funktion f : A → B die Funktion Star (f ) : A∗ → B ∗ 7→ (a1, . . . , an) 7→ (f (a1), . . . , f (an)) Der Mengenfunktor P : Set → Set ordnen jeder Menge A die Potenzmenge P(A) zu und jeder Funktion f : A → B die Funktion P(f ) : P(A) → P(B) C 7→ {f (c) | c ∈ C} Sei E eine Menge von Fehlermeldungen, Ausnahmewerten o.¨a. Der Ausnahmefunktor + E : Set → Set ordnet jeder Menge A die Menge A + E zu (siehe Kapitel 2) und jeder Funktion f : A → B die Funktion f +E :A+E → B+E (a, 1) 7→ (f (a), 1) (e, 2) 7→ (e, 2) Sei S eine Menge.
141
Der Potenz- oder Leserfunktor S : Set → Set u¨ber S ordnet jeder Menge A die Menge S → A zu und jeder Funktion f : A → B die Funktion f S : AS → B S g 7→ f ◦ g Der Copotenz- oder Schreiberfunktor × S : Set → Set u¨ber S ordnet jeder Menge A die Menge A × S zu und jeder Funktion f : A → B die Funktion f ×S :A×S → B×S (a, s) 7→ (f (a), s) Der Transitionsfunktor ( × S)S : Set → Set komponiert den Leser- mit dem Schreiberfunktor u¨ber S: Er ordnet also jeder Menge A die Menge (A×S)S zu und jeder Funktion f : A → B die Funktion (f × S)S : (A × S)S → (B × S)S g 7→ λs.(f (π1(g(s))), π2(g(s))) Aufgabe Zeigen Sie, dass die hier definierten Funktionen tats¨achlich Funktoren sind, also (2) und (3) erfu¨llen, und dass sie sich von Set auf SetS fortsetzen lassen. o 142
Seien F, G : K → L Funktoren. Eine natu ¨ rliche Transformation τ : F → G ordnet jedem K-Objekt A einen L-Morphismus τA : F (A) → G(A) derart, dass fu¨r alle KMorphismen f : A → B folgendes Diagramm kommutiert: τA F (A) G(A) F (f ) g F (B)
G(f ) τB
g G(B)
Ein Funktor M : K → K heißt Monade, wenn es zwei natu¨rliche Transformationen η : Id K → M (Einheit) und µ : M ◦ M → M (Multiplikation) gibt, die fu¨r alle A ∈ K das folgende Diagramm kommutativ machen:
M (A)
ηM (A) M (ηA) M (M (A)) ≺ M (A) (4)
M (idA)
µA g ≺ M (A)
(5) M (idA)
M (M (M (A))) M (µA) g M (M (A))
µM (A) M (M (A)) (6)
µA
µA g M (A) 143
Beispiele Viele der o.g. Funktoren sind Monaden. Einheit bzw. Multiplikation sind wie folgt definiert: Seien A, E, S Mengen. • Listenfunktor: ηA : A → A∗ a 7→ (a)
µA : (A∗)∗ → A∗ (w1, . . . , wn) 7→ w1 · . . . · wn
• Mengenfunktor: ηA : A → P(A) a 7→ {a}
µA : P(P(A)) → P(A) S S 7→ S
• Ausnahmefunktor: ηA : A → A + E a 7→ (a, 1)
µA : (A + E) + E → A + E ((a, 1), 1) 7→ (a, 1) ((e, 2), 1) 7→ (e, 2) (e, 2) 7→ (e, 2)
144
• Leserfunktor: ηA : A → A S
µA : (AS )S → AS
a 7→ λs.a
f 7→ λs.f (s)(s)
• Schreiberfunktor: Hier muss S die Tr¨agermenge eines Monoids M = (S, ∗, e) sein. ηA : A → A × S
µA : (A × S) × S → A × S
a 7→ (a, e)
((a, s), s0) 7→ (a, s ∗ s0)
• Transitionsfunktor: ηA : A → (A × S)S
µA : ((A × S)S × S)S → (A × S)S
a 7→ λs.(a, s)
f 7→ λs.π1(f (s))(π2(f (s)))
Aufgabe Zeigen Sie, dass fu¨r diese Beispiele (4)-(6) gilt.
o
Seien A und B Mengen. Der bind-Operator = : M (A) × (A → M (B)) → M (B) wird wie folgt aus M und der Multiplikation von M abgeleitet: 145
Fu¨r alle A ∈ K und f : A → M (B), (= f ) = µB ◦ M (f ).
(7)
Intuitiv stellt man sich ein monadisches Objekt m ∈ M (A) als Berechnung vor, die eine – evtl. leere – Menge von Werten in A erzeugt. Ein Ausdruck der Form m = f wird dann wie folgt ausgewertet: Die von m berechneten Werte a ∈ A werden als Eingabe an die Berechnung f u¨bergeben und von f (a) verarbeitet. Die Betrachtung der Elemente von M (A) als Berechnungen, die eine Ausgabe in A produzieren, l¨asst sich besonders gut am Beispiel der Transitionsmonade begru¨nden. Aus der Multiplikation der Transitionsmonade und der allgemeinen Definition des bindOperators ergibt sich n¨amlich die folgende Charakterisierung des bind-Operators der Transitionsmonade: Fu¨r alle g : S → A × S und f : A → (S → B × S), g = f = µB (M (f )(g)) = µB ((f × S)S (g)) = µB (λs.(f (π1(g(s))), π2(g(s)))) = λs.π1((λs.(f (π1(g(s))), π2(g(s))))(s))(π2((λs.(f (π1(g(s))), π2(g(s))))(s))) = λs.π1(f (π1(g(s))), π2(g(s)))(π2(f (π1(g(s))), π2(g(s)))) = λs.f (π1(g(s)))(π2(g(s))).
146
Die Anwendung der Funktion (g = f ) : S → B ×S auf den Zustand s besteht demnach • in der Anwendung von g auf s, die die Ausgabe a = π1(g(s)) und den Folgezustand s0 = π2(g(s)) liefert, • und der darauffolgenden Anwendung von f (a) auf s0. Sei A, B, C Mengen, a ∈ A, m ∈ M (A), m0 ∈ M (M (A)), f : A → M (B), g : B → M (C) und h : A → B. Aus (4)-(7) erh¨alt man die folgenden Eigenschaften von =: m = ηA ηA(a) = f (m = f ) = g
= = =
m, f (a), m = λa.f (a) = g.
(8) (9) (10)
(2)-(4) und (7) implizieren die folgenden Charakterisierungen von M (h) bzw. µA: M (h)(m) = m = ηB ◦ h,
(11)
µA(m0) = m0 = idM (A). Mit dem bind-Operator werden monadische Objekte sequentiell verknu¨pft. Plusmonaden haben zusa¨tzlich eine parallele Komposition, die – analog zu η und µ – fu¨r Monaden M : Set → Set als natu¨rliche Transformation ⊕ von M × M = × ◦ ∆ ◦ M nach M definiert wird. Mit ⊕ l¨asst sich z.B. das Backtracking bzw. der Nichtdeterminismus eines monadischen Compilers realisieren (siehe Kapitel 6). 147
Die Komposition von Monaden fu¨hrt zu weiteren Monaden: Sei M eine Monade mit Einheit η, Multiplikation µ und paralleler Komposition ⊕ und S eine Menge. • Lesermonade u¨ber (M, ⊕): M 0 =def λA.M (A)S Die Morphismenabbildung von M , η, µ und ⊕ werden wie folgt auf M 0 fortgesetzt: Sei h : A → B. M 0(h) : M 0(A) → M 0(B) f 7→ M (h) ◦ f ηA : A → M 0(A) µA : M 0(M 0(A)) → M 0(A) f 7→ λs.f (s) = λg.g(s) ⊕ : M 0(A) × M 0(A) → M 0(A) (f, g) 7→ λs.f (s) ⊕ g(s)
148
• Transitionsmonade u¨ber (M, ⊕): M 0 =def λA.M (A × S)S Die Morphismenabbildung von M , η, µ und ⊕ werden wie folgt auf M 0 fortgesetzt: Sei h : A → B. M 0(h) : M 0(A) → M 0(B) f 7→ λs.f (s) = λ(a, s).η(h(a), s) ηA : A → M 0(A) a 7→ λs.η(a, s) µA : M 0(M 0(A)) → M 0(A) f 7→ λs.f (s) = λ(g, s).g(s) ⊕ : M 0(A) × M 0(A) → M 0(A) (f, g) 7→ λs.f (s) ⊕ g(s) Die Implementierung von Monaden in Haskell wird in Kapitel 15 behandelt, monadische Compiler in Kapitel 16. Letztere sind Transitionsmonaden u¨ber Ausnahmemonaden, wobei S die Menge X ∗ der zu verarbeitenden W¨orter ist. Weitere Monadenbeispiele finden sich z.B. in [28], Kapitel 7. 149
Compilermonaden Sei S eine Menge, M : SetS → SetS eine Monade mit Einheit η, bind-Operator =, natu¨rliche Transformationen ⊕ : M × M → M und set : M → P (wobei P hier den Mengenfunktor fu¨r S-sortige Mengen bezeichnet) und E = {m ∈ M (A) | setA(m) = ∅, A ∈ SetS } (“Menge der Ausnahmewerte”). M heißt Compilermonade, wenn fu¨r alle Mengen A, B, m, m0, m00 ∈ M (A), e ∈ E, f : A → M (B), h : A → B und a ∈ A Folgendes gilt: (m ⊕ m0) ⊕ m00 = m ⊕ (m0 ⊕ m00), M (h)(e) = e, M (h)(m ⊕ m0) = M (h)(m) ⊕ M (h)(m0), setA(m ⊕ m0) = setA(m) ∪ setA(m0),
(CM 1) (CM 2) (CM 3)
setA(ηA(a)) = {a}, S setB (m = f ) = {setB (f (a)) | a ∈ setA(m)}.
150
Nach Definition der Einheit η P und des bind-Operators =P der Mengenmonade P machen die letzten beiden Gleichungen set zum Monadenmorphismus. Aus ihnen folgt n¨amlich: setA ◦ ηA
=
ηAP ,
setB (m = f )
=
setA(m) =P setB ◦ f.
Außerdem erh¨alt man fu¨r alle S-sortigen Mengen A, S-sortigen Funktionen h : A → B und m ∈ M (A): S setB (M (h)(m)) = setB (m = ηB ◦ h) = {setB (ηB (h(a)) | a ∈ setA(m)} S = {{h(a)} | a ∈ setA(m)} = h(setA(m)). Satz 5.2 Listen-, Mengen- und Ausnahmefunktoren sind Compilermonaden. Beweis. Sei A eine Menge, ⊕ = · und setA : A∗ → P(A) definiert durch setA() = ∅ und setA(s) = {a1, . . . , an} fu¨r alle s = (a1, . . . , an) ∈ A+. Damit ist Star eine Compilermonade. Sei A eine Menge, ⊕ = ∪ und setA : P(A) → P(A) definiert durch idP(A). Damit ist P eine Compilermonade.
151
Seien A und E disjunkte Mengen, ⊕ = λ(m, m0).m und setA : A + E → P(A) definiert durch setA(e) = ∅ fu¨r alle e ∈ E und setA(a) = {a} fu¨r alle a ∈ A. Damit ist λA.A + E eine Compilermonade. o Monadenbasierte Parser und Compiler S Sei G = (S, BS, R) eine CFG, X = BS, Σ(G) = (S, I, F ) und M : SetS → SetS eine Compilermonade. Wie bereits in Kapitel 1 informell beschrieben wurde, soll ein Compiler fu¨r G in die als Σ(G)-Algebra A formulierten Zielsprache einen Parser fu¨r G mit der Faltung in A der vom Parser erzeugten Syntaxba¨ume komponieren: compileA G
∗ parseG
M (fold A )
= X −→ M (TΣ(G)) −→ M (A).
(12)
152
Gilt (12), dann u¨bertr¨agt sich die Kommutativit¨at von Diagramm (1) wie folgt auf die Kommutativit¨at des folgenden Diagramms: X
compileA G
∗
compileSem G
M (A) M (evaluate)
(13)
g M (Sem)
M (encode)
g M (Mach)
(12)
A M (evaluate) ◦ compileA G = M (evaluate) ◦ M (fold ) ◦ parseG (1)
M ist Funktor
=
M (evaluate ◦ fold A) ◦ parseG = M (encode ◦ fold Sem ) ◦ parseG
M ist Funktor
M (encode) ◦ M (fold Sem ) ◦ parseG = M (encode) ◦ compileSem G .
=
(12)
Da TΣ(G) initial ist, stimmt fold TΣ(G) mit der Identit¨at auf TΣ(G) u¨berein. Also gilt: parseG = idM (TΣ(G)) ◦ parseG = M (idTΣ(G) ) ◦ parseG = M (fold TΣ(G) ) ◦ parseG (12)
T
= compileGΣ(G) .
153
Da TΣ(G) eine Σ(G)-Algebra und fold A Σ(G)-homomorph ist, ist (12) ein Spezialfall folgender Bedingung: Fu¨r alle Σ(G)-Homomorphismen h : A → B, B M (h) ◦ compileA G = compileG .
(14)
T
Sei parseG = compileGΣ(G) und unparseG =def fold Word (G). Die Korrektheit von parseG l¨asst sich wie folgt formalisieren: Fu¨r alle w ∈ X ∗, P(unparseG)(setTΣ(G) (parseG(w))) ⊆ {w},
(15)
in Worten: Die Faltung jedes von parseG(w) berechneten Syntaxbaums in der Algebra Word (G) stimmt mit w u¨berein. Wegen P(unparseG) ◦ setTΣ(G) ◦ parseG = setWord (G) ◦ M (unparseG) ◦ parseG Word (G)
= setWord (G) ◦ compileG ist (15) ¨aquivalent zu
Word (G)
setWord (G)(compileG
(w)) ⊆ {w}.
(16)
(15) erlaubt die Leerheit von setTΣ(G) (parseG(w)). Der Parser parseG ist vollst¨ andig, wenn er jedes Wort w ∈ L(G) in mindestens einen Syntaxbaum fu¨r w u¨bersetzt, d.h. er erfu¨llt folgende Bedingung: Word (G)
∀ w ∈ L(G) : setWord (G)(compileG
(w)) 6= ∅.
(17) 154
Zusammenfassend ergibt sich folgende Definition: Ein generischer Compiler fu ¨ r G ist eine AlgΣ(G)-sortige Menge ∗ compileG = (compileA G : X → M (A))A∈AlgΣ(G) ,
die (14), (16) und (17) erfu¨llt. Sei W = Word (G). (16) und (17) machen setW ◦ compileW G zu der Summenextension (siehe Kapitel 2) [λw.{w}, λw.∅] : L(G) + X ∗ \ L(G) → P(X ∗).
L(G)
incL(G)
X∗ ≺
incX ∗\L(G)
X ∗ \ L(G)
setW ◦ compileW G λw.{w}
λw.∅ g ≺ P(X ∗)
U.a. ist dann die Einschr¨ankung von parseG auf L(G) rechtsinvers zu unparseG: setW ◦ M (unparseG) ◦ parseG ◦ incL(G) = setW ◦ M (fold W ) ◦ parseG ◦ incL(G) (12)
= setW ◦ compileW G ◦ incL(G) = λw.{w}. 155
Schließlich gilt (14) genau dann, wenn compileG : const(X ∗) → M ◦ U eine natu¨rliche Transformation ist, wobei const(X ∗), U : AlgΣ(G) → SetS die Funktoren bezeichnen, die • jeder Σ(G)-Algebra A die S-sortige Menge (X ∗)s∈S bzw. die Tr¨agermenge von A und • jedem Σ(G)-Homorphismus h die S-sortige Funktion (idX ∗ )s∈S bzw. die h zugrundeliegende S-sortige Funktion zuordnen.
156
6 LL-Compiler
Der in diesem Kapitel definierte generische Compiler u¨bertr¨agt die Arbeitsweise eines klassischen LL-Parsers auf Compiler mit Backtracking. Das erste L steht fu¨r seine Verarbeitung des Eingabewortes von links nach rechts, das zweite L fu¨r seine – implizite – Konstruktion einer Linksableitung. Da diese Arbeitsweise dem mit der Wurzel beginnenden schrittweisen Aufbau eines Syntaxbaums entspricht, werden LL-Parser auch top-down-Parser genannt. S Sei G = (S, BS, R) eine nicht-linksrekursive CFG, X = BS, Z = {B ∈ BS | |B| = 1}, M eine Compilermonade, errmsg : X ∗ → E, A eine Σ(G)-Algebra und s ∈ S. compileG heißt LL-Compiler, wenn ∗ compileA G,s : X → M (As )
wie folgt definiert ist: Fu¨r alle w ∈ X ∗, A (1) compileA G,s (w) = transs (w) = λ(a, w).if w = then ηA (a) else errmsg(w),
wobei fu¨r alle fu¨r alle s ∈ S ∪ BS ∗ ∗ transA s : X → M (As × X )
wie folgt definiert ist: 157
Fall 1: s ∈ BS. Fu¨r alle x ∈ X und w ∈ X ∗, transA s (xw) = if x ∈ s then ηA×X ∗ (x, w) else errmsg(xw) transA s ()
= errmsg()
Fall 2: s ∈ S. Fu¨r alle w ∈ X ∗, transA s (w)
=
M
tryrA(w).
(2)
r=(s→e)∈R
Fu¨r alle r = (s → (e1, . . . , en)) ∈ R und w ∈ X ∗, transA e1 (w) = λ(a1 , w1 ). transA (w ) = λ(a , w ). 1 2 2 e2 tryrA(w) = ... transA (w ) = λ(a , w ).η A n−1 n n A×X ∗ (fr (ai1 , . . . , aik ), wn ), en
(3)
wobei {i1, . . . , ik } = {1 ≤ i ≤ n | ei ∈ S ∪ BS \ Z}. W¨ahrend alle Summanden von (2) auf das gesamte Eingabewort w angewendet werden, wird es von tryrA Symbol fu¨r Symbol verarbeitet: Zuna¨chst wird transA e1 auf w angewendet, A A dann transA e2 auf das von transe1 nicht verarbeitete Suffix w1 von w, transe3 auf das von transA e2 nicht verarbeitete Suffix w2 von w1 , usw. 158
Gibt es 1 ≤ j ≤ n derart, dass transA ej (w) scheitert, d.h. existiert kein aus ej ableitbares Pr¨afix von w, dann u¨bergibt tryrA das gesamte Eingabewort zur Parsierung an den n¨achsten Teilcompiler tryrA0 der Argumentliste von ⊕ in (2) (Backtracking). Ist transA ¨r alle 1 ≤ i ≤ n erfolgreich, dann schließt der Aufruf von tryrA mit ei (w) jedoch fu der Anwendung von frA auf die Zwischenergebnisse ai1 , . . . , aik ∈ A. Klassische LL-Parser sind deterministisch, d.h. sie erlauben kein Backtracking, sondern setzen voraus, dass die ersten k Symbole des Eingabewortes w bestimmen, welcher der A Teilcompiler trys→e aufgerufen werden muss, um zu erkennen, dass w zu L(G)s geh¨ort. CFGs, die diese Voraussetzung erfu¨llen, heißen LL(k)-Grammatiken. Im Gegensatz zur Nicht-Linksrekursivit¨at l¨asst sich die LL(k)-Eigenschaft nicht immer durch eine Transformation der Grammatik erzwingen, auch dann nicht, wenn sie eine von einem deterministischen Kellerautomaten erkennbare Sprache erzeugt! Monadische Ausdru¨cke werden in Haskell oft in der do-Notation wiedergegeben. Sie verdeutlicht die Korrespondenz zwischen monadischen Berechnungen einerseits und imperativen Programmen andererseits. Die Ru¨cku¨bersetzung der do-Notation in die urspru¨nglichen monadischen Ausdru¨cke ist induktiv wie folgt definiert:
159
Sei m ∈ M (A), a ∈ A und m0 ∈ M (B). do m; a ← m0 = m = λa. do m0 do m; m0
= m do m0
Gleichung (10) von Kapitel 5 impliziert die Assoziativit¨at des Sequentialisierungsoperators (;), d.h. do m; m0; m00 ist gleichbedeutend mit do (do m; m0); m00 und do m; (do m0; m00). Beispiel 6.1 SAB (siehe Beispiel 4.5) Die Regeln r1 = S → aB,
r2 = S → bA,
r3 = S → ,
r4 = A → aS,
r5 = A → bAA,
r6 = B → bS,
r7 = B → aBB von SAB liefern nach obigem Schema die folgende Transitionsfunktion des LL-Compilers in eine beliebige SAB-Algebra alg: Fu¨r alle x, z ∈ {a, b} und w ∈ {a, b}∗, trans_z(xw) = if x = z then η(z,w) else errmsg(xw) trans_z() = errmsg() 160
trans_S(w) = try_r1(w) ⊕ try_r2(w) ⊕ try_r3(w) trans_A(w) = try_r4(w) ⊕ try_r5(w) trans_B(w) = try_r6(w) ⊕ try_r7(w) try_r1(w) try_r2(w) try_r3(w) try_r4(w) try_r5(w)
try_r6(w) try_r7(w)
= do (x,w) <- trans_a(w); (c,w) <- trans_B(w); = do (x,w) <- trans_b(w); (c,w) <- trans_A(w); = η(f_r3^alg,w) = do (x,w) <- trans_a(w); (c,w) <- trans_S(w); = do (x,w) <- trans_b(w); (c,w) <- trans_A(w); (d,w) <- trans_A(w); = do (x,w) <- trans_b(w); (c,w) <- trans_S(w); = do (x,w) <- trans_a(w); (c,w) <- trans_B(w); (d,w) <- trans_B(w);
η(f_r1^alg(c),w) η(f_r2^alg(c),w)
η(f_r4^alg(c),w)
η(f_r5^alg(c,d),w) η(f_r6^alg(c),w)
η(f_r7^alg(c,d),w)
o
161
Sei W = Word (G). Um sp¨ater zeigen zu k¨onnen, dass der LL-Compiler vollst¨andig ist, setzen wir voraus, dass • fu¨r alle s ∈ S, v ∈ L(G)s und w ∈ X ∗ r = (s → (e1, . . . , en)) ∈ R und fu¨r alle 1 ≤ i ≤ n vi ∈ L(G)ei mit v1 . . . vn = v und setW 2 (tryrW (w)) ⊆ setW 2 (transW s (w)) existieren.
(LLC )
Gibt es keine Anordnung der Regeln in (2), die diese Bedingung erfu¨llt, dann mu¨ssen ggf. neue Sorten fu¨r die Vorkommen einer Sorte in bestimmten Kontexten eingefu¨hrt und die Regeln von R entsprechend modifiziert werden. Beispiel 6.2 Ein solcher Fall wu¨rde z.B. in JavaLight+ auftreten (siehe Kapitel 13), wenn wir dort anstelle der drei Sorten ExpSemi , ExpBrac und ExpComm die zun¨achst naheliegende eine Sorte Exp und die folgenden Regeln verwenden wu¨rden:
162
Command Exp Sum Sumsect Prod Prodsect Factor Disjunct Conjunct Literal Actuals Actuals0
→ → → → → → → → → → → →
String = Exp; | write Exp; | . . . Sum | Disjunct Prod Sumsect ... | Factor Prodsect ... | String | String Actuals | . . . Conjunct | . . . Literal | . . . String | String Actuals | . . . () | (Actuals0 Exp) | Exp, Actuals0
(A) (B)
(C)
Ein LL-Compiler fu¨r Command wu¨rde z.B. die Eingabe z = x<=11; als syntaktisch inkorrekt betrachten, weil der Teilcompiler fu¨r Exp zun¨achst nach dem l¨angsten aus Sum ableitbaren Pr¨afix von x<=11 sucht, x als solches erkennt und deshalb das Wort x<=11 nicht bis zum Ende liest. Die Ersetzung von Regel (B) durch Exp → Disjunct|Sum l¨ost das Problem nicht, denn nun wu¨rde der Compiler z.B. die Eingabe z = x+11; als syntaktisch inkorrekt betrachten, weil der Teilcompiler fu¨r Exp zun¨achst nach dem l¨angsten aus Disjunct ableitbaren Pr¨afix 163
von x+11 sucht, x als solches erkennt und deshalb das Wort x+11 nicht bis zum Ende liest. Ersetzt man hingegen (A)-(C) durch Command ExpSemi ExpBrac ExpComm Actuals0
→ → → → →
String = ExpSemi | write ExpSemi | . . . Sum; | Disjunct; Sum) | Disjunct) Sum, | Disjunct, ExpBrac | ExpComm Actuals0
dann wird alles gut: Jetzt erzwingt das auf Sum oder Disjunct folgende Terminal (Semikolon, schließende Klammer bzw. Komma), dass die Compiler fu¨r ExpSemi , ExpBrac und ExpComm die jeweilige Resteingabe stets bis zu diesem Terminal verarbeiten. Natu¨rlich genu¨gt ein Compiler fu¨r alle drei Sorten. Man muss ihn lediglich mit dem jeweiligen Terminal parametrisieren (siehe Java2.hs). o Satz 6.4 transA ist wohldefiniert. Beweis durch Noethersche Induktion. Da S endlich und G nicht linksrekursiv ist, ist die folgende Ordnung > auf S ∪ BS Noethersch, d.h., es gibt keine unendlichen Ketten s1 > s2 > s3 > · · · : s > s0
⇔def
+
∃ w ∈ (S ∪ BS)∗ : s →G s0w. 164
Wir erweitern > zu einer ebenfalls Noetherschen Ordnung auf X ∗ × (S ∪ BS): (v, s) (w, s0)
⇔def
|v| > |w| oder (|v| = |w| und s > s0).
Nach Definition von transs(w) gibt es r = (s → e1 . . . en) ∈ R mit A A A transA s (w) = . . . transe1 (w) . . . transe2 (w1 ) . . . transen (wn−1 ) . . .
Da w1, . . . , wn echte Suffixe von w sind, gilt s > e1 und |w| > |wi| fu¨r alle 1 ≤ i < n, also (w, s) (w, e1) und (w, s) (wi−1, ei) fu¨r alle 1 < i ≤ n. Die rekursiven Aufrufe von transA haben also bzgl. kleinere Argumente. Folglich terminiert jeder Aufruf von transA, m.a.W.: transA ist wohldefiniert.
o
Der Beweis, dass compileG Gleichung (15) von Kapitel 5 erfu¨llt, verwendet die folgenden Zusammenh¨ange zwischen einer Monade M und ihrem bind-Operator: Lemma 6.5 Sei M : SetS → SetS eine Monade und h : A → B eine S-sortige Funktion. Fu¨r alle m ∈ M (A), f : A → M (A) und g : B → M (B), M (h)(m = f ) = m = M (h) ◦ f, M (h)(m) = g = m = g ◦ h.
(4) (5) 165
Sei Σ eine Signatur, m1, . . . , mn ∈ M (A), h : A → B Σ-homomorph, fu¨r alle 1 ≤ i ≤ n, fi : A → · · · → A → M (A),
gi : B → · · · → B → M (B),
und t ∈ TΣ(V ) mit var(t) = {x1, . . . , xn}, fi(a1) . . . (ai−1) = mi fi+1(a1) . . . (ai−1), fn+1(a1) . . . (an) = ηA(fa∗(t)) fu¨r alle a = (a1, . . . , an) ∈ A und gi(b1) . . . (bi−1) = M (h)(mi) gi+1(b1) . . . (bi−1), gn+1(b1) . . . (bn) = ηB (gb∗(t)) fu¨r alle b = (b1, . . . , bn) ∈ B, wobei fa : V → A und gb : V → B durch fa(xi) = ai und gb(xi) = bi fu¨r alle 1 ≤ i ≤ n definiert sind. Dann gilt M (h)(f1) = g1.
(6)
Beweis von (4). M (h)(m = f ) (10) in Kap. 5
=
=
(m = f ) = ηB ◦ h
m = λa.f (a) = ηB ◦ h
(11) in Kap. 5
=
(11) in Kap. 5
m = λa.M (h)(f (a)) = m = M (h) ◦ f. 166
Beweis von (5). M (h)(m) = g = (m = ηB ◦ h) = g (9) in Kap. 5
=
(10) in Kap. 5
=
m = λa.ηB (h(a)) = g
m = λa.g(h(a)) = m = g ◦ h.
Beweis von (6). (4)
M (h)(f1) = M (h)(m1 f2) = m1 = M (h) ◦ f2 = m1 = λa1.M (h)(f2(a1)) (4)
= m1 = λa1.M (h)(m2 = f3(a1)) = m1 = λa1.m2 = M (h) ◦ f3(a1) = m1 = λa1.m2 = λa2.M (h)(f3(a1)(a2)) = · · · = m1 = λa1.m2 = · · · = λan.M (h)(fn+1(a1) . . . (an)) = m1 = λa1.m2 = · · · = λan.M (h)(ηA(fa∗(t))) = m1 = λa1.m2 = · · · = λan.ηB (h(fa∗(t))) = m1 = λa1.m2 = · · · = λan.ηB ((h ◦ fa)∗(t)) h◦fa =gh(a)
=
∗ m1 = λa1.m2 = · · · = λan.ηB (gh(a) (t))
(7)
167
(5)
g1 = M (h)(m1) = g2 = m1 = g2 ◦ h = m1 = λa1.g2(h(a1)) = m1 = λa1.M (h)(m2) = g3(h(a1)) = m1 = λa1.m2 = g3(h(a1)) ◦ h = m1 = λa1.m2 = λa2.g3(h(a1))(h(a2)) = · · · = m1 = λa1.m2 = · · · = λan.gn+1(h(a1)) . . . , (h(an)) ∗ = m1 = λa1.m2 = · · · = λan.ηB (gh(a) (t))
(8) o
Aus (7) und (8) folgt (6). Satz 6.6
Sei h : A → B ein Σ(G)-Homomorphismus. Der oben definierte LL-Compiler erfu¨llt Gleichung (14) aus Kapitel 5, also A compileB G = M (h) ◦ compileG .
(9)
Beweis. Sei transB = M (h × X ∗) ◦ transA.
(10)
Dann gilt (9): Fu¨r alle w ∈ X ∗, (1)
B compileB G (w) = trans (w) = λ(b, w).if w = then ηB (b) else errmsg(w) 168
(10)
= M (h × X ∗)(transA(w)) = λ(b, w).if w = then ηB (b) else errmsg(w)
(11) in Kap. 5
=
(transA(w) = (ηB×X ∗ ◦ (h × X ∗))) = λ(b, w).if w = then ηB (b) else errmsg(w)
= (transA(w) = λ(a, w).ηB×X ∗ (h(a), w)) = λ(b, w).if w = then ηB (b) else errmsg(w) (10) in Kap. 5
=
transA(w) = λ(a, w).ηB×X ∗ (h(a), w) = λ(b, w).if w = then ηB (b) else errmsg(w)
(9) in Kap. 5
=
transA(w) = λ(a, w).if w = then ηB (h(a)) else errmsg(w)
(CM 1)
= transA(w) = λ(a, w).if w = then ηB (h(a)) else M (h)(errmsg(w))
(9),(11) in Kap. 5
=
transA(w) = λ(a, w).if w = then ηA(a) = ηB ◦ h else errmsg(w) = ηB ◦ h
= transA(w) = λ(a, w).(if w = then ηA(a) else errmsg(w)) = ηB ◦ h (10) in Kap. 5
=
(transA(w) = λ(a, w).if w = then ηA(a) else errmsg(w)) = ηB ◦ h
= compileA G (w) = ηB ◦ h
(11) in Kap. 5
=
M (h)(compileA G (w)). 169
Beweis von (10) durch Noethersche Induktion bzgl. der im Beweis von Satz 6.4 definierten Ordnung : Fall 1: s ∈ BS. Fu¨r alle x ∈ X und w ∈ X ∗, ∗ M (h × X ∗)(transA s (xw)) = if x ∈ s then M (h × X )(ηA×X ∗ (x, w))
else M (h × X ∗)(errmsg(xw)) η ist nat. Transformation, (CM 1 )
=
(h×X ∗ )(x,w)=(h(x),w)=(x,w)
=
if x ∈ s then ηB×X ∗ ((h × X ∗)(x, w)) else errmsg(xw)
if x ∈ s then ηB×X ∗ (x, w) else errmsg(xw) = transB s (xw), (CM 1)
∗ B M (h × X ∗)(transA s ()) = M (h × X )(errmsg()) = errmsg() = transs ().
Fall 2: s ∈ S. Sei r = (s → w0) ∈ R. Fu¨r alle w ∈ X ∗, M (h × X ∗)(tryrA(w)) A transe1 (w) = λ(a1, w1). (3) . ) = M (h × X ∗)( .. transA (w ) = λ(a , w ).η A ∗ (f (a , . . . , a ), w ) n−1 n n A×X j j n en r 1 k A transe1 (w) = λx1. . ∗ = M (h × X )( .. ) transA (w ) = λx .η A ∗ (f (π (x ), . . . , π (x )), π (x )) en
n−1
n
A×X
r
1
j1
1
jk
2
n
170
M (h × X ∗)(transA e1 (w)) = λx1 . . .. 6.5 (6) = ) ∗ A M (h × X )(trans (w )) n−1 en B ∗ = λxn.ηB×X (fr (π1(xj1 ), . . . , π1(xjk )), π2(xn)) ∗ A M (h × X )(transe1 (w)) = λ(b1, w1). . = .. M (h × X ∗)(transA (w )) = λ(b , w ).η B ∗ (f (b , . . . , b ), w ) n−1 n n B×X j1 jk n r en B transe1 (w) = λ(b1, w1). ind. hyp. . .. = transB (w ) = λ(b , w ).η B ∗ (f (b , . . . , b ), w ) en
n−1
n
n
B×X
r
j1
jk
(3)
= tryrB (w).
n
(11)
Daraus folgt (10): (2)
∗ A M (h × X ∗)(transA s (w)) = M (h × X )(⊕r=(s→e)∈R tryr (w)) (CM 2)
(11)
(2)
= ⊕r=(s→e)∈R M (h × X ∗)(tryrA(w)) = ⊕r=(s→e)∈R tryrB (w) = transB s (w). o 171
Lemma 6.7 Sei M : SetS → SetS eine Compilermonade, f : AN → A und m1, . . . , mn ∈ M (A). setA(m1 = λa1. . . . mn = λan.ηA(f (a1, . . . , an))) V = {f (a1, . . . , an) | ni=1 ai ∈ setA(mi)}. Beweis. setA(m1 = λa1. . . . mn = λan.ηA(f (a1, . . . , an))) S = {setA(m2 = λa2. . . . mn = λan.ηA(f (a1, . . . , an))) | a1 ∈ setA(m1)} S S = { {setA(m3 = λa3. . . . mn = λan.ηA(f (a1, . . . , an))) | a2 ∈ setA(m2)} | a1 ∈ setA(m1)} =
S
{setA(m3 = λa3. . . . mn = λan.ηA(f (a1, . . . , an))) | a2 ∈ setA(m2), a1 ∈ setA(m1)}
= ... S V = {setA(ηA(f (a1, . . . , an))) | ni=1 ai ∈ setA(mi)} V S = {{f (a1, . . . , an)} | ni=1 ai ∈ setA(mi)} V = {f (a1, . . . , an) | ni=1 ai ∈ setA(mi)}. o
172
Satz 6.8 Der oben definierte LL-Compiler ist korrekt, d.h. fu¨r alle w ∈ X ∗ gilt: Word (G)
setWord (G)(compileG
(w)) ⊆ {w}
(12)
(siehe (16) in Kapitel 5). Beweis. Sei W = Word (G). Fu¨r alle w ∈ X ∗ und s ∈ S ∪ BS gelte folgende Bedingung: 0 ∀ (v, v 0) ∈ setW 2 (transW s (w)) : vv = w.
(13)
Dann gilt auch (14): setW (compileW G,s (w)) (1)
0 0 0 = setW (transW s (w) = λ(v, v ).if v = then ηW (v) else errmsg(v )) S = {setW (if v 0 = then ηW (v) else errmsg(v 0)) | (v, v 0) ∈ setW 2 (transW s (w))} (13) S ⊆ {setW (if v 0 = then ηW (v) else errmsg(v 0)) | vv 0 = w} S = {if v 0 = then setW (ηW (v)) else setW (errmsg(v 0)) | vv 0 = w} S = {if v 0 = then {v} else ∅ | vv 0 = w} = {w}.
Beweis von (15) durch Noethersche Induktion bzgl. der im Beweis von Satz 6.4 definierten Ordnung . 173
Fall 1: s ∈ BS. Sei x ∈ X, w ∈ X ∗ und (v, v 0) ∈ setW 2 (transW s (xw)). Dann gilt (v, v 0) ∈ setW 2 (if x ∈ s then ηW 2 (x, w) else errmsg(xw)) = if x ∈ s then setW 2 (ηW 2 (x, w)) else setW 2 (errmsg(xw)) = if x ∈ s then {(x, w)} else ∅, also vv 0 = xw. Fall 2: s ∈ S. Sei w ∈ X ∗ und (v, v 0) ∈ setW 2 (transW s (w)). Dann gilt L (2) W (v, v 0) ∈ setW 2 (transW (w))) = set ( 2 W s r=(s→e)∈R tryr (w)) (CM 3) S W ⊆ r=(s→e)∈R setW 2 (tryr (w)). Also gibt es r = (s → e1 . . . en) ∈ R mit (v, v 0) ∈ setW 2 (tryrW (w)). Sei w0 = w. Dann gilt (v, v 0) ∈ setW 2 (tryrW (w0)) (3)
= setW 2 (transW e1 (w0 ) = λ(v1 , w1 ). ...
W transW en (wn−1 ) = λ(vn , wn ).ηW 2 (fr (vj1 , . . . , vjk ), wn )) V Lemma 6 .7 = {(frW (vj1 , . . . , vjk ), wn) | ni=1(vi, wi) ∈ setW 2 (transW ei (wi−1 ))} V = {(v1 . . . vn, wn) | ni=1(vi, wi) ∈ setW 2 (transW (14) ei (wi−1 ))}. 174
V Also gibt es v1, . . . , vn, w1, . . . , wn ∈ X ∗ mit ni=1(vi, wi) ∈ setW 2 (transW ei (wi−1 )), V n v = v1 . . . vn und v 0 = wn. Nach Induktionsvoraussetzung folgt i=1 viwi = wi−1, also vv 0 = v1 . . . vnwn = w0 = w.
o
Satz 6.9 Der oben definierte LL-Compiler ist vollst¨andig, d.h. fu¨r alle w ∈ L(G) gilt: Word (G)
setW (compileG
(w)) 6= ∅.
(15)
Beweis. Sei W = Word (G). Fu¨r alle s ∈ S ∪ BS, v ∈ L(G)s und w ∈ X ∗ gelte: (v, w) ∈ setW 2 (transW s (vw)).
(16)
Dann gilt auch (15): Sei w ∈ L(G). Word (G)
setW (compileG,s
(w))
(1)
0 0 0 = setW (transW s (w) = λ(v, v ).if v = then ηW (v) else errmsg(v )) S = {setW (if v 0 = then ηW (v) else errmsg(v 0)) | (v, v 0) ∈ setW 2 (transW s (w))} S = {setW (ηW (v)) | (v, ) ∈ setW 2 (transW s (w))} ∪ S 0 {setW (errmsg(v 0)) | (v, v 0) ∈ setW 2 (transW s (w)), v 6= } S S 0 = {{v} | (v, ) ∈ setW 2 (transW (w))} ∪ {∅ | (v, v 0) ∈ setW 2 (transW s s (w)), v 6= }
= {v | (v, ) ∈
setW 2 (transW s (w))}
(16)
6= ∅. 175
Beweis von (16) durch Noethersche Induktion bzgl. der im Beweis von Satz 6.4 definierten Ordnung . Fall 1: s ∈ BS. Dann ist v ∈ X und damit setW 2 (transW s (vw)) = setW 2 (ηW 2 (v, w)) = {(v, w)}. Fall 2: s ∈ S. Wegen (LLC ) gibt es r = (s → (e1, . . . , en)) ∈ R und fu¨r alle 1 ≤ i ≤ n vi ∈ L(G)ei mit v1 . . . vn = v und setW 2 (tryrW (w)) ⊆ setW 2 (transW s (w)).
(17)
Nach Induktionsvoraussetzung folgt n ^ (vi, vi+1 . . . vnw) ∈ setW 2 (transW ei (vi . . . vn w)).
(18)
i=1
Mit wi =def vi+1 . . . vnw fu¨r alle 0 ≤ i ≤ n ist (18) a¨quivalent zu: n ^ (vi, wi) ∈ setW 2 (transW ei (wi−1 )).
(19)
i=1
Aus (14), (17) und (19) folgt schließlich (v, w) = (v1 . . . vn, wn) ∈ setW 2 (tryrW (w0)) = setW 2 (tryrW (w)) ⊆ setW 2 (transW s (w)). o 176
7 LR-Compiler
LR-Compiler lesen ein Wort w wie LL-Compiler von links nach rechts, konstruieren dabei jedoch eine Rechtsreduktion von w, d.h. die Umkehrung einer Rechtsableitung. Da dies dem schrittweisen, mit den Bl¨attern beginnenden Aufbau eines Syntaxbaums entspricht, werden LR-Compiler auch bottom-up-Compiler genannt. ¨ Im Gegensatz zum LL-Compiler ist die entsprechende Ubersetzungsfunktion eines LRCompilers iterativ. Die Umkehrung der Ableitungsrichtung (Reduktion statt Ableitung) macht es m¨oglich, die Compilation durch einen Automaten, also eine iterativ definierte Funktion, zu steuern. W¨ahrend LL-Compiler keine linksrekursiven CFGs verarbeiten k¨onnen, sind LR-Compiler auf LR(k)-Grammatiken beschr¨ankt (s.u.). Sei G = (S, BS, R) eine CFG und X =
S
BS.
Wir setzen jetzt voraus, dass S das Symbol start enth¨alt und dieses nicht auf der rechten Seite einer Regel von R auftritt.
177
¨ Ablauf der LR-Ubersetzung auf Ableitungsb¨ aumen start
φ
ε
vw
Ableitungsbäume Eingabe
v
w
Ableitungsbäume Eingabe
vw
ε
Ableitungsbaum Eingabe
G heißt LR(k)-Grammatik, falls das Vorauslesen von k noch nicht verarbeiteten Eingabesymbolen genu¨gt, um zu entscheiden, ob ein weiteres Zeichen gelesen oder eine Reduktion durchgefu¨hrt werden muss, und, wenn ja, welche. Außerdem mu¨ssen die Basismengen von BS paarweise disjunkt sein. Beispiel 7.1 Die CFG G = ({S, A}, {∗, b}, {S → A, A → A ∗ A, A → b}) ist fu¨r kein k eine LR(k)-Grammatik.
178
Nach der Reduktion des Pra¨fixes b ∗ b des Eingabewortes b ∗ b ∗ b zu A ∗ A liegt ein shiftreduce-Konflikt vor. Soll man A ∗ A mit der Regel A → A ∗ A zu A reduzieren oder erst die Resteingabe ∗b lesen und dann b mit A → b zu A reduzieren? Die Resteingabe determiniert liefert keine Antwort. o first- und follow-Wortmengen Sei CS = BS ∪ Z, k > 0, α ∈ (S ∪ BS)∗ und s ∈ S. ∗
∗
first k (α) = {β ∈ CS k | ∃ γ ∈ CS ∗ : α →G βγ} ∪ {β ∈ CS
-> -> -> ->
prog $end statems exp . statems assign ; | ID : = exp exp + exp | exp * exp | (exp) | NUMBER | ID
So besteht z.B. der Zustand 0 aus den beiden Tripeln ($accept, , $end) und (statems, , ). Die beim Lesen eines Punktes im Zustand 0 ausgefu¨hrte Aktion ist eine Reduktion mit Regel 3, also mit statems → . Der Folgezustand von 0 ist bei Eingabe von prog bzw. statems der Zustand 1 bzw. 2. Link zur graphischen Darstellung des Parserlaufs auf dem Eingabewort ID : = NUM ; ID : = ID + NUM ; NUM * ID + ID . Den Sonderzeichen entsprechen in der input-Spalte des Parserlaufs und den u.a. Tabellen passende Wortsymbole. Die Knoten der Syntaxb¨aume sind wie in Beispiel 7.3 mit Regeln markiert. 194
195
196
Im Folgenden sind die goto- bzw. Aktionstabelle noch einmal getrennt wiedergegeben. op (open) und cl (close) bezeichnen eine ¨offnende bzw. schließende Klammer. end steht fu¨r das leere Wort . Wieder wird auf den Pfeil zwischen linker und rechter Seite einer Regel verzichtet.
197
198
199
Im Folgenden werden die Regeln von G um C-Code erweitert, der eine Σ(G)-Algebra implementiert, die dem Zustandsmodell von JavaLight (siehe 11.5) ¨ahnelt.
200
o
201
LR(k)
LALR(k) SLR(k)
LL(k)
eindeutige kf. Gramm.
A
aAa|a
nicht LR(k)
S B E C D
aB|eE Cc|Dd Cd|Dc b b
LR(1), nicht LALR(1)
S B C D
Ba|aCd Cc|Dd b b
LALR(1), nicht SLR(k)
S A B C D E
aA|bB Ca|Db Cc|Da E E ε
LL(1), nicht LALR(k)
Hierarchie der CFG-Klassen Zur Definition von LL(k)-Grammatiken verweisen wir auf die einschl¨agige Literatur. Kurz gesagt, sind das diejenigen nicht-linksrekursiven CFGs, deren LL-Parser ohne Backtracking auskommen. 202
eindeutige kontextfreie
det. kf. Sprachen =LR(1)-Spr. =SLR(1)-Spr. =LALR(1)-Spr. LL(k)Spr. Sprachen Hierarchie der entsprechenden Sprachklassen Fu¨r jeden Grammatiktyp T bedeutet die Formulierung L ist eine T -Sprache lediglich, dass eine T -Grammatik existiert, die L erzeugt.
203
Wa¨hrend der LL-Compiler von Kapitel 6 – nach Beseitigung von Linksrekursion – jede kontextfreie Grammatik verarbeitet, selbst dann, wenn sie mehrdeutig ist, zeigt die obige Grafik, dass die Forderung, dabei ohne Backtracking auszukommen, die Klasse der kompilierbaren ¨ Sprachen erheblich einschr¨ankt: Unter dieser Bedingung ist die bottom-up-Ubersetzung offenbar m¨achtiger als die top-down-Compilation. Umgekehrt w¨are es den Versuch wert (z.B. in Form einer Bachelorarbeit), in Anlehnung an den obigen Compiler fu¨r LR(1)-Grammatiken einen bottom-up-Compiler mit Backtracking zu entwickeln. Da die Determinismusforderung wegfiele, br¨auchten wir keinen Lookahead beim Verarbeiten der Eingabe, womit die Zusta¨nde generell nur aus Tripeln bestu¨nden – wie im Beispiel 7.4.
204
8 Haskell: Typen und Funktionen
Die Menge 1 wird in Haskell unit-Typ genannt und mit () bezeichnet. () steht auch fu¨r das einzige Element von 1. Die Menge 2 entspricht dem Haskell-Typ Bool . Ihre beiden Elemente 0 und 1 werden mit False bzw. True bezeichnet. Alle Typen von Haskell sind aus Standardtypen wie Bool , Int oder F loat, Typvariablen sowie Typkonstruktoren wie × (Produkt), + (Summe oder disjunkte Vereinigung) oder → (Funktionsmenge) aufgebaut. Jeder Typ bezeichnet eine Menge, jeder Typkonstruktor eine Funktion auf Mengen von Mengen. Typnamen beginnen stets mit einem Großbuchstaben, Typvariablen mit einem Kleinbuchstaben. Typvariablen stehen fu¨r Mengen, Individuenvariablen fu¨r Elemente einer Menge. Beide mu¨ssen mit einem Kleinbuchstaben beginnen. Das (kartesische) Produkt A1 × · · · × An von Mengen A1, . . . , An wird in Haskell wie seine Elemente, die n-Tupel (a1, . . . , an), mit runden Klammern und Kommas notiert: (A1, . . . , An).
205
Die Summe oder disjunkte Vereinigung SumAn von Mengen A1, . . . , An wird durch einen (Haskell-)Datentyp implementiert (siehe Kapitel 10). Funktionen werden benannt und durch rekursive Gleichungen definiert (s.u.) oder als λAbstraktion λp.e (Haskell-Notation: \p -> e) dargestellt, wobei p ein Muster fu¨r die m¨oglichen Argumente (Parameter) von λp.e ist, z.B. p = (x, (y, z)). Muster bestehen aus Individuenvariablen und (Individuen-)Konstruktoren. Jede Variable kommt in einem Muster h¨ochstens einmal vor. (Die λ-Abstraktionen von Kapitel 2 haben nur Variablen als Muster.) Der “Rumpf” e der λ-Abstraktion λp.e ist ein aus beliebigen Funktionen und Variablen zusammengesetzter Ausdruck. Ein Ausdruck der Form f (e) heißt Funktionsapplikation (auch: Funktionsanwendung oder -aufruf). Ist f eine λ-Abstraktion, dann nennt man f (e) eine λ-Applikation. Die λ-Applikation (λp.e)(e0) is auswertbar, wenn der Ausdruck e0 das Muster p matcht. Beim Matching werden die Variablen von p in e durch Teilausdru¨cke von e0 ersetzt. Die Auswertung einer Applikation von e wie z.B. (λ(x, y).x ∗ y + 5 + x)(7, 8), besteht in der Bildung der Instanz 7 ∗ 8 + 5 + 7 der λ-Abstraktion λ(x, y).x ∗ y + 5 + x und deren anschließender Auswertung: (λ(x, y).x ∗ y + 5 + x)(7, 8) ; 7 ∗ 8 + 5 + 7 ; 56 + 5 + 7 ; 68
206
Die ghci-Befehle :type \(x,y)->x*y+5+x
bzw.
:type (\(x,y)->x*y+5+x)(7,8)
liefern die Typen Num a => (a,a) -> a
bzw.
Num a => a
der λ-Abstraktion λ(x, y).x ∗ y + 5 + x bzw. λ-Applikation (λ(x, y).x ∗ y + 5 + x)(7, 8). Backslash (\) und Pfeil (->) sind offenbar die Haskell-Notationen des Symbols λ bzw. des Punktes einer λ-Abstraktion. Num ist die Typklasse fu¨r numerische Typen. Allgemein werden Typklassen in Kapitel 5 behandelt. Link zur schrittweisen Auswertung der λ-Applikation (λ(x, y).x ∗ y + 5 + x)(7, 8) Der Redex, d.i. der Teilausdruck, der im jeweils n¨achsten Schritt ersetzt wird, ist rot gef¨arbt. Das Redukt, d.i. der Teilausdruck, durch den der Redex ersetzt wird, ist gru¨n gef¨arbt. Link zur schrittweisen Auswertung der λ-Applikation (λx.x(true, 4, 77) + x(false, 4, 77))(λ(x, y, z).if x then y + 5 else z ∗ 6)
207
Eine geschachelte λ-Abstraktion λp1.λp2. . . . .λpn.e kann durch λp1 p2 . . . pn.e abgeku¨rzt werden. Sie hat einen Typ der Form t1 → (t2 → . . . (tn → t) . . . ), wobei auf diese Klammerung verzichtet werden kann, weil Haskell Funktionstypen automatisch rechtsassoziativ klammert. Anstelle der Angabe eines λ-Ausdrucks kann eine Funktion benannt und dann mit f mit Hilfe von Gleichungen definiert werden: f = \p -> e
ist ¨aquivalent zu
f p = e (applikative Definition)
Funktionen, die andere Funktionen als Argumente oder Werte haben, heißen Funktionen h¨ oherer Ordnung. Der Typkonstruktor → ist rechtsassoziativ. Also ist die Deklaration (+) :: Int -> (Int -> Int)
ist ¨aquivalent zu
(+) :: Int -> Int -> Int
Die Applikation einer Funktion ist linksassoziativ. Also ist ((+) 5) 6
ist ¨aquivalent zu
(+) 5 6
(+) ist zwar als Pr¨afixfunktion deklariert, kann aber auch infix verwendet werden. Dann entfallen die runden Klammern um den Infixoperator: 5 + 6
ist ¨aquivalent zu
(+) 5 6 208
Das Gleiche gilt fu¨r jede Funktion f eines Typs der Form A → B → C. Besteht f aus Sonderzeichen, dann wird f bei der Pr¨afixverwendung in runde Klammern gesetzt, bei der Infixverwendung nicht. Beginnt f mit einem Kleinbuchstaben und entha¨lt f keine Sonderzeichen, dann wird f bei der Infixverwendung in Akzentzeichen gesetzt, bei der Pr¨afixverwendung nicht: mod :: Int -> Int -> Int mod 9 5 ist ¨aquivalent zu
9 `mod` 5
Die Infixnotation wird auch verwendet, um die in f enthaltenen Sektionen (Teilfunktionen) des Typs A → C bzw. B → C zu benennen. Z.B. sind die folgenden Sektionen Funktionen des Typs Int -> Int, w¨ahrend (+) und mod den Typ Int -> Int -> Int haben. (+5) (9`mod`)
ist ¨aquivalent zu ist ¨aquivalent zu
(+) 5 mod 9
ist ¨aquivalent zu ist ¨aquivalent zu
\x -> x+5 \x -> 9`mod`x
Eine Sektion wird stets in runde Klammern eingeschlossen. Die Klammern geh¨oren zum Namen der jeweiligen Funktion.
209
Der Applikationsoperator ($) :: (a -> b) -> a -> b f $ a = f a fu¨hrt die Anwendung einer gegebenen Funktion auf ein gegebenes Argument durch. Sie ist rechtsassoziativ und hat unter allen Operationen die niedrigste Priorit¨at. Daher kann durch Benutzung von $ manch schließende Klammer vermieden werden: f1 $ f2 $ ... $ fn a
;
f1 (f2 (...(fn a)...)))
Demgegenu¨ber ist der Kompositionsoperator (.) :: (b -> c) -> (a -> b) -> a -> c (g . f) a = g (f a) zwar auch rechtsassoziativ, hat aber – nach den Pr¨afixoperationen – die h¨ochste Priorit¨at. (f1 . f2 . ... . fn) a
;
f1 (f2 (...(fn a)...)))
210
U.a. benutzt man den Kompositionsoperator, um in einer applikativen Definition Argumentvariablen einzusparen. So sind die folgenden drei Definitionen einer Funktion f : a → b → c a¨quivalent zueinander: f a b = g (h a) b f a = g (h a) f = g . h Welchen Typ hat hier g bzw. h? Auch die folgenden drei Definitionen einer Funktion f : a → b sind ¨aquivalent zueinander: f a = g . h a f a = (g.) (h a) f = (g.) . h Welchen Typ hat hier g bzw. h?
211
Monomorphe und polymorphe Typen Ein Typ ohne Typvariablen heißt monomorph. Ein Typ mit Typvariablen wie z.B. a -> Int -> b heißt polymorph. Eine Funktion mit monomorphem oder polymorphem Typ heißt monomorphe bzw. polymorphe Funktion. Eine Funktion heißt mono- bzw. polymorph, wenn ihr Typ mono- bzw. polymorph ist. Ein Typ u heißt Instanz eines Typs t, wenn u durch Ersetzung der Typvariablen von t aus t entsteht. Typvariablen stehen fu¨r Mengen, Individuenvariablen stehen fu¨r Elemente einer Menge. Sie mu¨ssen ebenfalls mit einem Kleinbuchstaben beginnen. Eine besondere Individuenvariable ist der Unterstrich (auch Wildcard genannt). Er darf nur auf der linken Seite einer Funktionsdefinition vorkommen, was zur Folge hat, dass er fu¨r einen Teil eines Argumentmusters der gerade definierten Funktion steht, der ihre Werte an Stellen, die das Muster matchen, nicht beeinflusst (siehe Beispiele im na¨chsten Kapitel). Die oben definierten Funktionen ($) und (.) sind demnach polymorph.
212
Weitere polymorphe Funktionen ho ¨herer Ordnung Identit¨at
id :: a -> a id a = a id = \a -> a
¨aquivalente Definition
const :: a -> b -> a const a b = a const a = \b -> a const = \a -> \b -> a const = \a b -> a
konstante Funktion ¨aquivalente Definitionen
update :: Eq a => (a -> b) -> a -> b -> a -> b update f a b a' = if a == a' then b else f a'
update f
:: a -> b -> a -> b
update f a
:: b -> a -> b
Funktionsupdate (nicht im Prelude)
¨aquivalente Schreibweisen update(f) update(f)(a) (update f) a
213
update f a b
:: a -> b
update(f)(a)(b) ((update f) a) b
update f a b a' :: b
update(f)(a)(b)(a') (((update f) a) b) a'
flip :: (a -> b -> c) -> b -> a -> c flip f b a = f a b
Vertauschung der Argumente
flip mod 11 ist ¨aquivalent zu
(`mod` 11) (s.o.)
curry :: ((a,b) -> c) -> a -> b -> c curry f a b = f (a,b)
Kaskadierung (Currying)
uncurry :: (a -> b -> c) -> (a,b) -> c uncurry f (a,b) = f a b
Dekaskadierung
214
9 Haskell: Listen
Sei A eine Menge. Die Menge A∗ (siehe Kapitel 2) wird in Haskell mit eckigen Klammern notiert, also durch [A] — ebenso wie ihre Elemente: Fu¨r (a1, . . . , an) ∈ A∗ schreibt man [a1, . . . , an]. Eine n-elementige Liste kann extensional oder als funktionaler Ausdruck dargestellt werden: [a1, . . . , an]
ist ¨aquivalent zu
a1 : (a2 : (. . . (an : []) . . . ))
Die Konstante [] (leere Liste) vom Typ [A] und die Funktion (:) (Anfu¨gen eines Elementes von A ans linke Ende einer Liste) vom Typ A → [A] → [A] heißen Konstruktoren, weil sie nicht wie andere Funktionen Werte berechnen, sondern dazu dienen, die Elemente eines Typs aufzubauen. Auch werden sie ben¨otigt, um die Zugeh¨origkeit eines Elementes eines Summentyps zu einem bestimmten Summanden wiederzugeben (siehe Kapitel 4). Die Klammern in a1 : (a2 : (. . . (an : []) . . . )) k¨onnen weggelassen werden, weil der Typ von (:) keine andere Klammerung zul¨asst. Die durch mehrere Gleichungen ausgedru¨ckten Fallunterscheidungen bei den folgenden Definitionen von Funktionen auf Listen ergeben sich aus verschiedenen Mustern der Funktionsargumente bzw. Bedingungen an die Argumente (Boolesche Ausdru¨cke hinter |).
215
Seien x, y, s Individuenvariablen. s ist ein Muster fu¨r alle Listen, [] das Muster fu¨r die leere Liste, [x] ein Muster fu¨r alle einelementigen Listen, x : s ein Muster fu¨r alle nichtleeren Listen, x : y : s ein Muster fu¨r alle mindestens zweielementigen Listen, usw. length :: [a] -> Int length (_:s) = length s+1 length _ = 0
length [3,44,-5,222,29] ; 5
Link zur schrittweisen Auswertung von length [3,44,-5,222,29] head :: [a] -> a head (a:_) = a
head [3,2,8,4] ; 3
tail :: [a] -> [a] tail (_:s) = s
tail [3,2,8,4] ; [2,8,4]
(++) :: [a] -> [a] -> [a] (a:s)++s' = a:(s++s') _++s = s
[3,2,4]++[8,4,5] ; [3,2,4,8,4,5]
216
(!!) :: [a] -> Int -> a (a:_)!!0 = a (_:s)!!n | n > 0 = s!!(n-1)
[3,2,4]!!1 ; 2
init :: [a] -> [a] init [_] = [] init (a:s) = a:init s
init [3,2,8,4] ; [3,2,8]
last :: [a] -> a last [a] = a last (_:s) = last s
last [3,2,8,4] ; 4
take take take take
:: Int -> [a] -> [a] take 3 [3,2,4,8,4,5] ; [3,2,4] 0 _ = [] n (a:s) | n > 0 = a:take (n-1) s _ [] = []
drop drop drop drop
:: Int -> [a] -> [a] drop 4 [3,2,4,8,4,5] ; [4,5] 0 s = s n (_:s) | n > 0 = drop (n-1) s _ [] = [] 217
Funktionslifting auf Listen map :: (a -> b) -> [a] -> [b] map f (a:s) = f a:map f s map _ _ = [] map (+1) [3,2,8,4] ; [4,3,9,5] map ($ 7) [(+1),(+2),(*5)] ; [8,9,35] map ($ a) [f1,f2,...,fn] ; [f1 a,f2 a,...,fn a] Link zur schrittweisen Auswertung von map(+3)[2..9] zipWith :: (a -> b -> c) -> [a] -> [b] -> [c] zipWith f (a:s) (b:s') = f a b:zipWith f s s' zipWith _ _ _ = [] zipWith (+) [3,2,8,4] [8,9,35] ; [11,11,43] zip :: [a] -> [b] -> [(a,b)] zip = zipWith (,) zip [3,2,8,4] [8,9,35] ; [(3,8),(2,9),(8,35)] 218
Strings sind Listen von Zeichen Strings werden als Listen von Zeichen betrachtet, d.h. die Typen String und [Char] sind identisch. Z.B. haben die folgenden Booleschen Ausdru¨cke den Wert True: "" == [] "H" == ['H'] "Hallo" == ['H','a','l','l','o'] Also sind alle Listenfunktionen auf Strings anwendbar. words :: String -> [String] und unwords :: [String] -> String zerlegen bzw. konkatenieren Strings, wobei Leerzeichen, Zeilenumbru¨che ('\n') und Tabulatoren ('\t') als Trennsymbole fungieren. unwords fu¨gt Leerzeichen zwischen die zu konkatenierenden Strings. lines :: String -> [String] und unlines :: [String] -> String zerlegen bzw. konkatenieren Strings, wobei nur Zeilenumbru¨che als Trennsymbole fungieren. unlines fu¨gt '\n' zwischen die zu konkatenierenden Strings.
219
Listenfaltung Faltung einer Liste von links her f
f
foldl f state [a ,a ,a ,a ,a ] 1 2 3 4 5
Endzustand
f f f state Anfangszustand
a1
a2
a3
a4
a5
Eingaben
foldl :: (a -> b -> a) -> a -> [b] -> a foldl f a (b:s) = foldl f (f a b) s foldl _ a _ = a
a ist Zustand, b ist Eingabe f ist Zustandsu ¨berfu ¨hrung
Link zur schrittweisen Auswertung von foldl(+)(0)[1..5] foldl1 :: (a -> a -> a) -> [a] -> a foldl1 f (a:s) = foldl f a s sum = foldl (+) 0 and = foldl (&&) True minimum = foldl1 min
product or maximum
= foldl (*) 1 = foldl (||) False = foldl1 max 220
concat
= foldl (++) []
concatMap :: (a -> [b]) -> [a] -> [b] concatMap f = concat . map f
Parallele Faltung zweier Listen von links her fold2 f state [a1,a2,a3,a4,a5] [b1,b2,b3,b4,b5]
f
f f f
f state a1
b1
a2
b2
a3
b3
a4
b4
a5
b5
fold2 :: (a -> b -> c -> a) -> a -> [b] -> [c] -> a fold2 f a (b:s) (c:s') = fold2 f (f a b c) s s' fold2 _ a _ _ = a
221
listsToFun :: Eq a => b -> [a] -> [b] -> a -> b listsToFun = fold2 update . const Beginnend mit const b, erzeugt listsToFun b schrittweise aus einer Argumentliste as und einer Werteliste bs die entsprechende Funktion: ( bs!!i falls i = max{k | as!!k = a, k < length(bs)}, listsToFun b as bs a = b sonst. Faltung einer Liste von rechts her entspricht der Auswertung ihrer Konstruktordarstellung in einer Algebra A, die die Konstruktoren (:) :: b -> [b] -> [b] und [] :: [b] als Funktion (:)A bzw. Konstante []A interpretiert (siehe Kapitel 2). (:)A :
foldr f a [b1,b2,b3,b4,b5]
f
f
(:)A :
f f
(:)A :
(:)A :
f b1
b2
b3
b4
b5
a
b1
b2
b3
b4
b5
(:)A : [] []A
222
foldr :: (b -> a -> a) -> a -> [b] -> a foldr f a (b:s) = f b $ foldr f a s foldr _ a _ = a
Der Applikationsoperator $ als Parameter von Listenfunktionen foldr ($) a [f1,f2,f3,f4]
;
f1 $ f2 $ f3 $ f4 a
foldl (flip ($)) a [f4,f3,f2,f1]
;
f1 $ f2 $ f3 $ f4 a
map f [a1,a2,a3,a4] map ($a) [f1,f2,f3,f4]
; ;
[f a1,f a2,f a3,f a4] [f1 a,f2 a,f3 a,f4 a]
zipWith ($) [f1,f2,f3,f4] [a1,a2,a3,a4] ; [f1 a1,f2 a2,f3 a3,f4 a4]
223
Listenlogik any :: (a -> Bool) -> [a] -> Bool any f = or . map f
any (>4) [3,2,8,4] ; True
all :: (a -> Bool) -> [a] -> Bool all f = and . map f
all (>2) [3,2,8,4] ; False
elem :: Eq a => a -> [a] -> Bool elem a = any (a ==)
elem 2 [3,2,8,4] ; True
notElem :: Eq a => a -> [a] -> Bool notElem a = all (a /=)
notElem 9 [3,2,8,4] ; True
filter :: (a -> Bool) -> [a] -> [a] filter (<8) [3,2,8,4] ; [3,2,4] filter f (a:s) = if f a then a:filter f s else filter f s filter f _ = []
224
Jeder Aufruf von map, zipWith, filter oder einer Komposition dieser Funktionen entspricht einer Listenkomprehension: map f s = [f a | a <- s] zipWith f s s' = [f a b | (a,b) <- zip s s'] filter f s = [a | a <- s, f a] zip(s)(s’) ist nicht das kartesische Produkt von s und s’. Dieses entspricht der Komprehension [(a,b) | a <- s, b <- s’]. Allgemeines Schema von Listenkomprehensionen: [e(x1, . . . , xn) | x1 ← s1, . . . , xn ← sn, be(x1, . . . , xn)] :: [a] • x1, . . . , xn sind Variablen, • s1, . . . , sn sind Listen, • e(x1, . . . , xn) ist ein Ausdruck des Typs a, • xi ← si heißt Generator und steht fu¨r xi ∈ si, • be(x1, . . . , xn) heißt Guard und ist ein Boolescher Ausdruck. Jede endlichstellige Relation l¨asst sich als Listenkomprehension implementieren, z.B. die Menge aller Tripel (a, b, c) ∈ A1 × A2 × A3, die ein Pr¨adikat p : A1 × A2 × A3 → Bool erfu¨llen, durch [(a,b,c) | a <- a1, b <- a2, c <- a3, p(a,b,c)]. 225
10 Haskell: Datentypen und Typklassen
Zun¨achst das allgemeine Schema einer Datentypdefinition: data DT x_1 ... x_m = C_1 typ_11 ... typ_1n_1 | ... | C_k typ_k1 ... typ_kn_k typ11, . . . , typknk sind beliebige Typen, die außer x1, . . . , xm keine Typvariablen enthalten. DT heißt rekursiv, wenn DT in mindestens einem dieser Typen vorkommt. Die durch DT implementierte Menge besteht aus allen Ausdru¨cken der Form C_i e_1 ... e_n_i, wobei 1 ≤ i ≤ n und fu¨r alle 1 ≤ j ≤ ni ej ein Element des Typs typij ist. Als Funktion hat Ci den Typ typ_i1 -> ... -> typ_in_i -> DT a_1 ... a_m. Alle mit einem Großbuchstaben beginnenden Funktionssymbole und alle mit einem Doppelpunkt beginnenden Folgen von Sonderzeichen werden vom Haskell-Compiler als Konstruktoren eines Datentyps aufgefasst und mu¨ssen deshalb irgendwo im Programm in einer Datentypdefinition vorkommen. 226
Die Unterschiede in der Schreibweise von Konstruktoren bei Infix- bzw. Pra¨fixverwendung sind dieselben wie bei anderen Funktionen. Beispiel 10.1 Der Haskell-Standardtyp fu ¨ r Listen data [a] = [] | a : [a] Fu¨r jede Menge A besteht [A] aus • allen endlichen Ausdru¨cken a1 : . . . : an : [] mit a1, . . . , an ∈ A und • allen unendlichen Ausdru¨cken a1 : a2 : a3 : . . . mit {ai | i ∈ N} ⊆ A. [A] ist die gr¨oßte L¨osung der Gleichung M = {[]} ∪ {a : s | a ∈ A, s ∈ M }
(1)
in der Mengenvariablen M und damit [A] eine Haskell-Implementierung der Menge CTList(A) aller List(A)-Grundterme. Als Elemente von [Int] lauten die List(Z)-Grundterme blink und blink’ wie folgt: blink,blink' :: [Int] blink = 0:blink' blink' = 1:blink 227
Die endlichen Ausdru¨cke von [A] bilden die kleinste L¨osung von (1) und damit eine HaskellImplementierung der Menge TList(A) der List(A)-Grundterme endlicher Tiefe (siehe 2.13). o Beispiel 10.2 (siehe 2.13) TReg(BS) ist isomorph zur kleinsten und CTReg(BS) zur gr¨oßten L¨osung der Gleichung M = {par(t, u) | t, u ∈ M } ∪ {seq(t, u) | t, u ∈ M } ∪ {iter(t) | t ∈ M } ∪ {base(B) | B ∈ BS}
(2)
in der Mengenvariablen M . Beide Mengen werden deshalb durch folgenden Datentyp implementiert: data RegT bs = Par (RegT bs) (RegT bs) | Seq (RegT bs) (RegT bs) | Iter (RegT bs) | Base bs o
Summentypen Die Summe oder disjunkte Vereinigung A1 + · · · + An =def {(a, 1) | a ∈ A1} ∪ · · · ∪ {(a, n) | a ∈ An} von n > 1 Mengen A1, . . . , An (siehe Kapitel 2) wird durch einen nicht-rekursiven Datentyp mit n Konstruktoren C1, . . . , Cn implementiert, welche die Summanden voneinander 228
trennen, m.a.W.: es gibt eine Bijektion zwischen A1 + · · · + An und der Menge {C1(a) | a ∈ A1} ∪ · · · ∪ {Cn(a) | a ∈ An}. Z.B. implementiert der Standardtyp data Maybe a = Nothing | Just a die bin¨are Summe 1 + A, die A um ein Element zur Darstellung “undefinierter” Werte erweitert. Damit lassen sich partielle Funktionen totalisieren wie die Funktion lookup, mit der der Graph einer Funktion von A nach B modifiziert wird (siehe Kapitel 2): lookup :: Eq a => a -> [(a,b)] -> Maybe b lookup a ((a',b):r) = if a == a' then Just b else lookup a r lookup _ _ = Nothing Der Standardtyp Either implementiert beliebige bin¨are Summen: data Either a b = Left a | Right b Die Menge aller ganzen Zahlen kann als dreistellige Summe implementiert werden: data INT = Zero | Plus PosNat | Minus PosNat data PosNat = One | Succ PosNat 229
PosNat implementiert die Menge aller positiven natu¨rlichen Zahlen (und ist rekursiv). Datentypen mit Destruktoren Um auf die Argumente eines Konstruktors zugreifen zu ko¨nnen, ordnet man ihnen Namen zu, die field labels genannt werden und Destruktoren im Sinne von Kapitel 2 wiedergeben. In obiger Definition von DT wird C_i typ_i1 ... typ_in_i erweitert zu: C_i {d_i1 :: typ_i1, ..., d_in_i :: typ_in_i} Wie Ci , so ist auch dij eine Funktion. Als solche hat sie den Typ DT a1 ... am -> typ_ij Destruktoren sind invers zu Konstruktoren. Z.B. hat der folgende Ausdruck den Wert ej : d_ij (C_i e_1 ... e_ni) Destruktoren nennt man in OO-Sprachen Attribute, wenn ihre Wertebereiche aus Standardtypen zusammengesetzt ist, bzw. Methoden (Zustandstransformationen), wenn der 230
Wertebereich mindestens einen Datentyp mit Destruktoren entha¨lt. Außerdem schreibt man dort in der Regel x.d ij anstelle von d ij(x). Mit Destruktoren lautet das allgemeine Schema einer Datentypdefinition also wie folgt: data DT a_1 ... a_m = C_1 {d_11 :: typ_11,..., d_1n_1 :: typ_1n_1} | ... | C_k {d_k1 :: typ_k1,..., d_kn_k :: typ_kn_k} Elemente von DT k¨onnen mit oder ohne Destruktoren definiert werden: obj = C_i e_i1 ... e_in_i ist ¨aquivalent zu obj = C_i {d_i1 = e_i1,..., d_in_i = e_in_i} Die Werte einzelner Destruktoren von obj k¨onnen wie folgt ver¨andert werden: obj' = obj {d_ij_1 = e_1',..., d_ij_m = e_m'} obj 0 unterscheidet sich von obj dadurch, dass den Destruktoren d ij 1,...,d ij m neue Werte, n¨amlich e 1’,...,e m’zugewiesen wurden.
231
Destruktoren du¨rfen nicht rekursiv definiert werden. Folglich deutet der Haskell-Compiler jedes Vorkommen von attrij auf der rechten Seite einer Definitionsgleichung als eine vom gleichnamigen Destruktor verschiedene Funktion und sucht nach deren Definition. Dies kann man nutzen, um dij doch rekursiv zu definieren, indem in der zweiten Definition von obj (s.o.) die Gleichung d ij = ej durch d ij = d ij ersetzt und d ij lokal definiert wird: obj = C_i {d_i1 = e_1,..., d ij = d_ij,..., d_in_i = en_i} where d_ij ... = ... Ein Konstruktor darf nicht zu mehreren Datentypen geh¨oren. Ein Destruktor darf nicht zu mehreren Konstruktoren unterschiedlicher Datentypen geh¨oren. Beispiel Listen mit Destruktoren k¨onnten in Haskell durch folgenden Datentyp definiert werden: data ListD a = Nil | Cons {hd :: a, tl :: ListD a} Man beachte, dass die Destrukturen hd :: ListD a -> a
und
tl :: ListD a -> ListD a, 232
die den Kopf bzw. Rest einer nichtleeren Liste liefern, partielle Funktionen sind, weil sie nur auf mit dem Konstruktor Cons gebildete Elemente von ListD(A) anwendbar sind. o Die Destruktoren eines Datentyps DT sind immer dann totale Funktionen, wenn DT genau einen Konstruktor hat. Wie das folgende Beispiel nahelegt, ist das aus semantischer Sicht keine Einschr¨ankung: Jeder Datentyp ohne Destruktoren ist isomorph zu einem Datentyp mit genau einem Konstruktor und einem Destruktor. Beispiel 10.3 Listen mit totalen Destruktoren (siehe 2.13) DTcoList(A) ist isomorph zur gr¨oßten L¨osung der Gleichung M = {coListC(Nothing)} ∪ {coListC(Just(a, s)) | a ∈ A, s ∈ M }
(3)
in der Mengenvariablen M und wird deshalb durch folgenden Datentyp implementiert: data ColistC a = ColistC {split :: Maybe (a,ColistC a)} Wie man leicht sieht, ist die gr¨oßte L¨osung von (3) isomorph zur gr¨oßten L¨osung von (1), also zu CTList(A). Die Einschr¨ankung von CTList(A) auf unendliche Listen ist isomorph zu DTStream(A) und wird daher durch folgenden Datentyp implementiert: 233
data StreamC a = (:<) {hd :: a, tl :: StreamC a} Als Elemente von StreamC(Int) lauten die Stream(Z)-Coterme blink und blink’ wie folgt: blink,blink' :: StreamC Int blink = 0: