Semantik und Analyse: insbesondere Striktheitsanalyse · SAFP, WS 20012/13, Striktheits-Analyse, 5....

Kapitel 1

Semantik und Analyse:insbesondereStriktheitsanalyse

Kernsprachen, Reduktion und Eigenschaften

1.0.1 Funktionale Kernsprache KFPTS

Die ungetypte Kernsprache KFPTS soll als Grundlage fur Analysen dienen, ins-besondere fur eine Striktheitsanalyse und deren Anwendung. Die Demandana-lyse ist eine Erweiterung, die wir nicht behandeln werden. Die Sprache KFPTSist zwar ungetypt, aber kennt Konstruktoren mit fester Stelligkeit und Typen,wobei nur das case-Konstrukt durch Typen beschrankt ist.Eine einfache kontextfreie Grammatik fur KFPTS-Ausdrucke (Terme, Expres-sions) ist:

Definition 1.0.1 Es gibt eine Menge von Typsymbolen und Konstruktor-symbolen c, jeder Konstruktor c hat eine Stelligkeit ar(c), und ist genau einemTyp zugeordnet. Ebenso eine Menge von Superkombinatorsymbolen mit Stellig-keit.

1

SAFP, WS 20012/13, Striktheits-Analyse, 5. Februar 2013 2

EXP ::= Variable | λV . EXP wobei V eine Variable ist.::= Superkombinatorname

| (Konstruktor EXP1 . . . EXPn) wobei n = ar(Konstruktor).| (EXP EXP )| (caseTY P EXP (Pat1 → Exp1) . . . (Patn → Expn))Hierbei muss im case-Ausdruck n die Anzahl der Konstruktorenvon TYP sein und fur jeden Konstruktor von TYPmuss es genau ein Pattern geben.Das Konstrukt Pati → Expi heißt auch case-Alternative.

Pat ::= Konstruktor V1 . . . VnHier muss n die Stelligkeit des Konstruktors sein.Die Variablen Vi mussen alle verschieden sein.

Ein Programm besteht aus einer Liste von Superkombinatordefinitionen derForm s x1 . . . xn = e womit s die Stelligkeit n bekommt. Es gibt den ausge-zeichneten Superkombinator main, dessen Auswertung den Wert des Programmsergibt.

Beispiel 1.0.2 Fur Ausdrucke, Funktionen und Superkombinatoren:

Id := λx.x IdentitatK := λx.λy.x konstanter KombinatorD := λf.λx.f(x x)Y := λf.D f (D f) FixpunktkombinatorA := λz.λx.x (z z x)YTu := (A A) Turings Fixpunktkombinator

map f x := case x of Nil→ Nil; (y : ys)→ (f x) : (map f x ys)(++) xs ys := case xs of Nil→ ys; (z : zs)→ z : (zs ++ ys)

1.0.2 Auswertungsregeln, Normalordnungsreduktion

Definition 1.0.3 Ein Wert bzw. eine WHNF (weak head normal form, schwa-che Kopfnormalform) in KFPTS ist ein Ausdruck von der Form c t1 . . . tn,wobei c ein Konstruktor ist und n = ar(c), oder eine Abstraktion: λx . e, oderein Ausdruck (s t1 . . . tm), wobei s ein Superkombinator der Stelligkeit n > mist.Wir unterscheiden die Werte nach ihrer Struktur als

• FWHNF, wenn die WHNF eine Abstraktion ist, oder ein Ausdruck derForm (c s1 . . . sn), c ein Konstruktor und ar(c) > n, oder

• CWHNF ( constructor WHNF), wenn die WHNF ein Ausdruck der Form(c s1 . . . sn), c ein Konstruktor und ar(c) = n

Wir definieren Programmkontexte:


Definition 1.0.4 Ein Programmkontext (ein Kontext) ist ein Ausdruck, deran einer Stelle ein “Loch“ hat, an dem ein Ausdruck eingesetzt werden kann.Ein Kontext kann sein:

C ::= [] | (e C) | (C e) | (λx . C) |(c e1 . . . ei−1 C ei+1 . . . ear(c)) |caseT C (p1 → t1) . . . (pn → tn) |caseT t (p1 → t1) . . . (pi → C) . . . (pn → tn)

Beispiel 1.0.5 Damit sind als Kontexte z.B. definiert:

• [] : der leere Kontext. Setzt man einen Ausdruck e in den leeren Kontextein, so ergibt sich e selbst.

• (x (· y)). Einsetzen von e in den Kontext ergibt (x (e y))

• caseT (x ·) (p1 → t1) . . . (pn → tn). Einsetzen von e in den Kontextergibt caseT (x e) (p1 → t1) . . . (pn → tn)

Beachte, dass innerhalb eines Pattern kein Loch sein kann, ebenso ist der Kon-text λ · .e nicht moglich.Innerhalb von Kontexten erlauben wir das Einfangen von freien Variablen. D.h.es tritt der Effekt auf, dass die Namen von gebundenen Variablen eine Rollespielen, sofern das Loch innerhalb des Rumpfs einer Abstraktion ist. Z.B. istder Kontext λx . [] vom Kontext λu . [] verschieden, da beim Einsetzen von xjeweils andere Ausdrucke entstehen. Wir werden den Begriff der Gleichheit undUngleichheit von Ausdrucken noch formaler spezifizieren.

Definition 1.0.6 Auswertungsregeln (Reduktionsregeln):

Beta((λx.t) s)

t[s/x]

Case(caseT (c t1 . . . tn) . . . (c x1 . . . xn → s) . . .)

s[t1/x1, . . . , tn/xn]

SKBeta(k s1 . . . sn)

ek[s1/x1, . . . , sn/xn]Wenn der Superkombinator k die Stelligkeit n hat

Wir nennen das die unmittelbare Reduktion von Ausdrucken.Die Reduktionsregeln kann man in allen Programmkontexten verwendet. D.h.Wenn s → t in einem Schritt auswertet, dann gilt auch C[s] → C[t] fur jedenProgrammkontext C.Die Reduktionsrelation schreiben wir als s → t, wenn die Reduktion in ei-nem Schritt erfolgt. Die transitive bzw. reflexiv-transitive Hulle schreiben wir

als s+−→ t bzw. s

∗−→ t.Der Begriff des Redex (reducible expression) kann jetzt definiert werden: Wennin C[s] das s unmittelbar reduziert werden kann, dann ist s (zusammen mitseiner Position) ein Redex in C[s].


Fur die Normalordnungs-Reduktion (Normal-Ordnungs-Reduktion, Standard-Reduktion), braucht man Reduktionskontexte:

Definition 1.0.7 Reduktionskontexte sind:

R ::= [] | (R e) | caseT R (p1 → t1) . . . (pn → tn)

Das Loch eines Reduktionskontextes ist nicht unter einem Konstruktor oder imRumpf einer Abstraktion, ebenso nicht im Argument einer Anwendung.Die Normalordnungs-Reduktion ist diejenige, die immer in einem Reduktions-kontext den Ausdruck unmittelbar reduziert:

Definition 1.0.8 Sei R[s] ein Ausdruck, so dass R ein Reduktionskontext ist,wobei s keine WHNF ist, und s reduziert unmittelbar zu t:Dann ist R[s]→ R[t] die Normalordnungsreduktion (Standardreduktion, normalorder reduction) von R[s].Der Unterterm s zusammen mit seiner Position wird auch Normalordnungs-redex genannt. Die Reduktionsrelation wird mit der Markierung no versehen.Analog wie oben bezeichnen wir die transitive und reflexiv-transitive Hulle mitno,+−−−→ bzw.

no,∗−−−→.Wenn ein geschlossener Term t mittels Normalordnungsreduktionen zu einerWHNF reduziert, dann sagen wir, t terminiert (bzw. konvergiert) (englisch:terminates, converges) und bezeichnen dies mit t⇓. Andernfalls divergiert t,bezeichnet mit t⇑.

Manchmal sagen wir auch, t hat eine WHNF, wenn t zu einer WHNF re-duziert. Die WHNF, zu der t unter Normalordnung reduziert, ist eindeutig,aber es gibt i.a. viele WHNFs zu denen ein Term t reduzieren kann. Z.B.t ≡ (cons ((λx.x) True)) Nil) ist selbst in WHNF, aber (cons True Nil) istebenfalls eine WHNF zu t.Damit haben wir alle zur Auswertung von Ausdrucken notwendigen Begriffedefiniert und konnen jetzt Ausdrucke auswerten.

Beispiel 1.0.9 ((λx.x) Nil)no−→ Nil

((λx.λy.x) s t)no−→ ((λy.s) t)

no−→ s.

Lemma 1.0.10 Es gilt:

• Jede unmittelbare Reduktion in einem Reduktionskontext ist eine Normal-ordnungsreduktion.

• Der Normalordnungsredex und die Normalordnungsreduktion sind eindeu-tig in einem Term t, falls diese existieren.

• Eine WHNF hat keinen Normalordnungsredex und erlaubt keine Normal-ordnungsreduktion.


Wir benutzen KFPT und KFPTS als Basis-Sprachen fur die weiteren Betrach-tungen, ebenso wie fur die folgende Striktheitsanalyse.

Bei KFPTS wird i.a. der Ausdruck zu main als der dynamische Ausdruck be-trachtet, und die anderen Definitionen als statisch, wahrend in KFPT dieseUnterscheidung nicht existiert. Wir werden sehen, dass es auch einen wichti-gen formalen Unterschied gibt zwischen dem main-Ausdruck und den anderenAusdrucken in KFPTS.

1.0.3 Eigenschaften der Normalordnungsreduktion

Wenn KFPTS gemeint ist, dann betrachten wir alles innerhalb des main-Ausdrucks und sehen die Superkombinator-Definitionen als global definiert an.

Definition 1.0.11 Seien s, t zwei Ausdrucke. Wir definieren

s ≤c t :⇐⇒ ∀C[] : C[s]⇓ ⇒ C[t]⇓

und sagen s approximiert t kontextuell. s ∼c t ist definiert als s ≤c t ∧ t ≤c s.

s ∼c t ⇐⇒ ∀C[] : C[s]⇓ ⇐⇒ C[t]⇓

Wir sagen dann: s, t, sind kontextuell aquivalent.

In Analogie zu den Church-Rosser-Satzen gelten Aussagen zur kontextuellenAquivalenz. Daruber hinaus hat man auch noch Aussagen zur Reduktionslange.Es gilt, dass ≤c eine Prakongruenz und dass ∼c eine Kongruenz ist. D.h.s ∼c t =⇒ C[s] ∼c C[t] fur alle s, t, C, und s ≤c t =⇒ C[s] ≤c C[t] fur alles, t, C.Außerdem ist ≤c eine Praordnung und ∼c eine Aquivalenzrelation; d.h. ≤c isteine Prakongruenz und ∼c eine Kongruenz.Wir benotigen einige Eigenschaften der Sprache KFPTS, die wir hier wiederho-len, bzw. ohne Beweis darstellen.

Satz 1.0.12 Sei t ein (evtl. offener) Ausdruck. Wenn t⇓, d.h. tno,∗−−−→ t1, t1 ist

eine WHNF, und t → t′ mit einer (auch nicht-Normalordnungs-) Reduktion.Dann gilt t′⇓.

Beweis. (siehe andere Skripte) 2

Satz 1.0.13 (Standardisierung). Sei t ein (evtl. offener) Ausdruck. Wenn

t∗−→ t1 mit beliebigen (Beta), (SKBeta) und (case)-Reduktionen, wobei t1 eine

WHNF ist, dann existiert eine WHNF tNF , so dass tno,∗−−−→ tNF , und tNF

∗−→ t1.

Beweis. (siehe andere Skripte) 2


Satz 1.0.14 (Invarianz der Terminierung) Seien t, t′ (evtl. offene) Ausdruckemit t→ t′. Dann gilt t⇓ ⇐⇒ t′⇓

Beweis. Das folgt aus Satz 1.0.13 (Standardisierung) und Satz 1.0.12:Sei t→ t′ und t⇓. Dann folgt aus Satz 1.0.12, dass t′⇓.Sei t→ t′ und t′⇓. Dann ist t→ t′

∗−→ tWHNF und Satz 1.0.13 impliziert t⇓.Sei 2

Korollar 1.0.15 Seien t, t′ (evtl. offene) Ausdrucke mit t→ t′.Dann gilt t ∼c t

′

Die kontextuelle Approximation kann man erkennen, auch wenn man die Ein-schrankung macht, dass C]s], C[t] geschlossen ist,

Aussage 1.0.16 Seien s, t Ausdrucke: Dann gilt:

s ≤c t :⇐⇒ ∀C[] : Wenn C[s], C[t] geschlossen sind, dann C[s]⇓ ⇒ C[t]⇓

Beweis. Es ist klar, dass⇒ gilt. Um die andere Richtung zu zeigen, nehmen wirmal an, dass die rechte Bedingung gilt, und dass fur einen gegebenen KontextC die Relation C[s]⇓ gilt. Sei {x1, . . . , xn} die Menge der freien Variablen in

C[s], C[t]. Dann definiere C ′ := (λx1 . . . xn.C) ⊥ . . .⊥. Man sieht dass, C ′[s]∗−→

σ(r)⇓, wobei σ = {x1 7→ ⊥, . . . xn 7→ ⊥} ist. Aus der Voraussetzung folgtdass auch C ′[t]⇓ gilt. Genauso wie fur s sieht man mit vollstandiger Induktion,

dass C ′[t]∗−→ σ(u)⇓ gilt wobei C[t]

∗−→ u. Das kann aber nur sein, wenn u eineAbstraktion oder ein Konstruktorausdruck ist, und somit gilt auch C[t]⇓. 2

