Kapitel5

Entschachtelung von SAL-Prograllllllen

Den Anfang dieses Kapitels bildet die formale Definition der Syntax und Reduk­tionssemantik getypter Kombinatorsysteme. Diese sind die Zielsprache des Ent­schachtelungsprozesses, der im AnschluB daran beschrieben wird. Durch eine wei­tere Transformation, die in Abschnitt 5.3 erliiutert wird, erzielt man die Erzeugung von Superkombinatorsystemen im Sinne von [Hughes 82]. 1m Hinblick auf die lm­plementierung 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 Funktionsgleichungs­systeme hoherer Ordnung bestehend aus einer endlichen Anzahl von Funktionsde­finitionen 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 Aus­druck 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 Kombinatordefinitio­nen im Kombinatorsystem den Prozedurdeklarationen. Der applikative Ausdruck reprasentiert das Hauptprogramm.

Kombinatorprogramme entsprechen speziellen SAL-Ausdriicken, bei denen Re­kursion 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 Teil­klasse der SAL-Programme.

Auch die Reduktionssemantik lieBe sich auf diese Weise auf Kombinatorpro­gramme 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 auf­treten, auszunutzen.

Indem man bei der Reduktionssemantik ein festes Kombinatorsystem zugrun­delegt, kann man auf die Reduktionsregeln fUr die {3- und letrec-Reduktion ver­zichten und an deren Stelle spezielle Kombinatorreduktionen definieren.

Zur Definition der nichtdeterministischen Reduktionssemantik fUr Kombina­torsysteme gehen wir wie in SAL von einer strikten flachen Interpretation A = (A.l' ¢A) der Basissignatur aus und wahlen wie bisher fiir die Datenstruktursig­natur 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-Be­rechnungsausdriicke. Insbesondere ist also die Substitution entsprechend Defini­tion 1.3.4 auch fUr applikative Berechnungsausdriicke erkHirt. Die Berechnungs­ausdrucke 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 letrec­Reduktionsregeln werden allerdings ersetzt durch die einfachere Kombinatorreduk­tion.

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 Kombina­torsystem. 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 Kombi­natorprogramm transformiert werden kann.

5.2. DER ENTSCHACHTELUNGSALGORITHMUS 99

5.2 Der Entschachtelungsalgorithmus

Der Entschachtelungsalgorithmus baut auf der einfachen Idee auf, lokale Funk­tionsdefinitionen in einem SAL-Programm - also >'-Abstraktionen und letrec­Ausdriicke - 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 herausabstra­hiert 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 ap­plikativ 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 applikati­ven 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 Argumentva­riablen 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 Ent­schachtelungsalgorithmus, der das zu entschachtelnde Programm "top-down", also von auBen nach innen durchliiuft. 1m allgemeinen Fall enthalten die >.- und letrec­Ausdriicke 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 Va­riablen, 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 Variablen­namen, 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 Varia­bIen 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 ge­wahlt. Die Stetigkeit von We,u beziiglich (P(Arl U Loc), ~r ist offensicht­lich. 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 Aus­druck, 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 Funk­tionsvariable 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 Komponen­tenfunktionen 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 definier­ter 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 Kom­binatordefinition 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 deut­lich, 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 so­genannter Superkombinatorsysteme angeben, beschreiben wir kurz die Entschach­telung 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-dmvn­Vorgehen erfordert - und daB die entstehenden Kombinatorsysteme keine "fully lazy"-Auswertung garantieren. Letzteres ist ein wesentlicher Nachteil des >.-lifting­Algori 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 Aus­druck, 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 Kombinator­kalkiil? 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 Kombinatorapplikatio­nen reprasentiert werden, sind beide Beschreibungen aquivalent. Durch das Ko­pieren von partiellen Kombinatorapplikationen kann es zu Mehrfachauswertungen von Teilausdriicken des Kombinatorrumpfes kommen, die nur von den in der par­tiellen Applikation vorhandenen Argumenten abhangen. Diese Teilausdriicke ent­sprechen 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 Teilaus­driicke wie folgt festgelegt.

5.3.1 Definition 1. Die Abbildung

subexp: Exp --+ P(Exp),

die jedem SAL-Ausdruck die Menge seiner (echten) Teilausdrucke zu­ordnet, 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 auftre­tenden 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 auftre­tenden -\-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 Bedin­gung in der Definition der freien Teilausdriicke eines Ausdruckes ist also nicht erfiillt. Diese Bedingung ist notwendig, da globale und lokal ge­bundene 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 Teilaus­driicke zu Argumenten der neu definierten Kombinatoren werden, so erhalt man eine spezielle Klasse von Kombinatorsystemen, die wir nun charakterisieren wer­den. Wir nennen diese Kombinatorsysteme wie [Hughes 82] Superkornbinatorsy­sterne.

Superkombinatorsysteme garantieren eine 'fully lazy' Auswertung, wenn sicher­gestellt 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 reduzierba­ren) Kombinatorapplikationen entsprechen, trivial- also Konstante oder Variable - sind. Konstante konnen nicht weiter reduziert werden. Variable sind Platzhal­ter 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 Hug­hes [Hughes 82/84] ein Superkombinatorsystem konstruiert werden, indem man aus jeder 'x-Abstraktion, die einer partiellen Applikation des Kombinators ent­spricht und die nicht-triviale maximal freie Teilausdriicke enthalt, diese maximal freien Teilausdriicke abstrahiert und die entstehende Abstraktion als neuen Kom­binator 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 er­folgt die Definition eines neuen Kombinators durch Abstraktion der nicht-trivialen maximal freien Teilausdriicke. Der neu definierte Kombinator erfiillt die Super­kombinatoreigenschaft. 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 ap­plikativer Ausdruck, der bereits zur Ubersetzungszeit reduziert werden konnte. Lt. Definition ist jede Kombinatorgleichung der Form F = e bereits eine Super­kombinatorgleichung 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 ver­zichten. In der hier beschriebenen Implementierung werden keinerlei Vorkehrungen getroffen, Mehrfachauswertungen 'nullstelliger' Kombinatoren zu vermeiden.

Das zweite Argument der Funktion super dient nur zur eindeutigen Bezeich­nung 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 nachein­ander aufrufenden Kombinatoren entspricht einer Kombinatorreduktion im ur­spriinglichen System eine Folge von Kombinatorreduktionen im Superkombinator­system.

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 mehr­fach auf und bei der Reduktion im urspriinglichen System, wiirde der Teil­ausdruck des Rumpfes von F3 , der nur von den ersten beiden Parametern abhangt, mehrfach ausgewertet. 1m Superkombinatorsystem ist die Appli­kation nicht partiell. Sie kann mit zwei Kombinatorreduktionsschritten, in denen die nur von den vorhandenen Argumenten abhangigen Teilausdriicke des urspriinglichen Kombinators als Argumentausdriicke der neu definier­ten Kombinatoren aufgebaut werden, reduziert werden. An diesem Beispiel erkennt man allerdings auch sofort die Nachteile von Superkombinatorsy­stemen. Wahrend etwa eine "vollstandige" Applikation des Kombinators F auf 3 Argumente urspriinglich eine Kombinatorreduktion erforderte, sind bei Zugrundelegung des entsprechenden Superkombinatorsystems 3 Kombi­natorreduktionen 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 Be­dingung (*) 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 Sharin­ganalyse, urn den Algorithmus von Hughes zur Erzeugung von Superkombinatoren dahingehend zu optimieren, daB Superkombinatoren nur fUr solche partiellen Kom­binatorapplikationen erzeugt werden, die bei der Reduktion des Kombinatorpro­gramms "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 Kombinatorre­duktionen durchgefUhrt werden miissen.

5.4. FLACHE KOMBINATORSYSTEME 115

5.3.8 Beispiel Betrachten wir das Kombinatorsystem R des letzten Beispie­les. 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 Kom­binators 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 Superkom­binatoralgorithmus 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 Nach­teile von Superkombinatorsystemen findet sich auch in [Peyton-Jones 87].

Wie wir bereits erwahnten, kann der im vorigen Abschnitt beschriebene Ent­schachtelungsalgorithmus so modifiziert werden, daB direkt Superkombinatorsy­sterne 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 ge­sondert 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 Kom­binatorsysteme 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 effizi­ente Implementierung ist der Aufbau der applikativen Ausdriicke aber ungiinstig, da die Erkennung von reduzierbaren Kombinatorapplikationen durch die Schach­telung 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 Reduk­tionsstrategie und

• Durchfiihrung der Reduktion.

Zur effizienten Durchfiihrung von Reduktionen haben wir in Kapitel 2 die we­sentlichen 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 durch­gefUhrt werden kann. Ein Durchlaufen des Graphen ist nicht mehr notwendig. Wie der Name schon sagt, ist die first-order Notation von Applikationen ausrei­chend 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 Funkti­onsausdriicke in Applikationen nicht nur Basisfunktionen oder Kombinatornamen sondern beliebige zusammengesetzte Ausdriicke, insbesondere Applikationen sein konnen. Wir werden einen expliziten Applikationsoperator ap benutzten, urn Ap­plikationen 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 be­zuglich der Kombinatordefinitionsgleichungen partie lien Applikationen von Kom­binatoren. Fur partielle Applikationen existiert keine Reduktionsregel in der zuvor definierten Reduktionsrelation, da eine solche Regel aus dem Bereich der applika­tiven 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 ap­plikativen Ausdriicke, die die rechten Seiten der sod ann definierten Hachen getyp­ten Kombinatorsysteme bilden. Anschliefiend formalisieren wir eine Reduktions­semantik 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 Funk­tionsausdrucke 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 Aus­drucke.

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 ver­loren 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 betrachte­ten 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 Kom­binatornamen als Funktionsausdriicke in Applikationen hoherer Ordnung entste­hen 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 folgen­den Reduktionsregeln. Der Substitutionsoperator fur flache Ausdrucke und Be­rechnungsausdriicke 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 Kombina­torreduktion aufgespalten wird in das eigentliche Uberschreiben der Kombinator­applikation durch den Rumpf (--+ Kopierregel) und das Erkennen von Kombina­torapplikationen durch "Aufsammeln" der Argumentlisten (--+ Sammelregeln). Es scheint zunachst, daB die Reduktion flacher Kombinatorsysteme durch die zusatz­lichen 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 Sam­melregeln 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 Reduk­tionsrelation

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 Kombinatorsy­stem und einem £lachen applikativen Ausdruck yom Basistyp. Die Reduktionsse­mantik fUr £lache Kombinatorprogramme wird vollkommen analog zu Definition 5.1.6 erkHirt.

Als nachstes formalisieren wir die Transformation von 'higher-order' Kombi­natorsystemen 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 Rang­funktion 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, Konstruk­toren und Kombinatornamen vor die Applikation gezogen werden und dafi meh­rere 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 Definiti­onsbereich 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 Kom­binatorsystemen 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 Kombina­torsystem:

( 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 Kom­binatoren 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 ge­wohnliches 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 Defini­tionsbereich 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 de­flatten.

5.4.13 Lemma Sei C ~ Fun, rg : Fun- -t :IN eine Rangfunktion mit Definiti­onsbereich 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 unter­schieden 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 applika­tiven Ausdrucke, dafi fur alle solchen Ausdrucke e die Abbildungen flatten und deflatten zueinander invers sind. Fur VariabIen, Kombinatornamen, Ba­sisfunktionen und Konstruktoren gilt naturlich obige Gleichheit. Fur Ver­zweigungen, 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 Be­rechnungsausdrucke 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 Be­rechnungsausdriicke zu F. Dann gilt:

'if U E FComp:F: U =*:F flatten(deflatten(u)).

d.h. jeder Berechnungsausdruck kann zu einem vollstandig flachen Be­rechnungsausdruck 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 ho­herer Ordnung

ap( Uo, ... , urn)

mit Uo E n u rue, wobei C die Menge der in F auftretenden Kombina­tornamen 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 Reduktions­relation 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 Induktionsvor­aussetzung.

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 Definiti­onsbereich 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 Defini­tion 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 Verzwei­gungsreduktionen 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 Durch­fiihrung 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 nicht­flachen und flachen Kombinatorsystemen bzgl. ihrer nichtdeterministischen Re­duktionssemantik.

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 hinzuwei­sen. 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 Reduk­tionsstrategie 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 Berechnungsaus­driicke, die wir als K ombinatornormalform bezeichnen. Die Kombinatornormal­form 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 ombinatornormal­form, 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 Kombinatorapplikatio­nen.

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 Kombina­tornormalform. 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 Applikatio­nen alle Argumente so weit wie moglich reduziert werden. Dies gilt insbesondere auch fiir Konstruktorapplikationen. An dieser Stelle unterscheiden sich die Kom­binatornormalform 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 Kombina­tornormalform, 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 Verzweigungsre­duktion 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 Kombinatornor­malform 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 Kombinatornormal­form 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 Kombinator­normalform 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 Kombinator­normalform 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 Kombina­tornormalform 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 Re­duktionsstrategie 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 Funk­tionssymbole einschlieBlich der Konstruktoren sehr viele Moglichkeiten zur Paral­lelisierung des Reduktionsprozesses.

1m folgenden Kapitel werden wir ein Verfahren zur Entdeckung von potentieller Parallelitat in Kombinatorprogrammen mit nicht-strikter Semantik entwickeln.