[informatik-fachberichte] parallele implementierung funktionaler programmiersprachen volume 232 ||...
TRANSCRIPT
Kapitel5
Entschachtelung von SAL-Prograllllllen
Den Anfang dieses Kapitels bildet die formale Definition der Syntax und Reduktionssemantik getypter Kombinatorsysteme. Diese sind die Zielsprache des Entschachtelungsprozesses, der im AnschluB daran beschrieben wird. Durch eine weitere Transformation, die in Abschnitt 5.3 erliiutert wird, erzielt man die Erzeugung von Superkombinatorsystemen im Sinne von [Hughes 82]. 1m Hinblick auf die lmplementierung erfolgt schlieBlich in Abschnitt 5.4 der Ubergang zu sogenannten ftachen Kombinator- bzw. Superkombinatorsystemen.
5.1 Monomorph getypte Kombinatorsysteme
Getypte Kombinatorsysteme sind nichts anderes als getypte Funktionsgleichungssysteme hoherer Ordnung bestehend aus einer endlichen Anzahl von Funktionsdefinitionen der Form
wobei 'body' ein applikativer Ausdruck ist, der gewissen Bedingungen geniigt. Wir beginnen die formale Beschreibung der Syntax von Kombinatorsystemen
mit der Definition der Syntax der Kombinatorriimpfe. Wie in Kapitel 1 gehen wir von einer Basissignatur E = (8,0) und einer Datenstruktursignatur DS(E) = (D, r) aus. Ebenso legen wir wieder die Alphabete Arg, Loc und Fun fUr die Argument-, lokalen und Funktionsvariablen zugrunde.
R. Loogen, Parallele Implementierung funktionaler Programmiersprachen© Springer-Verlag Berlin Heidelberg 1990
94 KAPITEL 5. ENTSCHACHTELUNG VON SAL-PROGRAMMEN
5.1.1 Definition Die Familie der getypten applikativen SAL-Ausdriicke
AppExp = (AppExpt It E Typ(S, D))
ist die Teilfamilie von SAL-Ausdriicken, die aus
• Variablen und Konstanten mittels
• Verzweigung
• Applikation
• lokaler Deklaration und
• Pattern matching
aufgebaut sind, d.h.:
1. Vart C AppExpt (t E Typ(S, D))
2. n(€,s) ~ AppExps (s E S) n(S! ... Sn,S) C AppExpS! X ... XSn- S (Sl,"" Sn, S E S, n ~ 1)
3. r(€,d) C AppExpd (d E D) r(S!",sm,d) C AppExpS! X ... xsm-d
(SI, ... ,Sm E SUD,d E D,m ~ 1) 4. e E AppExpbool, el, e2 E AppExpt
==} if e then el else e2 fi E AppExpt (t E Typ(S, D))
5. e E AppExpt mit t = tl X •.• X tk -+ to, (k ~ 1, to, . .. , tk E Typ(S, D)) ei E AppExpt. fUr i E {I, ... ,k}
==} (e, el, ... , ek) E AppExpto
6. lokale Deklaration
Yi E Loct• paarweise verschieden, ei E AppExpt. (1 ~ i ~ k), e E AppExpto (to, ... , tk E Typ(S, D))
==} let Yl = el and ... and Yk = ek in e E AppExpto
7. case-Ausdruck
e E AppExl mit d E D, red) =: {Cl, ,"' ,Ck} mit Cj E r(t,! ... t,m"d) fUr j E {I, ... ,k}, Yji E Loct,. paarweise verschieden (1 ~ i ~ mj), ej E AppExpt (1 ~ j ~ k)
(t E Typ(S,D),tll, ... ,tlmp ... ,tkl, ... ,tkmk E SUD) ==} case e of
CI(Yll, .. ·,YlmJ el;
Ck(Ykl, ... , Ykmk) ek esac E AppExpt
5.1. MONOMORPH GETYPTE KOMBINATORSYSTEME 95
Diese Definition entspricht der Definition der Familie der SAL-Ausdrucke bis auf die Falle der A-Abstraktion und Rekursion, die in rein applikativen Ausdrucken nicht zugelassen sind. Insbesondere gilt also:
AppExp ~ Exp.
5.1.2 Definition 1. Ein Kombinatorsystem ist ein endliches System von Kom-binatordefinitionen
n = ((( ... (Fi' Xill"" Xik.J·· .), X~.ll···' X~.kln) = ei I 1::; i ::; r},
wobei r ~ 1, Fi E Fun (1::; i ::; r), X~l E Arg (1::; i ::; r,1 ::; j ::; ni, 1 ::; I ::; kij ), ni ~ 0 (1::; i ::; r), kij ~ 1 (1::; j ::; ni, 1 ::; i ::; r),
und alle Typen passen, also:
falls fur 1 ::; i ::; r : typ(Fd = til x ... x tl k.} ---t ( ••• ---t (t~.l X ... X t~.kln ---t ti) ... ) mit t~l E Typ(S, D) und ti E Typ(S, D), •
so ist X~l E Argt;, fur 1 ::; j ::; ni und 1 ::; I ::; kij sowie ei E Expt.( {X~l 11 ::; j ::; ni, 1 ::; I ::; kij}, 0, {Fl , ... , Fr}).
2. Ein Kombinatorprogramm vom Typ s E SUD ist ein Paar
(n,e)
bestehend aus einem Kombinatorsystem n und einem applikativen Ausdruck e vom Basistyp s:
e E AppExps mit free(e) ~ {Fl , ... , Fr},
wobei Fl, ... ,Fr die in n definierten Kombinatoren seien.
Verglichen mit imperativen Programmen entsprechen die Kombinatordefinitionen im Kombinatorsystem den Prozedurdeklarationen. Der applikative Ausdruck reprasentiert das Hauptprogramm.
Kombinatorprogramme entsprechen speziellen SAL-Ausdriicken, bei denen Rekursion und Abstraktion nur in ganz bestimmter Form auf dem obersten Level zugelassen sind. Die Fixpunktsemantik eines Kombinatorprogramms
(n,e)
mit
n = ((( ... (Fi' Xill"" XikJ" ')X~il"'" X~.k.n) = ei I 1::; i ::; r}
wird erklart als die Semantik des SAL-Programms:
96 KAPITEL 5. ENTSCHACHTELUNG VON SAL-PROGRAMMEN
letrec Fl = >.( xt 1 , ... , xtklJ ).
and and Fr = >'(xll" .. ,xlkrJ· in e.
Kombinatorprogramme bilden unter Beriicksichtigung dieser Festlegung eine Teilklasse der SAL-Programme.
Auch die Reduktionssemantik lieBe sich auf diese Weise auf Kombinatorprogramme iibertragen. Dies ist aber nicht ratsam, da es moglich ist - und dies ist ein wesentlicher Grund fUr die Betrachtung von Kombinatorsystemen - bei der Definition der Reduktionsregeln die spezielle Struktur der Kombinatorprogramme, in denen wie gesagt Rekursion und Abstraktion nur auf dem obersten Level auftreten, auszunutzen.
Indem man bei der Reduktionssemantik ein festes Kombinatorsystem zugrundelegt, kann man auf die Reduktionsregeln fUr die {3- und letrec-Reduktion verzichten und an deren Stelle spezielle Kombinatorreduktionen definieren.
Zur Definition der nichtdeterministischen Reduktionssemantik fUr Kombinatorsysteme gehen wir wie in SAL von einer strikten flachen Interpretation A = (A.l' ¢A) der Basissignatur aus und wahlen wie bisher fiir die Datenstruktursignatur die Interpretation CT DS(E)(A) der unendlichen r-Baume iiber A.l. Als Berechnungsausdriicke wahlen wir die Menge der rein applikativen Ausdriicke, in denen an Stelle von Argumentvariablen Werte aus A (= A.l \ {1.}) bzw. Ausdriicke der Form c( Ul, .•. ,urn) mit C E r auftreten konnen. Formal definieren wir also:
5.1.3 Definition Die Familie der getypten applikativen Berechnungsausdrucke iiber A und CT DS(E)(A)
AppComp:= (AppCompt It E Typ(S, D))
ist die kleinste Typ(S, D)-sortierte Mengenfamilie, fUr die gilt:
O. AS ~ AppComps (8 E S) C E r(S!,,,sm,d) mit m ~ 1, Ui E AppComps, (1 ::; i ::; m)
~ C(Ul, .•• , urn) E AppCompd
1. Loct ~ AppCompt (t E Typ(S, D)) Funt C AppCompt (t E Typ(S, D) \ (S U D))
2. - 7. analog zur Definition der applikativen Ausdriicke (Definition 5.1.1)
1st Rein Kombinatorsystem mit den Funktionsvariablen Fl , ... , Fr , so ist die Familie der Berechnungsausdriicke von R iiber A und CT DS(E)(A) definiert durch
Compn:= {u E AppComp I free(u) ~ {Fl , ... ,Fr }}.
5.1. MONOMORPH GETYPTE KOMBINATORSYSTEME 97
Die applikativen Berechnungsausdrucke bilden eine Teilfamilie der SAL-Berechnungsausdriicke. Insbesondere ist also die Substitution entsprechend Definition 1.3.4 auch fUr applikative Berechnungsausdriicke erkHirt. Die Berechnungsausdrucke eines Kombinatorsystems sind applikative Berechnungsausdrucke, die nur die Kombinatornamen als Funktionsvariable frei enthalten.
Die Reduktionsregeln fur Kombinatorberechnungsausdrucke entsprechen grof3-tenteils den Reduktionsregeln fUr SAL-Berechnungsausdrucke. Die (3- und letrecReduktionsregeln werden allerdings ersetzt durch die einfachere Kombinatorreduktion.
5.1.4 Definition Sei
R= ((( ... (Fi,xi1, ... ,xik.J···),X~.1···X~.k.n) =ei I 1 ~ i ~ r)
ein Kombinatorsystem und ComPR die Familie der Berechnungsausdrucke zu R. Die Reduktionsregeln
werden wie folgt erkHirt:
1. Konstantenreduktion
(J, a1,···, an) ~R <PA(J)(a1, ... , an) fUr f E O(Sl ... Sn,S), ai E AS'(l ~ i ~ n), Sl, ... , Sn, S E S
2. Konstruktorreduktion
(C,U1, ... ,Um) ~R C(U1, ... ,Um) fUr C E r(sl ... sm,d), Ui E Comps '(l ~ i ~ m), Sl, ... , Sm E S U D,d E D
3. Verzweigungsreduktion
if T then U1 else U2 fi ~R U1, if F then U1 else U2 fi ~R U2 fUr U1, U2 E ComPR
4. let-Reduktion
let Y1 = U1 and ... and Yk = Uk in U ~R U[yl/u1, ... , Yk/Uk] fUr u, U1 , ... , Uk E Compn t
5. case-Reduktion
case Cj(Uj1, ... , UjmJ of··· Cj(Yj1, ... , Yjm J ) : Uj··· esac ~n Uj[Yjl/Uj1, ... , Yjm)Ujm,] fUr Uj1, ... , UjmJ ' Uj E Compn
t Man beachte, daB Ul, ..• , Uk keine freien Variablen auBer Funktionsvariablen enthalten.
98 KAPITEL 5. ENTSCHACHTELUNG VON SAL-PROGRAMMEN
6. Kombinatorreduktion
(( ... (Pi, Uu,···, Ulk'l)" .), Un,l,"" Unikoni ) -+n. ei [X1l / Uu, ... , xlkil / Ulk'l , ... , X~,l / Un,l, ... , X~,kon / un,kon, l
fur Ulj E Compn. (1 ~ j ~ kil , 1 ~ 1 ~ ni),'1 ~ i ~ r
Die Kombinatorreduktionen sind bestimmt durch das vorgegebene Kombinatorsystem. Die Reduktion einer Kombinatorapplikation ist nur moglich, wenn der Kombinator entsprechend seiner Definition im Kombinatorsystem "voll appliziert" ist. Dadurch wird sichergestellt, daf3 die Berechnungsausdrucke rein applikativ bleiben.
5.1.5 Definition Die Reduktionsrelation
=?n.~ Compn. x Compn.
wird induktiv uber den Aufbau der applikativen Berechnungsausdriicke zu R festgelegt:
1. 1st Ul -+n. U2 eine Reduktionsregel (Ul,U2 E Compn.), so gilt:
Ul =?n. U2· 2. Fur U E Compn. gilt: U =?n. u ..
3. Mit U =?n. U',Ui =?n. u~,(i E {1,2}) ist auch
if U then Ul else U2 fi =?n. if u' then ui else u~ fi
4. Falls U =?n. u' und Ui =?n. u~ (1 ~ i ~ k), so gilt auch:
• (U,Ul, ... ,Uk) =?n. (u',ui, .. ·,u~), • let Yl = Ul and .. , and Yk = Uk in U
=?n. let Yl = ui and ... and Yk = u~ in u'
• case U of Cl(YU,"" Ylml) : Ul;"'; Ck(Ykl,"" Ykmk) : Uk esac =?n. case u' of Cl (Yll, ... , Yl ml) : ui; ... ;
Ck(Ykl, ... , Ykmk) : u~ esac
Der Nachweis der Konfluenzeigenschaft dieser Reduktionsrelation kann analog wie im Fall der Reduktion von SAL-Berechnungstermen erbracht werden.
Die Reduktionssemantik von Kombinatorsystemen wird unter Zugrundelegung der Church-Rosser-Eigenschaft wie folgt erklart:
5.1.6 Definition Sei P = (R,e) ein Kombinatorprogramm vom Typ s E SUD. Die Reduktionssemantik red[P]A des Kombinatorprogramms P ist dasjenige a E AU Tr(A) mit e *n. a, falls es existiert:
red[P]A = a :{:=::} e *n. a.
1m folgenden zeigen wir, daB jedes SAL-Programm in ein aquivalentes Kombinatorprogramm transformiert werden kann.
5.2. DER ENTSCHACHTELUNGSALGORITHMUS 99
5.2 Der Entschachtelungsalgorithmus
Der Entschachtelungsalgorithmus baut auf der einfachen Idee auf, lokale Funktionsdefinitionen in einem SAL-Programm - also >'-Abstraktionen und letrecAusdriicke - durch Applikationen neu definierter Kombinatoren auf die freien Variablen der Abstraktion bzw. Rekursion zu ersetzen. Betrachten wir etwa den einfachen Fall einer >'-Abstraktion
>'(X1,'" ,xk).e,
wobei e rein applikativ (ohne innere >'-Abstraktionen oder letrec-Ausdriicke) sei und auiler Xl, ... , Xk nur die Argumentvariablen Xl, ... , Xm als freie Variablen enthalte. Diese >'-Abstraktion kann bei Definition eines Kombinators
durch die Applikation
ersetzt werden. Die Korrektheit dieser Transformation wird sofort klar, wenn man als Zwischenschritt zunachst die freien Variablen der >'-Abstraktion herausabstrahiert und dann dem Funktionsausdruck den Namen Fneu gibt:
>'(X1,"" Xk).e
1 Umkehrung der ~-Reduktion (>'(X1, ... , Xm).>'(X1" .. , Xk).e, Xl, .. . ,Xm)
, f ... =: Fneu
Rekursive Ausdriicke konnen in ahnlicher Weise behandelt werden. Sie fiihren zur Definition von rekursiven Kombinatoren. Auch hier betrachten wir zunachst einen sehr einfachen Fall. Der letrec-Ausdruck
letrec F = >'(X1"" ,xk).e in e enthaIt nur eine rekursive Funktionsdefinition. Die Ausdriicke e und e seien applikativ und der Rumpf der rekursiven Definition >'(X1,"" xk).e enthalte frei nur die Argumentvariablen Xl, ... ,Xm und die Funktionsvariable F. Es gilt:
100 KAPITEL 5. ENTSCHACHTELUNG VON SAL-PROGRAMMEN
letrec F = A(XI, ... , xk).e in e lletrec-Reduktion
e[Fj letrec F = A(XI, ... , xk).e in A(XI, ... , xk).e] , v ~
:=EF
Der sich so ergebende Ausdruck enthaIt nur den Ausdruck EF als nicht applikativen Teilausdruck. Zur Ersetzung dieses Ausdruckes definiert man den rekursiven Kombinator
wobei jedes Vorkommen von F in e durch (Fneu, Xl, ... , Xm) ersetzt wird. Der Ausdruck EF entspricht dann der Applikation
und der gesamte letrec-Ausdruck kann somit durch den Ausdruck
ersetzt werden.
Diese Transformation kann wie folgt begriindet werden:
Wiederum werden die freien Variablen Xl, ... ,Xm herausabstrahiert und der Funktionsausdruck als neuer Kombinator definiert:
(EF =) letrec F = A(XI, ... ,xk).e in A(XI, ... ,Xk).e
1 umgekehrte (3-Reduktion
(A(XI, . .. , Xm).letrec F = A(XI, ... , Xk).e inA (XI, ... , xk).e, XI, .. . , xm). , v I
=: Fneu
Fiir diesen Kombinator gilt:
5.2. DER ENTSCHACHTELUNGSALGORITHMUS
>'(Xl' ... ,xm).letrec F = >'(Xl' ... ,xk).e in >'(Xl' ... ,Xk).e
1 Reduktion der Rekursion
101
>'(Xl,"" Xm).>'(Xl, ... , xk).e[F / letrec F = >'(Xl,"" xk).e in >'(Xl,"" xk).e], , ., v
also
Schwieriger wird die Entschachtelung im Fall simultaner Rekursion. Urn dies zu verdeutlichen, betrachten wir wieder einen einfachen Beispielausdruck
letrec Fl = >'(xu, ... ,xlkJ.el and F2 = >'(X2l"" ,x2k2).e2 in e
wobei e, el und e2 rein applikative Ausdriicke seien. Fiir i E {1,2} enthalte ei neben Xil, ... ,Xik, und eventuell Fl und/oder F2 nur die Argumentvariablen Xil, ... ,Xim, als freie Variable.
Bei der Definition der Kombinatoren werden in ei die Funktionsvariablen Fl und F2 durch Applikationen der neuen Kombinatoren auf die freien Argumentvariablen der entsprechenden Ausdriicke >'(Xil"" ,xik,).ei ersetzt. Dies fiihrt dazu, daf3 die globalen Variablen von e2 durch F2 in el importiert werden konnen und umgekehrt. Treten also sowohl Fl in e2 als auch F2 in el auf, so werden die Kombinatoren
((Fl,neu, xn, ... ,Xlm], X2l, ... ,X2m2)' Xn, ... ,Xlk]) = el[Ft!(Fl,neu, Xu, .. · ,X2m2)' F2/(F2,neu, xn, ... , x2m2)]
((F2,neu, Xu, ... ,Xlm], X2l, ... ,x2m2)' X21, ... ,X2k2) = e2[Ft!(Fl ,neu, Xu, ... , x2m2)' F2/(F2,neu, Xu, ... , X2mJ]
definiert und der gesamte letrec-Ausdruck durch
e [ FI / (Fl,neu, Xu, ... , Xl m], X2l," ., X2mJ, F2 / (F2,neu, xn, ... ,Xlm]l X21, ... ,X2m2) 1
ersetzt.
Diese einfachen Beispiele verdeutlichen die prinzipielle Arbeitsweise des Entschachtelungsalgorithmus, der das zu entschachtelnde Programm "top-down", also von auBen nach innen durchliiuft. 1m allgemeinen Fall enthalten die >.- und letrecAusdriicke nicht nur Argumentvariablen als freie Variable, sondern auch lokale und
102 KAPITEL 5. ENTSCHACHTELUNG VON SAL-PROGRAMMEN
insbesondere Funktionsvariable. Durch die "Top-Down"-Vorgehensweise sind zu den freien Funktionsvariablen bereits die Kornbinatoren und insbesondere die Variablen, die durch sie irnportiert werden, bekannt. Urn Narnenskonflikte zwischen lokal gebundenen und irnportierten Variablen zu verrneiden, werden wir in dern irn folgenden beschriebenen Algorithrnus irnportierte Variablen immer urnbenennen.
5.2.1 Beispiel Betrachten wir den Ausdruck
mit der globalen Variablen Xl. Entschachteln fUhrt hier etwa zur Definition des Kornbinators
((F2,neu,Xt},X2) = (*,XI,X2)
fUr F2. Die globale Variable Xl wird durch F2 nach >'xI.(F2' xt} irnportiert. Sie rnuB aber zur Verrneidung von Konflikten urnbenannt werden. Fiir FI wird etwa der Kornbinator
definiert und der Gesarntausdruck wird durch
ersetzt.
Urn die neu definierten Kornbinatoren und die Variablen, die sie irnportieren, eindeutig zu benennen, benutzen wir durch Worte aus IN* indizierte Variablennamen, die verschieden von den in den SAL-Ausdriicken auftretenden Variablen seien. Wir erweitern also die Variablenalphabete Ary und Fun urn durch Worte aus IN* indizierte Variable und bezeichnen die erweiterten Alphabete mit ArgO und Funo. Die Menge der iiber den erweiterten Variablenalphabeten gebildeten applikativen Ausdriicke bezeichnen wir entsprechend mit AppExl. Die Menge aller Kornbinatordefinitionen der Form
(( ... (F, Xu, ... , XlkJ .. . ), Xml, ••• , Xmkm ) = e
mit FE FunO,xij E AryO (paarweise verschieden) und e E AppExpo mit free(e) n (A rgo U Loc) ~ {xu, . .. ,Xmkm } bezeichnen wir mit Comdef.
Bevor wir die Entschachtelungsfunktion angeben, definieren wir die globalen Variablen zu (mittels letrec) rekursiv definierten Funktionen unter Bezug auf eine Ersetzung der in ihnen frei vorkommenden Variablen. Global nennen wir dabei die freien Variablen zuziiglich der irnportierten Variablen.
5.2. DER ENTSCHACHTELUNGSALGORITHMUS 103
5.2.2 Definition Sei e = letrec Fl = el and··· and Fr = er in e ein rekursiver Ausdruck iiber dem Variablenalphabet Var := Arg U Loc U Fun und i E {I, ... , r}.
Sei a : Var ~ Expo eine Zuordnung von applikativen Ausdriicken zu VariabIen aus Var.
Die Menge der unter a globalen Variablen zu Fi in e
global(Fi , e, a)
ist die i-te Komponente des kleinsten Fixpunktes der Abbildung
We,u : (Ptt(Argo U Loc)f ~ (P(Arl U Loc)f
mit We,u(Gl, ... ,Gr ):= (Cl, ... ,Cr ), wobei
Also:
Gj := UvarEfree(eJ)\{F1, ... ,Fr } free(a( var)) n (ArgO U Loc)
U UFkEfree(eJ)n{Fl , ... ,Fr } Gk .
global(Fi,e,a):= proji(fixWe,u).
Ais Halbordnung wird dabei die komponentenweise Mengeninklusion gewahlt. Die Stetigkeit von We,u beziiglich (P(Arl U Loc), ~r ist offensichtlich. Wir verzichten daher hier auf einen formal en Beweis.
In dieser Definition wird durch die Funktion a die eventue11e Umbenennung globaler Variablen bzw. die Substitution von globalen Funktionsvariablen durch Kombinatorapplikationen beriicksichtigt.
Wir beschreiben den Entschachtelungsalgorithmus durch eine Funktion lift, die fUr beliebige SAL-Ausdriicke definiert ist und aus zwei Komponentenfunktionen besteht. Die erste Komponentenfunktion liftl liefert den entschachtelten Ausdruck, wahrend die zweite Komponentenfunktion lift2 die Kombinatordefinitionen sammelt, die bei der Entschachtelung des Ausdruckes entstehen. Ais Parameter erwartet die Funktion lift neben dem zu entschachtelnden Ausdruck zwei weitere. Zum einen ist dies eine Funktion a : Var ~ AppExpo, die fUr jede in dem Ausdruck frei auftretende Funktionsvariable die Kombinatorapplikation, durch die die Funktionsvariable ersetzt werden so11, und fUr jede globale Variable die Umbenennung dieser angibt. Fiir alle iibrigen Variablen entspricht a der Identitatsabbildung. Zum anderen wird der Funktion lift ein Wort aus IN* zur eindeutigen Bezeichnung neu zu definierender Kombinatoren und zur eindeutigen Umbenennung globaler Variablen iibergeben.
ttMit P(M)bezeichnen wir die Potenzmenge aner beliebigen Menge M
104 KAPITEL 5. ENTSCHACHTELUNG VON SAL-PROGRAMMEN
5.2.3 Definition Die Entschachtelungsfunktion
lift: Exp X (Var - AppExl) X IN* - - AppExpo X P( Comdef)
wird induktiv iiber die Struktur der SAL-Ausdriicke definiert.
Sei im folgenden u~: Var - AppExpO und w E IN*. Die beiden Komponentenfunktionen von lift werden mit liftl und lift2 bezeichnet. Dann ist:
1. lift ( var, u, w) := (u( var), 0) fiir var E Var
2. lift(p" u, w) := (p,,0) fiir p, E n u r 3. lift(if el then e2 else ea fi, u, w)
:= (if liftl(eI,u,w.l) then lift l (e2,u,w.2) else liftl(ea,u,w.3) fi, a U lift2(ei, u, w.i)) i=l
4.lift((eO,el, ... ,ek),u,w) := (( lift I (eo, u, w.O), ... , lift I (ek' u, w.k )),
k
U lift2(ei, u, w.i)) i=O
5. lift(let YI = el and ... and Yk = ek in eo, u, w) := (let YI = liftl(el,u,w.l) and ... and Yk = liftl(ek,u,w.k)
in liftl(eo,u,w.O), k
U lift 2 ( ei, a, w.i)) i=O
6. lift(case eo of··· Cj(Yjl, ... ,YjmJ ) : ej ... esac, u,w) := (case liftl(eO,u,w.O) of
... Cj(Yjt. ... , YjmJ : lift I (ej, u, w.j) ... esac, k
U lift2(ei, u, w.i)). i=O
7.lift().(XI, ... ,xk).e,u,w) := ((Fw.t. varI, ... , varm),
{(( ... ((Fw.t. xi·I, ... , x:·l ), Xl,···, Xk),·· .), Xnl,···, XnkJ = lift I (body(e), 0-, w.l)}
u lift2( body(e) , 0-, w.l))
wobei body (e) := if e = ).(xn, ... , xlkJ.el then body(et} else e fi,
t Als Werte treten bei dieser F\mktion nur Variablen und Applikationen von Kombinatoren auf. Die Definition ist zur Vereinfachung allgemein gehalten.
5.2. DER ENTSCHACHTELUNGSALGORITHMUS 105
u free(a(var)) n (ArgO U Loc) vaT E/ree (>.( Xl , ••• ,Xk ).e)
0- = a[vart/xtl, .. . , varm/x~·ll mit typ(xr· 1) = typ( vari),
also 0-( var) = {X,:"l falls var = vari (1 ~ i ~ m) a( var) sonst
und e = >'(xn, ... , XlkJ.>'(X21, ... , X2k2)· .. · >'(Xnl, ... , xnkJ.body(e) mit n ~ O,kl' ... ,kn E IN\ {O},Xjl E Arg, 1 ~ j ~ n. Fw .1 sei entsprechend seiner Definitionsgleichung getypt.
8. lift(letrec Fl = el and ... and Fr = er in e, a, w) := (lift1(e,0-,w.0),
lift2(e, 0-, w.O) u{((· .. ((Fw .i , xiI·i, . .. , xr';J, xiI'· .. , XikJ,·· .), X~l'· .. , X~kJ
= liftl(body(ei)),o-i,W.i) 11 ~ i ~ r} r
U U lift 2 ( body( ei)), o-i, w.i)) i=l
wobei 0- := a[ Ft/(Fw .1, varn, ... , varlmJ,
Fr/(Fw .n varrl,···, varrmr ) 1 mit {varil, ... ,varim,}:= globals(Fi,e,a)
(e = letrec Fl = el and··· and Fr = e r in e), o-i = o-[varit/xiI·i, ... , varim.!Xr'; lund ei = >'(X111 ... , XikJ·>'(X;l' ... , X;~2)· ... >'(X~l' ... , X~kJ. body ( ei) (1 ~ i ~ r) mit body ( e) = if e = >'( ... ).e' then body( e') else e fl.
Die Funktion lift ersetzt in dem zu entschachtelnden Ausdruck >'-Abstraktionen und letrec-Konstrukte durch Applikationen von neu definierten Kombinatoren auf die globalen Variablen der Abstraktion. In der Kombinatordefinition erfolgt eine Umbenennung der globalen Variablen. Diese Umbenennung ist notwendig, da durch die Ersetzung von Funktionsvariablen durch Applikationen neu definierter Kombinatoren auf globale Variable Namenskonflikte entstehen konnen (siehe Beispiel 5.2.1). AuBerdem werden mittels der Umbenennung freie lokale Variable durch Argumentvariablen ersetzt.
Direkt ineinandergeschachtelte >'-Abstraktionen werden jeweils in einer Kombinatordefinition zusammengefaBt. Jede >'-Abstraktion wird dazu in die Folge der >'-Abstraktionen und den von einer >'-Abstraktion verschiedenen Rumpf (body) zerlegt.
Bei der Definition der Entschachtelung von rekursiven Ausdriicken wird deutlich, daB alle globalen Variablen zu einer rekursiven Funktion Fj iiber den Aufruf
106 KAPITEL 5. ENTSCHACHTELUNG VON SAL-PROGRAMMEN
(Fw.j, Varjl, ... , varjmJ ) importiert werden mussen, auch wenn sie im Rumpf von Fj nur zu anderen Kombinatoren "durchgeschoben" werden. Dies ist der Preis, der fur die Dezentralisierung der Umgebungsstruktur gezahlt werden mufi.
Das zu einem SAL-Programm gehorige Kombinatorprogramm ergibt sich durch einen Aufruf der Entschachtelungsfunktion lift mit der 1dentitatsfunktion id lVar als Variablenumbenennungsfunktion und dem Startkennwort 1.
5.2.4 Definition Sei e E Prog. Dann heifit
(ft, e) := (lijt2( e, id lVar , 1), liftl (e, id lVar , 1))
mit e E AppExpO, ft ~ P( Comdef) das zu e gehorige Kombinatorprogramm.
5.2.5 Lemma (ohne Beweis)
1. Fur e E Prog gilt: lift2(e, id lVar , 1) ist ein getyptes Kombinatorsystem.
2. Fur e E Prog gilt: 1st (ft, e) das zu e gehorige Kombinatorprogramm, dann ist
red[e]A,r = red.R[(ft, e)]A,r.
Bevor wir eine Modifikation des Entschachtelungsalgorithmus zur Erzeugung sogenannter Superkombinatorsysteme angeben, beschreiben wir kurz die Entschachtelung des in Kapitel 1 betrachteten Beispielprogramms.
5.2.6 Beispiel Zu dem in Beispiel 1.1.8 gegebenen 'Quicksort' SAL-Programm erhalt man durch Anwendung des Entschachtelungsalgorithmus folgendes Kombinatorprogramm. Es werden Kombinatoren QSort, Filter und Append fUr die rekursiv definierten Funktionen quicksort, filter und append definiert, deren Rumpf unverandert bleibt, da keine globalen Variablen darin enthalten sind. Aufierdem werden fUr die funktionalen Argumente der Funktion filter zwei neue Kombinatoren Tgeq und Tit vom Typ int -+ int -+ bool definiert.
(( (QSort, [intlist):= case lof NIL : NIL;
CONS(y~nt, y~ntlist) :
esac
(Append, (QSort, (Filter, (Tit, yd, Y2)), (CONS, Yl, (QSort, (Filter, (Tgeq, yd, Y2))))
5.3. SUPERKOMBINATORSYSTEME 107
(Filter, testint ..... booi, I'intiist):= case l' of NIL : NIL CONS( hint, tintiist) :
esac (Append, I~ntiist, Ikntiist) := case 11 of
NIL: 12 ;
if (test,h) then (CONS, h, (Filter, test, t)) else (Filter, test, t) fi
CONs(yint , y~ntiist): (CONS,Y1 ,(Append,Y2,l2)) esac
(( Tgeq, x~nt), xknt) := (~, X2, xd ((Tit, x~nt),xknt) := «,x2,xd ) ;
(QSort, (CONS, 4, (CONS, 3, (CONS, 1, (CONS, 2, NIL))))))
Der hier vorgestellte Entschachtelungsalgorithnus entspricht dem in [Johnsson 85] entwickelten, sogenannten '>.-lifting'-Algorithmus. Er unterscheidet sich von dem in Abschnitt 2.4 skizzierten Algorithmus von [Hughes 82/84] dadurch, daB er die direkte Behandlung simultaner Rekursion beinhaltet - welche ein Top-dmvnVorgehen erfordert - und daB die entstehenden Kombinatorsysteme keine "fully lazy"-Auswertung garantieren. Letzteres ist ein wesentlicher Nachteil des >.-liftingAlgori thmus.
1m folgenden Abschnitt definieren wir daher entsprechend [Hughes 82/84] den Begriff der Superkombinatorsysteme, die 'full laziness' gewahrleisten, und zeigen. daB der Entschachtelungsalgorithmus in einfacher Weise so modifiziert werden kann, daB Superkombinatorsysteme erzeugt werden.
5.3 Superkombinatorsysteme
Bei der Diskussion der Graphreduktion in Abschnitt 2.3 haben wir bereits die Begriffe 'lazy' und 'fully lazy' Auswertung flir den >.-Kalkiil erHiutert:
1. Eine Auswertung heiBt 'lazy', falls kein Argumentausdruck, d.h. kein Ausdruck, der flir eine Variable substituiert wird, mehrfach ausgewertet wird.
2. Eine Auswertung heiBt 'fully lazy', falls kein Teilausdruck nach Bindung der in ihm auftretenden Variablen mehrfach ausgewertet wird [Hughes 84].
Wie wir gesehen haben, ist einc 'fully lazy' Auswertung sichergestellt, wenn bei der ,B-Reduktion ein Kopieren der maximal freien Teilausdriicke der >'-Abstraktion vermieden wird.
108 KAPITEL 5. ENTSCHACHTELUNG VON SAL-PROGRAM MEN
Was bedeutet nun der Begriff 'fully lazy' Auswertung in einem Kombinatorkalkiil? In [Hudak/Goldberg 85a] wird folgende Prazisierung gegeben:
Eine Kombinatorreduktion heifit 'fully lazy', falls kein Teilausdruck eines Kombinatorrumpfes infolge einer bzgl. der Kombinatordefinition partiellen Applikation des Kombinators, die an verschiedenen Stellen als gemeinsamer Teilausdruck auf tritt, mehrfach ausgewertet wird.
Da A-Abstraktionen im Kombinatorkalkiil durch partielle Kombinatorapplikationen reprasentiert werden, sind beide Beschreibungen aquivalent. Durch das Kopieren von partiellen Kombinatorapplikationen kann es zu Mehrfachauswertungen von Teilausdriicken des Kombinatorrumpfes kommen, die nur von den in der partiellen Applikation vorhandenen Argumenten abhangen. Diese Teilausdriicke entsprechen genau den - bzgl. der durch die partielle Applikation reprasentierten A-Abstraktion - maximal freien Teilausdriicken des KombinatoITumpfes.
In der Sprache SAL werden die Begriffe 'frei' und 'maximal frei' fUr Teilausdriicke wie folgt festgelegt.
5.3.1 Definition 1. Die Abbildung
subexp: Exp --+ P(Exp),
die jedem SAL-Ausdruck die Menge seiner (echten) Teilausdrucke zuordnet, wird induktiv definiert durch
(a) Falls e E Var U n u r, so gilt:
subexp(e) := 0.
(b) Falls e = if el then e2 else e3 fi, so gilt:
3
subexp(e) := U({ed U subexp(ei)) i=l
(c) Falls e = A(Xl, ... ,xk).e, so ist:
subexp( e) := {e} u subexp( e)
5.3. SUPERKOMBINATORSYSTEME 109
(d) Falls e = (eO,el, ... ,ek) oder e = let Yl = el and ... and Yk = ek in eo oder e case eo of Cl (Yn, ... , YlmJ el;
Ck(Ykl, ... , Ykm,J ek esac oder
e = letrec Fl el and and
Fk = ek in eo,
so gilt: k
subexp( e) := U ({ ej} U subexp( ej)). j=O
2. Die Menge der freien Teilausdrucke
Jree-exp( e)
eines SAL-Ausdruckes e wird definiert durch:
Jree-exp(e) := {e' E subexp(e) I Jree(e') ~ free(e) /\ V e" E subexp( e) : e' E subexp( e")
:::} Jree(e') ~ free(e")}
3. Fur e E Exp wird durch
mJe( e) := {e' E Jree-exp( e) I Ve" E Jree-exp( e) : e' rt. subexp( e")}
die Menge der maximal freien Teilausdriicke von e festgelegt.
Ein Teilausdruck eines SAL-Ausdruckes heiBt frei, wenn aIle in ihm frei auftretenden Variablen auch freie Variablen des Gesamtausdruckes sind. Eine in dem Teilausdruck frei auftretende Variable darf also in einem umgebenden Ausdruck nicht gebunden werden. Insbesondere ist der Rumpf einer im Ausdruck auftretenden -\-Abstraktion nur dann frei, wenn die Abstraktionsvariable nicht in ihm auftritt. Nicht jeder Teilausdruck eines freien Teilausdruckes ist notwendigerweise frei.
5.3.2 Beispiele 1. Die freien Teilausdriicke einer -\-Abstraktion mit rein ap-plikativem Rumpf ohne let-, case-, -\- und letrec-Teilausdriicke
-\(Xl, ... ,xk).e
sind die Teilausdriicke, in denen die Variablen Xi (1 < z ~ k) nicht auftreten.
110 KAPITEL 5. ENTSCHACHTELUNG VON SAL-PROGRAMMEN
2. Fiir den SAL-Ausdruck
gilt:
Jree-exp( e) = {Xl, 5, *, +} und Jree-exp(e)= subexp(e) \ {Xl, (*, Xl, (+, 5, X2))},
da Xl in e gebunden wird.
3. Fiir den SAL-Ausdruck
gilt: Jree-exp( e) = {x', x", +, *, AX'.( *, x', x")}
Der Rumpf der inneren A-Abstraktion ist nicht frei, obwohl
Jree((*, x', x")) = {x', x"} = Jree(e),
weil x' aus (*, x', x") in AX'.( *, x', x") gebunden wird. Die zweite Bedingung in der Definition der freien Teilausdriicke eines Ausdruckes ist also nicht erfiillt. Diese Bedingung ist notwendig, da globale und lokal gebundene Variable denselben Namen haben konnen. Freie Teilausdriicke diirfen aber lediglich freie Vorkommen globaler Variablen enthalten.
4. Fiir e = letrec Fl = AX1.(*,Xl,(F2,X2)) and F2 = AX2.(+,(*,Xl,X2),X2)
gilt:
Maximal freie Teila1}.sdriicke sind freie Teilausdriicke, die nicht Teilausdruck eines weiteren freien Teilausdruckes sind.
Modifiziert man den Entschachtelungsalgorithmus dahingehend, daB anstatt globaler Variablen, die minimal freie Teilausdriicke sind, maximal freie Teilausdriicke zu Argumenten der neu definierten Kombinatoren werden, so erhalt man eine spezielle Klasse von Kombinatorsystemen, die wir nun charakterisieren werden. Wir nennen diese Kombinatorsysteme wie [Hughes 82] Superkornbinatorsysterne.
Superkombinatorsysteme garantieren eine 'fully lazy' Auswertung, wenn sichergestellt wird, daB kein Argumentausdruck mehrfach ausgewertet wird.
5.3. SUPERKOMBINATORSYSTEME 111
5.3.3 Definition Sei
ein Kombinatorsystem. Sei 1 E {I, ... , r}.
Fl heiBt Superkombinator, falls fiir jedes j E {I, ... ,nil gilt:
(*) mfe('x(x~l, ... ,X~kJ ..... 'x(X~ll, ... ,X~'kln,).el) ~ VarUnur.
R heiBt Superkombinatorsystem, falls jeder Kombinator Fi fUr 1 < < r Superkombinator ist.
Die Bedingung (*) in der Definition der Superkombinatoren stellt sicher, daB die maximal freien Ausdriicke in den 'x-Abstraktionen, die partiellen (nicht reduzierbaren) Kombinatorapplikationen entsprechen, trivial- also Konstante oder Variable - sind. Konstante konnen nicht weiter reduziert werden. Variable sind Platzhalter fUr Argumentausdriicke. Bereits die Vermeidung der Mehrfachauswertung von Argumentausdriicken gewahrleistet also, daB keine maximal freien Teilausdriicke von 'x-Abstraktionen, die durch partielle Kombinatorapplikationen reprasentiert werden, mehrfach ausgewertet werden. Zu einem beliebigen Kombinator kann in sehr einfacher Weise analog zu dem in Kapitel 2 skizzierten Algorithmus von Hughes [Hughes 82/84] ein Superkombinatorsystem konstruiert werden, indem man aus jeder 'x-Abstraktion, die einer partiellen Applikation des Kombinators entspricht und die nicht-triviale maximal freie Teilausdriicke enthalt, diese maximal freien Teilausdriicke abstrahiert und die entstehende Abstraktion als neuen Kombinator definiert.
5.3.4 Definition Die Abbildung
super: Comdef x IN+ -+ P( Comdef)
wird wie folgt definiert:
super( (( ... (F, Xu,· .. , Xlk 1 )·· .), Xnl, ... , XnkJ = e, w.i) {((Fw.i, xi"i, ... , xk'·i), Xnl, ... , XnkJ = e[mfedxi"i, ... , mfek/xk'"i]U} u super( (( ... (F, Xu,.·., Xlk 1 )·· .), Xn-l,l,···, Xn-l,kn_1 )
= (Fw .i , mfe 1 , •.• , mfek), w.(i + 1)) falls n ~ 1 und mfe('x{xnl, ... ,xnkJ.e) C£ Varunur, wobei {mfe 1 , ••• , mfed
:= mfe('x(xnl, ... , xnkJ.e) n (Exp \ (Fun U n u r)),
sonst.
112 KAPITEL 5. ENTSCHACHTELUNG VON SAL-PROGRAMMEN
Die Abbildung super beschreibt die von Hughes vorgeschlagene Transformation. Enthalt die innerste 'x-Abstraktion nicht-triviale maximal freie Teilausdriicke erfolgt die Definition eines neuen Kombinators durch Abstraktion der nicht-trivialen maximal freien Teilausdriicke. Der neu definierte Kombinator erfiillt die Superkombinatoreigenschaft. Die urspriingliche Kombinatordefinitionsgleichung wird dahingehend modifiziert, daB die innere 'x-Abstraktion durch die Applikation des neuen Superkombinators auf die maximal freien Ausdriicke ersetzt wird.
Sind die maximal freien Ausdriicke der inneren 'x-Abstraktion Konstante oder Variable, so ist der vorliegende Kombinator bereits ein Superkombinator, denn wie man leicht sieht, gilt fiir alle j E {I, ... ,n}
Jree-exp('x(Xjl, ... , XjkJ ) •••• 'x(Xnl, ... , xnkJ.e) ~ Jree-exp('x(xnl, ... , Xnkn).e)
Liegt eine Kombinatorgleichung der Form F = e vor (Fall n = 0), so ist e ein variablenfreier, nur aus Kombinatornamen und Konstanten aufgebauter applikativer Ausdruck, der bereits zur Ubersetzungszeit reduziert werden konnte. Lt. Definition ist jede Kombinatorgleichung der Form F = e bereits eine Superkombinatorgleichung und daher ist auch super(F = e) = {F = e}.
Urn Mehrfachauswertungen der Riimpfe solcher Kombinatoren zu vermeiden, werden diese Kombinatordefinitionen in [Peyton-Jones 87] gesondert behandelt. Wir werden in dieser Arbeit auf eine Diskussion solcher Sonderbehandlungen verzichten. In der hier beschriebenen Implementierung werden keinerlei Vorkehrungen getroffen, Mehrfachauswertungen 'nullstelliger' Kombinatoren zu vermeiden.
Das zweite Argument der Funktion super dient nur zur eindeutigen Bezeichnung der neu definierten Kombinatoren. Das zu einem Kombinatorsystem gehorige Superkombinatorsystem wird dann wie folgt festgelegt.
5.3.5 Definition Sei
ein Kombinatorsystem.
Das zu R gehOrige Superkombinatorsystem super(R) wird definiert durch
super(R) :=
U~-l super((( ... (Fi,xil,···,xh )···),x~ U· .. xni'k ) =ei,i.l). - .1 t " tn,
5.3.6 Lemma Sei Rein Kombinatorsystem.
1. Dann ist super (R) ein Kombinatorsystem.
UErsetze in e die Ausdriicke mfej durch die Variablen x~·; fUr aIle 1 ~ j~ k.
5.3. SUPERKOMBINATORSYSTEME 113
2. R und super (R) sind aquivalent, d.h.
red[R]A,r = red[super(R)]A,r.
Wir verzichten hier auf einen formalen Beweis dieses Lemmas. Aussage 1 folgt direkt aus der Definition der Funktion super. Aussage 2 kann induktiv iiber den Aufbau der Reduktionsrelation gezeigt werden, wobei vor allem der Fall der Kombinatorreduktion interessant ist.
Durch die "Aufspaltung" jedes Kombinators in ein System von sich nacheinander aufrufenden Kombinatoren entspricht einer Kombinatorreduktion im urspriinglichen System eine Folge von Kombinatorreduktionen im Superkombinatorsystem.
Wir betrachten ein einfaches Beispiel:
5.3.7 Beispiel Gegeben sei folgendes Kombinatorsystem
D b · ·It 1 1 2 2 3 3 3 A int d 2 A int-int I . a e1 gl . xu' x l .2, X2l, X 22, Xl!, X2l ' X3l E rg un Xl1 E rg , a so. Fl E Funmtxmt-mt.
Das zu R gehorige Superkombinatorsystem hat folgende Form:
Da Fl und F2 bereits Superkombinatoren sind, bleiben sie unverandert. F3 hingegen wird ersetzt durch ein System von 3 Superkombinatoren. Das so entstehende Superkombinatorsystem garantiert eine 'fully lazy' Auswertung.
Betrachten wir etwa eine Reduktion des Ausdruckes (Fl , 4, 5).
(F1, 4, 5) :::} (F2,((F3,4),5),4,5) :::} ( +, (( (F3 , 4), 5), 4), ( (F3 , 4), 5), 5) ---- ----
114 KAPITEL 5. ENTSCHACHTELUNG VON SAL-PROGRAMMEN
((F3,4),5) => ((F3.2 ,(*,4,4)),(*,5,5)) => (F3.1,(+,(*,4,4),(*,5,5)))
=> (+, ((F3 .1 , (+, (*,4,4), (*,5,5))),4), ((F3 .1 , (+, (*,4,4), (*,5,5))),5)) , , , .I
Y Y
=> (+, (+,(+,(*,4,4),(*,5,5)),(*,4,4)), , y ,
(+, (+, (*,4,4), (*,5,5)), (*,5,5))) , ~ ...
Die partielle A pplikation (( F3 , 4), 5) des Kombinators F3 tri tt hier mehrfach auf und bei der Reduktion im urspriinglichen System, wiirde der Teilausdruck des Rumpfes von F3 , der nur von den ersten beiden Parametern abhangt, mehrfach ausgewertet. 1m Superkombinatorsystem ist die Applikation nicht partiell. Sie kann mit zwei Kombinatorreduktionsschritten, in denen die nur von den vorhandenen Argumenten abhangigen Teilausdriicke des urspriinglichen Kombinators als Argumentausdriicke der neu definierten Kombinatoren aufgebaut werden, reduziert werden. An diesem Beispiel erkennt man allerdings auch sofort die Nachteile von Superkombinatorsystemen. Wahrend etwa eine "vollstandige" Applikation des Kombinators F auf 3 Argumente urspriinglich eine Kombinatorreduktion erforderte, sind bei Zugrundelegung des entsprechenden Superkombinatorsystems 3 Kombinatorreduktionen zur Erzielung desselben Resultates notwendig.
Legt man ein festes Kombinatorprogramm (R, e) zugrunde, so kann man die Definition von Superkombinatoren dahingehend abschwachen, daB man die Bedingung (*) aus Definition 5.3.3 nur fUr solche Kombinatoren Fl und solche j E {I, ... , nl} verlangt, fUr die wahrend der Reduktion des Programms eine partielle Applikation der Form
( ... ((Fl , Uu,···, Ulk/1)" .), Uj-l,l,···, Uj-l,k',J_l)
als gemeinsamer Teilausdruck ('geshared') auftreten kann. Denn nur fur solche partiellen Applikationen ist die Gefahr einer Mehrfachauswertung maximal freier Teilausdriicke gegeben. In [Goldberg 87] wird ein Verfahren zur Entdeckung des "Sharing" von partiellen Applikationen beschrieben. Goldberg benutzt die Sharinganalyse, urn den Algorithmus von Hughes zur Erzeugung von Superkombinatoren dahingehend zu optimieren, daB Superkombinatoren nur fUr solche partiellen Kombinatorapplikationen erzeugt werden, die bei der Reduktion des Kombinatorprogramms "geshared" auftreten konnen. Die Optimierung besteht darin, daB bei der Entschachtelung weniger und machtigere Kombinatoren erzeugt werden k6nnen, so daB bei einer Auswertung des Kombinatorprogramms weniger Kombinatorreduktionen durchgefUhrt werden miissen.
5.4. FLACHE KOMBINATORSYSTEME 115
5.3.8 Beispiel Betrachten wir das Kombinatorsystem R des letzten Beispieles. Bei der Reduktion des Kombinatorprogramms (R, (Fl' 4, 5)) tritt nur eine partielle Applikation von F3 auf zwei Argumente 'geshared' auf. Unter Berucksichtigung dieser Information kann man auf die Definition des Kombinators F3.2 in super(R) verzichten und anstattdessen F3 durch
((F3, X~l)' X~l) = (F3.1, (+, (*, X~l' X~l)' (*, X~l' X~l)))
festlegen. Bei der Reduktion des Kombinatorprogrammes (R, (F3, 1,2,3)) tritt keine partielle Applikation 'geshared' auf, so daB bereits Reine 'fully lazy' Auswertung garantiert.
Wir machten an dieser Stelle nicht weiter auf Optimierungen des Superkombinatoralgorithmus eingehen, da fur unsere Arbeit nur wesentlich ist, daB jedes Kombinatorsystem in ein Kombinatorsystem transformiert werden kann, das eine 'fully lazy' Auswertung garantiert. Eine detaillierte Diskussion der Vor- und Nachteile von Superkombinatorsystemen findet sich auch in [Peyton-Jones 87].
Wie wir bereits erwahnten, kann der im vorigen Abschnitt beschriebene Entschachtelungsalgorithmus so modifiziert werden, daB direkt Superkombinatorsysterne erzeugt werden. Man abstrahiert anstatt der global in einem Ausdruck auftretenden Variablen die entschachtelten global auftretenden maximal freien Ausdrucke. Zur Garantierung der 'full laziness' muB zudem jede Abstraktion gesondert behandelt werden. Es ist nicht mehr maglich, einen einzigen Kombinator fur eine Folge von Abstraktionen zu erzeugen.
Wir verzichten hier auf die technisch aufwendige, formale Beschreibung dieser Modifikation des Entschachtelungsalgorithmus und wenden uns einer Klasse von Kombinatorsystemen zu, die sich in der Struktur von den bisher betrachteten Systemen unterscheiden.
5.4 Flache Kombinatorsysteme
Bevor wir die "applicative" und "normal order" Reduktionsstrategien fur Kombinatorsysteme formal erklaren, andern wir die Syntax der Kombinatorsysteme dahingehend ab, daB eine effizientere Implementierung moglich wird. Die zuvor beschriebenen Kombinatorsysteme lehnen sich bzgl. der Struktur der Ausdrucke sehr stark an die Sprache SAL an und entsprechen genau den Systemen, die wir durch die Entschachtelung von SAL-Programmen erhalten haben. Fur eine effiziente Implementierung ist der Aufbau der applikativen Ausdriicke aber ungiinstig, da die Erkennung von reduzierbaren Kombinatorapplikationen durch die Schachtelung von Applikationen erschwert wird.
116 KAPITEL 5. ENTSCHACHTELUNG VON SAL-PROGRAMMEN
Jeder Algorithmus zur Reduktion von Ausdriicken wiederholt so oft wie moglich folgende Arbeitsschritte:
• Erkennung des nachsten reduzierbaren Ausdruckes, entsprechend der Reduktionsstrategie und
• Durchfiihrung der Reduktion.
Zur effizienten Durchfiihrung von Reduktionen haben wir in Kapitel 2 die wesentlichen Techniken, die in der Literatur beschrieben sind, vorgestellt. Dabei fiel bei der Beschreibung der G-Maschine auf, dafi die Bestimmung des nachsten reduzierbaren Ausdruckes einen gewissen Aufwand erforderte, der, wie wir hier zeigen werden, vermeidbar ist. In unserer Notation entspricht eine reduzierbare Kombinatorapplikation
einem Graphen der Form:
• •
•
Da der Zugriff auf jeden Graphen nur iiber die Wurzel moglich ist, mufi der Graph bis zur Tiefe k durchlaufen werden, urn zu erkennen, ob und wie reduziert werden kann. Dieses Durchlaufen entspricht der UNWIND-Phase der G-Maschine, in der auf Grund des vollstandigen CUITyings aller Funktionen nur binare Graphen auftreten. Das Problem ist aber dasselbe.
5.4. FLACHE KOMBINATORSYSTEME 117
Die obige Graphstruktur spiegelt den Typ des Kombinators Fi wieder, der aber fUr die Reduktion ohne Bedeutung ist. Liegt die Kombinatorapplikation allerdings in sogenannter first-order- oder ftacher Notation vor, also in der Form
bzw. als Graph
so ist so fort - im Graphen an der Wurzel- erkennbar, welche Reduktion durchgefUhrt werden kann. Ein Durchlaufen des Graphen ist nicht mehr notwendig. Wie der Name schon sagt, ist die first-order Notation von Applikationen ausreichend fUr Funktionsgleichungs- oder Kombinatorsysteme erster Ordnung, in denen jede Applikation vom Basistyp ist. In beliebigen Kombinatorsystemen benotigt man auch die 'higher-order' oder geschachtelten Applikationen, da die Funktionsausdriicke in Applikationen nicht nur Basisfunktionen oder Kombinatornamen sondern beliebige zusammengesetzte Ausdriicke, insbesondere Applikationen sein konnen. Wir werden einen expliziten Applikationsoperator ap benutzten, urn Applikationen hoherer Ordnung in first-order Notation zu beschreiben:
wobei e vom Typ tl x ... X tk ~ t sei und fUr 1 ~ i ~ k ei den Typ ti habe. Der Applikationsoperator ap dient der einheitlichen Darstellung aller Applikationen in flacher Notation.
Zusammengesetzte Ausdriicke von funktionalem Typ sind insbesondere die bezuglich der Kombinatordefinitionsgleichungen partie lien Applikationen von Kombinatoren. Fur partielle Applikationen existiert keine Reduktionsregel in der zuvor definierten Reduktionsrelation, da eine solche Regel aus dem Bereich der applikativen Berechnungsausdrucke herausfUhren wiirde. Auch partielle Applikationen werden wir in flacher Notation
118 KAPITEL 5. ENTSCHACHTELUNG VON SAL-PROGRAMMEN
mit j ~ k beschreiben.
Die Gesamtanzahl der Parameter, die zur Reduktion der Applikation eines Kombinators notwendig ist, bezeichnen wir als Rang des Kombinators. Der Rang eines Kombinators ist bestimmt durch die Kombinatordefinitionsgleichung.
5.4.1 Definition 1. Sei
Fiir i E {I, ... ,r} heifit dann
n;
rg(Fi) := L mij j=l
der Rang von Fi.
2. Allgemein heifit eine Funktion
rg: Fun- ~ IN
Rangfunktion, falls fiir jedes F E Def(rg) mit
gilt:
typ(F) = (t n x ... X tIm} ~ (t21 X ••• X t2m2 ~ ... (tkl X ••• X tkmk ~ s) ... )
(s E SUD,tij E Typ(S,D) fUr 1 ~ i ~ k und 1 ~j ~ mi)
I
Es gibt ein I E {I, ... , k} mit rg(F) = L mj. j=l
Nach diesen Vorbereitungen definieren wir zunachst die Menge der flachen applikativen Ausdriicke, die die rechten Seiten der sod ann definierten Hachen getypten Kombinatorsysteme bilden. Anschliefiend formalisieren wir eine Reduktionssemantik fUr Hache Kombinatorsysteme und beschreiben, wie beliebige getypte Kombinatorsysteme in Hache Systeme transformiert werden konnen.
5.4.2 Definition Sei rg: Fun- ~ IN eine Rangfunktion mit Definitionsbereich Del( rg). Die Familie
FEXPrg = (FExp;g It E Typ(S, D))
der flachen applikativen Ausdrucke bezuglich der Rangfunktion rg ist die kleinste Typ(S, D) sortierte Menge mit
5.4. FLACHE KOMBINATORSYSTEME 119
1. Vart ~ FExp~g
2. O(£,s) ~ FExP:g O(SI ... S",S) C FExp(SI x ... xs,,-+s)
- rg
(t E Typ(S, D))
(s E S) (n ~ 1,SI, ... ,Sn,s E S)
3. r( £,d) ~ FExp~g r(sl ... sm,d) C FExp(SI x ... xsm-+d)
- rg
(d E D) (m ~ 1,SI, ... ,Sm E SUD,d E D)
4. Verzweigung
F'E bool F'P t e E XPrg, ell e2 E .DXPrg :::::} if e then el else e2 fi E FExp~g (t E Typ(S, D))
5. Lokale Deklaration
Yi E Loct• paarweise verschieden, ei E FExp~~ (1 :5 i :5 k), e E FExp~~ (to, ... , tk E Typ(S, D))
:::::} let YI = el and ... and Yk = ek in e E FExp~~
6. Case-Ausdruck
e E FExp~g mit dE D, red) =: {CI, .. . ,Ck} mit Cj E r(t,I ... t,m"d) fur j E {1, ... ,k}, Yji E Loct,; paarweise verschieden (1 :5 i :5 mj), ej E FExp~g (1:5 j :5 k)
(t E Typ(S,D),tu, ... ,tlm1 , ... ,tkl, ... ,tkm" E SUD) :::::} case e of
CI(Yu,···,Ylml) eli
Ck(Ykl,.·.,Ykm,,) ek esac E FExp~g
7. Basisfunktion- und Konstruktorapplikation
f E O(SI ... S",s) e' E FExps. (1 < i < n) " rg --:::::} f(el, ... ,en) E FExP:g
C E r(sl ... sm,d) e' E FExps. (1 < i < m) " rg --:::::} c(el, ... , em) E FExp~g
8. Kombinatorapplikation
FE Def(rg) mit typ(F) = (tll X ••• X tln1 -+ ( ... (tkl X ••• X tkn" -+ t) .. . )), E1=1 nj :5 rg(F), eij E FExp~~ (1:5 i :5 k,l :5 j :5 ni)
:::::} F( eu, ... , eln1 , e21, ...... , ekl, ... , ekn,,) E FExp~g
120 KAPITEL 5. ENTSCHACHTELUNG VON SAL-PROGRAMMEN
9. Applikation hoherer Ordnung
e E FExptl X ••• xtk-+t e· E FExpt, (1 < i < k) rg , Z rg __ ===> ap( e, el, ... , ek) E FExp~g
Die flachen getypten applikativen Ausdrucke unterscheiden sich lediglich in der Form der Applikationen von den applikativen Ausdrucken (Falle 7-9 in obiger Definition). Die Definition der Kombinatorapplikationen umfaf3t auch den Fall der partiellen Applikation, da weniger Argumentausdrucke zugelassen sind als der Rang des Kombinators. In Applikationen hoherer Ordnung sind aus technischen Grunden auch Kombinatornamen, Basisfunktionen und Konstruktoren als Funktionsausdrucke zugelassen, obwohl diese Falle gesondert behandelt werden.
5.4.3 Definition Ein flacher applikativer Ausdruck e E FExPrg heifit vollstandig flach, falls fur jede in ihm enthaltene Applikation hoherer Ordnung
gilt:
• e ft De! ( rg) U 0 u r und
• e ist nicht von der Form F(el, ... , ek) mit F E De!(rg) und k < rg(F).
CFExPrg bezeichne im folgenden die Familie der vollstandig flachen Ausdrucke.
In vollstandig flachen applikativen Ausdrucken treten Applikationen hoherer Ordnung nur dort auf, wo sie unvermeidbar sind. Wie wir spater sehen werden, kann bei der Reduktion von vollstandig flachen Ausdrucken diese Eigenschaft verloren gehen.
5.4.4 Definition Ein flaches Kombinatorsystem ist ein endliches System von flachen Kombinatordefinitionen.
wobei r ~ 1,Fi E Fun (1 ~ i ~ r), x~ E Arg (1 ~ i ~ r, 1 ~ j ~ r), rgF: Fun- --+ IN mit De!(rgF) = {F1, ... ,Fr }
und rgF(Fi ) := ri (1 ~ i ~ r) ist Rangfunktion, ei E CFExPrg;F mitjree(ei) ~ {xL···,x~JU{Fl, ... ,Fr}
(1 ~ i ~ r) und alle Typen passen.
5.4. FLACHE KOMBINATORSYSTEME 121
Flache Kombinatorsysteme haben eine sehr einfache Struktur und sind, wie wir bereits erHiutert haben und wie sich im weiteren Verlauf zeigen wird, einfacher und effizienter zu implementieren als beliebige "hohere" Kombinatorsysteme. Dies ist auch ersichtlich an der Struktur der Reduktionsregeln fur Kombinatorsysteme. Die fiachen Berechnungsausdrucke enthalten wie ublich keine Argumentvariablen, keine freien lokalen Variablen und als Funktionsvariable nur die des betrachteten fiachen Kombinatorsystems. Sie konnen allerdings Konstante aus AU Tr(A) - unter Zugrundelegung der ublichen strikten Interpretation A = (A, <PA) der Basissignatur - enthalten.
Da wahrend der Reduktion auch Basisfunktionen, Konstruktoren sowie Kombinatornamen als Funktionsausdriicke in Applikationen hoherer Ordnung entstehen konnen, kann man sich nicht auf vollstandig flache Berechnungsausdrucke beschranken. Spezielle Reduktionsregeln werden aber die Reduktion solcher nicht vollstandig fiacher Applikationen hOherer Ordnung zu first-order Applikationen ermoglichen.
5.4.5 Definition Sei rg : Fun- --+ IN eine Rangfunktion.
Die Familie der flachen applikativen Berechnungsausdrucke uber Tr(A)
FComPrg := (FComp~g It E Typ(S,D))
ist die kleinste Typ(S, D) sortierte Menge mit
o. Tr(A) ~ FComp~g (s E SUD)
1. Loct U Fun t ~ FComp~g, (t E Typ( S, D))
2. - 9. analog zur Definition 5.4.2 der fiachen applikativen Ausdrucke
Die Reduktionssemantik fur flache Kombinatorsysteme basiert auf den folgenden Reduktionsregeln. Der Substitutionsoperator fur flache Ausdrucke und Berechnungsausdriicke sei dabei in naheliegender Weise (d.h. analog wie bisher unter Berucksichtigung der veranderten Syntax) definiert.
5.4.6 Definition Sei
F = (Fi (x~ , ... ,x~J = ei 11 ~ i ~ r)
ein fiaches Kombinatorsystem und
FComPF:= {u E FComPrg:r I free(u) ~ {FI , ... , Fr } }
mit rgF(Fi ) = ri(1 ~ i ~ r) die Familie der Berechnungsausdrucke zu F. Wir definieren folgende Reduktionsregeln
--+:F~ FCompF x FComPF
122 KAPITEL 5. ENTSCHACHTELUNG VON SAL-PROGRAMMEN
1. K onstantenreduktion
/(al,'''' an) --+:F ¢A(f)(al, ... , an) (f E n(s1 ... sn,s),ai E AS'(1:5 i:5 n),SI, ... ,sn,s E S)
2. Verzweigungsreduktion
if T then Ul else U2 ft --+:F Ul, if F then Ul else U2 ft --+:F U2 (Ul,U2 E FComP:F)
3. let-Reduktion
let Yl = Ul and ... and Yk = Uk in U --+:F u[yI/UI, ... , Yk/Uk] (u, Ul, ... , Uk E FComP:F)
4. case-Reduktion
case Cj(Ujl, ... , Ujm,) of .. · Cj(Yjl, ... , Yjm'): Uj'" esac --+:F Uj[YjI/Ujl,"" Yjm,!Ujm,] (uj, Ujl, ... , Ujm, E FComP:F)
5. Kombinatorreduktion (Kopierregel)
Fi(Ul, ... , Ur.) --+:F ei[xUul,"" X~.IUr.l (Ul, ... , ur, E FComP:F,1 :5 i :5 r)
6. Applikationsreduktionen (Sammelregeln)
ap(J.t,Ul, ... ,Um ) --+:F J.t(Ul, ... ,Um) (I' E nUrU{F1, ... ,Fr })
ap(F(Ul, ... , Ut), UHl, ... , UT) --+:F F(Ul, ... , Ut, UHl, ... , UT) falls T :5 rg:F(F)
Die Reduktionsregeln fUr flache Berechnungsausdriicke unterscheiden sich von den bisherigen Reduktionsregeln vor allem dadurch, daB die komplexe Kombinatorreduktion aufgespalten wird in das eigentliche Uberschreiben der Kombinatorapplikation durch den Rumpf (--+ Kopierregel) und das Erkennen von Kombinatorapplikationen durch "Aufsammeln" der Argumentlisten (--+ Sammelregeln). Es scheint zunachst, daB die Reduktion flacher Kombinatorsysteme durch die zusatzlichen Regeln noch aufwendiger als die iibliche Reduktion wird. Dies ist aber nicht der Fall, da ja durch die vollstandige flache Struktur der Kombinatorriimpfe i.a. eine Anwendung der Applikationsreduktionsregeln nicht notwendig ist. Die Sammelregeln kommen nur zum Einsatz, wenn dynamisch durch Funktionsparameter oder Reduktion von funktionswertigen Ausdriicken 'higher-order' Applikationen von Kombinatoren und Basisfunktionen oder Konstruktoren entstehen.
Die Reduktionsrelation fUr flache Kombinatorsysteme wird wie iiblich erklart. Wir geben die formale Definition hier der Vollstandigkeit halber dennoch an.
5.4. FLACHE KOMBINATORSYSTEME 123
5.4.7 Definition Mit den Voraussetzungen aus Definition 5.4.6 wird die Reduktionsrelation
wie folgt festgelegt:
1. ---. :F~=}:F,
2. idFCompF ~=}:F,
3. Mit U =}:F u', Ui =}:F ui (1 5 i 5 k, u, u', Ui, ui E FComP:F) gilt auch:
• if u then UI else U2 fi =}:F if u' then u~ else u~ fi
• let YI = UI and ... Yk = Uk in U I 'd ,., =}:F et YI = UI an ... Yk = uk In U
• case U of ... U· .•• esac =}:F case u' of ... u'· ... esac , , • f.L(UI, ... , Uk) =}:F f.L(u~, ... , U~),
wobei f.L E n u r u {FI' ... , Fr}U {ap}
Auch diese Reduktionssemantik ist kon£luent.
Ein £laches Kombinatorprogramm besteht aus einem £lachen Kombinatorsystem und einem £lachen applikativen Ausdruck yom Basistyp. Die Reduktionssemantik fUr £lache Kombinatorprogramme wird vollkommen analog zu Definition 5.1.6 erkHirt.
Als nachstes formalisieren wir die Transformation von 'higher-order' Kombinatorsystemen in £lache Kombinatorsysteme. Dabei bezeichne
ComE,DS(E)
die Menge der getypten Kombinatorsysteme iiber der Basissignatur "E und der Datenstruktursignatur DS(E) und
FlatComE,DS(E)
die Menge der £lachen getypten Kombinatorsysteme. Weiterhin bezeichne fiir Kombinatornamen F I , ... ,Fr E Fun:
AppExp{F1, ... ,Fr } := {e E AppExp I free(e) n Fun ~ {FI , ... ,Fr } }
die Menge der applikativen Ausdriicke iiber {FI' ... ,Fr } und bei Zugrundelegung einer Rangfunktion rg mit Definitionsbereich {FI , ... , Fr }:
FExp{F1, ... ,Fr },r9 = {e E FExPr9 I free(e) n Fun ~ {FI , ... , Fr } }
die Menge der £lachen applikativen Ausdriicke iiber {PI, ... ,Fr } mit Rangfunktion rg. Wir definieren zunachst induktiv iiber den Aufbau der applikativen Ausdriicke die Transformation in £lache Ausdriicke.
124 KAPITEL 5. ENTSCHACHTELUNG VON SAL-PROGRAMMEN
5.4.8 Definition Sei C = {Fl , . .. , Fr} ~ Fun und rg : Fun- --+ 1N eine Rangfunktion mit Definitionsbereich C. Die Transformation
fiatten := fiattenc,rg : AppExpc --+ FExPC,rg
wird induktiv definiert durch:
1. fiatten( var) := var fur var E Arg U Loc. 2. fiatten(J-L) := J-L fur J-L E 0 U r U C. 3. fiatten(if e then el else e2 fi)
:= if fiatten( e) then fiatten( et) else fiatten( e2) fi fUr e, el, e2 E AppExpc.
4. fiatten(let Yl = el and ... and Yk = ek in e) := let Yl =fiatten(et) and ... and Yk = fiatten(ek) in flatten(e)
fUr e, el, ... , ek E AppExpc.
5. fiatten(case e of .. . Cj(Yjl, ... ,Yjm,): ej ... esac) := casefiatten(e) of ... Cj(Yjl, ... ,Yjm,): fiatten(ej) ... esac
6. fiatten((e,el, ... ,ek)):= J-L(fiatten((et), ... ,fiatten(ek)) falls J-L = fiatten(e) und
(J-L E 0 U r oder (J-L E C mit rg(J-L) ~ k)),
F(el, ... , em,fiatten(el), ... ,fiatten(ek)) falls fiatten(e) = F(el, ... ,em) und rg(F) ~ m + k,
ap(fiatten(e),fiatten(ed, ... ,fiatten(ek)) sonst.
Die Transformation von applikativen Ausdrucken in flache Ausdriicke geschieht also dadurch, dafi element are Funktionsbezeichner wie Basisfunktionen, Konstruktoren und Kombinatornamen vor die Applikation gezogen werden und dafi mehrere Parameterlisten von Kombinatoren, solange bis der Rang des Kombinators erreicht ist, verschmolzen werden. AIle ubrigen Applikationen werden mit Hilfe des ap-Symbols reprasentiert. Insbesondere gilt:
5.4.9 Korollar Sei C ~ Fun, rg: Fun- --+ 1N eine Rangfunktion mit Definitionsbereich C.
VeE AppExpc: fiatten(e) ist vollstandig flach.
Beweis: Annahme, fiatten( e) enthalt eine Applikation hoherer Ordnung
ap(e, el, ... , em)
mit e E Cuo ur oder e = F(el, ... , ek) mit k ~ rg(F)§. Aus der Definition
§Aufgrund des strengen Typkonzeptes ist k < rg(F) gleichbedeutend mit k + m ~ rg(F).
5.4. FLACHE KOMBINATORSYSTEME 125
der Abbildung flatten, Punkt 6., folgt unmittelbar, dafi beide FaIle nicht moglich sind. 0
Unter Verwendung dieses Resultates ergibt sich folgende Ubersetzung von Kombinatorsystemen in Hache Kombinatorsysteme.
5.4.10 Definition
Flat: COmI;,DS(I;) --+ FlatComI;,DS(I;)
ist definiert durch:
Flat ( (( ... (Fi' xlI'· .. ,xim.J,··· ,Xi,l'···' xi.m.kJ = €i 11 :5 i :5 r)) := (Fi(xil'··· ,xim'l ' ... ,Xi,l' ... ,xi,m'k ) = flattenc,rg (€i) 11 :5 i :5 r), .
wobei C := {FI' ... ,Fr} und rg : Fun- --+ 1N mit De/( rg) = C und rg(Fi) = E;~l mij.
5.4.11 Beispiel Zu dem in Beispiel 5.2.6 gegebenen Kombinatorsystem erhaIt man durch Anwendung der Transformation Flat folgendes Hache Kombinatorsystem:
( QSort (lintlist):= case lof NIL: NIL; CONs(yint, y~ntlist) :
Append ( QSort (Filter (Tlt(YI), Y2)), CONS(YI, QSort(Filter (Tgeq(YI), Y2))))
esac Filter (testint-+bool, l,intlist):= case [' of
NIL: NIL CONs(hint, tintlist) :
esac Append (l~ntlist, lkntlist):= case It of
NIL: 12 ;
if ap( test, h) then CONS( h, Filter( test, t)) else Filter (test, t) fi
CONs(yint , yhntlist) : CONs(YI,Append(Y2, 12 ))
esac := ~ (X2' xt) := < (X2,Xt) )
126 KAPITEL 5. ENTSCHACHTELUNG VON SAL-PROGRAMMEN
In diesem Kombinatorsystem treten zwei partielle Applikationen der Kombinatoren Tgeq und Tit auf. Die Applikation hoherer Ordnung (test, h) im Rumpf des Kombinators Filter wird mittels des Symbols ap in eine flache Notation iiberfiihrt.
Jedes flache Kombinatorsystem kann natiirlich in einfacher Weise in ein gewohnliches Kombinatorsystem umgewandelt werden. Auch diese Transformation wollen wir formalisieren, da wir sie spater beim Beweis der Aquivalenz beider Kombinatorsystemtypen benutzen werden.
5.4.12 Definition Sei C = {FI , ... , Fr} ~ Fun und rg : Fun- ~ IN mit Definitionsbereich C eine Rangfunktion. Die Transformation
deflatten := deflattenc,rg : FExPC,rg ~ AppExpc
ist induktiv iiber den Aufbau der flachen applikativen Ausdriicke definiert durch:
1. deflatten( var) := var fiir var E Arg U Loc.
2. deflatten(J1.):= J1. fiir J1. E 0 U r U C.
3. deflatten(if e then el else e2 fi) := if deflatten( e) then deflatten( et) else deflatten( e2) fi
fiir e, el, e2 E AppExpc.
4. deflatten(let YI = el and ... and Yk = ek in e) := let YI =deflatten(et) and ... and Yk = deflatten (ek)
in deflatten (e) fiir e,el, ... ,ek E AppExpc.
5. deflatten(case e of ... Cj(Yjl,"" Yjk,) : ej ... esac) := case deflatten( e) of
... Cj(Yjl, ... ,Yjk,) : deflatten( ej) ... esac
6. deflatten(J1.( el, ... ,em)) := (J1., deflatten( et), ... , deflatten( em)) fiir J1. E 0 U r.
7. deflatten(F( eu, ... ,eInl , e21, ... ,e2n2' ...... ,ekl, ... ,eknk)) := (( ... (F, deflatten(eu), ... , deflatten(eInJ), .. . ),
deflatten(ekd, ... , deflatten(eknk)) falls typ(F) = (tu X ... X tInl ~ ( ... (tki X ... X tknk ~ t) ... ) und eij E FExpt., (1 :5 i :5 k, 1 :5 j :5 ni).
8. deflatten( ape e, el, ... , ek)) := (deflatten( e), deflatten( ed, ... , deflatten( ek))
(e, el, ... ,ek E FExPC,rg)'
5.4. FLACHE KOMBINATORSYSTEME 127
Damit folgt dann
DeFlat : FlatCom~,DsCE) -t COm~,DS(~)
mit
DeFlat( (Fi(xL ... ,x~ ) = ei 11 :$ i :$ r)) := ((((Fi,xL ... :xtJ···),xL+l,· .. ,X~J = deflatten{Fl, ... ,Fr},rg(ei)
11:$i:$r),
wobei 1 :$ kil :$ ... :$ kil :$ r i mit typ(F;) = (tl x ... x tk'l -t (tk'l+l x ... x tk,2 -t ( ...
(tk,,+l x .,. X t r , -t t) .. . )),
Es bestehen folgende Beziehungen zwischen den Transformationen flatten und deflatten.
5.4.13 Lemma Sei C ~ Fun, rg : Fun- -t :IN eine Rangfunktion mit Definitionsbereich C. Es gilt:
1. VeE AppExPC,rg: deflatten(flatten(e)) = e.
2. Fiir beliebiges e E FExPC,rg gilt nicht immer flatten( deflatten( e) )=e, aber fUr vollsUindig flache Ausdriicke e gilt:
flatten( deflatten( e) )=e.
Beweis: zu (i): Der Beweis erfolgt induktiv iiber den Aufbau der applikativen Ausdriicke. Interessant ist lediglich der Fall der Applikation (e, el, ... ,ek), bei dem entsprechend der Definition der Abbildung flatten drei Fane unterschieden werden. Die Behauptung folgt dann mit der Definition von deflatten unter Ausnutzung der Induktionsvoraussetzung.
zu (ii): Ein einfacher flacher Ausdruck, fUr den
flatten( deflatten( e)) =J. e
gilt, ist etwa der Ausdruck
mit K :$ rg(F). Wie man leicht sieht, ist dieser Ausdruck nicht vollstandig flach. Hat F etwa den Typ (tl x ... X tk -t (tk+1 X ... X tK -t t)), so gilt:
128 KAPITEL 5. ENTSCHACHTELUNG VON SAL-PROGRAMMEN
aber
flatten(((F, el, ... , ek), ek+1,"" eK)) = F(el,"" ek, ek+1,' .. ,eK) =f. ap(F(el"" ,ek),ek+l,'" ,eK)'
Wir beweisen induktiv uber die Struktur der vollstandig flachen applikativen Ausdrucke, dafi fur alle solchen Ausdrucke e die Abbildungen flatten und deflatten zueinander invers sind. Fur VariabIen, Kombinatornamen, Basisfunktionen und Konstruktoren gilt naturlich obige Gleichheit. Fur Verzweigungen, let- und case-Abstraktionen sowie first-order Applikationen von Basisfunktionen, Konstruktoren und Kombinatoren folgt die Aussage sofort mittels der Induktionsvoraussetzung.
Der einzig interessante Fall ist der Fall der Applikation hoherer Ordnung. Der Ausdruck e habe also die Form
wobei eo rt. n u rue und eo nicht von der Form F( e~, ... ,eD mit k ::; rg(F) ist. Es gilt:
deflatten(ap( eo, ... ,em)) = (deflatten( eo), ... , deflatten( em)).
Laut Induktionsvoraussetzung ist flatten( deflatten( eo) )=eo. Aufgrund der Einschrankung auf vollstandig flache Ausdrucke ist in der Definition von flatten fUr Applikationen nur der dritte Fall moglich, d.h.
flatten( deflatten( ap( eo, ... , em) ) ) = ap(flatten( deflatten( eo)), ... , flatten( deflatten( em))) = ap(eo, ... , em) (It. Induktionsvoraussetzung)
o
Die Abbildungen flatten und deflatten lassen sich in kanonischer Weise fur Berechnungsausdrucke erweitern. Fur Konstante a E AU Tr(A) wahlt man dabei:
flatten(a) := a bzw. deflatten(a) := a.
Fur Berechnungsterme C(UI, ... , um ) mit C E r gelte
flatten ( c( UI, ... ,um)) := c(flatten( ut), ... ,flatten( um)).
Unter Zugrundelegung dieser Erweiterungen gilt:
5.4.14 Lemma 1. Die Aussagen von Lemma 5.4.13 geiten auch fUr Berech-nungsausdrucke.
5.4. FLACHE KOMBINATORSYSTEME 129
2. Sei Fein flaches Kombinatorsystem und FComP:F die Menge der Berechnungsausdriicke zu F. Dann gilt:
'if U E FComp:F: U =*:F flatten(deflatten(u)).
d.h. jeder Berechnungsausdruck kann zu einem vollstandig flachen Berechnungsausdruck reduziert werden.
Beweis: zu(i): Der Beweis von Lemma 5.4.13 ist direkt iibertragbar.
zu (ii): Wegen (i) gilt fUr alle vollstandig flachen Berechnungsausdriicke u:
u = flatten(deflatten(u)).
Nicht vollstandig flache Berechnungsausdriicke enthalten Applikationen hoherer Ordnung
ap( Uo, ... , urn)
mit Uo E n u rue, wobei C die Menge der in F auftretenden Kombinatornamen sei, oder Uo = F(Ul, ... , Uk) und k < rg(F). Diese Applikationen lassen sich aber mit den "Sammelregeln" fUr Applikationsreduktionen zu first-order Applikationen reduzieren. Jeder Berechnungsausdruck Hi-fit sich also zu einem vollstandig flachen Ausdruck reduzieren.
Dafi insbesondere u =*:F flatten( deflatten( u))
beweist man formal iiber die Struktur der flachen Berechnungsausdriicke. Wir betrachten hier den einzig interessanten Fall des Induktionsschlusses fUr Applikationen h6herer Ordnung. Der Ausdruck u habe also die Form
Dann gilt:
deflatten( ap( Uo, ... , Uk)) = (deflatten( uo), ... , deflatten( Uk)).
Gemafi der formalen Definition von flatten sind drei FaIle zu unterscheiden:
1. Falls deflatten( uo) E n U rue, so gilt:
flatten(deflatten(uo), ... , deflatten(uk)) = flatten( deflatten( Uo ) (flatten( deflatten( ut)), · .. ,flatten( deflatten( Uk)))
130 KAPITEL 5. ENTSCHACHTELUNG VON SAL-PROGRAMMEN
Lt. Induktionsvoraussetzung ist fur alle 0 ~ i ~ k:
Ui =* F flatten( deflatten( Ui)).
Mit der erst en Sammelregel folgt damit, da in diesem Fall
flatten( deflatten( uo)) = Uo :
ap(UO,Ul, ... ,Uk) =*FUO(Ul, ... ,Uk) =*F uo(flatten( deflatten( ut)), ... , flatten( deflatten( Uk)) , '
'" = flatten ( deflatten( ap( Uo, ... , Uk))
2. Falls flatten( deflatten( uo)) = F(Ul, ... , urn) fUr ein FEe mit rg( F) ~ m + k und Ul, ... ,Urn E FComPF. Dann gilt bekanntlich:
flatten( deflatten( uo)), ... , deflatten( Uk)) = F( Ul, ... , Urn, flatten( deflatten( Ul)), ... , fiatten( defiatten( Uk)).
Laut Induktionsvoraussetzung gilt wiederum:
Uo =* F flatten( defiatten( Uo)) = F( Ul, ... , Urn)
und fUr aIle 1 ~ i ~ k:
Uj =* F fiatten( defiatten( Uj))
Damit ergibt sich auf Grund der induktiven Definition der Reduktionsrelation unter Verwendung der zweiten Sammelregel fur Applikationen haherer Ordnung:
ap(uo, ... , Uk) =* F ap(F( Ul, ... , Urn), flatten( deflatten( ut)), ... , fiatten( defiatten( Uk))) => F F( Ul, ... , Urn, flatten( deflatten( Ul)), ... , flatten( defiatten( Uk)))
, .f
'" = fiatten( defiatten( ap( Uo, ... , Uk))
Damit folgt die Behauptung.
3. In dem iibrigen Fall folgt die Behauptung direkt aus der Induktionsvoraussetzung.
D
Folgender Zusammenhang zwischen dem Substitutionsoperator fur Ausdrucke bzw. Berechnungsausdrucke und der Abbildung defiatten sind zum Nachweis der Aquivalenz zwischen fiachen und nicht-fiachen Kombinatorsystemen von Nutzen.
5.4. FLACHE KOMBINATORSYSTEME 131
5.4.15 Lemma Sei C ~ Fun, rg : Fun- -+ :IN eine Rangfunktion mit Definitionsbereich C. Seien e E FExPC,rg' varl, ... , var p E Var und el, ... ,ep E FExPC,rg, wobei fiir i E {I, ... ,p} vari und ei denselben Typ haben mogen. Dann gilt:
deflatten(e[varl/el, ... , varp/ep]) = deflatten(e) [varl/ deflatten(ed, ... , varp/ deflatten(ep)).
Beweis: (induktiv iiber die Struktur von e)
1. Fiir Variablen var E Var gilt:
deflatten( var[varl/el, ... , varp/ep]) _ { deflatten( ei) falls var = var i fiir ein i E {I, ... ,p}, - var falls var tt. {varl' ... , var p} = deflatten( var)[varl/ deflatten(ed, ... , varp/ deflatten(ep))
2. Fiir Basisfunktionen und Konstruktoren ist die Aussage trivial.
3. In allen iibrigen Fallen folgt die Behauptung in einfacher Weise mittels der Induktionsvoraussetzung unter Ausnutzung der induktiven Definition des Substitutionsoperators.
o
Nach diesen Vorbereitungen zeigen wir nun den Satz, auf dem die Aquivalenz von Hachen und nicht-Hachen Kombinatorsystemen beruht.
5.4.16 Satz Sei n ein getyptes Kombinatorsystem und Compn die Familie der Berechnungsausdriicke zu n. Sei F das zu n gehorige Hache Kombinatorsystem und FComP:F die Familie der Berechnungsausdriicke zu F.
1. Fiir u, u' E Compn mit u =?n u' gilt:
flatten( u) =*:F flatten ( u').
2. Fiir u, u' E FCompn mit u =?:F u' gilt:
deflatten( u) =*n deflatten( u').
Beweis: Der Nachweis beider Aussagen erfolgt jeweils induktiv iiber den Aufbau der jeweiligen Reduktionsrelationen: zu (1): Seien u, u' E Compn mit u =?n u'.
132 KAPITEL 5. ENTSCHACHTELUNG VON SAL-PROGRAMMEN
• Falls U -+R u' Reduktionsregel ist, sind folgende FaIle zu unterscheiden:
1. Fiir Konstantenreduktionen, Konstruktorreduktionen und Verzweigungsreduktionen folgt die Behauptung direkt aus der Definition der Abbildung flatten.
2. Fiir let-Reduktionen
let Yl = Ul and ... and Yk = Uk in U -+R U[yl/ul, ... , Yk/Uk]
folgt: flatten(let Yl = Ul and ... and Yk = Uk in u) = let Yl = flatten(ud and ... and Yk = flatten(uk)
in flatten( u) -+ F flatten( u) [yl/ flatten( ud, ... , Yk / flatten( Uk)] ~ F flatten( deflatten(
flatten ( u)[yl/ flatten ( Ul), ... ,Yk/ flatten( Uk)])) (Lemma 5.4.14 (2))
= flatten ( deflatten (flatten ( u)) [Yl / deflatten(flatten ( Ul)), ... , Y k / deflatten(flatten( Uk))])
(Lemma 5.4.15) = flatten(u[yl/Ul, ... , Yk/Uk]) (Lemma 5.4.14 (1))
3. Fiir case-und Kombinatorreduktionen erfolgt der Nachweis vollig analog zum Fall der let-Reduktionen.
• Mittels eines einfachen Induktionsschlusses, auf dessen explizite Durchfiihrung wir hier verzichten, folgt dann die Behauptung (1).
zu (2): Seien nun u, u' E FComPF mit U =*F u'.
• Falls U -+ F u' Reduktionsregel ist, unterscheiden wir folgende FaIle:
1. Die Giiltigkeit der Behauptung fiir Konstanten-, Verzweigungs-, let-, case- und Kombinatorreduktionen folgt in einfacher Weise mit Lemma 5.4.15.
2. 1m Fall der Applikationsreduktionen gilt sogar
deflatten(u) = deflatten(u'),
also insbesondere die Behauptung.
• Per Induktionsschlu:B folgt dann sofort die Behauptung.
o
Ais direkte Konsequenz dieses Satzes ergibt sich die Aquivalenz von nichtflachen und flachen Kombinatorsystemen bzgl. ihrer nichtdeterministischen Reduktionssemantik.
5.5. REDUKTIONSSTRATEGIEN 133
5.4.17 Korollar Sei (R,e) ein Kombinatorprogramm vom Typ s E SUD und sei :F das zu R gehorige Hache System. Dann gilt:
red[(R, e}] = red[(:F,jlatten(e)}]
Beweis: Sei a E AS U Tr(A). Dann gilt:
red[(R,e}] = a {:} e =*n a {:} jlatten( e) =* F a {:} red[(:F,jlatten(e)}] = a.
(Definition) (Satz 5.4.16)
o
In Zukunft werden wir hauptsachlich Hache Kombinatorsysteme betrachten, da diese die Grundlage unserer Implementierung bilden. Mit Kombinatorsystemen meinen wir dann jeweils Hache Kombinatorsysteme, ohne explizit darauf hinzuweisen. Auch die normal order und applicative order Reduktionsstrategien prazisieren wir im folgenden nur fUr Hache Systeme.
5.5 Reduktionsstrategien
In diesem Abschnitt definieren wir die normal order und applicative order Reduktionsstrategie fiir Hache Kombinatorsysteme. Die Definitionen dieser Strategien ergeben sich aus den Definitionen der Strategien fiir SAL durch Ubertragung auf den Fall von Hachen Berechnungsausdriicken.
Wir beginnen mit der Definition einer Normalform fiir Hache Berechnungsausdriicke, die wir als K ombinatornormalform bezeichnen. Die Kombinatornormalform entspricht der 'weak head normalform' fiir A-Ausdriicke [Peyton-Jones 87].
5.5.1 Definition Sei:F ein Haches Kombinatorsystem mit den Kombinatoren F1, ... , Fr und zugehoriger Rangfunktion rg.
Ein geschlossener Berechnungsausdruck u zu F heifit in K ombinatornormalform, falls
1. u E A UTr(A) U 0+ oder
2. U = Jl(Ul, ... , urn) mit Jl E r oder Jl E {F1, ... , Fr } mit rg(Jl) < m.
Ausdriicke in Kombinatornormalform sind also Konstante, nicht-nullstellige Basisfunktionen, Konstruktorapplikationen oder partielle Kombinatorapplikationen.
134 KAPITEL 5. ENTSCHACHTELUNG VON SAL-PROGRAMMEN
5.5.2 Definition Sei Fein flaches Kombinatorsystem und FComPF die Familie der geschlossenen Berechnungsausdrucke zu F.
Die normal order oder call-by-name Reduktionsstrategie
fur flache Kombinatorsysteme F wird wie folgt festgelegt:
1. ~F~=>}'
2. 1st f(al, ... ,ai-I,Ui, ... ,Um) E FComPF mit aj E AUTr(A) fur 1:5 j :5 i - 1 und Ui rt. AU Tr(A), so impliziert Ui =>} u~:
3. 1st if UI then U2 else U3 fi E FComPF mit UI rt. {T, F}, so impliziert UI =>} u~:
if UI then U2 else U3 fi =>} if u~ then U2 else U3 fi
4. 1st case U of ... Cj(YjI, ... , Yjm,) : Uj ... esac E FComPF und U ist nicht in Kombinatornormalform, so impliziert U =>} u':
case U of ... esac =>} case u' of ... esac
Die normal order Strategie reduziert Berechnungsausdrucke bis zur Kombinatornormalform. Moglichkeiten zu paralleler Reduktion ergeben sich nur fur die Argumentausdriicke von Basisfunktionen.
Der Vollstandigkeit halber definieren wir auch die applicative order Strategie fiir Kombinatorsysteme. Bei dieser Strategie werden Berechnungsausdriicke zu strikter Kombinatornormalform reduziert, da vor der Reduktion von Applikationen alle Argumente so weit wie moglich reduziert werden. Dies gilt insbesondere auch fiir Konstruktorapplikationen. An dieser Stelle unterscheiden sich die Kombinatornormalform und die strikte Kombinatornormalform.
5.5.3 Definition Sei Fein flaches Kombinatorsystem mit den Kombinatoren F1 , .•. , Fr und Rangfunktion rg.
Ein geschlossener Berechnungsausdruck U zu F heiBt in strikter Kombinatornormalform, falls
1. U E AU Tr(A) U n+ oder
2. U=Jl(UI, ... ,Um) mit
• Jl E {FI, ... , Fr } und rg(Jl) < m oder
5.5. REDUKTIONSSTRATEGIEN 135
• JL E r und Ul, ... ,Urn sind in strikter Kombinatornormalform.
Damit ergibt sich folgende Definition der applicative order Reduktionsstrategie fUr Kombinatorsysteme.
5.5.4 Definition Sei Fein £laches Kombinatorsystem und FComP:F die Familie der geschlossenen Berechnungsausdrucke zu F.
Die applicative order oder call-by-value Reduktionsstrategie
wird definiert durch
1. Falls fUr u, u' E FComP:F: U -:F u' Konstanten- oder Verzweigungsreduktion ist, so gilt auch:
a , u~:F U.
2. Fur let Yl = Ul and .. . in U E FComP:F gilt:
(a) Falls fur ein i E {I, ... , k} Ul, ... ,Ui-l in strikter Kombinatornormalform sind und Ui nicht in strikter Kombinatornormalform ist, so ist mit
auch
let Yl = Ul and ... Yi = Ui ... and Yk = Uk in U
~F let Yl = Ul ... Yi = u~ ... Yk = Uk in u.
(b) Falls fur aIle i E {I, ... , k} Ui in strikter Kombinatornormalform ist, gilt:
let Yl = Ul and ... and Yk = Uk in U ~F U[yt/Ul,"" Yk/Ukj.
3. Fur case U of ... Cj(Yjl, ... , YjrnJ : Uj ... esac E FComP:F gilt:
(a) Falls U nicht in strikter Kombinatornormalform ist, ist mit
auch case U of ... esac ~ F case u' of ... esac
(b) Falls U = Cj(Ujl, ... , UjmJ ) fur ein j in strikter Kombinatornormalform ist, so gilt:
136 KAPITEL 5. ENTSCHACHTELUNG VON SAL-PROGRAMMEN
4. Fur f-l(Ul, ... ,Uk) E FComp;: mit f-l E nUrU{F1, ... Fr } gilt:
(a) Falls fur ein i mit 1 ::; i ::; k Ul, ... , Ui-l in strikter Kombinatornormalform sind und Ui noch nicht, so ist mit
auch f-l( Ul, .•. , Uk) =>} f-l( Ul, ..• , u~, . .. ,Uk)
(b) Falls f-l = Fj E {FI , ... , Fr } mit rg(f-l) = k und fur alle 1 ::; i ::; k Ui in strikter Kombinatornormalform ist, gilt:
wobei Fj(Xjl,'" ,Xjk) = ej
die Kombinatordefinitionsgleichung von Fj in :F sei.
5. Fur ap( U, UI, ... , Uk) E FComp~ gilt:
(a) Falls fUr ein i mit 1 ::; i ::; k UI," ., Ui-l in strikter Kombinatornormalform sind und Ui noch nicht, so ist mit
auch
(b) Falls UI, ... , Uk in strikter Kombinatornormalform sind, aber U noch nicht, so ist mit
U =>} u'
auch ap(u, UI,"" Uk) =>} ap(u', UI, ... , Uk)
(c) Falls U E n U r U {FI , ... , Fr } und UI, ... , Uk in strikter Kombinatornormalform sind, gilt:
Falls U = F(ih, ... , urn) mit m < rg(F) und UI, ... , Uk in strikter Kombinatornormalform, so ist
5.5. REDUKTIONSSTRATEGIEN 137
Die applicative order Reduktionsstrategie entspricht der applicative order Reduktionsstrategie fUr SAL-Ausdriicke mit dem Unterschied, dafi 'x-Abstraktionen hier als partielle Applikationen von Kombinatoren auftreten.
Die Reihenfolge der Auswertung der Argumente bei Applikationen h6herer Ordnung entspricht der Reihenfolge der Auswertung von Applikationen in SAL bei Zugrundelegung der gleichen Reduktionsstrategie.
Die applicative order Strategie bietet durch die strikte Behandlung aller Funktionssymbole einschlieBlich der Konstruktoren sehr viele Moglichkeiten zur Parallelisierung des Reduktionsprozesses.
1m folgenden Kapitel werden wir ein Verfahren zur Entdeckung von potentieller Parallelitat in Kombinatorprogrammen mit nicht-strikter Semantik entwickeln.