Folgende Aussage wird eine wichtige Rolle spielen beim Nachweis der Korrekt-heit der Striktheitsanalyse.In KFP, KFPT und KFPTS gilt folgendes:

Aussage 1.0.17 Sei t ein (evtl. offener) Ausdruck. Wenn tno,k−−−→ t1 wobei t1

eine WHNF ist und t′ ist ein Ausdruck mit t→ t′.Dann terminiert die no-Reduktion von t′ und es gibt eine WHNF t′1 so dass:

t′no,k′

−−−→ t′1, t1∗→ t′1 und k ≥ k′.

t

kno

��

// t′

≤kno

��

t1∗ //______ t′1

Beweis. Siehe andere Skripte. 2

Definition 1.0.18 Wir definieren fur jeden Term t mit t⇓ die Lange einer Nor-malordnungsreduktion zur WHNF als rln(t). Hierbei nehmen wir auch an, dass


das Resultat ∞ ist im Falle, dass t eine unendliche Normalordnungsreduktionhat oder die Reduktion auf einen Typfehler trifft. Falls t freie Variablen hat,und die Normalordnung mit einem Term der Form R[x] stoppt, dann ist rln(t)undefiniert.

Damit kann man Aussage 1.0.17 (fur die Sprachen KFP, KFPT und KFPTS)anders formulieren und etwas erweitern:

Aussage 1.0.19 Sei t ein (evtl. offener) Ausdruck, rln(t) sei definiert und

t∗→ t′.

Dann ist rln(t′) ≤ rln(t).

Nachteil der rln(t)-Definition ist, dass es zu weit weg ist von der wirklichen Im-plementierung: Call-by-name benutzt kein Sharing, sondern kopiert die Argu-mente und setzt diese in den Rumpf ein, so dass hier potentielle Vermehrfachungvon Redexen passieren kann.

Bemerkung 1.0.20 Nimmt man eine etwas andere Relation auf Ausdrucken,die statt Terminierung die Reduktion auf gleiche Werte betrachtet, dann erhaltman eine Relaitonndie auf higher-order Funktionen die Funktionen zu stark un-terscheidet.Sei ein Wert definiert als ein Ausdruck, der nur aus Konstruktoren und Ab-straktion besteht. Die Relation sei definiert:s ∼v t :⇐⇒ fur alle C, Werte v: C[s]⇓v ⇐⇒ C[t]⇓vEs gilt s ∼v t =⇒ s ∼c t. Nachweis, indem man die Konstruktoren etwasumprogrammiert.Die Umkehrung gilt nicht, da bei Abstraktionen als Werte verlagt wird, dass diese(bis auf Umbenennung) gleich sind. Z.B. gibt es Abstraktionen: λx.Nil ++ x ∼c

λx.x, aber die Abstraktionen sind verschieden.Außerdem wird die Auswertung in Haskell nur bis zur WHNF durchgefuhrt.

Die nachste Variante einer Gleichheitsrelation ware:s ∼′v t :⇐⇒ fur alle C, Boolsche Werte v: C[s]⇓v ⇐⇒ C[t]⇓v.Diese Relation ∼′v macht interessanter Weise λx.⊥ und ⊥ gleich, da λx.⊥ nichtals Wert zahlt, aber λx.⊥⇓ und ⊥⇑.

1.1 Wiederholung: andere Sprachabstraktionen:Die ungetypte Kernsprache KFP

Zur Erinnerung hier nochmal die Definition der Sprache KFP, die eine sehreinfache Syntax und wenig Reduktionsregeln hat.

Syntax: Es gibt Konstantensymbole, die jeweils eine feste Stelligkeit haben.Diese nennen wir Konstruktoren. Die Anzahl der Konstruktoren sei N , die Kon-struktoren seien mit ci, i = 1, . . . , N bezeichnet.


Wir nehmen an, dass es eine Moglichkeit gibt, alle Konstruktoren mit Stelligkeitanzugeben, ohne dass wir diese Methode naher spezifizieren. Zum Beispiel alseine Auflistung aller Konstruktoren mit Stelligkeit.

Definition 1.1.1 Eine einfache kontextfreie Grammatik fur KFP-Ausdrucke(Terme, Expressions EXP ) ist:

EXP ::= V V sind Variablen| λV . EXP wobei V eine Variable ist.| (EXP EXP )| (c EXP1 . . . EXPn) wobei n = ar(c)| (case EXP {Pat1 → Exp1; . . . ;PatN+1 → ExpN+1})

Hierbei ist Pati Pattern zum Konstruktor i, undPatN+1 das Pattern lambda.(Pati → Expi) heißt auch case-Alternative.

Pat ::= (c V1 . . . Var(c)) | lambdaDie Variablen Vi mussen alle verschieden sein.

Wesentlich ist die andere Struktur des jetzt ungetypten case-Konstruktes: Esgibt nur ein case, und es sind stets alle Konstruktoren als Alternativen vorhan-den, ebenso eine weitere Alternative, die mit dem Pattern lambda abgedecktwird, und die zum Zuge kommt, wenn der zu untersuchende Ausdruck eineAbstraktion ist.

1.2 Programmtransformationen und Optimie-rungen

Im folgenden verwenden wir KFPTS, da es naher an Haskell liegt, und beiAnalysebeispielen zT auch sinnvollere Angaben liefert. Z.B. kann man leichterAussagen uber ungetypte Argumenteinsetzungen u.a vermeiden.Man kann auch leichter mit rekursiven Funktionen umgehen. Die Ein-schrankung, die wir hinnehmen mussen, ist dass wir die Betrachtungen auf denmain-Ausdruck beschranken mussen, und die Superkombinatordefinitionen alsglobale Definitionen ansehen. Allgemeiner: man kann die Analysen und Ergeb-nisse immer dann anwenden, wenn man lokal nur Definitionen von Superkom-binatoren verwendet hat, die man als global ansehen kann.

Definition 1.2.1 Korrekte Programmtransformationen sind binare RelationenP R P ′, die die Semantik der Programme nicht verandern, d.h. P R P ′ ⇒ P ∼c

P ′.

An leicht nachweisbaren korrekten Programmtransformationen hatten wir diepartielle Auswertung. D.h. s → t fur Unterausdrucke, und ebenso induktiv be-weisbare Gleichungen, die rekursive definierte Funktionen betrafen, wie z.B.


foldr g e (xs++ys) ∼c foldr g (foldr g e ys) xs

foldl f e xs ∼c foldr (flip f) e (reverse xs)

xs++nil ∼c xs

xs++(ys++zs) ∼c (xs++ys)++zsDiese Gleichungen kann man einsetzen, um Programme zu transformieren undhoffentlich auch zu optimieren.Als Gegenbeispiel, das als Warnung vor inkorrekten Transformationen dienenkann, und zeigt, warum man sich in KFPTS erst mal nur auf den main-Ausdruckbeschrankt, hier ein Beispiel von David Sands:

Beispiel 1.2.2 Die Funktionen repeat und tail seien definiert durch

repeat x = x : repeat x

tail x = case x of (Nil -> bot) (y:ys -> ys)

Man kann nachweisen, dass fur alle Elemente x die Gleichung

tail(repeat x) = (repeat x)

gilt. Benutzt man diese Gleichung im Rumpf der Funktion repeat, erhalt mandie neue Funktion:

repeat’ x = x : tail(repeat’ x)

Leider hat diese Funktion andere Eigenschaften als repeat, z.B. kann manden tail von repeat′ x nicht mehr berechnen: tail (repeat’ a) →tail (a: tail(repeat’ a)) → tail(repeat’ a)), und die Reduktion ist ineiner Schleife.D.h. repeat und repeat’ sind nicht kontextuell aquivalent.Hier hat man in unzulassiger Weise die rekursive Definition einer Funktionverandert.

Als praktischen Hinweis geben wir hier Bedingungen an, unter denen die Me-thode bei Anwesenheit von rekursiv definierten Superkombinatoren korrekt ist:

• Wenn die Ersetzung s = t an einer Position vorgenommen wurde, sodass die kontextuelle Gleichheit von s ∼c t ohne Bezugnahme auf die-se Position gezeigt werden kann. Genauer: es gibt ein Unterprogramm P ′,(das abgeschlossen ist bzgl. aller Definitionen), so dass s ∼c t eine Glei-chung bzgl. des Unterprogramms P ′ ist. Dann kann man die Ersetzungin allen Ausdrucken machen, die außerhalb von P ′ sind. Z.B. kann mantail(repeat x) = (repeat x) an Stellen verwenden, die außerhalb derDefinitionen von tail und repeat liegen.

• Wenn die Ersetzung s→ t einerseits so ist, dass s ∼c t gilt, und anderer-seits die Anzahl der Normalordnungsreduktionen dadurch in keinem Termvergroßert wird (siehe unten im Abschnitt

”Verbesserungen“).


1.2.1 Verbesserungen (Improvements)

Dies ist adaptiert aus den Arbeiten von David Sands, (1994,1996,1999) undformalisiert den Zeitbedarf von Ausdrucken unter Benutzung der Anzahl vonNormalordnungs-Schritten. In den Papieren von D. Sands ist das Maß entwederdie Anzahl der Funktionsaufrufe oder die Anzahl der Schritte einer abstraktenMaschine (i.a. Mark-1 von Sestoft), so dass wir die Resultate dort nicht ganzdirekt ubernehmen konnen.Wir verwenden als Maß die Anzahl der Normalordnungsreduktionen. Dadurchkann man Methoden studieren, die nachweisen, dass die Ersetzung eines Aus-drucks s durch einen

”besseren“Ausdruck t in einem Programm stets eine Opti-

mierung bzgl. der Zeit darstellt. Wichtig ist, dass man den Begriff so formuliert,dass die Ersetzung immer weniger oder gleich viel Zeit benotigt, unabhangigdavon, wo man den Ausdruck in einem Programm durch einen anderen ersetzt.Leider sagt diese Verbesserungsbeziehung nichts uber den Platzbedarf aus.Ebenso muss man die ubliche Vorsicht walten lassen, wenn man die Anzahl derSchritte im formalen Modell ubertragen will auf die von einer Implementierungverbrauchte Zeit.Problematisch bei der Formalisierung ist, dass ein call-by-name Kalkul zugrundeliegt, der kein Sharing berucksichtigt. Deshalb sind die Ergebnisse (d.h. Aussa-gen zu Optimierungen) dieser Theorie in vielen Fallen nicht auf Haskell ubert-ragbar, da in Haskell Sharing berucksichtigt wird. Die Ergebnisse sind brauch-bar, wenn bei den Reduktionen keine Terme verdoppelt werden. Dies ist in denBeispielen unten der Fall.

Definition 1.2.3 Seien s, t zwei Ausdrucke mit s ∼c t. Wenn

∀C[] : rln(C[s]) ≤ rln(C[t])

dann schreiben wir s � t und sagen s ist optimaler als t.Wenn s � t und es einen Kontext C[] gibt mit rln(C[s]) < rln(C[t]), dannschreiben wir s ≺ t und sagen s ist echt optimaler als t.

Bei D. Sands heißt diese Beziehung strong improvement.Es gilt offenbar, dass � eine reflexive und transitive Relation ist (d.h. eine Pra-Ordnung).Weiter gilt: s � t⇒ C[s] � C[t].Eine einfache Optimierung ist die Ersetzung von s durch ein Redukt:

Satz 1.2.4 Sei s→ t fur zwei (auch offene) KFPT-Ausdrucke. Dann gilt t � s,d.h. t ist eine Verbesserung von s.

Beweis. Sei C ein Kontext und s→ t. Dann gilt auch C[s]→ C[t], da Reduktio-nen uberall erlaubt sind. Nach Aussage 1.0.19 gilt C[s] ∼c C[t]. Nach Aussage1.0.17 gilt rln(C[s]) ≥ rln(C[t]). Da das fur alle Kontexte gilt, gilt auch t � s.2

Es gilt der folgende Satz: (Improvement Theorem von David Sands:)


Satz 1.2.5 Wenn in einer rekursiven Definition von Superkombinatoren eineErsetzung t durch s durchgefuhrt wurde, und vor der Ersetzung galt s � t, dannsind alle Ausdrucke r vor und nach der Ersetzung semantisch gleichwertig. D.h.Terminierung bleibt erhalten.

Dadurch kann man nicht nur in KFPT an von Definitionen unabhangigenStellen optimieren mittels �, sondern auch innerhalb von Definitionen.

Ein Multikontext C[., . . . , .] ist ein Ausdruck mit n Lochern, wobei jedes Lochgenau einmal vorkommen muss. Genauer: Seien []i die Bezeichnung fur Loch i.Dann ist ein Ausdruck C[[]1, . . . , []n] (der erzeugt wird wie ein Ausdruck, aber []iist ebenfalls erlaubt als Unterausdruck) ein Multi-kontext mit den n Lochern,wenn jedes Loch []i genau einmal vorkommt. Der Ausdruck C[t1, . . . , tn] be-zeichnet die Einsetzung der Ausdrucke in die Locher, ohne Umbenennung vonVariablen: C[t1, . . . , tn] = C[[]1, . . . , []n][t1/[]1, . . . , tn/[]n].

Aussage 1.2.6 Wenn si � ti fur i = 1, . . . , n, dann gilt auch C[s1, . . . , sn] �C[t1, . . . , tn] fur einen Multikontext C[., . . . , .].

Beweis. Mit Induktion nach i. Es gilt: C[s1, s2, . . . , sn] � C[t1, s2, . . . , sn] �. . . � C[t1, t2, . . . , tn−1, sn] � C[t1, t2, . . . , tn−1, tn]. Daraus folgt die Behaup-tung, da � transitiv ist. 2

