Zuweisbare Variablen -------------------- Wir erweitern den einfach typisierten Lambdakalkuel um globale integer - Variablen, in denen man Werte abspeichern und wieder auslesen kann. Zur Unterscheidung von den Lambdakalkuel Variablen bezeichnen wir diese als Referenzen. Dazu nehmen wir eine Menge Loc von solchen Referenzen an und fuehren neue Typen ein, die in Beispielen nuetzlich sein werden. tau ::= unit | int | bool | ref | tau1->tau2 | tau1*tau2 e ::= () | x | l | tt | ff | if e1 then e2 else e3 | e1 e2 | lambda x.e | !e | e1:=e2 | e.1 | e.2 wobei l:Loc und x:Var. Hierbei ist !e der Wert der (durch e bezeichneten) Referenz und := bezeichet die Wertzuweisung. unit ist ein Typ mit nur einem Element, welches man mit () bezeichnet. tau1*tau2 ist das kartesiche Produkt von tau1 und tau2, seine Elemente sind Paare der Form (x,y) wobei x:tau1 und y:tau2. Auf die Komponenten eines solchen Paares greift man mit den Projektionen .1 und .2 zu. Als Abkuerzung fuehren wir ein let x=e1 in e2 == (lambda x.e2)e1 e1;e2 == let z = e1 in e2 wobei z nicht frei in e2 vorkommt. Oft wird auch let-in als Primitivum hinzugenommen, weil man so die Hintereinanderausfuehrung von Funktionstypen getrennt studieren kann. Beispielprogramme: ASSIGNER == lambda x.l:=x : int -> unit COUNTER == lambda x.(lambda u.x:=!x+1,lambda u.!x,lambda u.!x:=0) : ref -> (unit->unit) * (unit->int) * (unit->unit) Nimmt eine Referenz als Argument und verwendet sie um ein Zaehlerobjekt zurueckzugeben. MEMO == lambda l1.lambda l2.lambda f. l1:=0; l2:=f 0; lambda x.if x = !l1 then !l2 else let fx = f x in l1:=x;l2:=fx;fx : ref -> ref -> (int -> int) -> int -> int Ein Memoisierungsfunktional. Es nimmt zwei Referenzen und eine Funktion f als Argument. Es liefert eine Funktion fmem zurueck, die dasselbe tut wie f aber moeglicherweise effizienter: fmem speichert naemlich jeweils das letzte Argument, mit dem es aufgerufen wurde, in der Referenz l1 ab und legt in l2 den dazugehoerigen f-Wert ab. Ruft man also fmem mehrmals hintereinander mit demselben Wert auf, so wird nur beim ersten Mal tatsaechlich eine Auswertung f angestossen. Hier noch der Vollstaendigkeit halber eine Auswahl der Typisierungsregeln: Gamma |- e1 : ref Gamma |- e2 : int ----------------------------------------- Gamma |- e1 := e2 : unit Gamma |- e : ref ------------------ Gamma |- !e : int Gamma |- e : bool Gamma |- e1 : tau Gamma |- e2 : tau -------------------------------------------------------------- Gamma |- if e then e1 else e2 : tau Wie immer ist Gamma eine Zuweisung von Typen an Variablen. Denotationelle Semantik ----------------------- Wir werden fuer die Referenzen keine Auswerteregeln angeben, sondern vielmehr zeigen, wie man auch in Gegenwart imperativer Konzepte, Terme und Funktionen als mathematische Funktionen auffassen kann. Diese Art der Semantikgebung, die man als denotationelle Semantik bezeichnet, kann man auch fuer andere Systeme verwenden. Wir nehmen also die Referenzen als Vehikel um diese Technik zu illustrieren. Aus Gruenden der Vereinfachung, nehmen wir die Rekursion, also fix aus unserer Sprache zunaechst wieder heraus. Dadurch terminieren alle Programme und wir koennen mit ganz normalen totalen Funktionen arbeiten. Es spraeche nichts dagegen, eine for-Schleife hinzuzunehmen, aber wegen des notationellen Aufwandes werden wir das nicht offiziell tun. Wir ordnen also jedem Typ eine Menge zu durch folgende Definition: [[int]] = Z [[unit]] = {()} [[tau1*tau2]] = [[tau1]] * [[tau2]] (kart Prod von Mengen) [[ref]] = Loc [[bool]] = {tt,ff} [[tau1->tau2]] = [[tau1]] -> T([[tau2]]), wobei T(X) = Store->Store*X und Store = Loc -> int Die letzte Klausel bedarf der Erlaeuterung. Fuer Mengen X, Y bedeutet X->Y die Menge aller Funktionen von X nach Y. Haetten wir keine Referenzen, wollten wir also dem "reinen" Lambdakalkuel eine denotationelle Semantik geben, so schrieben wir einfach [[tau1->tau2]] = [[tau1]]->[[tau2]] Nun aber liefert ja ein Funktionsterm wie lambda x.l:=x nicht einfach nur ein Element vom Typ unit zurueck, sondern hat auch noch den Seiteneffekt, dass eben das Argument x der Referenz l zugewiesen wird. In der Semantik wird dem durch den Operator T( - ) Rechnung getragen, bei dem es sich um eine sogenannte Monade handelt. T(X) ist hier einfach eine Abkuerzung fuer Funktionen, die angeben, wie man aus einem Speicherzustand den neuen Speicherzustand, sowie das Ergebnis in X bekommt. Sei Gamma ein Typkontext. Eine Umgebung fuer Gamma ist eine Funktion eta, die jeder Variablen x:dom(Gamma) ein Element eta(x) : [[Gamma(x)]] zuordnet. Wenn nun Gamma |- e : tau, so definieren wir ein Element [[e]]eta : T([[tau]]) durch die folgenden Klauseln. Man beachte, dass [[e]]eta kein Element von [[tau]] selbst ist, sondern von T([[tau]]), da ja schon die Auswerung von e selbst Seiteneffekte haben kann. So hat man etwa l:=9;78 : int die Denotation dieses Terms ist die Funktion, die einem Speicher sigma das Paar sigma[l:=9],78 zuweist. Hier haben wir l als Konstante aufgefasst. Ist l hingegen eine Variable, so ergaebe sich (sigma[eta(l):=9],78). Nun also die definierenden Klauseln fuer diese semantische Funktion. [[x]]eta = val(eta(x)) wobei val(v)(s) = (s,v) [[(e1,e2)]]eta(s) = sei (s1,v1) = [[e1]]eta(s) und sei (s2,v2) = [[e2]]eta(s1) in (s2,(v1,v2)) [[e1 e2]]eta(s) = sei (s1,f) = [[e1]]eta(s) und sei (s2,v) = [[e2]]eta(s1) in f(v)(s2) [[lambda x.e]]eta = val(f) wobei f(v) = [[e]]eta[x|->v] [[if e1 then e2 else e3]] = sei (s1,v) = [[e1]]eta(s) in [[e2]]eta(s1), falls v=tt [[e3]]eta(s1), falls v=ff [[e1:=e2]]eta(s) = sei (s1,l) = [[e1]]eta(s) in sei (s2,v) = [[e2]]eta(s1) in (s2[l|->v],()) [[!e]]eta(s) = sei (s1,l) = [[e]]eta(s) in (s1, s1(l)) Die verbleibenden semantischen Gleichungen verbleiben als Uebung. Rechne als Beispiel die Semantiken der Beispielprogramm ASSIGNER COUNTER MEMO aus. Die A-Normalform ---------------- Man kann beliebige Terme semantikerhaltend so transformieren, dass der Term let-Ausdruecke enthaelt und die Termformer (-,-), .1, .2, Applikation (soweit nicht in let's benutzt), -!, :=, nur auf Variablen oder Konstanten angewandt werden und ausserdem in der Abfrage eines if-Terms nur Variablen oder Konstanten stehen. Zum Beispiel wird aus g (!x) (!(f y)) der Term let u = !x in let l = f y in let v = !l in let h = g u in h v Diese Form bezeichnet man als A-Normalform (administrative normal form [Felleisen et al]). Setzt man voraus, dass ein Term bereits in ANF vorliegt, so vereinfachen sich die semantischen Gleichungen erheblich. Man muss allerdings eine explizite Gleichung fuer das let hinzunehmen: [[let x=e1 in e2]]eta(s) = sei (s1,v1) = [[e1]]eta(s) und sei (s2,v2) = [[e2]]eta[x|->v1](s1) in (s2,v2) [[(x,y)]]eta = val(eta(x),eta(y)) [[x.1]]eta = val(eta(x).1) [[!x]]eta(s) = (s,s.eta(x)) [[x:=y]]eta(s) = (s[eta(x)|->eta(y)],()) etc. Man verwendet die A-Normalform auch in der Kompilierung. Sie ist eng verwandt mit der SSA (static single assignment) Form. Frage: Warum ist if x then e1 else e2 ---> let y1=e1 in let y2=e2 in if x then y1 else y2 nicht semantikerhaltend? Semantisch gerechtfertigte Programmaequivalenzen ------------------------------------------------ Haben zwei Programmstuecke (Terme) gleiche Semantik, so koennen sie gegeneinander ersetzt werden. Folgende Gleichungen gelten in diesem Sinne, wobei v, v1, v2 Werte sind, das sind Terme, die durch folgende Grammatik gegeben sind: v ::= x | l | c | lambda x.e | (v1,v2) | v.1 | v.2 | if v then v1 else v2 | () Werte sind gerade die Terme, die keine Seiteneffekte aufweisen; fuer Werte gilt insbesondere [[v]]eta(s) = (s,w) mit w unabhaengig von s. (lambda x.e)v = e[v/x] (v1,v2).1 = v1 (v1,v2).2 = v2 v = () /* Falls v ein Wert vom Typ unit ist */ v = (v.1,v.2) /* Falls v ein Wert vom Typ tau1*tau2 ist */ v = lambda x.vx /* Falls v ein Wert vom Typ tau1->tau2 ist */ Darueberhinaus gelten einige Gleichungen fuer Fallunterscheidungen, wie z.B. if x then (if x then e1 else e2) else (if x then e3 else e4) = if x then e1 else e4 Beispielanwendung: let x=e in let y=e in e'[x,y] ==== let z = (e,e) in e'[z.1,z.2] Metasprache und Monaden ----------------------- Die Ausdruecke auf der rechten Seite der semantischen Gleichungen sehen sehr stark nach programmiersprachlichen Termen aus. Man kann das formal machen und dementsprechend eine Metasprache einfuehren, mit deren Hilfe dann verschiedene objektsprachliche Konstrukte interpretiert werden koennen. In der Tat war dies auch eine der Motivationen fuer ML (SML OCAML): ML=metalanguage! Solch eine Metasprache ist dann ein einfach typisierter Lambdakalkuel mit einem zusaetzlichen Typformer T, der je nach Bedarf instanziiert werden kann. Im Beispiel waere etwa T(X) = Store->Store*X, sowie Konstrukte let und val, die den Typregeln Gamma |- e1 : T(tau1) Gamma,x:tau1 |- e2 : T(tau2) -------------------------------------------------------------- Gamma |- let x=e1 in e2 : T(tau2) und Gamma |- e:tau ------------------------ Gamma |- val(e) : T(tau) genuegen. Zur Definition einer Monade gehoert neben dem Operator an sich immer noch das let und val, genau wie zu einer Gruppe nicht nur die Traegermenge, sondern auch noch die Multiplikationsoperation gehoert. Genau wie bei Gruppen koennen auch die Monaden axiomatisch gefasst werden. Hinzu kommen Typ- und Termformer und Konstanten, die sich aus der spezifischen Instanzierung der Monade T ergeben. Zum Beispiel bei uns: := : ref -> int -> T(unit) ! : ref -> T(int) Will man exceptions modellieren, so verwendet man T(tau)=tau + exn, wobei E eine Menge (Typ) der Exceptions ist. Man hat dann: throw : exn -> T(tau) catch : (exn * T(tau)) -> T(tau) In der Metasprache sind Funktionstypen pur, haben also a priori keine Seiteneffekte. Den Funktionstyp der Objektsprache interpretiert man dann als tau1 -> T(tau2). In Haskell kann man selber Monaden definieren und hat syntaktische Konzepte zur Verfuegung, die einem vorgaukeln, man befinde sich in der Objektsprache, wo doch in Wirklichkeit mit der rein-funktionalen Metasprache gearbeitet wird. Die Metasprache ist etwas reicher als die Objektsprache, weil es ja in der Objektsprache kein Pendant zu Typen wie int->int gibt, welche also (in der Metasprache!) seiteneffektfreie Funktionen bezeichnen. Effekte ------- Es ist jetzt unser Ziel, mithilfe von Typen genauere Informationen ueber die Art der Seiteneffekte zu gewinnen. Fuer jede Referenz l:Loc fuehren wir den Typ ref_l ein, der nur aus dieser Referenz besteht. Ein "Singleton - Typ". Ausserdem fuehren wir die beiden Elementareffekte rd(l) (Lesen) und wr(l) (Schreiben) ein. Ein Effekt ist nun eine Menge von Elementareffekten und die verfeinerten Typen sind gegeben durch die Grammatik: sigma ::= int | unit | bool | ref_l | sigma_1 -> T_eff(sigma_2) wobei l:Loc und eff ein Effekt ist. Das verfeinerte Typurteil bekommt die Form Gamma |- e : T_eff(sigma) wobei nunmehr Gamma Variablen auf verfeinerte Typen abbildet. Das verfeinerte Typurteil besagt, dass die Auswertung von e in einer Umgebung, die die verfeinerten Typen in Gamma hat, ein Ergebnis des verfeinerten Typs sigma liefert und ausserdem bei dieser Auswertung hoechstens die in eff aufgefuehrten Seiteneffekte stattfinden koennen. T_eff is hier ein rein syntaktisches Konzept. Viele Autoren notieren diese verfeinerten Typen auch wie folgt: sigma1-eff->sigma2 statt sigma1->T_eff(sigma2) Gamma |- e:sigma,eff statt Gamma |- e:T_eff(sigma) Man spricht bei eff in sigma1->T_eff(sigma2), bzw sigma1-eff->sigma2, vom latenten Effekt eff, da er ja nicht sofort, sondern erst bei Ausfuehrung der so typisierten Funktion zum Tragen kommt. So haben wir beispielsweise fuer jedes beliebige l:Loc die verfeinerten Typisierungen |- l:=9 : T_{wr(l)}(unit) |- l:=l+1 : T_{wr(l),rd(l)}(unit) |- lambda x.l:=x : T_0(int -> T_{wr(l)}(unit)) |- COUNTER : T_0(ref_l -> T_0((unit->T_{rd(l),wr(l)}(unit)) * (unit->T_{rd(l)}(int)) * (unit->T_{wr(l)}(unit)))) Der Einfachheit halber lassen wir die Annotation T_0 in Zukunft weg, schreiben also: |- COUNTER : ref_l -> (unit->T_{rd(l),wr(l)}(unit)) * (unit->T_{rd(l)}(int)) * (unit->T_{wr(l)}(unit)) Schliesslich haben wir |- MEMO : ref_{l1} -> ref_{l2} -> (int->T_eff1(int)) -> T_eff2(int->T_eff3(int)) wobei eff1 ein beliebiger Effekt ist und eff2=eff1+{wr(l1),wr(l2)} und eff3=eff1+{rd(l1),wr(l1),rd(l2),wr(l2)} Wir sehen hier, dass die Effektannotation nur eine Approximation an das tatsaechliche Verhalten eines Programms darstellt. Die memoisierte Funktion MEMO l1 l2 f kann zwar, muss aber nicht, den latenten Effekt eff1 exhibieren; das kommt eben darauf an, ob f ausgefuehrt wird, oder nicht. Zu jedem verfeinerten Typ sigma definieren wir den unterliegenden einfachen Typ |sigma| durch |sigma1->T_eff(sigma2)| = |sigma1|->|sigma2| homomorph fortgesetzt auf alle verfeinerten Typen, Kontexte und Typurteile. Effektsystem ------------ Wir geben jetzt Typisierungsregeln an, die das verfeinerte Typurteil formal definieren. Dabei gehen wir von der A-Normalform aus, d.h., die Typregeln erfassen nur Terme, die bereits in A-Normalform gebracht wurden. Dadurch spart man sich einiges an Schreibarbeit. ----------------------- Gamma |- x : T_0(sigma) --------------------------- Gamma |- c : T_0(typeof(c)) Gamma(x) = ref_l und Gamma(y)=int --------------------------------- Gamma |- x:=y : T_{wr(l)}(unit) Gamma(x) = ref_l ---------------------------- Gamma |- !x : T_{rd(l)}(int) Gamma |- e1 : T_eff1(sigma1) Gamma,x:sigma2 |- e2 : T_eff2(sigma2) eff=eff1 u eff2 -------------------------------------------------------- Gamma |- let x=e1 in e2 : T_eff(sigma2) Gamma(x) = sigma1->T_eff(sigma2) Gamma(y) = sigma1 -------------------------------- Gamma |- xy : T_eff(sigma2) Gamma |- e1 : T_eff1(sigma) Gamma |- e2 : T_eff2(sigma) eff=eff1 u eff2 Gamma(x)=bool -------------------------------------------- Gamma |- if x then e1 else e2 : T_eff(sigma) sigma1 <: sigma2 eff1 Teilmenge von eff2 Gamma |- e : T_eff1(sigma1) ------------------------------------------- Gamma |- e : T_eff2(sigma2) Hierbei ist sigma1 <: sigma2 die durch die folgenden Regeln definierte Subtyprelation: ------------ sigma<:sigma sigma1 <: sigma2 sigma3 <: sigma4 eff1 <: eff2 ----------------------------------------------------------- sigma2->T_eff1(sigma3) <: sigma1->T_eff2(sigma4) Effektpolymorphie und Typinferenz --------------------------------- Genau wie beim einfach typisierten Lambdakalkuel kann man auch hier Typschemata betrachten, um allgemeinstmoegliche Typen zu erhalten. Diese enthalten nunmehr Typvariablen, die ueber beliebige Typen rangieren, Effektvariablen, die ueber beliebige Effekte rangieren und Referenzvariablen, die ueber beliebige Referenzen rangieren. Die oben in den Beispielen angegebenen Typen koennen bereits als solche Typschemata gedeutet werden, wenn man die in ihnen vorkommenden Effekte und Referenzen als Variablen deutet. Genau wie bei der ML Typinferenz erlaubt man auch hier polymorphe Typen fuer let-gebundene Variablen, die dann auf verschiedene Art instanziert werden koennen. So koennen wir beispielsweise folgenden Term mit den o.a. Regeln nicht typisieren, wohl aber mithilfe von Typschemata: let f = lambda x.x:=0 in (f l1);(f l2) sofern l1 und l2 zwei verschiedene (feste) Referenzen sind. Mit Typschemata erhaelt f den schematischen Typ ref_l -> T_{wr(l)}(unit), der dann in den beiden nachfolgenden Anwendungen jeweils mit l=l1 und =l2 instanziert wird. Zu gegebenem Term existiert nun wiederum ein allgemeinster verfeinerter (schematischer) Typ, den man mit einer naheliegenden Erweiterung des Hindley-Milner Algorithmus effektiv und effizient berechnen kann. Wir werden dieses Thema spaeter nocheinmal im Zusammenhang mit dem auf let und Rekursion erweiterten Hindley-Milner Algorithmus. Fuer den Moment kehren wir zu den einfachen (nichtschematischen) Typen zurueck wobei wir uns im klaren darueber sind, dass ein bestimmter Term mehrere, ja im allgemeinen unendlich viele, Typen haben kann. Die Typschemata sind letztlich nichts anderes als eine kompakte Notation fuer solche unendlichen Familien von Typen. Effektbasierte Programmtransformation ------------------------------------- Wir wollen nun die Effektinformation dazu nutzen, Programmtransformationen vorzunehmen. Hier ist ein erstes Beispiel einer solchen Programmtransformation: Dead code elimination: Kommt in einem Term ein Subterm e vor, sodass in seinem Kontext e wie folgt typisiert werden kann: Gamma |- e : T_eff(unit) wobei {l | wr(l):eff} = 0, so kann e durch () ersetzt werden (vulgo, weggelassen werden). In welchem Sinne ist so eine Ersetzung zulaessig? Die Semantik der beiden ineinander zu ueberfuehrenden Terme ist auf jeden Fall nicht gleich. Bevor wir weitere Beispiele solcher Programmtransformationen betrachten fuehren wir noch folgende Notationen ein: reads(eff) = {l | rd(l) : eff} writes(eff) = {l | wr(l) : eff} Hier sind nun weitere Beispiele von solchen Programmtransformationen: Code motion: Lassen sich zwei Terme in ihrem Kontext wie folgt typisieren: Gamma |- e1 : T_eff1(tau) Gamma |- e2 : T_eff2(tau) und gilt reads(eff1) & writes(eff2) = 0 writes(eff1) & reads(eff2) = 0 writes(eff1) & writes(eff2) = 0 [ & bezeichnet Schnittmenge, 0 die leere Menge] so kann (e1,e2) durch (e2,e1) ersetzt werden. Das bedeutet zusammen mit den allgemeingueltigen Ersetzungsregeln, dass man die Ausfuehrung von e1 mit der Ausfuehrung von e2 vertauschen kann. Duplicated code: Laesst sich e in seinem Kontext wie folgt typisieren Gamma |- e : T_eff(tau) und ist reads(eff) & writes(eff) = 0, so kann man (e,e) durch let x=e in (x,x) ersetzen. Im Zusammenhang mit den allgemeingueltigen Ersetzungsregeln bedeutet dies, dass man die doppelte Ausfuehrung von e zu einer Einzigen zusammenziehen kann. Pure Lambda Hoist: Laesst sich e in seinem Kontext wie folgt typisieren Gamma |- e : T_0(tau) hat also e ueberhaupt keine Seiteneffekte, so sind lambda x.let y=e in e'(x,y) und let x=e in lambda y.e'(x,y) ersetzungsgleich. Das bedeutet also, dass man aus einem Methodenrumpf seiteneffektfreie Berechnungen, die zudem nicht von den formalen Parametern abhaengen extrahieren kann und ein fuer alle Mal vorab berechnen kann. Es kann passieren, dass die fuer die Anwendbarkeit solch einer Aequivalenz verlangte Typisierung nur unter Annahmen an die Typisierung der freien Variablen (man denke an anderswo definierte Methoden) moeglich ist. So hat man zum Beispiel f:unit->T_eff(tau) |- f(l:=1) : T_{eff+wr(l)}(tau) Der Term f(l:=1) passt also auf "Duplicated Computation" unter der Bedingung, dass reads(eff) & (writes(eff) + l) = 0. Die Effekttypisierung erlaubt einem also, Infomration ueber Seiteneffekte zu den Spezifikationen einer Funktion (Methode), hier f, hinzuzunehmen und diese Information dann an den Verwendungsstellen (call sites) der Funktion fuer Programmtransformationen zu nutzen. Beobachtungsgleichheit ---------------------- In welchem Sinne sollen diese Aequivalenzen gelten? Semantikerhaltend sind sie zumindestens im allgemeinen nicht, da ja die Semantik die Annahmen ueber Argumente und freie Variablen, unter denen die Aequivalenzen gelten sollen, nicht modelliert. Ein konkretes Beispiel: Wir haben lambda x.lambda y.x:=3;y:=4 : ref_l1 -> ref_l2 -> T_{wr(l1),wr(l2)}(unit) wobei l1 =/= l2 Derselbe Typ gilt fuer lambda x.lambda y.x:=4;y:=3 : ref_l1 -> ref_l2 -> T_{wr(l1),wr(l2)}(unit) und gemaess "code motion" sind beide aequivalent. Semantisch sind die beiden aber verschieden und intuitiv gleich verhalten tun sie sich ja auch nur unter der Annahme, dass die beiden Referenzargumente voneinander verschieden sind. Noch extremer verhaelt es sich bei der Aequivalenz lambda f.f() = lambda f.() die ja z.B. bei der Typisierung (unit->T_eff(unit)) -> T_eff(unit) gefolgert werden kann unter der Bedingung, dass writes(eff)=0. Eine Moeglichkeit, solche Aequivalenzen formal zu deuten, besteht darin, sie auf konkrete Beobachtungen zurueckzufuehren. Zwei Terme sind beobachtungsgleich, wenn sie sich in beliebigem Kontext die gleiche beobachtbare Wirkung haben. Formal definieren wir das so: Definition [Beobachtungsgleichheit fuer geschlossene Werte]: Seien v1, v2 geschlossene Werte eines verfeinerten Typs tau, also |- v1 : tau oder strenggenommen |- v1 : T_0(tau) |- v2 : tau oder strenggenommen |- v2 : T_0(tau) v1 und v2 sind beobachtungsgleich bei tau, i.Z. |= v1 = v2 : tau wenn fuer alle geschlossenen Werte v : tau -> T_eff(bool) mit beliebigem Effekt eff gilt: [[v v1]](s0) = (s1,b1) [[v v1]](s0) = (s2,b2) impliziert b1=b2. Hier ist s0 der initiale Speicherzustand, definiert etwa durch s0(l)=0 fuer alle l. Der Wert v ist also sozusagen die Beobachtung die man macht; der Speicherzustand nach der Beobachtung wird verworfen. In unserer Situation gilt allerdings sogar folgendes: wenn |= v1 = v2 : tau und |- v : tau -> T_eff(bool) und [[v v1]](s) = (s1,b1) [[v v2]](s) = (s2,b2) dann sogar s1=s2. Waere naemlich s1 =/= s2, so muesste es ein l:Loc geben mit s1(l) =/= s2(l). Sei etwa s1(l)=c. Wir definieren dann eine neue Beobachtung v' durch v' := lambda x.vx;(!l)==c welche v1 und v2 dann unterscheidet. Das ist nicht so, wenn man auch lokale Variablen zulaesst, die von einer aeusseren Beobachtung nicht eingesehen werden koennen. Definition [Beobachtungsgleichheit fuer Terme]: Zwei Terme e1, e2, wobei x1:tau1,...,xn:taun |- e1, e2 :tau sind beobachtungsgleich, wenn lambda x1:tau1...lambda xn:taun.lambda y:unit.e1 fuer i=1,2 beobachtungsgleich beim Typ tau1->...->taun->unit->tau sind. Man beachte, dass Beobachtungsgleichheit stets typabhaengig ist. Satz: Haben zwei Terme gleiche Semantik, so sind sie insbesondere beobachtungsgleich. Die Umkehrung gilt nicht notwendigerweise. Beweis: Die Definition der Beobachtungsgleichheit nimmt nur auf die Semantik eines Termes bezug. Gegenbeispiele fuer die Umkehrung hatten wir bereits oben (z.B. lambda f.f() und lambda f.() bei (int->T_0(unit))->T_0(unit)). Insbesondere ist also die Beobachtungsgleichheit abgeschlossen unter beta-Reduktion fuer Werte. Relationale Semantik -------------------- Wir suchen nunmehr eine verfeinerte Semantik, die zum einen verfeinerte Typen mit gleichem unterliegendem einfachen Typ unterschiedlich interpretiert und uns zum anderen die oben genannten Programmaequivalenzen validiert. Natuerlich soll diese Semantik nicht groeber sein, als die Beobachtungsgleichheit; dafuer ist es jedoch schon ausreichend, wenn sie kompositional definiert ist und auf Basistypen der Gleichheit entspricht. Definition [Partielle Aequivalenzrelation (PER)]: Eine binaere Relation R auf einer Menge A heisst partielle Aequivalaenzrelation (PER), wenn R symmetrisch und transitiv ist. Der Traeger einer PER R ist supp(R) = {x:A | xRx}. Eingeschraenkt auf supp(R) ist R eine Aequivalenzrelation. Eine PER entspricht somit einer Einteilung einer Teilmenge von A in Klassen. Definition [Store-Relation]: Eine Store-Relation ist eine PER auf der Menge Store = Loc->Z der Speicherzustaende. Unser Ziel ist nun, fuer jeden verfeinerten Typ tau eine PER [[[tau]]] auf [[ |tau| ]] zu definieren, sodass der Traeger von [[[tau]]] gerade diejenigen semantischen Objekte ausschliesst, die die Effektinformation in tau *nicht* beruecksichtigen. Auf dem Traeger von [[[tau]]] soll [[[tau]]] dann als Aequivalenzrelation beobachtungsgleiche Elemente zusammenfassen. Wir definieren (x,y) : [[[bool]]] <==> x=y (x,y) : [[[int]]] <==> x=y (x,y) : [[[unit]]] <==> x=y (gilt immer) Fuer Referenzen setzen wir (x,y) : [[[ref_l]]] <==> x=y=l Der Traeger von [[[ref_l]]] besteht also nur aus der Referenz l. Kommen wir jetzt zu Berechnungen. Es wird sinnvoll sein, fuer jeden Typ tau und Effekt eff eine PER [[[T_eff tau]]] auf T([[ |tau| ]]) definieren, deren Traeger alle die Berechnungen, deren Seiteneffekte uber eff hinausgehen, ausschliesst. Auf dem Traeger soll die Relation beobachtungsgleiche Berechnungen zusammenfassen. Zum Zwecke der Motivation betrachten wir Berechnungen des Typs int, auf semantischer Seite also Funktionen f,f':Store->Store*Z. Betrachten wir zunaechst den Fall, wo eff=0, also Seiteneffektfreiheit vorliegt. Eine seiteneffektfreie Berechnung f ist letztendlich von der Form f(s)=(s,v), wobei v unabhaengig von s ist. Zwei solche Berechnungen sind beobachtungsgleich, wenn die entsprechenden Konstanten v gleich sind. Eine auf den ersten Blick vielleicht etwas umstaendliche Art, beides auszudruecken, ist die folgende: f [[[T_0 int]]] f' <==> fuer alle Relationen R auf Store gilt: wenn sRs' und (s1,v)=f(s) und (s1',v')=f'(s'), so folgt s1Rs1' und v=v'. Als naechstes studieren wir den Fall, wo eff={rd(l1),wr(l2)}. Eine solche Berechnung muss also aus s:Store ein Paar (s1,v) berechnen, welches nur von s.l1 abhaengt und darueberhinaus s1 sich von s hoechstens auf l2 unterscheidet. Zwei solche Berechnungen f und f' sind dann beobachtungsgleich, wenn sie als Funktionen extensional gleich sind. Betrachten wir jetzt den Fall, wo der Rueckgabewert von komplizierterem Typ ist. Hier sollten wir erlauben, dass bei zwei Speicherzustaenden s s', die auf l1 uebereinstimmen, die Ergebniswerte, wenn auch nicht exakt identisch, so doch beobachtungsgleich sind. All das laesst sich durch folgende Setzung erfassen: f [[[T_eff tau]]] f' <==> Fuer alle Relationen R auf Store mit (sRs' => s.l1=s'.l1 /\ sRs' => s[l2:=u] R s'[l2:=u]) folgt aus s R s' und (s1,v)=f(s) und (s1',v')=f'(s') dass s1 R s1' und v [[[tau]]] v' Geben wir nunmehr die allgemeine Definition von [[[tau]]]. (x,x') : [[[bool]]] <==> x=x' (x,x') : [[[int]]] <==> x=x' (x,x') : [[[unit]]] <==> x=x' (gilt immer) (x,x') : [[[ref_l]]] <==> x=x'=l (x,x') : [[[tau1*tau2]]] <==> (fst(x),fst(x')):[[[tau1]]] /\ (snd(x),snd(x')):[[[tau2]]] (f,f') : [[[tau1 -> T_eff tau2]]] <==> fuer alle (x,x'):[[[tau1]]]. f(x),f'(x') : [[[T_eff(tau2)]]] wobei (f,f') : [[[T_eff(tau)]]] <==> fuer alle R<:Store*Store. R respektiert eff => .fuer alle s,s'. s R s' und (s1,v)=f(s), (s1',v')=f'(s') => s1Rs1' /\ (v,v'):[[[tau]]] Hierbei setzt man: R respektiert 0, immer. R respektiert {rd(l)} <=> sRs'=>s.l=s'.l R respektiert {wr(l)} <=> sRs'=>s[l->n]Rs'[l->n] fuer alle n R respektiert eff1 u eff2 <=> R respektiert eff1 und R respektiert eff2. Satz [Fundamentallemma]: Sei Gamma |- e : T_eff tau und (eta(x),eta'(x)):[[[Gamma(x)]]] fuer alle x:dom(Gamma). Dann gilt auch ([[e]]eta, [[e]]eta') : [[[T_eff tau]]] Der Beweis erfolgt durch Induktion ueber Typherleitungen. Das Fundamentallemma besagt, dass die syntaktisch gewonnene Effektinformation tatsaechlich semantisch korrekt ist; also dass z.B. der Wert eines geschlossenen Terms, der als T_{wr(l)}(int) typisiert werden kann, tatsaechlich nicht vom Speciher abhaengt und diesen auch nur hoechstens bei l modifiziert. Satz [Beobachtungsgleichheit]: Seien e, e' Terme mit Gamma |- e : T_eff tau und Gamma |- e' : T_eff tau. Fuer alle eta, eta' mit (eta(x),eta'(x)):[[[Gamma(x)]]] fuer x:dom(Gamma) gelte ([[e]]eta,[[e']]eta'):[[[T_eff tau]]]. Satz [Programmaequivalenzen]: Die oben genanten Programmaequivalenzen "dead code", "code motion", "duplicated code", "pure lambda hoist" gelten semantisch in folgendem Sinne: Wenn Gamma |- e : T_eff unit und writes(eff)=0 und (eta(x),eta'(x)):[[[Gamma(x)]]] fuer alle x:dom(Gamma), so folgt ([[e]]eta, [[()]]eta') : [[[T_eff unit]]]. und analog fuer die anderen drei. Allgemeiner gilt: Laesst sich die Beobachtungsgleichheit zweier Terme e, e', wobei Gamma |- e:T_eff tau, Gamma |- e':T_eff tau syntaktisch herleiten unter Verwendung der vier Programmaequivalenzen, den allgemeingueltigen semantischen Aequivalenzen, sowie Gleichungslogik (refl,sym,trans,cong), so gilt fuer eta, eta' wie oben, dass ([[e]]eta,[[e]]eta'):[[[T_eff tau]]]. Erweiterung auf dynamisch allokierten Speicher ---------------------------------------------- Wir fuehren einen neuen Termformer ref ein, wobei gilt Gamma |- e : int -------------------- Gamma |- ref e : ref Die Idee ist, dass ref x eine neue Referenz erzeugt und mit dem Wert von e initialisiert. Dieses Konstrukt erlaubt eine elegantere Formulierung unserer Beispielprogramme COUNTER, MEMO: COUNTER == let x = ref 0 in (lambda u.x:=!x+1,lambda u.!x,lambda u.!x:=0) : (unit->unit) * (unit->int) * (unit->unit) MEMO == lambda f.let l1 = ref 0 in let l1 = ref (f 0) in lambda x.if x = !l1 then !l2 else let fx = f x in l1:=x;l2:=fx;fx : (int -> int) -> int -> int Um das semantisch zu modellieren, nehmen wir eine Menge Store von Speicherzustaenden an, die mit den folgenden Operationen ausgestattet ist: Fuer s:Store ist dom(s) eine endliche Teilmenge von Loc. Falls l:dom(s), so ist s.l:Z Falls l0:dom(s) und v:Z, so ist s[l0:=v] :Store und es gilt s[l0:=v].l = if l=l0 then v else s.l Es gibt eine Konstante empty:Store mit dom(empty)=0 Falls s:Store und v:Z, so ist new(s,v):Store * Loc und wenn new(s,v)=(s',l0), so folgt dom(s')=dom(s) + {l0} (disjunkte Vereinigung) und s'.l = if l=l0 then v else s.l Man kann diese Struktur konkret beispielsweise durch endliche Funktionen von Loc nach Z modellieren. Wir wollen uns aber bewusst nicht auf eine bestimmte Implementierung festlegen, insbesondere machen wir nicht die auf den ersten Blick plausibel erscheinende Annahme, dass die neu allokierte Referenz l0 bei new(s,v)=(s',l0) nur von dom(s) abhaengt. Wir setzen dann (unter Zugrundelegung von ANF) [[ref x]]eta s = new(s,eta(x)) Die anderen Gleichungen sind unveraendert. Literatur zu diesem Teil: Benton, Kennedy, Beringer, Hofmann: Reading, Writing, and Relations. Proc. APLAS 2006. Typisierung mit Regionen ------------------------ Wir wollen jetzt die verfeinerte Typisierung auf dynamische Allokierung erweitern. Hierzu teilen wir den gerade allokierten Speicherbereich *gedanklich* in disjunkte Regionen auf. "Gedanklich" bedeutet, dass das Laufzeitmodell, also die denotationelle Semantik von dieser Aufteilung unberuehrt bleibt. Es findet also keine physikalische Einteilung statt. Wir geben uns einen unendlichen Vorrat Reg an Regionen, genauer gesagt Regionenbezeichnern vor und fuehren die verfeinerten Typen ein: tau ::= ref_r | int | bool | unit | tau1*tau2 | tau1 -> T_eff tau2 eff <: {rd(r), wr(r), al(r) | r:Reg} Man ersetzt also individuelle Referenzen durch Regionen und fuegt ausserdem den neuen Allokationseffekt al(r) hinzu, der besagt, dass in der gegebenen Region eine Allokation getaetigt wurde. Die Typregeln sind ganz genau wie beim globalen Fall. Wir haben also zum Beispiel COUNTER : (unit->T_{rd(r),wr(r)}(unit)) * (unit->T_{rd(r)}(int)) * (unit->T_{wr(r)}(unit)) wobei r eine beliebige Region ist. Neu hinzukommt allerdings noch die Maskierungsregel: Gamma |- e : T_eff tau r kommt nicht in Gamma oder tau vor ----------------------------------------------------------------- Gamma |- e : T_{eff \ {wr(r),rd(r),al(r)}} tau Diese erlaubt es, Effekte, die eine Region r betreffen, die weder in den freien Variablen, noch im Ergebnis erwaehnt wird, zu streichen. Ist zum Beispiel e ein geschlossener Ausdruck des Typs int, der im Innern eines oder mehrere Instanzen des COUNTER benutzt, so laesst sich dieser zunaechst mit |- e : T_{rd(r), wr(r), al(r)} int typisieren, wobei r eine beliebige Region ist. Mithilfe der Maskierungsregel kann man dann den besseren Typ |- e : T_0 int herleiten. In unserer bei PPDP07 erscheinenden Arbeit erweitern wir (Benton, Kennedy, Beringer, MH) die relationale Semantik auf diese Situation und zeigen, dass die effektabhaengigen Programmaequivalenzen auch in Gegenwart der Maskierungsregel weiterhin gelten. Insbesondere duerfte man also auch den gerade erwaehnten integer-Ausdruck doppelt auswerten etc ohne das Endergebnis dabei zu beeinflussen. Urspurenglich wurde dieses Regionentypsystem von Tofte und Talpin entwickelt, um blockorientierte Speicherverwaltung ohne garbage collection zu ermoeglichen. Die Idee ist hierbei, ein Programm (automatisch) so zu typisieren, dass moeglichst oft die Maskierungsregel angewendet wird. Zur Laufzeit werden dann maskierte Regionen deallokiert (freigegeben), nachdem der maskierte Ausdruck vollstaendig ausgewertet wurde. Im Beispiel wuerden also die verwendeten COUNTER Objekte dann freigegeben. Um das durchzufuehren muessen natuerlich zur Laufzeit eine Regionentabelle mitgefuehrt werden. Man kann dann zeigen, dass durch solche Deallokation die Programmsemantik nicht veraendert wird. Tofte und Talpin verwenden diese Art der Speicherverwaltung in ihrem ML - Kit Compiler. Neuerdings taucht diese regionenbasierte Speicherverwaltung auch bei Real-tTime Java (aus naheliegenden Gruenden) auf (www.rtsj.org). Literatur: Mads Tofte, Jean-Pierre Talpin. Region-Based Memory Management. Information and Computation 1997.