Das System Fsub --------------- ist eine Erweiterung von System F um Subtypen. Es wurde von Cardelli und anderen eingefuehrt als Vehikel zur Semantikgebung objektorientierter Sprachen. Spaeter fanden Cardelli und Abadi, dass man der OOP besser mit Spezialkalkuelen beikomme, die Objekte als Primitiva eingebaut haben, anstatt sie durch bekanntes zu codieren. Trotzdem hat FSUB als Basiskalkuel fuer das Verstaendnis von Subtyping nach wie vor seine Bedeutung. Die Typen von FSUB sind gegeben durch: tau ::= Top | all X<:tau1.tau2 | tau1->tau2 Abkuerzungshalber fuehrt man ein all X.tau := all X<:Top.tau tau1*tau2 := all X.(tau1->tau2->X)->X Ein Subtypkontext hat die Form Theta ::= X1<:tau1,...,Xn<:taun wobei FTV(taui) <= {X1,...,X_{i-1}} Beispiel: X<:Top, Y<:Y->Y Wir definieren Theta(Xi) := taui Ein Typkontext hat die Form Gamma ::= x1:tau1,...,xn:taun Wir schreiben Theta |- tau ok wenn Theta=X1<:tau1,...,Xn<:taun ein Subtypkontext ist und ausserdem FTV(tau)<={X1..Xn} NB In diesem Fall ist auch Theta,X<:tau ein Subtypkontext. Analog schreiben wir Theta |- Gamma ok. Subtyping in FSUB ----------------- Das Subtypurteil Theta |- tau1 <: tau2 /* tau1 ist Subtyp von tau2 unter den Annahmen in Theta */ ist durch folgende Regeln induktiv definiert: Theta |- tau ok ------------------- REFL Theta |- tau <: tau Theta |- tau1 <: tau2 Theta |- tau2 <: tau3 -------------------------------------------------- TRANS Theta |- tau1 <: tau3 Theta Subtypkontext ---------------------- AX Theta |- X <: Theta(X) Theta |- tau ok ------------------- TOP Theta |- tau <: Top Theta |- tau12 <: tau11 Theta |- tau21 <: tau22 ------------------------------------------------------- FUN Theta |- tau11->tau21 <: tau12->tau22 Theta |- tau12 <: tau11 Theta,X<:tau12 |- tau21 <: tau22 X nicht in Theta gebunden ----------------------------------------------------------------- ALL Theta |- all X<:tau11.tau21 <: all X<:tau12.tau22 Will man die Regel ALL rueckwaertsanwenden, obwohl X in Theta gebunden ist, oder wenn die beiden gebundenen Variablen nicht uebereinstimmen, so fuehrt man vorher eine geeignete Umbennung durch (von unten nach oben lesen). X<:Top,U<:X |- U <: Top X<:Top,U<:X |- U<:X ----------------------------------------------- X<:Top,U<:X |- Top->U <: U->X -------------------------------------------- X<:Top |- all U<:Top.Top->U <: all U<:X.U->X -------------------------------------------- X<:Top |- all U<:Top.Top->U <: all U<:X.U->X -------------------------------------------- X<:Top |- all X<:Top.Top->X <: all Z<:X.Z->X Fuer Produkttypen haben wir die abgeleitete Subtypregel: Theta |- tau11 <: tau12 Theta |- tau21 <: tau22 ------------------------------------------------------- PROD Theta |- tau11*tau21 <: tau12*tau22 Typisierung in FSUB ------------------- Theta;Gamma |- e : tau ist induktiv wie folgt und so aehnlich wie bei System F definiert: Theta |- Gamma ok --------------------------- T-VAR Theta;Gamma |- x : Gamma(x) Theta;Gamma |- e1 : tau1->tau2 Theta;Gamma |- e2 : tau1 ---------------------------------- T-APP Theta;Gamma |- e1 e2 : tau2 Theta;Gamma,x:tau1 |- e : tau2 --------------------------------------------- T-LAM Theta;Gamma |- lambda x:tau1.e : tau1 -> tau2 Theta,X<:tau1;Gamma |- e:tau2 Theta |- Gamma ok -------------------------------------------------- T-TLAM Theta;Gamma |- Lambda X<:tau1.e : all X<:tau1.tau2 Theta;Gamma |- e : all X<:tau1.tau2 Theta |- sigma <: tau1 ---------------------------------------- T-TAPP Theta;Gamma |- e[sigma] : tau2[X:=sigma] Theta;Gamma |- e : tau1 Theta;Gamma |- tau1 <: tau2 --------------------------- T-SUB Theta;Gamma |- e : tau2 Beispiel: T<:Top,Y<:Top,W<:Top;f:Y->W->T |- Lambda X<:Y*W.lambda x:X.(x,f x.1 x.2) : all X<:Y*W.X->X*T (Die zum Produkt gehoerigen Termformer verstehen sich als die entsprechenden zur Kodierung des Produkts gehoerigen und aus System F bekannten Definitionen.) Codierung von Verbundtypen -------------------------- Man gibt sich eine Menge von Labels vor, z.B. die natuerlichen Zahlen. Sind l1,...ln paarweise verschiedene Labels und tau1,...,taun Typen, so bildet man den Verbundtyp (Record) {l1:tau1,...,ln:taun}, der durch die folgenden Typ und Subtypregeln bestimmt ist: {k1,...,km} <= {l1,...,ln} (Teilmenge) fuer j=1..m: falls li=kj dann Theta |- taui<:sigmaj ----------------------------------------------------------- Theta |- {l1:tau1,...,ln:taun} <: {k1:sigma1,...,km:sigmam} Theta;Gamma |- ei:taui fuer i=1..n -------------------------------------------------------- Theta;Gamma |- {l1=e1,...ln=en} : {l1:tau1,...,ln:taun} Theta;Gamma |- e : {l1:tau1,...,ln:taun} ----------------------------------------- Theta;Gamma |- e.li : taui Beispiel: Point = {x:int, y:int} CPoint = {x:int, y:int, c:color} Es gilt CPoint <: Point Ist die Menge aller Labels linear geordnet, z.B. wenn die Labels gleich den natuerlichen Zahlen sind, so lassen sich Records durch Produkttypen unter Einhaltung der entsprechenden Subtyprelation wie folgt codieren: Sei N = max{l1,...ln} {l1:tau1,...ln:taun} = (((((sigma1*sigma2)*sigma3)*....)*sigmaN)*Top wobei sigmai = tauj, falls lj=i und sigmai=Top, sonst. Zum Beispiel {1:int,5:float, 3:CPoint} = ((((int * Top) * CPoint) * Top) * float) * Top und {3:Point, 5:float} = ((((Top * Top) * Point) * Top) * float) * Top In der Tat ist ersteres Subtyp von letzterem. Das mag in der Praxis ineffizient sein; man weiss aber durch diese Kodierung, dass bei der Hinzunahme von Verbundtypen mit keinen essentiell neuen Schwierigkeiten zu rechnen ist. Algorithmisches Subtyping ------------------------- Will man von zwei vorgelegten Typen tau1, tau2 entscheiden, ob tau1<:tau2 gilt, so kann man versuchen, eine Herleitung durch Rueckwaertsanwendung der Subtypregeln zu finden. Probleme bereitet hierbi die Regel TRANS, bei der ja der "mittlere" Typ geraten werden muss. Ganz aehnlich ist es ja bei der Schnittregel (Einfuehrung von Lemmas, Verstaerkung von Induktionshypothesen) in Beweiskalkuelen, die dort aus den gleichen Gruenden die automatische Beweissuche behindert. Zum Glueck kann man zeigen, dass die Regel TRANS auf wenige Instanzen beschraenkt werden kann. Das algorithmische Subtypurteil Theta |-a tau1 <: tau2 ist durch folgende Regeln induktiv definiert: *) REFL, aber beschraenkt auf Variablen *) FUN, ALL, TOP *) VAR wobei Theta |- Theta(X) <: tau ------------------------ VAR Theta |- X <: tau Lemma: Wenn Theta |-a tau1 <: tau2, so auch Theta |- tau1 <: tau2 Beweis: Formal durch Induktion ueber algorithmische Herleitungen. Die einzig neue Regel ist VAR, die kann aber durch AX und TRANS wie folgt simuliert werden --------------------- AX Theta |- X <: Theta(X) Theta |- Theta(X) <: tau ---------------------------------------------------------- TRANS Theta |- X <: tau Satz: Wenn Theta |- tau1 <: tau2, so auch Theta |-a tau1 <: tau2 Zunaechst bemerken wir, dass wir, ggf nach Umschreiben, annehmen duerfen, dass in der Herleitung von Theta |- tau1 <: tau2 die linke Praemisse einer Instanz von TRANS niemals selbst unmittelbar durch TRANS gewonnen wurde. Kommt naemlich in der Herleitung das Muster Phi |- alpha1 <: alpha2 Phi |- alpha2 <: alpha3 -------------------------------------------------- Phi |- alpha1 <: alpha3 Phi |- alpha3 <: alpha4 ------------------------------------------------------------------------------- Phi |- alpha1 <: alpha4 vor, so ersetzen wir es durch Phi |- alpha2 <: alpha3 Phi |- alpha3 <: alpha4 -------------------------------------------------- Phi |- alpha1 <: alpha2 Phi |- alpha2 <: alpha4 ------------------------------------------------------------------------------- Phi |- alpha1 <: alpha4 Der Schnittrang einer Herleitung von Theta |- tau1 <: tau2 ist definiert als die Laenge des laengsten Typs, der in einer Instanz von TRANS eliminiert wird (also in den Praemissen, aber nicht in der Konklusion erscheint), wobei wir aber Instanzen von TRANS unmittelbar nach AX, also diejenigen, die durch die Regel VAR subsumiert werden, nicht mitrechnen. Wir schreiben |tau| fuer die Laenge von tau, die sich einfach als die Zahl der Typformer versteht, also |Top -> Top| = 3, |(Top->Top) -> Top| = 5 etc. Wir zeigen nun die Behauptung durch Induktion ueber den Schnittrang der gegebenen Herleitung und nachgeordneter Induktion ueber Herleitungen. Wir machen eine Fallunterscheidung nach der letzten Regel in der Herleitung von Theta |- tau1<:tau2. Fall TOP: Dann ist tau2=Top und wir erhalten Theta |-a tau1 <: tau2 mit TOP. Fall FUN: Dann ist tau1 = tau11->tau21 und tau2=tau12->tau22 und Theta |- tau12 <: tau11 und Theta |- tau21 <: tau22 mit kuerzeren Herleitungen von gleichem Schnittrang. Nach Induktionshypothese gilt dann Theta |-a tau12 <: tau11 und Theta |-a tau21 <: tau22 und Theta |-a tau1 <: tau2 mit Regel FUN. Fall ALL: Dann ist tau1=all X<:tau11.tau21 und tau2=all X<:tau12.tau22 und wie im letzten Fall bekommt man mit der Induktionshypothese Theta |-a tau12 <: tau11 und Theta,X<:tau12 |-a tau21 <: tau22. Es folgt Theta |- tau1 <: tau2 mit Regel ALL. Fall REFL: Man verwendet hier ein separat durch Induktion ueber den Typaufbau zu beweisendes Lemma: Falls Theta |- tau ok, so folgt Theta |-a tau <: tau. Fall AX: Man verwendet die Regel VAR und das eben erwaehnte Lemma. Fall TRANS: Wir haben dann Herleitungen Theta |- tau1 <: sigma und Theta |- sigma <: tau2. Wir betrachten zunaechst den Unterfall, wo tau1 eine Variable X ist. Die erste Herleitung kann nach der eingangs obdA gemachten Annahme nur mit REFL oder AX aufhoeren. Die Induktionshypothese angewandt auf die zweite Herleitung zusammen mit VAR liefert das Gewuenschte. Ansonsten liefert uns die Induktionshypothese Herleitungen Theta |-a tau1 <: sigma und Theta |-a sigma <: tau2. Wir machen jetzt eine weitere Fallunterscheidung gemaess der letzten Regeln, die in diesen beiden Herleitungen zur Anwendung kamen. Fall: FUN,FUN: Hier ist sigma = sigma1->sigma2, tau1=tau11->tau21, tau2=tau12->tau22 und wir haben Herleitungen Theta |-a sigma1 <: tau11 Theta |-a tau12 <: sigma1 Theta |-a tau21 <: sigma2 Theta |-a sigma2 <: tau22 Mit der Regel TRANS liefern diese wiederum Herleitungen Theta |- tau12 <: tau11 Theta |- tau21 <: tau22 von Schnittrang |sigma1|, bzw |sigma2|. Die Induktionshypothese laesst sich darauf anwenden und liefert Theta |-a tau12 <: tau11 Theta |-a tau21 <: tau22 Somit Theta |-a tau1 <: tau2 mit FUN wie gewuenscht. Fall ALL,ALL: Hier ist sigma = all X<:sigma1.sigma2, tau1=all X<:tau11.tau21, tau2=all X<:tau12.tau22 und wir haben Herleitungen Theta |-a sigma1 <: tau11 Theta |-a tau12 <: sigma1 (A) Theta,X<:sigma1 |-a tau21 <: sigma2 (B) Theta,X<:tau12 |-a sigma2 <: tau22 Wie im vorherigen Fall erhaelt man nun eine Herleitung Theta |- tau12 <: tau11 vom Schnittrang |sigma1|. Ausserdem erhaelt man aus den Herleitungen (A) und (B) eine Herleitung Theta,X<:tau12 |- tau21<:sigma2 vom Schnittrang <= |sigma1|. Formal muss man das als separates Lemma formulieren. Die Idee ist, bei jeder VAR Regel mit X in (B) die Herleitung (A) mit TRANS einzuspleissen. Unter Anwendung von TRANS erhaelt man nunmehr eine Herleitung Theta,X<:tau12 |- tau21 <: tau22 von Schnittrang <= max(|sigma1|, |sigma2|) < |sigma|. Somit laesst sich die Indutkionshypothese anwenden und liefert Theta,X<:tau12 |-a tau21 <: tau22 Man konkludiert mit der Regel ALL. Dies deckt alle Moeglichkeiten ab. QED. Algorithmisches Typechecking in FSUB: ------------------------------------- Zu gegebenen Kontexten und Term kann mithilfe der algorithmischen Typisierungsregeln ein Typ ausgerechnet werden (und dann evtl mit einem vorgegebenen verglichen werden) Das algorithmische Typisierungsurteli Theta;Gamma |-a e : tau ist induktiv definiert durch die Regeln T-TVAR, T-LAM, T-TLAM, T-TAPP, sowie die algorithmische Applikationsregel: Theta;Gamma |-a e1 : tau1->tau2 Theta;Gamma |-a e2 : tau1' Theta |-a tau1'<:tau1 --------------------------------------------------- T-APP-A Theta;Gamma |-a e1 e2 : tau2 Satz: Theta;Gamma |- e : tau genau dann, wenn ein Typ tau' existiert mit Theta;Gamma |-a e : tau' und Theta |- tau' <: tau. Unentscheidbarkeit von FSUB --------------------------- Die algorithmischen Subtypregeln sind syntaxgerichtet und erlauben einem eine Herleitung durch systematische Rueckwaertsanwendung aufzufinden, sofern eine existiert. Dennoch beinhalten sie noch kein Entscheidungsverfahren, da sich die Nichtexistenz einer Typherleitung sowohl durch "Steckenbleiben" (keine Regel ist anwendbar) wie auch durch Nichttermination der Suche kundtun kann. In vielen anderen Typsystemen kann man leicht einsehen, dass die Rueckwaertsanwendung der Typisierungsregeln immer terminiert; in FSUB ist das leider nicht so und --- wie von Pierce gezeigt --- kann es auch gar kein terminierendes Verfahren geben, da die Subtyprelation in FSUB unentscheidbar ist. Wir geben hier einen neuen Beweis der Unentscheidbarkeit durch Reduktion auf den Lambdakalkuel. Der originale Beweis von Pierce (Bounded Quantification is Undecidable) benutzt eine zweistufige Reduktion auf two-counter-machines. Definition: Man definiert, wann ein Typ tau positiv, bzw. negativ in einer Typvariablen X ist: *) X ist positiv in X *) Y und Top sind sowohl positiv als auch negativ in X (falls Y =/= X) *) tau1->tau2 ist positiv/negativ in X, falls tau1 negativ/positiv und tau2 positiv/negativ in X ist. *) all Y<:tau1.tau2 ist positiv/negativ in X, falls tau1 negativ/positiv und tau2 positiv/negativ in X ist. Lemma: Ist tau positiv in X und sigma positiv in Y, so ist tau[X:=sigma] positiv in Y. Analoges gilt fuer die anderen Vorzeichen (minus mal minus gibt plus!). Lemma: Ist tau positiv (negativ) in X und gilt Theta |- sigma1 <: sigma2 (Theta |- sigma2 <: sigma1) so folgt Theta |- tau[X:=sigma1] <: tau[X:=sigma2]. Lemma: Ist tau1 positiv in X und kommt X in tau3 ueberhaupt nicht vor, so gilt Theta |- all X<:Top.tau1 <: all X<:tau2.tau3 genau dann, wenn Theta |- tau1[X:=tau2] <: tau3. Beweis: Wenn Theta |- tau1[X:=tau2] <: tau3 so auch Theta,X<:tau2 |- tau1[X:=tau2] <: tau3 und mit AX, TRANS und vorigem Lemma Theta,X<:tau2 |- tau1 <: tau3, also Theta |- all X<:Top.tau1 <: all X<:tau2.tau3 mit ALL und TOP. Hat man umgekehrt Theta |- all X<:Top.tau1 <: all X<:tau2.tau3 so muss wegen der Aequivalenz von deklarativem und algorithmischem Subtyping auch Theta,X<:tau2 |- tau1 <: tau3 der Fall sein. Ersetzt man nun X durch tau2, so folgt die Behauptung (formal mit Substitutionslemma). Ab jetzt werden bis auf weiteres alle Subtypurteile im leeren Subtypkontext gefaellt, weswegen wir das Theta weglassen. Wir fuehren die folgenden Abkuerzungen ein: Definition: := all U<:tau1.tau2, wobei U eine frische Variable ist. 0 := all X<:Top.X 1 := ~0. Man beachte, dass negativ in X und positiv in Y ist. Lemma: Ist X positiv in tau, so gilt: all X.tau <: genau dann, wenn tau[X:=tau1] <: tau2 ~ <: 1 genau dann wenn tau1 <: tau2 Man kann jetzt versuchen, untypisierte Lambdaterme wie folgt zu codieren: \x.e := all x.e e1 e2 := ~> * := 1 (Durch Induktion zeigt man leicht, dass e positiv in x ist) Man hat nun in der Tat (\x.e) e' <: 1 genau dann wenn e[x:=e'] <: 1 und die algorithmische Beweisuche bei (\x.xx)(\x.xx) <: 1 terminiert nicht. Leider bleibt aber die Beweissuche bei einem Goal wie (\x\y.x y) * * <: 1 stecken und man kann aus diesem Grunde nicht zeigen, dass gilt (Falsche!) Behauptung: e <: 1 genau dann wenn whnf(e)=*. Strategie zur Reparatur: Versuche Stacks irgendwie so zu codieren, dass gilt: e <: S genau dann, wenn (e,S) ->* (*,[]) Man muss dann also erreichen, dass \x.e <: e'::S genau dann, wenn e[x:=e'] <: S e1 e2 <: S genau dann, wenn e1 <: e2 :: S Wir verwenden wiederholt das folgende Muster: Es komme X in tau1 nur negativ, in tau2 nur positiv vor. all X.~ <: genau dann, wenn tau1[X:=tau3] <: tau2[X:=tau3] Mit diesem Muster kann man also von der rechten Seite einen beliebigen Typ ueber X einlesen und dann ein neues (von X abhaengiges!) Subgoal auflegen. Dies legt die folgende Verfeinerung nahe: Codiere Stacks in einer noch naeher zu spezifizierenden Weise und versuche zu erreichen, dass e <: <[e1;...;en],1> genau dann wenn whnf(e e1 e2 ... en) = * Man muss dann erreichen, dass i) \x.e <: genau dann wenn e[x:=e'] <: ii) e1 e2 <: genau dann wenn e1 <: iii) * <: <[],1> ist wahr. Folgende Setzungen loesen dies (fast!!!): \x.e := all S.~ e1 e2 := all S.~> e::S := > [] := 1 * := <[],1> Das Problem mit dieser Setzung nehmen wir gleich vorweg: der Rumpf von \x.e, also ~ ist negativ in S, also lassen sich die Lemmas nicht anwenden. Tun wir fuer den Moment einmal so, als waere das nicht der Fall. Dann koennten wir rechnen: e1 e2 <: gdw all S.~> <: gdw e1 <: \x.e <: gdw ~ <: 1 gdw all x.e <: > gdw e[x:=e'] <: Wir lassen die restlichen Eigenschaften weg, da es so ja eh nicht funktioniert. Neben dem Problem, dass S negativ im Rumpf von \x.e vorkommt, haben wir auch noch das weitere Problem, dass e1 e2 nicht positiv in e2 ist, weswegen man hier nicht induktiv zeigen kann, dass e positiv in x ist. Gluecklicherweise koennen diese beiden Probleme gleichzeitig durch das Einstreuen von Negationen kuriert werden. Waere nur eines der beiden Probleme isoliert vorhanden, so wuerde es wirklich schwierig: Hier also die endgueltige Kodierung des Lambdakalkuels: e :: s ::= ~> /* positiv in e und s */ \x.e ::= all s.~<~~allx.e,~s> /* positiv in e, Rumpf positiv in s */ e1 e2 ::= all s.~> /* positiv in e1 e2, Rumpf positiv in s */ [] ::= 0 * ::= <[],1> Um nun formal aus dieser Codierung die Unentscheidbarkeit von FSUB folgern zu koennen, muessen wir noch ein bisschen genauer studieren, wie sich die Subtypurteile unter Reduktion verhalten. Falls sigma<:tau, so bezeichne h(sigma,tau) die Laenge der eindeutig bestimmten algorithmischen Herleitung. Lemma: Falls X positiv in tau vorkommt, und all X.tau <: so ist h(tau[X:=tau1], tau2) < h(all X.tau,). Beweis: Sei eine algorithmische Herleitung von all X.tau <: vorgegeben. Es gibt dann eine kuerzere Herleitung von X<:tau1 |- tau <: tau2 Aufgrund des nur positiven Vorkommens von X in tau kann diese Herleitung X nur in Form der Regel VAR, nicht aber der Regel REFL benutzen. Formal zeigt man das durch Indutkion ueber die Herleitung. Man erhaelt eine Herleitung von tau[X:=tau1] <: tau2 indem man die Instanzen von VAR mit X einfach streicht und ansonsten dieselben Regeln benutzt. Wiederum formal durch Induktion. Lemma: Wenn (e,S) -> (e',S'), so folgt e <: genau dann wenn e' <: Beweis: Durch Inspektion der Regeln. Lemma: * <: und \x.e <: <[],1> gelten nicht. Beweis: Nachrechnen. Lemma: Wenn (e,S) -> (e',S') und e <: so ist h(e,) > h(e',). Beweis: Durch Inspektion der Regeln unter Verwendung des obigen Lemmas. Satz: whnf(e) = * genau dann wenn e <: <[],1> Beweis: Wenn whnf(e)=* so gilt (e,[]) ->* (*,[]), also e <: <[],1> genau dann wenn * <: <[],1>. Das aber folgt mit REFL. Ist hingegen whnf(e) =/= *, so gilt entweder (e,[]) ->* (*,e1::S) fuer bestimmte e1 und S (e,[]) ->* (\x.e1,[]) fuer bestimmtes e1 oder es existiert eine unendliche Folge (e,S) -> (e1,S1) -> (e2,S2) -> (e3,S3) -> ... Im ersten Fall folgt, dass e <: <[],1> nicht der Fall ist, nachdem ja * <: nicht der Fall ist. Der zweite Fall ist analog. Im dritten Falle nimmt man an, dass e<:. Dann aber auch e1<: und e2<: etc pp und das mit echt fallendem h-Wert. Das kann auch nicht sein, da die h-Werte nicht ad infinitum absteigen koennen. APPENDIX: WHNF -------------- Wir betrachten folgende Variante des untypisierten Lambdakalkuels: e ::= x | e1 e2 | \x.e | * Die weak-head-normal-form eines geschlossenen Terme e ist induktiv wie folgt definiert: ----------- whnf(*) = * whnf(e1) = \x.e ---------------------------- whnf(e1 e2) = whnf(e[x:=e2]) whnf(e1) = e' und e' nicht von der Form \x.e -------------------------------------------- whnf(e1 e2) = e e2 Fakten: whnf ist eine partielle Funktion. Ist e ein geschlossener Lambdaterm, so hat e die beta eta Normalform *, genau dann, wenn whnf(e)=*. Es ist unentscheidbar, ob whnf(e)=* gilt. Man kann die rekursive Definition der whnf auch iterativ fassen: Eine Konfiguration ist ein Paar (e,S), sobei e ein geschlossener Lambdaterm ist und S eine Liste von geschlossenen Lambdatermen, der sogenannte Stack, ist Man definiert die Einschrittauswertung durch (e1 e2,S) -> (e1,e2::S) (\x.e,e1::S) -> (e[x:=e1],S) Es gilt: whnf(e e1 e2 e3 ... en) = e' genau dann wenn (e, [e1;e2;e3; ... ;en]) ->* (e',[]) Wir notieren Listen wie in OCAML: [] ist die leere Liste, e::s ist die Liste mit Kopf e und Rest s. Konkrete Listen koennen auch [a;b;c] geschrieben werden. Es gilt z.B.: d::[a;b;c] = [d;a;b;c].