Korollar 1.2.7 Wenn si � ti, fur i = 1, . . . , n, dann gilt c s1 . . . sn � c t1 . . . tnfur einen Konstruktor c der Stelligkeit n.

1.2.2 Eine Methode zum Nachweis von �Wir geben eine Moglichkeit an, s � t zu zeigen. Dies ist in Analogie zum Induk-tionsschema zum Nachweis der kontextuellen Aquivalenz.

Definition 1.2.8 Zunachst definieren wir die Menge List der geschlossenenListenausdrucke als den großten Fixpunkt der Bedingung:s ∈ List wenn s geschlossen und:

• s = ⊥ oder

• s = Nil oder

• s ∼c s1 : s2 und s2 ∈ List. 2

Beachte: s ∼c s1 : s2 ∧ s2 ∈ List ist gleichwertig zu: sno,∗−−−→ t1 : t2 ∧ t2 ∈ List .

Um das Verfahren der Bildung eines großten Fixpunkts nochmals zu illustrieren,definieren wir den Operator Φ auf Mengen von KFPT-Ausdrucken:Φ(L) := {s | s ∼c ⊥ oder s ∼c Nil oder s ∼c s1 : s2 und s2 ∈ L}List ist dann der großte Fixpunkt von Φ auf der Menge der KFPT-Ausdruckeund kann erhalten werden als der unendliche Schnitt uber die Mengen


Φi(LKFPT ). Der Nachweis, dass ein Ausdruck s in List ist, kann mit Induktionfolgendermaßen gefuhrt werden: Wenn es fur jede Listentiefe n nicht moglichist, das Enthaltensein zu widerlegen, dann ist s ∈ List .

Beispiel 1.2.9 Fur alle xs, ys ∈ List gilt, dass xs ++ ys ∈ List: Die Induktiongeht nach Listentiefe n und Fallunterscheidung nach der Variablen xs.Wenn xs ∼c ⊥, dann ist auch xs ++ ys ∼c ⊥.Wenn xs ∼c Nil, dann ist xs ++ ys ∼c ys, und ys ist bereits in List. Das erfulltdie Bedingung.Wenn xs ∼c x

′ : xs′, wobei xs′ ∈ List, dann ergibt die Reduktion von (x′ :xs′)++ys ∼c x

′ : (xs′ ++ ys), und Induktion nach der Tiefe kann verwendetwerden.

Der nachste Schritt ist folgende Definition

Definition 1.2.10 Die Menge ImpListPaar von geschlossenen Ausdrucken istder großte Fixpunkt der Bedingung: Fur ein Paar (s, t) ∈ ImpListPaar sollgelten:

• (s, t) = (⊥,⊥); oder

• s no,k−−−→ Nil, tno,k′

−−−→ Nil und k ≤ k′; oder

• s no,k−−−→ s1 : s2, tno,k′

−−−→ t1 : t2, k ≤ k′, s1 � t1, und (s2, t2) ∈ ImpListPaar.2

Dies ist eine Menge von Paaren von geschlossenen Listenausdrucken (s, t), sodass s optimaler als t ist, aber zunachst im leeren Kontext.Wir benutzen im folgenden die Tatsache (ohne Beweis), dass aus (s, t) ∈ImpListPaar auch s ∼c t folgt.

Aussage 1.2.11 Wenn (s, t) ∈ ImpListPaar, dann gilt s � t.

Beweis. Wir zeigen dass fur einen beliebigen Multikontext C[., . . . , .] und Paare(si, ti) mit (si, ti) ∈ ImpListPaar oder si � ti die Aussage rln(C[s1, . . . , sn]) ≤rln(C[t1, . . . , tn]) gilt:Wenn rln(C[s1, . . . , sn]) undefiniert ist, dann auch rln(C[t1, . . . , tn]); und wennrln(C[s1, . . . , sn]) =∞, dann auch rln(C[t1, . . . , tn]) =∞, da C[s1, . . . , sn] ∼c

C[t1, . . . , tn]).In den anderen Fallen zeigen wir die Behauptung mit Induktion nach der An-zahl der Normalordnungsschritte von C[s1, . . . , sn], zweitens nach der Anzahlder Locher von C, drittens nach der Anzahl der Normalordnungsschritte vonC[t1, . . . , tn] (falls notig).Wenn es keinen Normalordnungsredex mehr gibt, dann ist C[s1, . . . , sn] eineWHNF und es gilt die Behauptung.Wenn es einen Normalordnungsredex in C[s1, . . . , sn] gibt, muss man Falle un-terscheiden:


1. Der Normalordnungsredex ist ganz in C[. . .]. Dann hat man nach einerNormalordnungsreduktion von C[s1, . . . , sn] und von C[t1, . . . , tn] eine Si-tuation, auf die man Induktion anwenden kann. Hier ist zu beachten, dassdie si, ti alle geschlossen sind, und evtl. kopiert werden.

2. Ein sj ist im Reduktionskontext, und sj � tj . Dann konnen wir an-nehmen, dass das Loch j in einem Reduktionskontext in C ist, un-abhangig von den anderen Argumenten im Multikontext. Dann ist tj eben-falls im Reduktionskontext. Man kann die Induktionsbehauptung anwen-den auf C[s1, . . . , sj−1, sj , sj+1, . . . , sn] und C[t1, . . . , tj−1, sj , tj+1, . . . , tn],da die Reduktionslange gleich ist und man einen Kontext C ′ :=C[·, . . . , ·, sj , ·, . . . , ·] mit einem Loch weniger als C hat. Es giltC[t1, . . . , tj−1, sj , tj+1, . . . , tn] � C[t1, . . . , tj−1, tj , tj+1, . . . , tn], und mankann die Induktionshypothese beweisen.

3. Der Normalordnungsredex ist in einem sj und es ist der ImpListPaar -Fall. Dann ist tj ebenfalls im Reduktionskontext. Man fuhrt jeweils einenNormalordnungsreduktionsschritt durch. In tj muss auch ein Normalord-nungsreduktionsschritt durchfuhrbar sein wegen der Vorr. Danach hatman eine analoge Situation, auf die man Induktion anwenden kann.

4. Der Normalordnungsredex in C[s1, . . . , sn] ist von der Form (sj t), und sjist in WHNF. Dann kann der Fall (sj , tj) ∈ ImpListPaar nicht auftreten,da sj ja in List ist und dies einen dynamischen Typfehler darstellt, undsomit wie ⊥ behandelt wird. Wg. Vorraussetzung gilt dann auch, dasstj ∼ ⊥.

5. Der Normalordnungsredex in C[s1, . . . , sn] ist von der Form case sj of altsund sj ist in WHNF. Beachte dass der case-Ausdruck zu C gehort.Auch hier kann sj nur einen Listenkonstruktor als Topkonstruktor ha-ben. Wenn tj nicht in WHNF ist, dann kann man einen Normalordnungs-schritt durchfuhren, und dann Induktion anwenden, Wenn tj in WHNF ist,dann hat der Normalordnungsredex von C[t1, . . . , tn] ebenfalls die Formcase tj of alts. In diesem Fall muss sj = sj1 : sj2 und tj = tj1 : tj2 seinmit sj1 � tj1 und (sj2, tj2) ∈ ImpListPaar sein. Nach der Ausfuhrungeiner case-Reduktion auf beiden Seiten kann man wieder Induktion an-wenden. 2

Was jetzt noch fehlt, ist ein einfaches Rezept zum Nachweis von (s, t) ∈ImpListPaar . Wir bezeichnen in der folgenden Aussage einen Ausdruck s mits[x], wenn wir andeuten wollen, dass er die Variable x (evtl. mehrfach) enthalt.

Aussage 1.2.12 Induktionsschema zum Nachweis folgender Aussage:Fur alle Listenausdrucke x ∈ List gilt: s[x] � t[x].Voraussetzung ist, dass schon nachgewiesen wurde, dass fur alle Listen x ∈ List:s[x] ∼c t[x] gilt.Angenommen, wir konnen fur jede der Einsetzunga ∈ {⊥, Nil, y : ys mit ys ∈ List} zeigen, dass eine der folgenden Aussagen gilt:


• s[a] ∼c ⊥ ∼c t[a].

• s[a]no,k−−−→ r, t[a]

no,k′

−−−→ r wobei k ≤ k′ und r ∈ List.

• s[a]no,k−−−→ r1 : s[r2], t[a]

no,k′

−−−→ r1 : t[r2] wobei k ≤ k′ und r2 ∈ List.

Dann gilt fur alle Listenausdrucke x ∈ List: s[x] � t[x].

Beachte, dass die Listenelemente syntaktisch die gleichen sein mussen.Dieses Induktionsschema kann erweitert werden auf andere rekursive Daten-strukturen wie Baume. Ebenso kann man das Induktionsschema ausdehnen aufGleichungen mit mehreren Variablen.

Beispiel 1.2.13 Wir zeigen, dass fur alle Listen xs, ys, zs gilt:

xs++(ys++zs) � (xs++ys)++zs

1. ⊥: Sowohl ⊥++(ys++zs) als auch (⊥++ys)++zs haben keine WHNF. Somit∞ ≤∞.

2. Nil: Nil++(ys++zs)no−→ case Nil . . .

no−→ (ys++zs)no−→ case ys (Nil →

zs) (u : us→ u : (us++zs)).

(Nil ++ys)++zsno−→ case (Nil++ys) (u : us → u : (us++zs))

no−→case (case Nil . . .) . . .

no−→ case ys (Nil→ zs) (u : us→ u : (us++zs)).Das sind jeweils 3 Normalordnungsreduktionen auf jeder Seite. Jetzt fehltnoch der Nachweis, dass xs ++ ys ∈ List. Das wurde in Beispiel 1.2.9behandelt.

3. xs′ = x : xs: Wir betrachten die Normalordnungsreduktion der linken undrechten Seite:

((x : xs)++ ys) ++ zsno−→ case ((x : xs)++ys) of (Nil→ . . .) (u : us→ u : (us++zs))no−→ case (case (x : xs) . . .) of (Nil→ . . .) (u : us→ u : (us++zs))no−→ case (x : (xs ++ ys)) of (Nil→ . . .) (u : us→ u : (us++zs))no−→ x : ((xs ++ ys)++zs)Die andere Reduktion ergibt:

(x : xs)++ (ys ++ zs)no−→ case (x : xs) of (Nil→ . . .)(u : us→ u : (us++(ys ++ zs)))no−→ x : (xs++ (ys ++ zs))

Die erste Reduktion benotigt 4 Normalordnungs-Schritte, die zweite Re-duktion benotigt nur 2 Reduktionen. Danach kann man Induktion (nachder Tiefe) auf die Ausdrucke ((xs ++ ys)++zs) und (xs++ (ys ++ zs))anwenden.


Also kann man jetzt mit dem Induktionsschema schließen, dass fur alle Listenxs, ys, zs gilt:xs++(ys++zs) � (xs++ys)++zs.

Beachte, dass hier nicht der allgemeine Nachweis gefuhrt wurde, dass jeder Aus-druck der Form ((s1 ++ s2) ++ s3) durch den Ausdruck (s1 ++ (s2 ++ s3))verbessert wird, da noch freie Variable vorkommen konnten.Das kann man aber ebenfalls allgemein nachweisen.

Beispiel 1.2.14 Wir wenden Aussage 1.2.12 versuchsweise auf die vermute-te Optimierung map (f . g) xs � map f (map g xs) bzw deren Umkehrungmap f (map g xs) � map (f . g) xs an.Zuerst probieren wir:map (f . g) xs � map f (map g xs)

Die Schritte sind:

map (f . g) (a:as) -> case a:as ...

-> (f.g) (a) : map (f . g) (as)

Getrennt berechnet man: (f.g) (a) → f (g a). Vergleicht man mit

map f (map g a:as) -> map f (case a:as ... )

-> map f (g a : map g as) -> case (g a: map g as) ..

-> f (g a) : map f (map g as)

dann sieht man, dass die erste Variante weniger Reduktionsschrittebenotigt. Leider ist das nicht in allen Kontexten so, denn im Kontext(λx.C[x, . . . , x]) (hd ·) ist der Aufwand fur die Auswertung von (f.g) (a) zu(f (g a)) evtl. mehrfach erforderlich.Die andere Richtung ist leicht als falsch einzusehen.Wenn man Sharing direkt (d.h. per Pointer oder Markierungen) verwendet,dann beobachtet man, dass map (f . g) xs gegenuber map f (map g xs) inallen einfachen Fallen eine Verbesserung ist. Allerdings ist das naive Sharingnicht ausreichend, da das Skoping berucksichtigt werden muss, denn solche ge-meinsam referenzierten Ausdrucke konnen ja kopiert werden.Das Beispiel zeigt damit, dass man zur vernunftigen Optimierung mittels Impro-vements das Sharing berucksichtigen muss, d.h. dass man eine Sprache benotigt,die das Sharing in der implementierten Auswertung (lazy evaluation) richtig mo-delliert. Genauer: man braucht ein let bzw. ein letrec in einem (erweiterten)Lambdakalkul. In den Kalkulen mit let bzw. letrec hat man aber komplexe-re Reduktionen, und man muss das Maß etwas verandern: die reinen “let”-Reduktionen darf man bei Betrachtungen zu Verbesserungen nicht mitzahlen.


1.3 Striktheitsanalyse (mit abstrakter Redukti-on)

(Erik Nocker: fur Clean, Marko Schutz fur Kernsprache, Artikel: Sabel, Schutzund Schmidt-Schauß, Safety of Nocker’s strictness analysis, J. Funct. Program.18(4), 2008, )

Motivation

Informell ist eine Funktion f strikt in ihrem i-ten Argument, wenn sie diesesArgument auf jeden Fall auswertet, um einen Wert zuruckzugeben. Zum Beispielist K mit K x y = x strikt im ersten Argument, aber nicht strikt im zweitenArgument. Wenn alle Funktionen ihre Argument ohnehin auswerten, wie z.B.in ML, dann braucht man keine Striktheitsanalyse.In Haskell stellt die Striktheitsanalyse Informationen bereit, die bei der Kompi-lation aus den Funktionsdefinitionen (bzw. Spezifikationen) sequentielle interneFunktionen macht.In einer Tabelle sind hier schlagwortigartig (und auch leicht vereinfacht) dieEigenschaften nicht-strikter und strikter (funktionaler) Programmier-Sprachenin Bezug auf Optimierung und Striktheit zusammengestellt:

Nicht-strikte mit Sharing Strikte

Auswertung Normalordnung Anwendungsordnung

Reihenfolge Bestimmt durch Rumpf, undzur Laufzeit durch Auswer-tungsanforderung.Programmablauf nicht amFunktionscode erkennbar

Komplett bestimmt durch denRumpfProgrammablauf am Funktions-code erkennbar

Spezifikation WAS WIE

Information Intention bzw. Idee noch sicht-bar

Idee oft durch die Sequentiali-sierung verdeckt

Transforma-tionen

Viele Wenige, da Auswertungs-Reihenfolge eingehalten werdenmuss

Parallelli-sierung

orientiert am Rumpf von Funk-tionen; automatische konserva-tive Parallelisierung; Semantikkann erhalten bleiben

orientiert am Rumpf von Funk-tionen; Parallelisierung mussReihenfolge einhalten; Parallel-lisierung fast nur durch Umpro-grammierung moglich

Es gibt verschiedene Grunde, siehe auch Tabelle oben, die eine Striktheitsanalysesinnvoll machen.

1. Striktheitsanalyse liefert Informationen, die eine Auswertungsumstellungerlauben, und damit eine Optimierung ermoglichen, ohne dass die Seman-tik verandert wird.

2. konservative und automatische Parallelisierung der Auswertung


benotigt Striktheitsinformation, wenn die Semantik nicht verandert wer-den soll. Die Striktheitsanalyse liefert die Information, welche Ausdruckeman schon vorher auswerten kann, da sie spater auf jeden Fall benotigtwerden. Damit kann man spekulative Auswertung vermeiden, d.h. nurwirklich erforderliche Ausdrucke auswerten. Z.B muss man im Ausdrucks+ t, falls der Wert benotigt wird, s und t auswerten, bevor ein Ergebnisberechnet werden kann. Damit kann man s, t auch parallel auswerten. DerVorteil der referentiellen Transparenz ist hier, dass die s, t-Auswertungensich nicht gegenseitig beeinflussen.

3. die Compilierung in eine abstrakte Maschine, G-Maschine oder STG-Maschine ergibt effizienteren Kode, wenn Striktheitsinformation vorliegt.Allerdings haben die Compilierungstemplates oft schon eine schwacheForm der Ausnutzung von Striktheitsinformationen eingebaut.

4. Es gibt (high-level) Transformationen, die als Vorbedingung Striktheits-informationen benotigen. Allerdings gibt es da auch andere interessanteVorbedingungen, z.B. Terminierung

In der einfachsten Variante einer abstrakten Maschine wird eine Funktion mitDefinition f x1 . . . xn = e so kompiliert, dass ein Knoten mit der Markierung(f t1 . . . tn) reduziert werden kann, d.h. durch den Graphen fur e ersetzt werdenkann, wobei die Variablenbindungen richtig verwaltet werden mussen.Der G-Maschinenkode macht in etwa folgendes:

• Aufbau eines Teilgraphen fur e unter Benutzung der Knoten fur t1 . . . tn

• Uberschreiben des Knotens (f t1 . . . tn) mit der Wurzel des neuen Teilgra-phen.

Wenn bekannt ist, dass eine Funktion f mit n Argumenten bestimmte Ar-gumente auf jeden Fall auswerten muss, dann kann man f deterministischerkompilieren: Wenn f strikt im i-ten Argument ist, dann kann man Auswertun-gen umstellen.

1.3.1 Striktheit

Definition 1.3.1 Die Funktion f nennt man strikt im i-ten Argument, wennf t1 . . . ti−1 ⊥ ti+1 . . . tn = ⊥ ist fur alle Ausdrucke tj, wobei ⊥ fur Terme ohneWHNF steht.

Beachte, dass diese Definition etwas allgemeiner ist als”f benotigt immer

das im i-te Argument“, da diese Bedingung auch dann erfullt ist, wennf t1 . . . ti−1 ⊥ ti+1 . . . tn nicht terminiert ohne ti auszuwerten. Die Funktionλx.⊥ ist z.B strikt in ihrem Argument, da sie nie terminiert wenn sie auf einArgument angewendet wird, aber das Argument wird nicht ausgewertet!


Wenn f strikt im Argument xi ist, dann ist folgende Auswertungsumstellungmoglich:f x1 . . . xi . . . xn wird kompiliert, so dass folgendes bei Auswertung von(f t1 . . . tn) passiert:

1. ti auswerten zu einer WHNF t′i

2. Aufbau des Graphen wie oben mit (f t1 . . . t′i . . . tn)

Definition 1.3.2 Ein Ausdruck s mit Unterausdruck t an der Stelle p, (fallsp nicht innerhalb einer Abstraktion oder in der Alternative eines case ist), iststrikt in t (an der Stelle p), wenn s[p 7→ ⊥] ∼c ⊥ gilt.

Das ist das gleiche wie zu definieren: λx.t[p 7→ x] ist strikt.

1.3.2 Vor- und Nachteile der Auswertungsumstellung

Vorteile der Vorauswertung von ti bei Kompilierung einer Funktion f , die striktim i-ten Argument ist gegenuber vorher (bzgl der Zeit):

1. Der Zwischencode (G-Maschinenkode bzw. STG-Maschinenkode) fur fkann dann davon ausgehen, dass t′i in WHNF ist, und kann dadurch Ab-fragen sparen, insbesondere die Abfrage, ob ti bereits ausgewertet ist.

Betrachte beispielsweise die Funktion quadrat x = x*x. Diese wird naivkompiliert als:

... Push x, Push x, Pushglobal *, Mkap, Mkap, Update, ...

Dies bewirkt den Aufbau eines Knotens, der sofort wieder ausgewertetwird. Da ∗ strikt in seinen Argumenten ist, weiß man, dass die Auswertungvon t ∗ t auf jeden Fall die Auswertung von t erfordert. Also kann man tvorher auswerten. Dies ergibt:

... Push x, Eval, Push x, Mul, Update, ...

2. Wenn strikte Argumente von einem Typ sind, der sich in einem (Halb-)Wort darstellen lasst, dann kann man diese direkt darstellen, nicht nuruber eine Indirektion. Das ist die Unboxing-Optimierung

3. Programmtransformationen und Optimierungen in der STG-Maschinebenotigen teilweise, dass Ausdrucke strikt in einem Unterausdruck sind.Diese Optimierungen sind nach Erkennung der Striktheit erlaubt. DieseErkennung kann man mit Striktheitsanalyse durchfuhren.In der STG-Maschine kann man Update-Operationen im Heap einsparen,wenn man die Auswertung umgestellt hat, da man zT die Auswertung nurunter Benutzung des Stacks ausfuhren kann.

In vielen Fallen wird auch weniger Speicher von den so veranderten Funktionenbenotigt: D.h. weniger Speicher-Anforderungen und -Freigaben.


Bemerkung 1.3.3 Es ist klar, dass man algorithmisch nicht jede Striktheits-information entdecken kann, da dies bedeuten wurde, dass man Terminierungentscheiden konnte. Denn: Striktheit ist unentscheidbar. Die Analysen werdenalso nur Approximationen berechnen konnen.

Wenn man “tiefe Striktheit“ verwenden will, dann wird leider in einigen Fallender Speicherverbrauch linear in der Eingabe, obwohl er vorher konstant war.Dies passiert beispielsweise bei Funktionen, die eine Liste erzeugen, die sum-miert wird. Die Veranderung kann bewirken, dass vor Anwenden der Additiondie ganze Liste erst aufgebaut wird, und dann erst verarbeitet, wahrend diesvorher nicht der Fall war.Im Beispiel sum [1..1000], wenn die Summation folgendermaßen definiert wur-de:

sum xs = foldl’ (+) 0 xs

foldl’ op e xs = case_lst xs of (nil -> e)

(u:us) -> strict (foldl’ op) (op e u) us

werden bei lazy Auswertung die Elemente der Liste in dem Moment erzeugt, indem die Addition sie braucht, d.h. konstanter Platzbedarf. Offenbar werden alleListenelemente ausgewertet. Nach einer “tiefen Striktheits“-Veranderung konn-te es hier passieren, dass zunachst die Liste bereitgestellt wird, und dann erstsummiert wird. Das ist offenbar eine nachteilige Veranderung der Auswertungs-reihenfolge.Man kann mit der Formalisierung der Verbesserungen (Improvements bzgl. An-zahl Reduktionen) – mit und ohne Sharing – formal nicht nachweisen, dassdie Striktheitsoptimierung wirklich eine Optimierung darstellt, da Striktheits-optimierung zwar die Reihenfolge der Reduktionen, nicht aber die Anzahl derReduktionen verandert.Man muss unterscheiden zwischen der KFPT-Reduktion die Argumente manch-mal verdoppelt, und der Reduktion mit Sharing. d.h.der lazy Auswertung.Zum Beispiel fur doppelt x = x+x wird die Reduktion von doppelt (1+1)

durch Striktheitsoptimierung verbessert.vorher: doppelt (1+1) → (1+1)+(1+1) → 2+(1+1) → 2+2 → 4nachher: doppelt (1+1) → doppelt 2 → 2+2 → 4Allerdings nutzt die Implementierung der lazy Reduktion ohnehin Sharing, sodass sich hierdurch keine Verbesserung ergibt. Die einzige Optimierung durchdie Reduktion vor Einsetzen in die Funktion entsteht durch Ausnutzen des Wis-sens, dass bestimmte Unterausdrucke in WHNF vorliegen. Die Ersparnis durchUmstellung besteht in einer Verminderung der

”Update“-Operationen der ab-

strakten Maschine.Es gilt z.B in einem Lambda-Kalkul mit letrec, dass t in Normalordnung ge-nausoviele case- und lazy-Beta-Reduktionen bis zu WHNF benotigt, wie untereiner Strategie, die Umstellung der Auswertung aufgrund von Striktheit erlaubt.Einen Kalkul, der auch diese Reduktionsanzahl bei lazy Auswertung richtigsimuliert, werden wir evtl. noch behandeln.


1.3.3 Abstrakte Reduktion

Die Idee der Striktheitsanalyse mittels abstrakter Reduktion ist ein symboli-scher Test auf Nichtterminierung:Betrachte abstrakte Ausdrucke (f > . . .> ⊥ > . . .>), unter Benutzung abstrak-ter Werte ⊥,>, wobei ⊥ fur einen Term ohne WHNF steht, und > fur beliebigeTerme. Dann reduziere den abstrakten Ausdruck, evtl. auch mit Fallunterschei-dung, bis sich nachweisen lasst, dass die Reduktion ⊥ ergibt. Fur diesen Nach-weis gibt es im wesentlichen die Kriterien:

1. ⊥ ist das Ergebnis der Reduktion, oder einer Alternative, die dann nichtmehr betrachtet werden muss.

2. Das Resultat ist ein ungetypter Ausdruck. (das kommt nicht vor bei einergetypten Striktheitsanalyse)

3. die abstrakte Reduktion lauft in eine Schleife.

Die Reduktion muss teilweise eine Fallunterscheidung machen, falls der Wertvon > benotigt wird.

Regeln fur die abstrakte Reduktion :

1. man darf reduzieren. Die erlaubten Reduktionsregeln sind wie in KFPTmit Kombinatoren: β-Reduktion, δ-Reduktion (d.h. Kombinatoreinset-zung), und case-Reduktion.

2. casetyp ⊥ alts→ ⊥

3. (⊥ e)→ ⊥

4. g . . .⊥ . . .→ ⊥, falls g strikt im entsprechenden Argument ist.

5. casetyp > . . . . . .→ ?In diesem Fall mussen alle Alternativen betrachtet werden. Es wird bei derUntersuchung des jeweiligen Falls > fur die Patternvariablen eingesetzt.

Fur den Gesamtausdruck muss nachweisbar sein, dass er ⊥ ergibt; d.h.jeder Fall ist zu betrachten.Hier ist der ungetypte Kalkul etwas problematisch, man muss eigentlichmehr Falle betrachten, kann sich aber auf getypte beschranken, wenn mannur getypte Verwendungen betrachten will.

Unklare Falle bzw. keine abstrakte Reduktion ist mehr moglich: Wenn Normal-ordnungsredex von der Form ist:

1. (> t) Fallunterscheidungen mussten alle Abstraktionen abdecken?

2. Normalordnungsredex is WHNF: Stopp, und Striktheit ist nicht erfullt.


Beispiel 1.3.4length lst s = case_lst lst of nil -> s; x:xs -> length xs (s+1)

Wir argumentieren mal intuitiv, dass length strikt in beiden Argumenten ist,und versuchen eine einfache Reduktionsmethode:

1. length ist strikt im ersten Argument:length ⊥ > → caselst ⊥ of . . .→ ⊥. D.h. die Behauptung gilt.

2. length ist strikt im zweiten Argument:

length > ⊥ → caselst > of Nil→ ⊥;x : xs→ length xs (⊥+ 1)→ 〈⊥, length > (⊥+ 1)〉→ 〈⊥, length > ⊥〉

Hier steht 〈⊥, length > (⊥+1)〉 fur eine Vereinigung der beiden Moglich-keiten.

Dies ergibt eine Schleife, also ist das Ergebnis = ⊥.

Aber: Im Beispiel oben haben wir Objekt- und Metalevel-Betrachtungengemischt: Die Nichtterminierung auf der Meta-Ebene haben wir als Nicht-Terminierung auf der Objektebene gedeutet. Es ist nicht offensichtlich, dassdieses Verfahren korrekt ist.

1.3.4 Striktheitstableaus

Um die Korrektheit zu zeigen und zu verstehen, formulieren wir abstrakte Re-duktion als Kalkul, der als Datenstruktur einen Baum benutzt, der im we-sentlichen der Reduktionsbaum der abstrakten Reduktionen und der Fallunter-scheidungen ist. Dieser Baum von Ausdrucken wird auch Tableau genannt. DieAussagen und Beweise beziehen sich dann auf den Kalkul auf einem Tableau.Dazu benotigen wir zunachst abstrakte Ausdrucke (Terme), und spater fur denKorrektheitsbeweis deren Konkretisierungen Abstrakte Ausdrucke (Terme) inKFPT sind KFPT-Ausdrucke, die um die Konstanten ⊥,> erweitert sind.Wir definieren eine abstrakte Reduktion eines abstrakten Ausdrucks (Terms) tals eine Reduktion des Terms t, wobei man in t die Konstanten ⊥,> behandelt,als waren es Konstanten c⊥, c>.Wir definieren eine abstrakte Normalordnungs-Reduktion eines abstrakten Termst als eine abstrakte Reduktion in Normalordnung.

Definition 1.3.5 Ein Striktheits-Tableau zu einem abstrakten (geschlossenen)Ausdruck t ist definiert als ein markierter endlicher Baum mit:

• die Knoten sind mit abstrakten Termen markiert.

• Die Wurzel ist markiert mit dem zu reduzierenden Term t.

• Wenn der Knoten A genau die Tochterknoten B1, . . . , Bn hat, und dieentsprechenden Terme tA, tBi

sind, dann wurden die Knoten Bi mit einerder Kalkulregeln aus Definition 1.3.6 aus A erzeugt.


Definition 1.3.6 (Kalkulregeln zum Aufbau des Tableaus) Folgende Regelnwerden verwendet:

1. Reduktion: Wenn t → t′ mit abstrakter Reduktion und t eine Markierungeines Blattes B ist, dann kann man t′ als neues Blatt B′ als Tochter vonB anhangen.

2. ⊥-Reduktion: Als weitere abstrakte Reduktionen verwenden wir folgende,wobei der Korrektheits-Beweis unten nur den Fall abdeckt, wenn dieseRegeln nicht innerhalb einer Abstraktion verwendet werden.

• (⊥ t)→ ⊥.

• (caseA ⊥ . . .)→ ⊥ und

• g t1 . . . ti−1 ⊥ ti+1 . . . tn → ⊥, wenn g n-stellig ist und bereits alsstrikt im i-ten Argument bekannt ist.

3. Fallunterscheidung: Wenn (caseA > e1 . . . en) ein Unterterm eines Termst an einem Blatt B ist und n die Anzahl der Konstruktoren fur A, dannkonnen wir n+ 1 neue Blatter Bi, i = 1, . . . , n anhangen, wobei der Aus-druck B0 als ⊥ definiert ist, und die Ausdrucke Bi dadurch, dass jeweilsim case -Ausdruck das > durch (cA,i > . . .>), i = 1, . . . n ersetzt ist.

4. Generalisierung: Wir konnen ein neues Blatt B′ unter B anhangen, wobeit′B gebildet wird aus tB, wobei an einer beliebigen Stelle im Term tB einUnterterm durch > ersetzt wurde.

Die Fallunterscheidung sollte man moglichst nur an Normalordnungsredexendurchfuhren, da die Anzahl der Falle sonst unnotig exponentiell wachsen kann.Der ⊥-Fall der Fallunterscheidung ist nicht notig, wie wir spater sehen werden.

Definition 1.3.7 Ein Striktheits-Tableau ist geschlossen, wenn alle Blatter Beine der beiden folgenden Eigenschaft haben:

1. das Blatt ist mit ⊥ markiert, oder

2. das Blatt B ist mit t markiert und hat einen Vorgangerknoten N derebenfalls mit t markiert ist, und auf dem Pfad von N nach B wur-de mindestens einmal ein abstrakter Normalordnungsschritt durchgefuhrt(d.h. nicht nur Nicht-Normalordnungsreduktionen, Fallunterscheidungenund Generalisierungen) In diesem Fall nennen wir den zum Blatt gehori-gen Knoten Rekursionvater. Falls dieser nicht eindeutig ist, wahlen wirimmer den am nachsten zur Wurzel gelegenen Knoten.

Beispiel 1.3.8 Die Funktion f sei definiert durch f x = f (f x). Man sieht,dass diese Funktion nicht terminiert. Ein geschlossenes Striktheits-Tableau siehtso aus:


f >| Normalordnungsreduktion

f (f >)| Generalisierung

f > Schleife

1.3.5 Nachweis der Korrektheit des Kalkuls

Zunachst brauchen wir die Semantik der abstrakten Ausdrucke (Terme).

Definition 1.3.9 Die Konkretisierung γ(t) eines abstrakten Ausdrucks t istdie Menge aller KFPT-Ausdrucke t′, die aus t entstehen durch Ersetzung von>-Konstanten durch beliebige geschlossene Ausdrucke und von ⊥ durch beliebigegeschlossene Ausdrucke die nicht konvergieren; d.h. mit unendlicher Normalord-nungsreduktion oder mit Typfehler.

Beispiel 1.3.10

• case_lst true (nil -> x) (x:xs -> x) ∈ γ(⊥), da der Ausdruck di-rekt ungetypt ist. Weitere Ausdrucke in γ(⊥) sind u.a. (Y Id), da dieNormalordnungsreduktion nicht terminiert, (Nil Nil),. . . .

• γ(>) = Menge aller geschlossenen Terme.

• γ(length > ⊥) = alle Terme der Form (length t1 t2), wobei t1 geschlos-sen ist und t2 ∈ γ(⊥).

Die Schwierigkeit mit den offenen Termen kommt daher, dass z.B. x alleine einAusdruck ist, der keine WHNF hat, aber der nach Einsetzungen in x sowohl ⊥sein kann als auch eine WHNF haben kann.Die Anzahl der Normalordnungsreduktionen von Termen ist dabei das wesent-liche Hilfsmittel.Es gilt:

Lemma 1.3.11 Sei t abstrakter Term, s ∈ γ(t) und t → t′ eine abstrakteNormalordnungs-Reduktion an Position p. Dann kann man s an Position pebenfalls in Normalordnung reduzieren – s→ s′ – und es gilt s′ ∈ γ(t′).

Lemma 1.3.12 Sei t ein geschlossener Term mit WHNF. Dann gilt:

1. Sei eine Reduktion red (von t startend zu einer WHNF) gegeben, wo-bei nur der letzte Term in red eine WHNF ist. Dann ist die Anzahl derNormalordnungsschritte in red ≤ rln(t). Hieraus folgt auch, dass s → timpliziert, dass rln(t) ≤ rln(s) ist.

2. Sei tno−→ t′ mit einem Normalordnungsreduktionsschritt. Dann ist

rln(t) = rln(t′) + 1.


3. Sei s ein echter Unterterm von t, so dass ein Normalordnungsredex von tunterhalb von s liegt.Dann gilt rln(t) > rln(s).

Beweis. Bis auf 3 folgen die Behauptungen aus Aussage 1.0.19. Teil 3 folgt ausder Uberlegung, dass jede Normalordnungsreduktion eines Terms t, die mit einerWHNF endet, auf jeden Fall erst jeden Unterterm s zu WHNF reduzieren muss,der zwischen t und dem Normalordnungsredex von t liegt. 2

Lemma 1.3.13 Sei ein innerer Knoten N mit Markierung t eines geschlosse-nen Tableaus gegeben und sei t0 ∈ γ(t) eine Konkretisierung, die eine WHNFhat. Dann gibt es einen Nachfolger N ′ von N mit einer Markierung t′ undt1 ∈ γ(t′); und es gilt t0 ≡ t1, oder t0

∗→ t1.

Beweis. Wir gehen die Kalkulregeln durch. Sei t0 ∈ γ(t).

1. Eine abstrakte Reduktion wurde angewendet, d.h. eine β-, δ- oder case-Reduktion. Dann kann man die gleiche Reduktion fur t0 machen und erhalteine Konkretisierung t1 von t′ (siehe Lemma 1.3.11).

2. Wenn eine ⊥-Reduktion durchgefuhrt wurde, dann ist t0 ebenfalls eineKonkretisierung von t′. Hier ist zu beachten, dass ⊥-Reduktionen nichtinnerhalb von Abstraktionen durchgefuhrt werden durfen und deshalb derRedex keine freie Variable enthalt.

3. Angenommen, eine Fallunterscheidung zum case wurde gemacht.

Wenn der erste Unterausdruck im case-Ausdruck der Konkretisierung kei-ne WHNF hat, dann kann man den Tochterknoten B0 wahlen, bei demcase > . . . durch ⊥ ersetzt wurde.

Wenn der case-Unterausdruck eine WHNF hat, dann gibt es wieder zweiFalle.

Wenn der case-Ausdruck insgesamt nicht getypt ist, dann kann man denB0-Zweig nehmen.

Wenn der Unterterm im case den richtigen Typ hat, kann weiterreduziertwerden. Dieser Unterterm hat dann eine WHNF, wobei ein Konstruktordes case-Typs das oberste Symbol des Terms ist. Es gilt die Beh., daman einen der Knoten Bi wahlen kann. Beachte, dass in diesem der ersteAusdruck durch (c > . . .>) ersetzt wurde.

4. Im Fall der Generalisierung kann man t1 = t0 wahlen.

2

Satz 1.3.14 Wenn fur eine Markierung der Wurzel mit einem Term t sichmit obigen Regeln ein geschlossenes Tableau aufbauen lasst, dann haben alleKonkretisierungen von t keine WHNF.


Beweis. Annahme, dies sei falsch. Dann gibt es eine Konkretisierung t0 derWurzel, so dass t0 eine WHNF hat. Diese Konkretisierung lasst sich im Tableauverfolgen, entsprechend dem obigen Lemma. Es gibt ein Blatt, das eine Konkre-tisierung mit WHNF hat. Dieses Blatt kann nicht mit ⊥ markiert sein. Also gibtes ein Rekursionsblatt, das einen Term mit WHNF als Konkretisierung hat.Wir wahlen unter den Blattern, die einen Term mit WHNF als Konkretisierunghaben, ein Blatt aus, das eine Konkretisierung t1 mit kleinstem rln(t1) hat. Un-ter diesen minimalen Blattern wahlen wir dasjenige aus, dessen Rekursionvaterminimalen Abstand zur Wurzel hat. Wegen der Bedingungen an geschlosseneTableaux ist die Konkretisierung t1 auch eine Konkretisierung des Rekursions-vaters. Wir verfolgen t1 bis zum nachsten Blatt. Wenn auf diesem Pfad eineabstrakte Normalordnungs-Reduktion durchgefuhrt wurde, dann ist die Kon-kretisierung, die man im Pfad verfolgen konnte, kleiner geworden bzgl. rln(.).Also gab es keine solche abstrakte Normalordnungs-Reduktion. Also muss derRekursionsvater des neuen Blattes noch naher an der Wurzel liegen, da nachBedingung mindestens eine abstrakte Normalordnungs-Reduktion zwischen Re-kursionsblatt und Rekursionsvater liegt. Dies widerspricht der minimalen Wahldes Vaterknotens.

◦

{{{{{{{{

>>>>>>>>>>>>>>>>>>

◦ t1

{{{{{{{{

vv

�{

q◦

{{{{{{{{

CCCCCCCC

��

MC

6

◦

��

>>>>>>>>

◦ t1

@G

F��

//

◦ ◦ ◦

Damit haben wir einen Widerspruch dazu, dass die Wurzel eine Konkretisierungmit WHNF enthalt. 2

Korollar 1.3.15 Wenn man fur einen n-stelligen Superkombinator f ein ge-schlossenes Striktheitstableau fur den Ausdruck f > . . .> ⊥︸︷︷︸

i

> . . .>

︸︷︷︸n

aufbau-

en kann, dann ist f strikt im i-ten Argument.

Beispiel 1.3.16 Betrachte die folgenden Funktionen, die als Argumente Paarehaben. Die Funktion g ist von der Methode der abstrakten Interpretation nichtals strikt in z erkennbar. Das ist kein Problem fur unsere Methode:

f (x,y) = x+y

g x (y,z) = f (if x then (y,z) else (z,y))

h x y z = g x (y,z)


Wir nehmen an, dass die Paar-Pattern mittels case kodiert sind, d.h.:

f u = case u of (x,y) -> x+y

g x u = case u of (y,z)-> f (if x then (y,z) else (z,y))

h x y z = g x (y,z)

Die Frage ist jetzt: ist h strikt im dritten Argument?Es ist leicht zu sehen, dass f strikt in beiden Komponenten des Tupels ist. DasTableau fur h > > ⊥ ist wie folgt:

h > > ⊥

g > (>,⊥)

f(if > then (>,⊥) else (⊥,>))

kkkkkkkkkkkkkkkkk

TTTTTTTTTTTTTTTTT

⊥ f(>,⊥) f(⊥,>)

⊥ ⊥Damit ist h als strikt in z erkannt.

Beispiel 1.3.17 Wir untersuchen Striktheit von foldl. Die Definition ist:foldl f z xs = case_lst xs of Nil-> z;y:ys-> foldl f (f z y) ys

Der erste Versuch fur ein Tableau zur Frage der Striktheit im zweiten Argumentsieht so aus:

foldl > ⊥ >

case > . . .

nnnnnnnnnnnnn

SSSSSSSSSSSSSS

case ⊥ . . . case Nil . . . case (>;>) . . .

⊥ ⊥ foldl > (> ⊥ >) >

Daraus kann man nichts weiter schließen, da foldl > > > terminierende Kon-kretisierungen hat. Wenn man aber das Argument f explizit drin lasst und an-nimmt, dass f strikt im ersten Argument ist, dann bekommt man folgendes:


foldl f ⊥ >

case > . . .

nnnnnnnnnnnn

RRRRRRRRRRRRRR

case ⊥ . . . case Nil . . . case (> : >) . . .

⊥ ⊥ foldl f (f ⊥ >) >

foldl f ⊥ >

oo

�

��

��

�

�

"*

3@

KRW[\^_

Beispiel 1.3.18 Striktheit von foldr. Die Definition ist:foldr f z xs = case_lst xs of Nil-> z;y:ys-> f y (foldr f z ys)

Analog zu foldl nehmen wir an, dass das Argument f explizit bleibt. Fur foldrnehmen wir an, dass f strikt im zweiten Argument ist. Dann bekommt manfolgendes Tableau:

foldr f ⊥ >

case > . . .

nnnnnnnnnnnn

SSSSSSSSSSSSSS

case ⊥ . . . case Nil . . . case (> : >) . . .

⊥ ⊥ f > (foldr f ⊥ >)

oo

�

�

�

%

*1

:FNTX\_

Hier muss man zum Schließen des Tableaus das Kriterium verwenden, dassein Unterterm des Terms am Blatt als Rekursionsvater vorkommt und dass derUnterterm in einem Reduktionskontext ist, unter Ausnutzung der Striktheit vonf .

Abbruchkriterium: Striktheit kann nicht mehr gefunden werden, wenn fol-gendes gilt

1. wenn ein Blatt eine WHNF als Markierung hat.

2. wenn ein Blatt > als Markierung hat


Unter bestimmten Bedingungen kann man daraus schließen, dass der Ausdruckan der Wurzel tatsachlich eine WHNF als Konkretisierung hat, (und damit fnicht strikt ist). Bei der Striktheitsanalyse kann man ebenso unter gewissenBedingungen schließen, dass der Kombinator nicht strikt ist. Z.B. wenn wederdie Regel Generalisierung auf dem Pfad zur WHNF verwendet wurde, und wennkein mittels δ- oder Beta-Reduktion kopiertes >-Symbol fur den Nachweis derWHNF benutzt bzw analysiert wurde.

Beispiel 1.3.19 from x := x : from (x+1)

from ⊥ = ⊥ : from (⊥+ 1) hat WHNF. Also ist from nicht strikt.

Beispiel 1.3.20 Folgendes Beispiel zeigt, dass eine Funktion strikt sein kann,obwohl in einem Ast ein > am Blatt steht:

f x y = case x of

True -> y

False -> case x of True -> x

False-> y

f > ⊥ ergibt auf jeden Fall ⊥, da x entweder True, False oder etwas anderesist, wodurch aber das jeweilige case zu ⊥ wird. Die Analyse zu f > ⊥ ergibt imFalse-Fall: case Top of True -> Top; False-> bot, also gibt es ein Blattmit >. Das liegt daran, dass > kopiert wird, und die Information, dass es sichan verschiedenen Stellen um den gleichen Term handelt, dabei verloren geht.In letrec-Kalkulen mit Sharing passiert das nicht.

Beispiel 1.3.21 Ein Beispiel aus (Pape,1999), leicht abgeandert, da es im Ori-ginal den Ausdruck case x of x -> True enthalt, der dem strict-Operator inder Sprache entspricht. Die Behauptung dort ist, dass es nur wenige Analyseme-thoden gibt die zeigen, dass die Funktion strange strikt im zweiten Argumentist.

strange n x y = if e then x else y

where e = case_int n of

0 -> (case_lst x of nil -> False; z:zs -> False);

succ z -> True

Betrachte strange > ⊥ >. Das reduziert abstrakt zu:

if e then ⊥ else >where e = caseint > of

0→ (caselst ⊥ of Nil → False;y : ys → False);

succ z → True

Danach kommt eine Fallunterscheidung zu caseint > . . .. Den ⊥-Fall lassenwir weg.


1.if e then ⊥ else >

where e = caseint 0 of

0 → (caselst ⊥ of Nil → False;y : ys → False);

succ z → True

−→

if e then ⊥ else >where e = (caselst ⊥ of Nil → False)

−→

if e then ⊥ else >where e = ⊥

−→ if ⊥ then ⊥ else >−→ ⊥

2.if e then ⊥ else >

where e = caseint (succ >) of

0 → (caselst ⊥ of Nil → False;y : ys → False);

succ z → True

−→ if e then ⊥ else > where e = True

−→ if True then ⊥ else >−→ ⊥

Damit sind alle Zweige behandelt und die Striktheitsanalyse ist erfolgreich been-det.

Wenn man die Striktheitstableau-Analyse auf die Sprache KFPTS + seq er-weitert, dann muss man nachprufen, dass alle Aussagen uber die Redukti-onslangen noch gelten. Dies Satze gelten jedoch genauso, so dass der Beweisder Korrektheit noch funktioniert. Der Ausdruck seq > t kann allerdings nichtwie ein case behandelt werden, sondern erfordert eigentlich eine erweiterte Fall-unterscheidung. Man sieht aber leicht, dass es ausreicht, die Falle ⊥ und alleanderen WHNFs zu betrachten, so dass sofort eine Normalordnungsreduktionzu seq > t→ t erfolgen kann.

1.3.6 Verbesserungen der Striktheitsanalyse

Die Regel zum Schließen des Tableaus lasst sich verbessern. Einerseits kannman optimieren, andererseits konnen diese Erweiterungen bewirken, dass mehrabstrakte Terme als zu ⊥ aquivalent nachgewiesen werden. Die Beschreibungdes Kalkuls verkompliziert sich dadurch.


Wir definieren eine (Subsumtions-) Ordnung auf Ausdrucken, die im wesentli-chen die Ordnung ⊥ ≤ s ≤ > mit Kontexten kompatibel macht.

1. s ≤sub s fur alle s.

2. s ≤sub > fur alle s.

3. ⊥ ≤sub s fur alle s.

4. Sei C[] ein Kontext und s ≤sub t. Dann soll auch C[s] ≤sub C[t] gelten.

Definition 1.3.22 Im erweiterten Striktheitstableau-Kalkul erlauben wir fol-gende Regeln:

• (Improvement-Anwendung): Wenn t eine Markierung an einem Blatt istund t′ � t, dann hange eine neues Blatt an mit der Markierung t′.

• Verbesserte Schlussregeln: Folgende Blatt-Abschlussregeln sind nochzusatzlich erlaubt:

– Das Blatt B mit Markierung t ist abgeschlossen, wenn es einenVorganger N mit Markierung t′ gibt und t ≤sub t

′, und wenn zwi-schen N und B eine abstrakte Normalordnungs-Reduktion durch-gefuhrt wurde.

– Das Blatt B mit Markierung tB ist abgeschlossen, wenn es einenVorganger N mit Markierung tN gibt und einen echten Untertermt′B von tB, so dass t′B in einem Reduktionskontext ist (Erweiterung:an einer strikten Position). D.h. t′B wird auf jeden Fall reduziert,wenn tB zu WHNF reduziert wird. Zusatzlich muss t′B ≤sub tN sein.

• Die case-Fallunterscheidung wird eingeschrankt: der ⊥-Fall muss nichtmehr betrachtet werden, er wird durch die Subsumtionsordnung erledigt:er ist immer redundant.

Begrundung fur die Korrektheit: Man muss den Satz 1.3.14 und den Beweisdieses Satzes an die neuen Regeln anpassen. Ebenso die Lemmas, die im Beweisverwendet werden.Hierzu muss man den Begriff “Konkretisierung“ abandern zu:

Ein Term ist ≤sub -Konkretisierung von t, wenn er ≤sub eine Kon-kretisierung ist. D.h. t0 ∈ γsub(t) gdw. ∃t1 : t0 ≤sub t1 ∈ γ(t)

Es gilt dann z.B. dass s ≤sub t⇒ γsub(s) ⊆ γsub(s).Eine weitere Veranderung der Beweise ist die Verwendung des Teils 3 von Lemma1.3.12, ebenso wie die Verwendung der Improvement-Relation.

Beispiel 1.3.23 Die Funktion (takeuchi) wird z.T. als Benchmark verwendet,um die Effizienz des Funktionsaufrufs in einer Implementierung einer Program-miersprache zu testen.


tak x y z = if x <= y

then z

else tak (tak (x-1) y z)

(tak (y-1) z x)

(tak (z-1) x y))

Lemma 1.3.24 tak ist strikt in allen Argumenten:

Beweis.

1. tak ⊥ > > → if ⊥ ≤ > then . . . else . . .) → ⊥, da ≤ strikt in denbeiden Argumenten ist.

2. tak > ⊥ > → if > ≤ ⊥ . . .→ ⊥, da ≤ strikt in den beiden Argumentenist.

3.

tak > > ⊥→ if > ≤ > then ⊥ else

(tak(tak (>− 1) > ⊥)(tak (>− 1) ⊥ >)(tak (⊥− 1) > >))→ if > then ⊥ else

(tak(tak (>− 1) > ⊥)(tak (>− 1) ⊥ >)(tak (⊥− 1) > >))→ 〈⊥, tak(tak (>− 1) > ⊥)(tak (>− 1) ⊥ >)(tak (⊥− 1) > >))〉→ 〈⊥, tak(tak (>− 1) > ⊥) ⊥ (tak (⊥− 1) > >))〉→ 〈⊥〉

Der letzte Schritt gilt, da vorher bereits nachgewiesen wurde, dass tak strikt inden ersten beiden Argumenten ist. Insgesamt ist tak strikt in allen Argumenten.2

1.3.7 Implementierung der Striktheitsanalyse

Benutzung einer Variante einer Reduktionsmaschine statt eines Tableaus:

• 〈s1, . . . , sn〉 ist eine syntaktische Vereinigung. Die Operation erfolgt aufdieser Datenstruktur.

• Hierauf wird jeweils ein Reduktionsschritt durchgefuhrt.

• Es wird mit der Ordnung ≤sub eine Maximierung auf der Vereinigungdurchgefuhrt.

Problem: Ist diese Implementierung korrekt?Diese Implementierungsmethode kann man als Striktheits-Tableau-Methode an-sehen, die auf einem gerichteten Graphen arbeitet statt auf einem Baum, undbei der als zusatzliche Schlussregel verwendet wird:


Das Blatt B mit Term t ist geschlossen, wenn es einen Knoten N mitTerm t′ gibt, und t ≤sub t

′ gilt. (Der Knoten N muss nicht notwendigein Vorganger sein.) und es wird eine gerichtete Kante von B nachN eingefugt.

Hierbei darf N irgendein Knoten sein. Die Idee dahinter ist, dass der Termi-nierungstest fur den Knoten N schwerer ist als fur B, deshalb testet man nurN .Wenn das Tableau geschlossen ist, muss allerdings noch folgende Bedingungerfullt sein, die dafur sorgt, dass man das Problem nicht innerhalb eines Zyklusvor sich herschiebt: Es darf keinen Zyklus der folgenden Art geben:B1, N1, B2, N2, . . . , Bn, Nn, Bn+1 mit Bn+1 = B1, so dass fur alle i

• Bi ≤sub Ni mit obiger Regel, oder Bi hat Rekursionvater Ni mit gleichenTermen

• Ni ist Vorganger von Bi+1 und der Pfad von Ni zu Bi+1 ist ohne abstrakteNormalordnungsreduktionen.

Im Bild, wobei gestrichelte Linien die Beziehung ≤sub andeuten sollen.

R

{{{{{{{{

CCCCCCCC

N0

≤sub

QQQQQQQQ N1

≤sub||

||

N2

≤sub||

||

B1 B2 B3

Diese Bedingung kann man auch einfach formulieren, wenn man die gerichtetenKanten des Tableaus mit einbezieht: Dann darf es keinen Zyklus geben, derweder eine Normalordnungskante hat noch eine strikte Subterm-Kante.

Diese Bedingung, dass es keine solchen Zyklen gibt, erlaubt zu schließen, dassrln(t0) in einem Zyklus ohne die Nebenbedingungen wirklich verkleinert wird.Man kann die obige Bedingung durch einfachere lokale Bedingungen ersetzen,die dann allerdings etwas schwacher sein konnten.Hieraus kann man Schlusse uber die Implementierung ziehen und erkennen,worauf zu achten ist.

1. Bei Sharing von Termen: Normalerweise werden Terme uber Pointer ge-meinsam verwendet. Wenn ein Term reduziert wird, dann kann dies imTableau eine Reduktion mehrerer Blatter bedeuten.

2. Beim Suchen der Rekursionsvater muss man beachten, dass die alten Mar-kierungen, d.h. Markierung nicht an den Blattern, nicht mehr reduziertwerden durfen.


1.3.8 Anwendungen der Striktheitsanalyse

Im Glasgow Haskell Compiler und im HBC sind Striktheitsanalyser eingebaut.Der Effizienzgewinn ist merklich. Allerdings sind bestimmte einfache Strikt-heitsanfragen bereits in den Kompilierschemata fur die G- bzw. STG-Maschineenthalten, und benotigen keine Unterstutzung durch die Striktheitsanalyse.Eingepackte Werte (Boxed values) sind mit Indirektion versehene Zahlen,Boolesche Werte usw. Zur Optimierung verwenden die Haskell-Compiler aus-gepackte (pure) Werte (unboxed values) zur Laufzeit. Diese lassen sich evtl. inRegister zwischenspeichern. Die abstrakten Maschinen sehen fur diese Werteeinen eigenen Stack vor (Z.B. ABC-Maschine von Clean) bzw. eine extra Be-handlung. Damit der Compiler die Erlaubnis hat, diese zu verwenden, mussbekannt sein, dass zu bestimmten Zeitpunkten diese Werte nicht nur potentiell,sondern ausgewertet vorliegen. Diese Information kann die Striktheitsanalyseliefern.Parallelisierung. Damit man parallelisieren kann, ohne spekulative Auswer-tung zu verwenden, benotigt man Information uber die Auswertungsreihenfolgeund ob Auswertung benotigt wird. Z.B wenn der Wert von (s+t) benotigt wird,kann man zunachst s, dann t auswerten. Da aber beide garantiert ausgewertetwerden mussen, kann man s und t auch parallel auswerten. Dies liegt daran,dass + strikt in beiden Argument ist. Allgemeiner genugt es zu wissen, dass eineFunktion f strikt in bestimmten Argumenten ist. Wenn der Wert von (f t1 . . . tn)benotigt wird, kann man die Ausdrucke an den strikten Argumentstellen paral-lel auswerten. Allerdings ist dies in der Praxis nicht so einfach, denn das naiveAusnutzen kann zu viele kleine Prozesse erzeugen, die keinen Effizienzgewinnbringen. Das korrespondiert zur moglicherweise schlechteren Platzkomplexitatbei Ausnutzen der Striktheit. D.h. bei Parallelisierung ist neben der Striktheitdie Granularitat (Anzahl und Große der Prozesse) ebenfalls zu beachten.

1.3.9 Charakteristische Menge einer Auswertungsmetho-de

Algorithmen oder Verfahren, die einen Ausdruck t “von oben“ her bis zu einerWHNF oder auch weiter auswerten, nennen wir Auswertungsmethode. Zum Bei-spiel ist die Normalordnungsreduktion eine solche Auswertungsmethode. Auchein Superkombinator S, angewendet auf einen Ausdruck t, bewirkt eine Aus-wertung von t, wenn man S t mit Normalordnungsreduktion auswertet.Eine durch einen Superkombinator vermittelte Auswertung nennen wir sequen-tiell. Im folgenden interessiert uns nur die Auswertung des oberen “Datenanteil“eines Ausdrucks. Wir ignorieren die Auswirkung auf Abstraktionen.Gegeben einen bereits teilweise ausgewerteten Ausdruck t, kann man die Mengeder Unterterme, die als nachstes ausgewertet werden konnen, so definieren:AuswertbareUnterterme(t) =

• {t} wenn t nicht in WHNF

• ∅ wenn t in FWHNF


•⋃

i=1,...,ar(c) AuswertbareUnterterme(t) wenn t eine CWHNFc t1 . . . tar(c) ist.

Normalerweise besteht ein Schritt einer deterministischen Auswertung darin,dass der bisherige Auswertungszustand inspiziert wird und dann ein weiterer,bisher nicht ausgewerteter Term unterhalb der Auswertungsgrenze ausgewertetwird, d.h. ein Term in AuswertbareUnterterme(t).Es gibt auch eine parallele bzw nicht-deterministische Variante, die wir hier abernicht weiter betrachten.Beachte, dass die Auswertung den Ausdruck t zu einem “unendlichen Objekt“machen kann.Die Wirkung einer deterministischen Auswertungsmethode auf die Argumentekann man in vielen Fallen, auch solchen, in denen diese Auswertung nicht durcheinen Superkombinator bewirkt wird, beispielsweise eine parallele Auswertung,folgendermaßen charakterisieren:Informell kann man eine Auswertungsmethode so charakterisieren:

Sei E eine deterministische Auswertungsmethode und M eineMenge von geschlossenen Ausdrucken.

E ist die zu M korrespondierende Auswertung,gdw.

M = NT (E) := {e | e geschlossen und (E e) hat keine WHNF }

Im allgemeinen beschranken wir uns auf solche Mengen, die zu einer (poly-morph) getypten Sprache passen.

Sei S ein Superkombinator in KFPTSP mit einem Typ T → Bool,wobei T keine Pfeil-Typen enthalt, und M eine Menge von geschlos-senen Ausdrucken.Die charakteristische Menge zur Auswertung durch S ist gdw.

NT (S) := {e | e geschlossen und (S e)⇑}

Die Menge NT (E) der geschlossenen Terme, fur die (E e) nicht konvergiert,kann man manchmal durch eine Untermenge (d.h. eine Annaherung bzw einenAbschluss) darstellen, die aber fur unsere Zwecke das gleiche leistet (Nachweisist im Skript der CEFP).

1.3.10 Erweiterungen: neue abstrakte Werte

Andere, endliche Darstellungen kann man durch Ausdrucke mit ⊥,> undKonstruktoren erhalten. Hierbei machen wir die Vereinfachung, dass dieAbstraktionen ignoriert werden, d.h. das es formal nur fur getyptes KFPT, d.h.KFPTSP, korrekt ist. Will man das ungetypte definieren, z.B. in KFPT(S),dann braucht man eine weitere Konstante Fun, die alle Abstraktionen re-prasentiert.


Eine Grammatik dazu ist

D ::= ⊥ | > | (c D1 . . . Dn) | 〈D1, . . . Dn〉wobei c ein n-stelliger Konstruktor ist, und die semantische Bedeutung von〈D1, . . . Dn〉 die Vereinigung ist.Wir werden eine weitere Variante verwenden, die Namen erlaubt:

• Es gibt eine unendliche Menge N von Namen zu Demands.

• Demands D sind aufgebaut entsprechend der Grammatik:D ::= ⊥ | > | N | (c D1 . . . Dn) | 〈D1, . . . Dn〉

Die Semantik ist:

• γ(⊥) := Menge der divergierenden geschlossenen Ausdrucke.

• γ(>) := Menge aller geschlossenen Ausdrucke.

• γ((c D1 . . . Dn)) := Menge aller geschlossenen Ausdrucke der Form(c s1 . . . sn) mit si ∈ γ(Di) und wobei c ein Konstruktor ist.

• γ(〈D1, . . . Dn〉) :=⋃

i γ(Di).

• γ(N) ist kleinster Fixpunkt der Definitionsgleichungen fur die Demandna-men.

Die formale Definition erganzt dann diese Definitionen durch einen Abschlussbzgl kontextueller Approximation.

Beispiel 1.3.25 Wir konnen jetzt schon solche Mengen hinschreiben und schonZusammenhange andeuten:

1. ⊥ beschreibt die WHNF Auswertung:Zu ⊥ gehort die Menge der Ausdrucke, deren Normalordnungs-Auswertung nicht mit einer WHNF terminiert.

2. 〈⊥, Nil,⊥ : >〉 beschreibt den sinnvollen Anteil der Auswertung, die eineListe zu WHNF auswertet, und, falls es eine nichtleere Liste ist, das ersteElement ebenfalls auswertet. Ist diese Auswertung durch einen Superkom-binator definiert (hd), dann mussten es eigentlich auch solche Elementesein, die die (dynamische) Typisierung verletzen, z.B. True.

3. Die Ruckgratauswertung ist die Auswertung, die eine Liste zu WHNF aus-wertet und danach rekursiv wieder den Tail genauso behandelt.

Die geschlossenen Listenausdrucke, fur die die Ruckgratauswertung nichtterminiert. kann man beschreiben als 〈⊥,> : ⊥,> : > : ⊥, . . .〉. Die rekur-sive Definition Inf = 〈⊥,> : Inf〉 beschreibt diese Menge. Diese Mengebesteht aus den Listen mit ⊥-Tail, und approximiert alle Listenausdrucke(unter Benutzung von club), bei denen man bei der Suche nach dem ite-rierten Tail niemals auf ein Ende (d.h. ein Nil) stoßt. Damit sind auchalle “unendlichen“ Listen erfasst.


Die Charakterisierung durch das komplementare Verhalten ist zunachst nichtintuitiv, erweist sich aber als sehr praktisch, denn die zugehorigen Mengenbe-schreibungen, die Demands, sind leicht rekursiv zu beschreiben und zu verar-beiten und sie haben die richtigen Eigenschaften. Im folgenden Kapitel werdenwir Demands als eine endliche Reprasentation solcher Mengen definieren.Man kann mit erweiterten Demands auch Mengen darstellen, die keiner Aus-wertung entsprechen: Z.B. {t | t hat Nil als WHNF } ist eine solche Menge.Eine andere ist die Menge der endlichen Listen:

Fin = 〈Nil,> : Fin〉

Fin entspricht keiner Auswertung im obigen Sinne, denn das Element ⊥ fehlt.Es gibt auch tatsachlich keine Auswertungsfunktion, die genau auf endlichenListen nicht terminiert.

1.3.11 Andere Striktheiten

Eine Moglichkeit der Erweiterung ist die Frage nach “tiefer“ Striktheit, Hy-perstriktheit, bedingter Striktheit, oder die Frage nach Striktheit in mehrerenPositionen.

• Die Auswertungsanforderung “werte die Liste und dann das erste Elementdes Listenargumentes aus“: entspricht z.B. hd mit hd (x:xs) = x. Diesentspricht dem abstrakten Wert (Demand) 〈⊥, Nil,⊥ : >〉

• Tail-strikt: Diese Anforderung wertet (rekursiv) den gesamten Tail derListe aus. Dies entspricht dem abstrakten Wert (Demand) Inf.

• hyperstrikt: Diese Anforderung wertet zur hyperstrikten Normalform (d.h.(Daten-) Normalform) aus. Eine hyperstrikte Normalform ist ein Aus-druck, der aus Konstruktoren und Abstraktionen besteht, entsprechendder Definition: HSNF ::= λx.s | (c HSNF . . .HSNF ).

Tailstriktheit

einer Funktion im Argument i bedeutet, dass diese Funktion das Listenargumentxi auf jeden Fall bis zum Listenende auswertet. Diese Eigenschaft kann manmittels der Methode der abstrakten Reduktion folgendermaßen zeigen: Mannimmt Inf mit Inf := 〈⊥,> : Inf〉 als abstrakten Wert, der als Test fur dietailstrikte Verarbeitung von Listen dient mitD.h. Inf ist rekursiv definiert als eine Vereinigung von ⊥ und > : Inf.Diesen Wert Inf nimmt man jetzt statt ⊥ an der interessierenden Argumentstel-le. Mit dem abstrakten Wert beschreibt man eine Testmenge, die die tailstrikteAuswertung durch Nichtterminierung anzeigt.


Definition 1.3.26 Zu abstrakten Werten mit einer Definition W =〈W1, . . . ,Wn〉n, gibt es eine extra Fallunterscheidungsregel:

C[W ]

C[W1] | . . . | C[Wn]

Diese sollte man bevorzugt an Stellen verwenden, an denen eine abstrakte Nor-malordnungsreduktion ermoglicht wird.

Eine tail-strikte Funktion kann bzgl der Platzkomplexitat verschiedenes Verhal-ten zeigen. Die optimale Variante tritt ein, wenn diese uber eine sehr große Listelaufen soll, und dies mit konstantem (oder logarithmischem) Platz durchfuhrenkann (Scan). Wenn man zu strikt programmiert hat, kann es sein, dass dieseFunktion einen linearen Platzbedarf hat, und man im wesentlichen die ganzeListe gleichzeitig im Speicher halten muss. In dem Fall ist es unmoglich, dieFunktion auf ein Argument anzuwenden, das zu einer sehr großen Liste auswer-tet.Wenn man mit Stromen programmiert, ist es eine interessante Information, obeine Funktion tail-strikt ist oder nicht. Denn tail-strikte Funktionen kann mannicht auf Strome anwenden. Z.B. length ist tail-strikt, kann also mit Stromennicht umgehen, wahrend map nicht tail-strikt im zweiten Argument ist.Mit der Tableuamethode kann man zeigen, dass Funktionen tail-strikt sind, alsoungeeignet fur Strome, aber nicht dass sie geeignet sind. Dafur benotigt manandere Methoden.

Beispiel 1.3.27 Eigenschaften der iterativen Variante von length.

length lst s = case_lst lst of nil -> s; x:xs -> length xs (s+1)

Behauptung: Die Funktion length ist tailstrikt im ersten Argument.

length Inf >

caselst Inf (Nil→ >) (x : xs→ length xs (>+ 1))

fffffffffffffffffffffffff

caselst ⊥ . . . caselst (> : Inf) (Nil→ >) (x : xs→ length xs (>+ 1))

⊥ length Inf (>+ 1)

length Inf > Schleife!


Wir geben weitere Beispiele an:

Beispiel 1.3.28 reverse xs = case_lst xs of nil -> nil; x:xs -> (reverse xs) ++ [x]

Diese Funktion dreht eine Liste um. Wir verwenden wieder

Inf := 〈⊥,> : Inf〉.

Wir zeigen mit Striktheitsanalyse, dass reverse die Liste tailstrikt verarbeitet:

reverse Inf

caselst Inf of Nil→ Nil;x : xs→ (reverse xs)++[x]

hhhhhhhhhhhhhhhhhhh

caselst ⊥ . . . (reverse Inf)++[>]

⊥caselst (reverse Inf) of Nil→ [>];

x : xs→ (reverse xs)++[x]

Schleife, da Vorgangerterm an strikter Position

und da ++ strikt im ersten Argument ist.

Hyperstriktheit

lasst sich folgendermaßen analysieren:

Man benotigt einen abstrakten Test-Ausdruck, der zur Hyperstriktheit passt.

HS = 〈 ⊥,cons1 HS > . . .>︸︷︷︸

ar(cons1)

, cons1 > HS > . . .>, . . . , cons1 > . . .> HS,

. . . ,consn HS > . . .>︸︷︷︸

ar(consn)

, consn > HS > . . .>, . . . , consn > . . .> HS,

〉

Hierbei lauft consi uber alle im Programm vorkommenden Konstruktoren, dienicht nullstellig sind. Die nullstelligen Konstruktoren durfen nicht in HS sein,denn deren Auswertung ist bereits durch das ⊥ abgedeckt. Aus dem gleichenGrund darf Fun (FWHNF) nicht in HS sein.


Der obige abstrakte Term beschreibt die Ausdrucke, die man mittels Auswer-tung von oben nicht zu Normalform auswerten kann. Hier ist eine Auswertunggemeint, die Daten vollstandig auswertet, aber nicht unter λ auswertet.Der Ausdruck HS enthalt alle geschlossenen Ausdrucke, die eine undefinierteStelle haben, und approximiert solche, die in mindestens einer

”Richtung“ un-

endlich tief auswertbar sind.

Beispiel 1.3.29 sum s xs = case_lst xs (nil ->s) (y:ys -> sum (s+y) ys)

Beh: sum ist hyperstrikt in xs. Hierbei gehen wir davon aus, dass die Zahlen inPeano-Kodierung vorliegen, und HS entsprechend wie oben definiert ist, dass sumbereits als strikt im ersten Element gezeigt wurde, und dass + bereits als hyper-strikt (bzw. strikt im ersten und zweiten Argument) gezeigt ist. (Die ungetyptenFalle sind weggelassen)

sum > HS

caselst HS (Nil→ >);(y : ys→ (sum (>+ y) ys))

ooooooooooooooo

UUUUUUUUUUUUUUUU

⊥caselst (> : HS) (Nil→ >);

(y : ys→ (sum (>+ y) ys))caselst (HS : >) (Nil→ >);

(y : ys→ (sum (>+ y) ys))

sum (>+>) HS sum (>+ HS) >

+ ist hyperstrikt

sum > HS sum ⊥ >

sum ist strikt in 1.

Schleife ⊥

1.3.12 Wadlers 4-Punkt-Domain-Analyse

Diese Analyse von listenverarbeitenden Funktionen basiert auf einem Domainmit 4 Elementen und benutzt abstrakte Interpretation. Diese Anayse soll hierkurz erlautert werden und dann gezeigt werden, dass man mit der Methodeder Striktheitstableaus die Information, die diese Analyse liefert, ebenfalls (imPrinzip) berechnen kann.Die 4PD-Analyse kann teilweise mehr herleiten als die Striktheitstableau-Methode, denn mit der 4-Punkt-Domain-Analyse kann man den Wert von Funk-tionen auf dem Domain berechnen (bzw approximieren), nicht nur die Verwen-dung von Datenstrukturen testen. Wenn man allerdings die abstrakten Werte in


die Striktheitsanalyse einbettet, und in gewissen Fallen Hilfsfunktionen verwen-det, dann ergibt sich die gleiche Information. Die 4PD-Analyse liefert weniger,wenn auch Fallunterscheidungen uber andere Datentypen notwendig zum exak-ten Berechnen sind.Diese Analyse wollen wir hier zum besseren Verstandnis in den Rahmen dersyntax-basierten Analysen stellen.Wir stellen diese 4 Werte als abstrakte Werte dar:

1. ⊥. Menge der nichtterminierenden Ausdrucke. Das entspricht Auswertungzu WHNF.

2. ⊥∞: ist dasselbe wie Inf. D.h. alle Listenausdrucke bei denen die rekursiveAuswertung des Tails nicht terminiert. Das entspricht Auswertung desRuckgrats einer Liste.

3. ⊥ε: Darstellbar als ⊥ε := 〈⊥,⊥ : >,> : ⊥ε〉. Das ist die Menge aller Li-sten, die keine WHNF haben, oder in denen mindestens ein Element keineWHNF hat. Dies entspricht Auswertung einer Liste und aller Elementezu WHNF. Es entspricht dem HS eingeschrankt auf Listen und deren Ele-mente.

4. >ε endliche Listen, in denen jedes Element eine WHNF hat. Dies hat keineEntsprechung als Auswertung.

(Wir werden diesen Wert hier nicht verwenden; bzw. ersatzweise > ver-wenden. Um diesen abstrakten Wert zu verwenden musste man auchden Ansatz (Nichtterminierungsnachweis) und den Beweis der Korrekt-heit abandern.) )

Die Ordnung auf dem Domain ist: ⊥ ≤ ⊥∞ ≤ ⊥ε ≤ >ε. Zu beachten ist,dass diese Ordnung nicht direkt mit der Vorstellung als Menge von Ausdruckenzusammenhangt.

Beispiel 1.3.30 sum s xs = case_lst xs (nil ->s) (y:ys -> sum (s+y) ys)

Die endrekursive Funktion sum wertet das Argument xs aus entsprechend ⊥ε :


sum > ⊥ε

caselst ⊥ε (Nil→ >)(y : ys→ sum (>+ y) ys)

⊥

ppppppppppppppp⊥:>

>:⊥ε

UUUUUUUUUUUUUUUU

⊥caselst (⊥ : >) (Nil→ >);(y : ys→ (sum (>+ y) ys))

caselst (> : ⊥ε) (Nil→ >);(y : ys→ (sum (>+ y) ys))

sum (>+⊥) > sum (>+>) ⊥ε

sum ⊥ > sum > ⊥ε

⊥ Schleife

In allen Fallen ergibt sich ⊥ oder eine Schleife, somit ist Nichtterminierunggezeigt, und wir wissen: die Funktion sum wertet im Listenargument die Listeund jedes Element der Liste zu WHNF aus.Dieses Wissen konnte man verwenden, um vor der Auswertung von sum bereitsTeile der Argumentliste und deren Element zu evaluieren.

Beispiel 1.3.31 Die 4PD-Analyse kann zeigen, dass map f : Inf → Inf. Umdas mit Striktheitsanalyse zu zeigen, konnte man folgende Idee verwenden:Man braucht die (eine) Auswertungsfunktion istliste, die zu Inf passt:

istliste xs = case_lst xs of Nil -> True; y:ys -> istliste ys

map f xs = case_lst xs of Nil -> Nil; y:ys -> f y : map f ys

Wenn wir zeigen konnen, dass istliste(map > Inf) = ⊥ ist, dann hatten wirdie gleiche Information wie map : Inf → Inf. Um das schließen zu durfen, istallerdings noch Arbeit in die Begrundung zu stecken, eine genaue Behandlungder ungetypten Ausdrucke, und evtl. eine Abanderung des Kalkuls bzgl. ungety-pten Ausdrucken. Dies wird in der Demandanalyse ohnehin gemacht. Deshalbhier nur eine Andeutung, wie ein passendes Tableau aussehen wurde:


istliste (map > Inf)

istliste (caselst Inf (Nil→ Nil)y : ys→ (> y) : (map > ys))

⊥jjjjjjjjjjjjjjjj

⊥:Inf

(istliste ⊥) istliste ((> >) : map > Inf)

⊥ (case ((> >) : map > Inf) . . .)

istliste (map > Inf)

Schleife

Die 4PD-Analyse kann zeigen, dass fur terminierende Funktionen f folgendesgilt: map f : >ε → >ε. Die Striktheitsanalyse kann das nicht zeigen, da es furendliche Listen keine charakteristische Auswertungsfunktion gibt. Umgekehrtkann die 4PD-Analyse manche Beziehungen nicht herleiten, da sie den typi-schen Beschrankungen der abstrakten Interpretation unterliegt: die abstrakteInterpretation der Unterfunktionen ist zu verwenden.

Bemerkung 1.3.32 Die Funktion length angewendet auf die Testmenge ⊥ε

ergibt, dass eine WHNF moglich ist. Z.B. ist ⊥ : Nil ∈ γ(⊥ε). Die Anwen-dung von length ergibt 2. Man sieht auch dass die Funktion length mit dieserMethode nicht als hyperstrikt nachgewiesen werden kann (und es auch nicht ist).

Beispiel 1.3.33 Ein weiteres Beispiel ist die Funktion f mit den Definitionen

f xs = length (concat xs)

concat xs = case_lst xs of Nil- > Nil; (y:ys) -> y ++ (concat ys)

von der man zeigen kann, dass sie jede Liste und alle Elemente (das sind Listenals Elemente) auswertet. Dazu muss man das Tableau fur (length(concat xs))berechnen. Wir benutzen ⊥ε := 〈⊥,⊥ : >,> : ⊥ε〉.Mit der Wurzel (length(concat ⊥ε)) ergibt sich fur die ersten beiden Alterna-tiven jeweils leicht ⊥. Bei der dritten erhalt man:(length(concat > : ⊥ε)), danachlength(> ++ (concat ⊥ε))Hier muss man drei Falle betrachten:


1. ⊥: In diesem Fall ist das Ergebnis sofort ⊥.

2. Nil: in dem Falle ergibt sich (length(concat ⊥ε)), der Term an der Wur-zel, und man kann den Pfad abbrechen.

3. > : >. In diesem Fall ergibt sich nach zwei Reduktionen: 1 +length(> ++ (concat ⊥ε)) und man kann mit dem Untertermkriteriumabbrechen.

Weitere Beispiele kann man dem Artikel von M.Schmidt-Schauß, David Sabel,und Marko Schutz: Deciding inclusion of set constants over infinite non-strictdata structures. RAIRO-Theoretical Informatics and Applications, 41(2):225-241, July 2007. entnehmen

1.3.13 Baume und Analyse

Beispiel 1.3.34 Die Haskell Notation zur Datenstruktur eines einfachenbinares Baumes ist:

data Tree a = Leaf a | Node (Tree a) (Tree a)

wobei Leaf und Node die Konstruktoren sind. Wir nehmen an, dass es nur dieBaume und Boolesche Werte gibt. Wir betrachten die eingeschrankte Menge derWHNFS vom Typ (Tree Boolean). Einige Demands sind:

Tr = ⊥ ∪ (Leaf B) ∪ (Node Tr Tr) (entspr. >Tree)B = ⊥ ∪ True ∪ False (entspr. >Bool)BF = ⊥ ∪ FalseBT = ⊥ ∪ TrueTF = ⊥ ∪ (Leaf BF) ∪ (Node TF TF)TT = ⊥ ∪ (Leaf BT) ∪ (Node TT Tr) ∪ (Node TF TT)TInf = ⊥ ∪ (Leaf ⊥) ∪ (Node TInf Tr) ∪ (Node Tr TInf)TInf2 = ⊥ ∪ (Leaf ⊥) ∪ (Node TInf2 TInf2))TT2 = ⊥ ∪ (Leaf BT) ∪ (Node TT Tr) ∪ (Node Tr TT2)

Der Demand TT korrespondiert zu einer Funktion fTrue∈, die einen Baum vomTyp (Tree Boolean) von links nach rechts durchscannt und ja sagt, wenn sie einBlatt mit Wert True findet. D.h. die Analyse zeigt an, dass fTrue∈ TT nichtterminiert.Der Demand TInf korrespondiert zu einer Funktion die die Anahl der Blatterzahlt. D.h. die Auswertung ist: werte alle inneren Knoten aus, inklusive Blatter,aber nicht die Inhalte der Blatter.Der abstrakte Wert TInf2 entspricht nicht dieser Auswertung:, denn auch ei-ne Funktion die das erste Blatt sucht, wurde hier nichtterminieren. Genauer:TInf2 entspricht der Auswertung: werte irgendein Blatt aus: das ist aber kei-ne Auswertung die zu einer deterministischen Funktion bzw SUoerkombinatorpasst.Die Inklusion TInf ⊆ TF gilt, aber dies kann nicht von der ≤sub-Relation er-kannt werden. Zum Beispiel gilt auch dass TT2 = TT ist.


Beispiel 1.3.35 Zu Baumdatenstruktur.

psum (Leaf a) = a

psum (Node k1 k2) = (psum k1) + (psum k2)

Der Demand, der der Auswertung aller Elemente in den Blattern entspricht,ist die Menge der Baume, die ein Blatt mit ⊥-Element haben, und bei denenentsprechend die Zwischenknoten auch ⊥ sein konnen:Eine Analyse, ob ein Kombinator F alle Elemente eines Baumes auswertet,kann man mit

F TInf

durchfuhren, und den Tableaukalkul zur abstrakten Reduktion darauf anwenden.Fur psum sieht das so aus:

Analyse durch Fallunterscheidung uber TInf :psum TInf =⇒

• psum ⊥ → ⊥.

• psum (Leaf ⊥)→ ⊥

• psum (Node TInf >)→ psum TInf + psum>Unterterm an strikter Position kommt als Vorganger vor!

• psum (Node > TInf )→ psum>+ psum TInfUnterterm an strikter Position kommt als Vorganger vor!

Date post:	06-Aug-2019
Category:	Documents
Upload:	nguyencong
View:	219 times
Download:	0 times

Semantik und Analyse: insbesondere Striktheitsanalyse · SAFP, WS 20012/13, Striktheits-Analyse, 5....

Documents