Compilerbau Vorlesung

Wintersemester 2008, 09, 10, 11

Johannes Waldmann, HTWK Leipzig 30. Januar 2012

– Typeset by FoilTEX –

Einleitung

– Typeset by FoilTEX – 1

Beispiel

Eingabe (≈ Java):

{ int i;
float prod;
float [20] a;
float [20] b;
prod = 0;
i = 1;
do {
prod = prod
+ a[i]*b[i];
i = i+1;
} while (i <= 20);
}

Ausgabe (Drei-Adress-Code):

L1: prod = 0
L3: i = 1
L4: t1 = i * 8
     t2 = a [ t1 ]
     t3 = i * 8
     t4 = b [ t3 ]
     t5 = t2 * t4
     prod = prod + t5
L6: i = i + 1
L5: if i <= 20 goto L4
L2:

Inhalt

• Motivation, Hintergründe

• lexikalische und syntaktische Analyse (Kombinator-Parser)

• syntaxgesteuerte Übersetzung (Attributgrammatiken)

• Code-Erzeugung (+ Optimierungen)

• statische Typsysteme

• Laufzeitumgebungen

Sprachverarbeitung

• mit Compiler:

– Quellprogramm → Compiler → Zielprogramm

– Eingaben → Zielprogramm → Ausgaben

• mit Interpreter:

– Quellprogramm, Eingaben → Interpreter → Ausgaben • Mischform:

– Quellprogramm → Compiler → Zwischenprogramm

– Zwischenprogramm, Eingaben → virtuelle Maschine → Ausgaben

Compiler und andere Werkzeuge

• Quellprogramm

• Präprozessor → modifiziertes Quellprogramm

• Compiler → Assemblerprogramm

• Assembler → verschieblicher Maschinencode

• Linker, Bibliotheken → ausführbares Maschinenprogramm

Phasen eines Compilers

• Zeichenstrom

• lexikalische Analyse → Tokenstrom

• syntaktische Analyse → Syntaxbaum

• semantische Analyse → annotierter Syntaxbaum

• Zwischencode-Erzeugung → Zwischencode

• maschinenunabhängige Optimierungen → Zwischencode • Zielcode-Erzeugung → Zielcode

• maschinenabhängige Optimierungen → Zielcode

– Typeset by FoilTEX – 6

Methoden und Modelle

• lexikalische Analyse: reguläre Ausdrücke, endliche Automaten

• syntaktische Analyse: kontextfreie Grammatiken, Kellerautomaten

• semantische Analyse: Attributgrammatiken

• Code-Erzeugung: bei Registerzuordnung:

Graphenfärbung

Anwendungen von Techniken des Compilerbaus

• Implementierung höherer Programmiersprachen

• architekturspezifische Optimierungen (Parallelisierung, Speicherhierarchien)

• Entwurf neuer Architekturen (RISC, spezielle Hardware)

• Programm-Übersetzungen (Binär-Übersetzer, Hardwaresynthese, Datenbankanfragesprachen)

• Software-Werkzeuge

Literatur

• Franklyn Turbak, David Gifford, Mark Sheldon: Design Concepts in Programming Languages, MIT Press, 2008.

http://cs.wellesley.edu/~fturbak/

• Guy Steele, Gerald Sussman: Lambda: The Ultimate Imperative, MIT AI Lab Memo AIM-353, 1976

(the original ’lambda papers’,

http://library.readscheme.org/page1.html)

• Alfred V. Aho, Monica S. Lam, Ravi Sethi and Jeffrey D. Ullman: Compilers: Principles, Techniques, and Tools (2nd edition) Addison-Wesley, 2007,

http://dragonbook.stanford.edu/

Organisation

• pro Woche eine Vorlesung, eine Übung.

• Prüfungszulassung: regelmäßiges und erfolgreiches Bearbeiten von Übungsaufgaben

• Prüfung: Klausur (120 min, keine Hilfsmittel)

Beispiel: Interpreter (I)

arithmetische Ausdrücke:

data Exp = Const Integer
          | Plus Exp Exp | Times Exp Exp
     deriving ( Show )
ex1 :: Exp
ex1 = Times ( Plus ( Const 1 ) ( Const 2 ) ) ( Const 3 )
value :: Exp -> Integer
value x = case x of
     Const i -> i
     Plus x y -> value x + value y
     Times x y -> value x * value y

Beispiel: Interpreter (II)

lokale Variablen und Umgebungen:

data Exp = ...
          | Let String Exp Exp | Ref String
ex2 :: Exp
ex2 = Let "x" ( Const 3 )
      ( Times ( Ref "x" ) (Ref "x" ) )
type Env = ( String -> Integer )
value :: Env -> Exp -> Integer
value env x = case x of
     Ref n -> env n
     Let n x b -> value ( \ m ->
       if n == m then value env x else env m )  b
     Const i -> i
     Plus x y -> value env x + value env y
     Times x y -> value env x * value env y

Übung (Haskell)

• Wiederholung Haskell

– Interpreter/Compiler: ghci http://haskell.org/

– Funktionsaufruf nicht f(a,b,c+d), sondern

  f a b (c+d)

– Konstruktor beginnt mit Großbuchstabe und ist auch eine Funktion

• Wiederholung funktionale Programmierung/Entwurfsmuster

– rekursiver algebraischer Datentyp (ein Typ, mehrere Konstruktoren) (OO: Kompositum, ein Interface, mehrere Klassen)

– Typeset by FoilTEX – 13

– rekursive Funktion

• Wiederholung Pattern Matching:

– beginnt mit case ... of, dann Zweige

– jeder Zweig besteht aus Muster und Folge-Ausdruck

– falls das Muster paßt, werden die Mustervariablen gebunden und der Folge-Ausdruck auswertet

Übung (Interpreter)

• Benutzung:

– Beispiel für die Verdeckung von Namen bei geschachtelten Let

– Beispiel dafür, daß der definierte Name während seiner Definition nicht sichtbar ist

• Erweiterung:

Verzweigungen mit C-ähnlicher Semantik:

Bedingung ist arithmetischer Ausdruck, verwende 0 als Falsch und alles andere als Wahr.

data Exp = ...
          | If Exp Exp Exp

– Typeset by FoilTEX – 15

Umgebungen

Umgebung ist (partielle) Funktion von Name nach Wert

Realisierungen: type Env = String -> Int
import Data.Map ; type Env = Map String Int

Operationen:

• empty :: Env leere Umgebung

• lookup :: Env -> String -> Int

Notation: e(x)

• extend :: Env -> String -> Int -> Env

Notation: e[x/v] Spezifikation:

• e[x/v](x) = v, x ≠ y ⇒ e[x/v](y) = e(y)

– Typeset by FoilTEX – 16

Inferenz-Systeme

Motivation

• inferieren = ableiten

• Inferenzsystem I, Objekt O, Eigenschaft I ⊢ O (in I gibt es eine Ableitung für O)

• damit ist I eine Spezifikation einer Menge von Objekten • man ignoriert die Implementierung (= das Finden von

Ableitungen)

• Anwendungen im Compilerbau:

Auswertung von Programmen, Typisierung von Programmen

– Typeset by FoilTEX – 17

Definition

ein Inferenz-System I besteht aus

• Regeln (besteht aus Prämissen, Konklusion)

Schreibweise \frac{P_{1},...,P_{n}}{K}

• Axiomen (= Regeln ohne Prämissen) eine Ableitung für F bzgl. I ist ein Baum:

• jeder Knoten ist mit einer Formel beschriftet

• jeder Knoten (mit Vorgängern) entspricht Regel von I • Wurzel ist mit F beschriftet Schreibweise: I ⊢ F

– Typeset by FoilTEX – 18

Inferenz-Systeme (Beispiel 1)

• Grundbereich = Zahlenpaare ℤ × ℤ

• Axiom:

\overline{(13, 5)}

• Regel-Schemata:

\frac{(x, y)}{(x − y, y)}, \frac{(x, y)}{(x, y − x)}

kann man (1, 1) ableiten? (−1, 5)? (2, 4)?

Inferenz-Systeme (Beispiel 2)

• Grundbereich: Zeichenketten aus {0, 1}^{∗}

• Axiom:

\overline{01}

• Regel-Schemata (für jedes u, v):

\frac{0u, v0}{u1v}, \frac{1u, v1}{u0v}, \frac{u}{reverse(u)}

Leite 11001 ab. Wieviele Wörter der Länge k sind ableitbar?

Inferenz-Systeme (Beispiel 3)

• Grundbereich: endliche Folgen von ganzen Zahlen

• Axiome: jede konstante Folge (Bsp. [3, 3, 3, 3])

• Schlußregeln: – swap_{k}: \frac{[…, x_{k}, x_{k+1}, …]}{[…, x_{k+1} + 1, x_{k} − 1, …]} – rotate: \frac{[x_{1}, …, x_{n}]}{[x_{2}, …, x_{n}, x_{1}]}

Aufgaben: • Ableitungen für [5, 3, 1, 3], [7, 7, 1]

• jede Folge der Form [z, 0, …, 0] ist ableitbar

• Invarianten, [5, 3, 3] ist nicht ableitbar

praktische Realisierung: http://www.siteswap.org/

und HTWK-Hochschulsport

– Typeset by FoilTEX – 21

Inferenz von Werten

• Grundbereich: Aussagen der Form wert(p, z) mit p ∈ Exp , z ∈ ℤ

  data Exp = Const Integer
            | Plus Exp Exp
            | Times Exp Exp

• Axiome: wert(Const z, z)

• Regeln:

\frac{wert(X, a), wert(Y, b)}{wert(Plus X Y, a + b)}, \frac{wert(X, a), wert(Y, b)}{wert(Times X Y, a · b)}, …

Umgebungen

• Grundbereich: Aussagen der Form wert(E, p, z)

(in Umgebung E hat Programm p den Wert z)

Umgebungen konstruiert aus ∅ und E[v := p]

• Regeln für Operatoren \frac{wert(E, X, a), wert(E, Y, b)}{wert(E, Plus XY, a + b)}, …

• Regeln für Umgebungen

\overline{wert(E[v := b], v, b)}, \frac{wert(E, v′, b′)}{wert(E[v := b], v′, b′)} für v ≠ v′

• Regeln für Bindung: \frac{wert(E, X, b), wert(E[v := b], Y, c)}{wert(E, let v = X in Y, c)}

Aussagenlogische Resolution

Formel (A ∨ ¬B ∨ ¬C) ∧ (C ∨ D) in konjunktiver Normalform dargestellt als {{A, ¬B, ¬C}, {C, D}} (Formel = Menge von Klauseln, Klausel = Menge von Literalen, Literal = Variable oder negierte Variable) folgendes Inferenzsystem heißt Resolution:

• Axiome: Klauselmenge einer Formel,

• Regel:

– Prämissen: Klauseln K_{1}, K_{2} mit v ∈ K_{1}, ¬v ∈ K_{2}

– Konklusion: (K_{1} \ {v}) ∪ (K_{2} \ {¬v})

Resolution (Eigenschaften)

die Formel (Klauselmenge) ist nicht erfüllbar ⟺ die leere Klausel ist durch Resolution ableitbar. Beweispläne:

• ⇒ : Gegeben ist die nicht erfüllbare Formel. Gesucht ist eine Ableitung für die leere Klausel. Methode: Induktion nach Anzahl der in der Formel vorkommenden Variablen.

• ⇐ : Gegeben ist die Ableitung der leeren Klausel. Zu zeigen ist die Nichterfüllbarkeit der Formel. Methode: Induktion nach Höhe des Ableitungsbaumes.

Semantische Bereiche

bisher: Wert eines Ausdrucks ist Zahl. jetzt erweitern (Motivation: if-then-else mit richtigem Typ):

data Val = ValInt Int
          | ValBool Bool

Dann brauchen wir auch

• data Val = ... | ValErr String

• vernünftige Notation (Kombinatoren) zur Einsparung von Fallunterscheidungen bei Verkettung von Rechnungen

  with_int  :: Val -> (Int  -> Val) -> Val

Continuations

Programmablauf-Abstraktion durch Continuations: Definition:

with_int  :: Val -> (Int  -> Val) -> Val
with_int v k = case v of
     ValInt i -> k i
     _-> ValErr "expected ValInt"

Benutzung:

value env x = case x of
     Plus l r ->
         with_int ( value env l ) $ \ i ->
         with_int ( value env r ) $ \ j ->
         ValInt ( i + j )

Aufgabe: if/then/else mit with_bool

– Typeset by FoilTEX – 27

Unterprogramme

Beispiele

• in verschiedenen Prog.-Sprachen gibt es verschiedene Formen von Unterprogrammen:

Prozedur, sog. Funktion, Methode, Operator, Delegate, anonymes Unterprogramm

• allgemeinstes Modell: Kalkül der anonymen Funktionen (Lambda-Kalkül),

Interpreter mit Funktionen

abstrakte Syntax:

data Exp = ...
  | Abs { formal :: Name , body :: Exp }
  | App { rator  :: Exp  , rand :: Exp }

konkrete Syntax (Beispiel):

let { f = \ x -> x * x }  in  f (f 3)

Semantik

erweitere den Bereich der Werte:

data Val = ... | ValFun ( Value -> Value )

erweitere Interpreter:

value :: Env -> Exp -> Val
value env x = case x of
     ...
     Abs { } ->
     App { } ->

mit Hilfsfunktion

with_fun :: Val -> ...

Testfall (1)

let { x = 4 }
in  let { f = \ y -> x * y }
     in  let { x = 5 }
         in  f x

Closures

bisher:

eval env x = case x of ...
  Abs n b -> ValFun $ \ v ->
     eval (extend env n v) b
  App f a ->
     with_fun ( eval env f ) $ \ g ->
     with_val ( eval env a ) $ \ v -> g v

alternativ: die Umgebung von Abs in die Zukunft transportieren:

eval env x = case x of ...
  Abs n b -> ValClos env n b
  App f a -> ...

Der Lambda-Kalkül

(Alonzo Church, 1936) Syntax:

• Variablen x, y, …

• Applikationen xx, (λx.xx)y

• Abstraktionen λx.xx, λx.(λy.x) Begriffe: freie Variablen (FV), gebundene Variablen (BV),

Small-Step-Semantik des Lambda-Kalküls

Basis-Operation ist A[x/B]: ersetze jedes freie Vorkommen von x in A durch B

• β-Konversion:

(λx.A)B →_{β} A[x/B]

wobei FV(B) disjunkt zu BV(A)

• α-Konversion: gebundene Umbenennung (λx.A) →_{α} (λy.A[x/y])

… und Abschluß unter Kontext (Inferenz-System?) Bemerkungen:

• warum ist die Bedingung bei →_{β} nötig? (Beispiele)

– Typeset by FoilTEX – 34

Mehrstellige Funktionen

… simulieren durch einstellige:

• Abstraktion: λxyz.B := λx.λy.λz.B

• Applikation: fP QR := ((fP)Q)R weiterer syntactic sugar:

let { f x =         A } in B
let { f   = \ x -> A } in B

Let und Lambda

• let { x = A } in Q

kann übersetzt werden in

  (\ x -> Q) A
• let { x = a , y = b } in Q

wird übersetzt in …

• beachte: das ist nicht das let aus Haskell

Rekursion?

• Das geht nicht, und soll auch nicht gehen:

let { x = 1 + x } in x

• aber das hätten wir doch gern:

let { f = \ x -> if x > 0
                   then x * f (x -1) else 1
     } in  f 5

(nächste Woche)

• aber auch mit nicht rekursiven Funktionen kann man interessante Programme schreiben:

– Typeset by FoilTEX – 37

Testfall (2)

let { t f x = f (f x) }
in  let { s x = x + 1 }
     in  t t t t s 0

• auf dem Papier den Wert bestimmen

• mit Haskell ausrechnen

• mit selbstgebautem Interpreter ausrechnen

Fixpunkte

Motivation

Das geht bisher gar nicht:

let { f = \ x -> if x > 0
                   then x * f (x -1) else 1
     } in  f 5

(Bezeichner f ist nicht sichtbar) Lösung:

( rec f ( \ x -> if x > 0
                   then x * f (x -1) else 1 )) 5

mit neuem AST-Knotentyp rec

Rekursion

abstrakt:

data Exp = ...
          | Rec Name Exp

Semantik von Rec n b in Umgebung E ist der Fixpunkt der Funktion (vom Typ Val → Val)

λc.Semantik von b in E[n/c]

Existenz von Fixpunkten

Fixpunkt von f :: C → C ist x :: C mit fx = x. Existenz? Eindeutigkeit? Konstruktion? Satz: Wenn C pointed CPO und f stetig, dann besitzt f genau einen kleinsten Fixpunkt. Begriffe:

• CPO = complete partial order = vollständige Halbordnung

• complete = jede monotone Folge besitzt Supremum (= kleinste obere Schranke)

• pointed: C hat kleinstes Element ⊥

• stetig: f(sup x⃗) = sup f⃗(x)

Dann fix(f) = sup[⊥, f(⊥), f^{2}(⊥), …]

– Typeset by FoilTEX – 41

Funktionen als CPO

• partielle Funktionen C = (B → B)

• Bereich B ∪ ⊥ geordnet durch ∀x ∈ B : ⊥ < x

• C geordnet durch f ≤ g ⟺ ∀x ∈ B : f(x) ≤ g(x),

• d. h. g ist Verfeinerung von f

• Das Bottom-Element von C ist die überall undefinierte Funktion.

Funktionen als CPO, Beispiel

Wert von

rec f ( \ x -> if (x==0) then 1
                 else x * f (x - 1) )

ist Fixpunkt der Funktion F =

\ f -> ( \ x -> if (x==0) then 1
                  else x * f (x - 1) )

Iterative Berechnung des Fixpunktes:

⊥ = ∅ überall undefiniert
F ⊥ = {(0, 1)} sonst ⊥
F (F ⊥) = {(0, 1), (1, 1)} sonst ⊥
F^{3}⊥ = {(0, 1), (1, 1), (2, 2)} sonst ⊥

Rechnen im Lambda-Kalkül

Daten als Funktionen

Simulation von Daten (Tupel) durch Funktionen (Lambda-Ausdrücke):

• Konstruktor: ⟨D_{1}, …, D_{k}⟩ ⇒ λs.sD_{1} … D_{k}

• Selektoren: s_{i} ⇒ λt.t(λd_{1} … d_{k}.d_{i}) dann gilt s_{i}⟨D_{1}, …, D_{k}⟩ →_{β}^{∗} D_{i} Anwendungen:

• Auflösung simultaner Rekursion

• Modellierung von Zahlen

– Typeset by FoilTEX – 44

Lambda-Kalkül als universelles Modell

• Wahrheitswerte:

True = λxy.x, False = λxy.y (damit läßt sich if-then-else leicht aufschreiben)

• natürliche Zahlen:

0 = λx.x; (n + 1) = ⟨False, n⟩ (damit kann man leicht x > 0 testen)

• Rekursion?

Fixpunkt-Kombinatoren

• Definition: Y := λf.((λx.f(xx))(λx.f(xx)))

• Satz: Y f ist Fixpunkt von f

• d.h. Y ist Fixpunkt-Kombinator

• Beweis: vergleiche (Y f) und f(Y f) wir benutzen eine Variante des Y: Y′ = λf.(λx.f(λy.xxy))(λx.f(λy.xxy))), weil sonst die Aufrufe (xx) nicht halten würden. Ü: weitere Fixpunktkombinatoren, Θ = (λxy.(y(xxy)))(λxy.(y(xxy)))

– Typeset by FoilTEX – 46

Lambda-Berechenbarkeit

Satz: (Church, Turing)

Menge der Turing-berechenbaren Funktionen (Zahlen als Wörter auf Band)

= Menge der while-berechenbaren Funktionen

(Zahlen als Registerinhalte) = Menge der Lambda-berechenbaren Funktionen

(Zahlen als Lambda-Ausdrücke)

Übung Fixpunkte

• Fixpunkt der Folge F^{k}(⊥) für

F h = \ x -> if x > 23 then x - 11
               else h (h (x + 14))

• Fixpunkt der Folge F^{k}(⊥) für

F h = \ x -> if x > 10 then x + 11
               else h (2 * x - 8)

• Turing-Fixpunkt-Kombinator mit Lambda-Calculator

http:
//joerg.endrullis.de/lambdaCalculator/

– Typeset by FoilTEX – 48

• Tupel-Konstruktor und Selektoren als Ausdrücke im Interpreter

• gegenseitige Rekursion (f, g) als Fixpunkt (Rec) einer geeigneten Funktion (benutzt Tupel)

• Hausaufgabe: vorige Aufgabe (im Interpreter) ohne Rec, sondern mit einem Fixpunkt-Kombinator

letrec

Beispiel (aus: D. Hofstadter, GEB)

letrec { f = \ x -> if x == 0 then 1
                       else x - g(f(x-1))
        , g = \ x -> if x == 0 then 0
                       else x - f(g(x-1))
} in f 15

Bastelaufgabe: für welche x gilt f(x) ≠ g(x)? AST-Knoten:

data Exp = ... | LetRec [(Name, Exp)] Exp

weitere Beispiele:

letrec { x = 3 + 4 , y = x * x } in x - y
letrec { f = \ x -> .. f (x-1) } in f 3

letrec nach rec

mithilfe der Lambda-Ausdrücke für select und tuple

LetRec [(n1,x1), .. (nk,xk)] y
=> ( rec t
       ( let n1 = select1 t
              ...
              nk = selectk t
         in  tuple x1 .. xk ) )
   ( \ n1 .. nk -> y )

Zustand/Speicher

Motivation

bisherige Programme sind nebenwirkungsfrei, das ist nicht immer erwünscht:

• direktes Rechnen auf von-Neumann-Maschine:

Änderungen im Hauptspeicher

• direkte Modellierung von Prozessen mit Zustandsänderungen ((endl.) Automaten)

Dazu muß semantischer Bereich geändert werden.

• bisher: Val, jetzt: State -> (State, Val)

Semantik von (Teil-)Programmen ist Zustandsänderung.

– Typeset by FoilTEX – 52

Speicher

Modellierung:

import qualified Data.Map as M
newtype Addr = Addr Int
type Store = M.Map Addr Val
newtype Action a =
     Action ( Store -> ( Store, a ))

spezifische Aktionen:

new :: Val -> Action Addr
get :: Addr -> Action Val
put :: Addr -> Val -> Action ()

Aktion ausführen, Resultat liefern:

run :: Store -> Action a -> a

Auswertung von Ausdrücken

Ausdrücke (mit Nebenwirkungen):

date Exp = ...
   | New Exp | Get Exp | Put Exp Exp

Resultattyp des Interpreters ändern:

value     :: Env -> Exp ->         Val
evaluate :: Env -> Exp -> Action Val

semantischen Bereich erweitern:

data Val = ...
     | ValAddr Addr
     | ValFun ( Val -> Action Val )

Aufruf des Interpreters:

run Store.empty $ evaluate undefined $ ...

Änderung der Hilfsfunktionen

bisher:

with_int :: Val -> ( Int -> Val ) -> Val
with_int v k = case v of
     ValInt i -> k i
     v -> ValErr "ValInt expected"

jetzt:

with_int :: Action Val
  -> ( Int -> Action Val ) -> Action Val
with_int m k = m >>= \ v -> case v of ...

Hauptprogramm muß kaum geändert werden (!)

Speicher-Aktionen als Monade

generische Aktionen/Verknüpfungen:

• nichts tun (return), • nacheinander (bind, >>=)

class Monad m where
  return :: a -> m a
  (>>=) :: m a
         -> (a -> m b) -- Continuation
         -> m b
instance Monad Action where
  return x = Action $ \ s -> ( s, x )
  Action a >>= f = Action $ \ s -> ...

Rekursion

… wird benötigt für Wiederholungen (Schleifen). mehrere Möglichkeiten zur Realisierung

• mit Fixpunkt-Kombinator

• semantisch (in der Gastsprache des Interpreters)

• (neu:) operational unter Benutzung des Speichers

Rekursion (operational)

Idee: eine Speicherstelle anlegen und als Vorwärtsreferenz auf das Resultat der Rekursion benutzen

evaluate env x = case x of ...
Rec n ( Abs x b ) ->
new ( ValErr "Rec" ) >>= \ a ->
with ( evaluate
          ( extend env n ... )
          ( Abs x ... ) ) $ \ v ->
put a v >>= \ () ->
return v

Rekursion (semantisch)

bisher:

fix :: ( a -> a ) -> a
fix f = f ( fix f )

jetzt:

import Control.Monad.Fix
class MonadFix m where
     mfix :: ( a -> m a ) -> m a
instance MonadFix Action where
mfix f = Action $ \ s0 ->
     let Action a = f v
         ( s1, v ) = a s0
     in  ( s1, v )

– Typeset by FoilTEX – 59

Speicher—Übung

Code aus Vorlesung:

http://dfa.imn.htwk-leipzig.de/cgi-bin/
gitweb.cgi?p=ws11-cb.git
git clone git://dfa.imn.htwk-leipzig.de/srv/git/ws11-cb

Fakultät imperativ:

let { fak = \ n ->
         { a := new 1 ;
           while ( n > 0 )
              { a := a * n ; n := n - 1; }
           return a;
         }
     } in  fak 5

1. Schleife durch Rekursion ersetzen und Sequenz durch

let:
fak = let { a = new 1 }
       in  Rec f ( \ n -> ... )

2. Syntaxbaumtyp erweitern um Knoten für Sequenz und Schleife

Monaden

Die Konstruktorklasse Monad

Definition:

class Monad c where
     return  :: a -> c a
     ( >>= ) :: c a -> (a -> c b) -> c b

Benutzung der Methoden:

evaluate e l >>= \ a ->
evaluate e r >>= \ b ->
return ( a + b )

Do-Notation für Monaden

evaluate e l >>= \ a ->
     evaluate e r >>= \ b ->
         return ( a + b )

do-Notation (explizit geklammert):

do { a <- evaluate e l
   ; b <- evaluate e r
   ; return ( a + b )
   }

do-Notation (implizit geklammert):

do a <- evaluate e l
   b <- evaluate e r
   return ( a + b )

Haskell: implizite Klammerung nach let, do, case, where

– Typeset by FoilTEX – 63

Die Zustands-Monade

Implementierung:

data State s a = State ( s -> ( s, a ))
instance Monad ( State s ) where ...

Benutzung:

import Control.Monad.State
tick :: State Integer ()
tick = do c <- get ; put $ c + 1
evalState ( do tick ; tick ; get ) 0

List als Monade

instance Monad [] where
     return = \ x - > [x]
     m >>= f = case m of
         []      -> []
         x : xs -> f x ++ ( xs >>= f )
do a <- [ 1 .. 4 ]
   b <- [ 2 .. 3 ]
   return ( a * b )

Kombinator-Parser

Datentyp für Parser

data Parser c a =
      Parser ( [c] -> [ (a, [c]) ] )

• über Eingabestrom von Zeichen (Token) c,

• mit Resultattyp a,

• nichtdeterministisch (List).

Beispiel-Parser, Aufrufen mit:

parse :: Parser c a -> [c] -> [(a,[c])]
parse (Parser f) w = f w

Elementare Parser (I)

-- | das nächste Token
next :: Parser c c
next = Parser $ \ toks -> case toks of
     [] -> []
     ( t : ts ) -> [ ( t, ts ) ]
-- | das Ende des Tokenstroms
eof :: Parser c ()
eof = Parser $ \ toks -> case toks of
     [] -> [ ( (), [] ) ]
     _-> []
-- | niemals erfolgreich
reject :: Parser c a
reject = Parser $ \ toks -> []

Monadisches Verketten von Parsern

instance Monad ( Parser c ) where
     return x = Parser $ \ s ->
         return ( x, s )
     Parser f >>= g = Parser $ \ s -> do
         ( a, t ) <- f s
         let Parser h = g a
         h t

beachte: das return/do gehört zur List-Monade

p :: Parser c (c,c)
p = do x <- next ; y <- next ; return (x,y)

Elementare Parser (II)

satisfy :: ( c -> Bool ) -> Parser c c
satisfy p = do
     x <- next
     if p x then return x else reject
expect :: Eq c => c -> Parser c c
expect c = satisfy ( == c )
ziffer :: Parser Char Integer
ziffer = do
     c <- satisfy Data.Char.isDigit
     return $ fromIntegral
             $ fromEnum c - fromEnum '0'

Kombinatoren für Parser (I)

• Folge (and then) (ist >>= aus der Monade)

• Auswahl (or)

( <|> ) :: Parser c a -> Parser c a -> Parser c a
Parser f <|> Parser g = Parser $ \ s -> f s ++ g s

• Wiederholung (beliebig viele)

many, many1 :: Parser c a -> Parser c [a]
many p = many1 p <|> return []
many1 p = do x <- p; xs <- many p; return $ x : xs
zahl :: Parser Char Integer = do
  zs <- many1 ziffer
  return $ foldl ( \ a z -> 10*a+z ) 0 zs

– Typeset by FoilTEX – 70

Kombinator-Parser und Grammatiken

Grammatik mit Regeln S → aSbS, S → ϵ entspricht

s :: Parser Char ()
s =   do { expect 'a' ; s ; expect 'b' ; s }
  <|> return ()
Anwendung: exec "abab" $ do s ; eof

Robuste Parser-Bibliotheken

Designfragen:

• asymmetrisches <|>

• Nichtdeterminismus einschränken

• Fehlermeldungen (Quelltextposition) Beispiel: Parsec (Autor: Daan Leijen)

http://www.haskell.org/haskellwiki/Parsec

Asymmetrische Komposition

gemeinsam:

(<|>) :: Parser c a -> Parser c a
       -> Parser c a
Parser p <|> Parser q = Parser $ \ s -> ...

• symmetrisch: p s ++ q s

• asymmetrisch: if null p s then q s else p s

Anwendung: many liefert nur maximal mögliche Wiederholung (nicht auch alle kürzeren)

Nichtdeterminismus einschränken

• Nichtdeterminismus = Berechnungsbaum = Backtracking

• asymmetrisches p <|> q : probiere erst p, dann q

• häufiger Fall: p lehnt ”sofort“ ab

Festlegung (in Parsec): wenn p wenigstens ein Zeichen verbraucht, dann wird q nicht benutzt (d. h. p muß erfolgreich sein) Backtracking dann nur durch try p <|> q

Fehlermeldungen

• Fehler = Position im Eingabestrom, bei der es ”nicht weitergeht“

• und auch durch Backtracking keine Fortsetzung gefunden wird

• Fehlermeldung enthält:

– Position

– Inhalt (Zeichen) der Position

– Menge der Zeichen mit Fortsetzung

Pretty-Printing (I)

John Hughes’s and Simon Peyton Jones’s Pretty Printer Combinators Based on The Design of a Pretty-printing Library in Advanced Functional Programming, Johan Jeuring and Erik Meijer (eds), LNCS 925

http://hackage.haskell.org/packages/archive/pretty/
1.0.1.0/doc/html/Text-PrettyPrint-HughesPJ.html

Pretty-Printing (II)

• data Doc abstrakter Dokumententyp, repräsentiert Textblöcke

• Konstruktoren:

  text :: String -> Doc

• Kombinatoren:

  vcat        :: [ Doc ] -> Doc -- vertikal
  hcat, hsep :: [ Doc ] -> Doc -- horizontal
• Ausgabe: render :: Doc -> String

Ablaufsteuerung/Continuations

Definition

(alles nach: Turbak/Gifford Ch. 17.9) CPS-Transformation (continuation passing style):

• original: Funktion gibt Wert zurück

  f == (abs (x y) (let ( ... ) v))

• cps: Funktion erhält zusätzliches Argument, das ist eine Fortsetzung (continuation), die den Wert verarbeitet:

  f-cps == (abs (x y k) (let ( ... ) (k v))
aus g (f 3 2) wird f-cps 3 2 g-cps

– Typeset by FoilTEX – 78

Motivation

Funktionsaufrufe in CPS-Programm kehren nie zurück, können also als Sprünge implementiert werden!

CPS als einheitlicher Mechanismus für

• Linearisierung (sequentielle Anordnung von primitiven Operationen)

• Ablaufsteuerung (Schleifen, nicht lokale Sprünge)

• Unterprogramme (Übergabe von Argumenten und Resultat)

• Unterprogramme mit mehreren Resultaten

CPS für Linearisierung

(a + b) * (c + d) wird übersetzt (linearisiert) in

( \ top ->
   plus a b $ \ x ->
   plus c d $ \ y ->
   mal  x y top
) ( \ z -> z )
plus x y k = k (x + y)
mal  x y k = k (x * y)

später tatsächlich als Programmtransformation (Kompilation)

CPS für Resultat-Tupel

wie modelliert man Funktion mit mehreren Rückgabewerten?

• benutze Datentyp Tupel (Paar):

  f : A -> (B, C)

• benutze Continuation:

  f/cps : A -> (B -> C -> D) -> D

CPS/Tupel-Beispiel

erweiterter Euklidischer Algorithmus:

prop_egcd x y =
     let (p,q) = egcd x y
     in  (p*x + q*y) == gcd x y
egcd :: Integer -> Integer
      -> ( Integer, Integer )
egcd x y = if y == 0 then ???
             else let (d,m) = divMod x y
                       (p,q) = egcd y m
                  in  ???

vervollständige, übersetze in CPS

CPS für Ablaufsteuerung

Beispiel label/jump

1 + label exit (2 * (3 - (4 + jump exit 5)))

Vergleiche:

• label <name> deklariert Exception-Handler

• jump <name> springt zum Handler

Semantik für CPS

Semantik von Ausdruck x in Umgebung E ist Funktion von Continuation nach Wert (Action)

value(E, label L B) = \ k ->
  value (E[L/k], B) k
value (E, jump L B) = \ k ->
  value (E, L) $ \ k' ->
  value (E, B) k'

Beispiel 1:

value (E, label x x)
  = \ k -> value (E[x/k], x) k
  = \ k -> k k

Beispiel 2

value (E, jump (label x x)(label y y))
= \ k ->
  value (E, label x x) $ \ k' ->
  value (E, label y y) k'
= \ k ->
  value (E, label y y) (value (E, label x x))
= \ k -> ( \ k0 -> k0 k0 ) ( \ k1 -> k1 k1 )

Semantik

semantischer Bereich:

type Continuation a = a -> Action Val
date CPS a
   = CPS ( Continuation a -> Action Val )
evaluate :: Env -> Exp -> CPS Val

Plan:

• Syntax: Label, Jump, Parser

• Semantik:

 – Verkettung durch >>= aus instance Monad CPS

– Einbetten von Action Val durch lift

– evaluate für bestehende Sprache (CBV)

– evaluate für label und jump

– Typeset by FoilTEX – 86

CPS als Monade

feed :: CPS a -> ( a -> Action Val )
      -> Action Val
feed ( CPS s ) c = s c
feed ( s >>= f ) c =
     feed s ( \ x -> feed ( f x ) c )
feed ( return x ) c = c x
lift :: Action a -> CPS a

Übung CPS

• Parser für Label String Exp, Jump Exp Exp

• Continuations als Werte (von Argumenten und Resultaten von Unterprogrammen)

• Rekursion (bzw. Schleifen) mittels Label/Jump (und ohne Rec oder Fixpunkt-Kombinator)

• jump (label x x) (label y y)

Typen

Grundlagen

Typ = statische Semantik (Information über mögliches Programm-Verhalten, erhalten ohne Programm-Ausführung) formale Beschreibung:

• P: Menge der Ausdrücke (Programme)

• T: Menge der Typen

• Aussagen p :: t (für p ∈ P, t ∈ T)

– prüfen oder

– herleiten (inferieren)

Inferenzsystem für Typen (Syntax)

• Grundbereich: Aussagen der Form E ⊢ X : T (in Umgebung E hat Ausdruck X den Typ T)

• Menge der Typen:

– primitiv: Int, Bool

– zusammengesetzt:

∗ Funktion T_{1} → T_{2}

∗ Verweistyp Ref T

∗ Tupel (T_{1}, …, T_{n}), einschl. n = 0

• Umgebung bildet Namen auf Typen ab

Inferenzsystem für Typen (Semantik)

• Axiome f. Literale: E ⊢ Zahl-Literal: Int, …

• Regel für prim. Operationen: \frac{E ⊢ X : Int, E ⊢ Y : Int}{E ⊢ (X + Y) : Int}, …

• Abstraktion/Applikation: …

• Binden/Benutzen von Bindungen: … hierbei (vorläufige) Design-Entscheidungen:

• Typ eines Ausdrucks wird inferiert

• Typ eines Bezeichners wird …

– in Abstraktion: deklariert

– in Let: inferiert

– Typeset by FoilTEX – 91

Inferenz für Let

(alles ganz analog zu Auswertung von Ausdrücken)

• Regeln für Umgebungen

– E[v := t] ⊢ v : t

– \frac{E ⊢ v′ : t′}{E[v := t] ⊢ v′ : t′} für v ≠ v′

• Regeln für Bindung:

\frac{E ⊢ X : s, E[v := s] ⊢ Y : t}{E ⊢ let v = X in Y : t}

Applikation und Abstraktion

• Applikation:

\frac{E ⊢ F : T_{1} → T_{2}, E ⊢ A : T_{1}}{E ⊢ (F A) : T_{2}}

vergleiche mit modus ponens

• Abstraktion (mit deklariertem Typ der Variablen)

\frac{E[v := T_{1}] ⊢ X : T_{2}}{E ⊢ (λ(v :: T_{1})X) : T_{1} → T_{2}}

Eigenschaften des Typsystems

Wir haben hier den einfach getypten Lambda-Kalkül nachgebaut:

• jedes Programm hat höchstens einen Typ

• nicht jedes Programm hat einen Typ.

Der Y -Kombinator (λx.xx)(λx.xx) hat keinen Typ

• jedes getypte Programm terminiert

(Begründung: bei jeder Applikation F A ist der Typ von F A kleiner als der Typ von F)

Übung: typisiere t t t t succ 0 mit

succ = \ x -> x + 1 und t = \ f x -> f (f x)

– Typeset by FoilTEX – 94

Polymorphe Typen

Motivation

ungetypt:

let { t = \ f x -> f (f x)
     ; s = \ x -> x + 1
     } in (t t s) 0

einfach getypt nur so möglich:

let { t2 = \ (f :: (Int -> Int) -> (Int -> Int))
               (x :: Int -> Int) -> f (f x)
     ; t1 = \ (f :: Int -> Int) (x :: Int) -> f (f x)
     ; s = \ (x :: Int) -> x + 1
     } in (t2 t1 s) 0

wie besser?

Typ-Argumente (Beispiel)

Typ-Abstraktion, Typ-Applikation:

let { t = \ ( t :: Type )
          ->  \ ( f :: t -> t ) ->
                 \ ( x :: t ) ->
                         f ( f x )
     ; s = \ ( x :: Int ) -> x + 1
     }
in  (((t [Int -> Int]) (t [Int])) s) 0

zur Laufzeit werden die Abstraktionen und Typ-Applikationen ignoriert

Typ-Argumente (Regeln)

neuer Typ-Ausdruck ∀t.T, Inferenz-Regeln:

• Typ-Abstraktion: erzeugt parametrischen Typ

\frac{E ⊢ …}{E ⊢ λ(t :: Type → X : …}

• Typ-Applikation: instantiiert param. Typ

\frac{E ⊢ F : …}{E ⊢ F [T_{2}] : …}

Ü: Vergleich Typ-Applikation mit expliziter Instantiierung von polymorphen Methoden in C#

Inferenz allgemeingültige Formeln

Grundbereich: aussagenlogische Formeln (mit Variablen und Implikation) Axiom-Schemata: \overline{X → (Y → X)}, \overline{(X → (Y → Z)) → ((X → Y) → (X → Z))}

Regel-Schema (modus ponens): \frac{X → Y, X}{Y} Beobachtungen/Fragen:

• Übung (autotool): Leite p → p ab.

• (Korrektheit): jede ableitbare Formel ist allgemeingültig

• (Vollständigkeit): sind alle allgemeingültigen Formeln (in dieser Signatur) ableitbar?

Typen und Daten

• bisher: Funktionen von Daten nach Daten

\ (x :: Int) -> x + 1

• heute: Funktionen von Typ nach Daten

\ (t :: Type) -> \ (x :: t) -> x

• Funktionen von Typ nach Typ (ML, Haskell, Java, C#)

\ (t :: Type) -> List t

• Funktionen von Daten nach Typ (dependent types)

\ (t :: Typ) (n :: Int) -> Array t n

Sprachen: Cayenne, Coq, Agda Eigenschaften: Typkorrektheit i. A. nicht entscheidbar, d. h. Programmierer muß Beweis hinschreiben.

Typ-Rekonstruktion

Motivation

Bisher: Typ-Deklarationspflicht für Variablen in Lambda. scheint sachlich nicht nötig. In vielen Beispielen kann man die Typen einfach rekonstruieren:

let { t = \ f x -> f (f x)
     ; s = \ x -> x + 1
     } in t s 0

Diesen Vorgang automatisieren! (zunächst für einfaches (nicht polymorphes) Typsystem)

Realisierung mit Constraints

Inferenz für Aussagen der Form E ⊢ X : (T, C)

• E: Umgebung (Name → Typ)

• X: Ausdruck (Exp)

• T: Typ

• C: Menge von Typ-Constraints wobei

• Menge der Typen T erweitert um Variablen

• Constraint: Paar von Typen (T_{1}, T_{2})

• Lösung eines Constraints: Substitution σ mit T_{1}σ = T_{2}σ

– Typeset by FoilTEX – 101

Inferenzregeln f. Rekonstruktion (Plan)

Plan:

• Aussage E ⊢ X : (T, C) ableiten,

• dann C lösen (allgemeinsten Unifikator σ bestimmen)

• dann ist T σ der (allgemeinste) Typ von X (in Umgebung E)

Für (fast) jeden Teilausdruck eine eigene (”frische“) Typvariable ansetzen, Beziehungen zwischen Typen durch Constraints ausdrücken. Inferenzregeln? Implementierung? — Testfall:

\ f g x y ->
   if (f x y) then (x+1) else (g (f x True))

– Typeset by FoilTEX – 102

Inferenzregeln f. Rekonstrukion

• primitive Operationen (Beispiel)

\frac{E ⊢ X_{1} : (T_{1}, C_{1}), E ⊢ X_{2} : (T_{2}, C_{2})}{E ⊢ X_{1} + X_{2} : (Int, \{T_{1} = Int, T_{2} = Int\} ∪ C_{1} ∪ C_{2})}

• Applikation

\frac{E ⊢ F : (T_{1}, C_{1}), E ⊢ A : (T_{2}, C_{2})}{E ⊢ (F A) : …}

• Abstraktion

\frac{…}{E ⊢ λx.B : …}

• (Ü) Konstanten, Variablen, if/then/else

– Typeset by FoilTEX – 103

Substitutionen (Definition)

• Signatur Σ = Σ_{0} ∪ … Σ_{k},

• Term(Σ, V) ist kleinste Menge T mit V ⊆ T und ∀0 ≤ i ≤ k, f ∈ Σ_{i}, t_{1} ∈ T, …, t_{i} ∈ T : f(t_{1}, …, t_{i}) ∈ T. (hier Anwendung für Terme, die Typen beschreiben)

• Substitution: partielle Abbildung σ : V → Term(Σ, V), Definitionsbereich: dom σ, Bildbereich: img σ.

• Substitution σ auf Term t anwenden: tσ

• σ heißt pur, wenn kein v ∈ dom σ als Teilterm in img σ vorkommt.

– Typeset by FoilTEX – 104

Substitutionen: Produkt

Produkt von Substitutionen: t(σ_{1} ∘ σ_{2}) = (tσ_{1})σ_{2} Beispiel 1: σ_{1} = {X ↦ Y }, σ_{2} = {Y ↦ a}, σ_{1} ∘ σ_{2} = {X ↦ a, Y ↦ a}. Beispiel 2 (nachrechnen!): σ_{1} = {X ↦ Y }, σ_{2} = {Y ↦ X}, σ_{1} ∘ σ_{2} = σ_{2} Eigenschaften:

• σ pur ⇒ σ idempotent: σ ∘ σ = σ

• σ_{1} pur ∧ σ_{2} pur impliziert nicht σ_{1} ∘ σ_{2} pur Implementierung:

import Data.Map
type Substitution = Map Identifier Term
times :: Substitution -> Substitution -> Substition

– Typeset by FoilTEX – 105

Substitutionen: Ordnung

Substitution σ_{1} ist allgemeiner als Substitution σ_{2}: σ_{1}< ∼σ_{2} ⟺ ∃τ : σ_{1} ∘ τ = σ_{2} Beispiele:

• {X ↦ Y }< ∼{X ↦ a, Y ↦ a},

• {X ↦ Y }< ∼{Y ↦ X},

• {Y ↦ X}< ∼{X ↦ Y }. Eigenschaften

• Relation < ∼ ist Prä-Ordnung (…, …, aber nicht …)

• Die durch < ∼ erzeugte Äquivalenzrelation ist die …

– Typeset by FoilTEX – 106

Unifikation—Definition

Unifikationsproblem

• Eingabe: Terme t_{1}, t_{2} ∈ Term(Σ, V)

• Ausgabe: ein allgemeinster Unifikator (mgu): Substitution σ mit t_{1}σ = t_{2}σ.

(allgemeinst: infimum bzgl. < ∼) Satz: jedes Unifikationsproblem ist

• entweder gar nicht

• oder bis auf Umbenennung eindeutig lösbar.

Unifikation—Algorithmus

mgu(s, t) nach Fallunterscheidung

• s ist Variable: …

• t ist Variable: symmetrisch

• s = (s_{1} → s_{2}) und t = (t_{1} → t_{2}): …

mgu :: Term -> Term -> Maybe Substitution

Unifikation—Komplexität

Bemerkungen:

• gegebene Implementierung ist korrekt, übersichtlich, aber nicht effizient,

• (Ü) es gibt Unif.-Probl. mit exponentiell großer Lösung,

• eine komprimierte Darstellung davon kann man aber in Polynomialzeit ausrechnen.

Rekonstruktion polymorpher Typen

… ist im Allgemeinen nicht möglich: Joe Wells: Typability and Type Checking in System F Are Equivalent and Undecidable, Annals of Pure and Applied

Logic 98 (1998) 111–156, http://citeseerx.ist.
psu.edu/viewdoc/summary?doi=10.1.1.6.6483

übliche Einschränkung (ML, Haskell): let-Polymorphismus: Typ-Abstraktionen nur für let-gebundene Bezeichner:

let { t = \ f x -> f(f x) ; s = \ x -> x+1 }
in t t s 0

folgendes ist dann nicht typisierbar (t ist monomorph):

( \ t -> let { s = \ x -> x+1 } in t t s 0 )
  ( \ f x -> f (f x) )

Implementierung

let-Polymorphie, Hindley/Damas/Milner

• Inferenzsystem ähnlich zu Rekonstruktion monomorpher Typen mit Aussagen der Form E ⊢ X : (T, C)

• Umgebung E ist jetzt partielle Abbildung von Name nach Typschema (nicht wie bisher: nach Typ).

• Bei Typinferenz für let-gebundene Bezeichner wird über die freien Typvariablen generalisiert.

• Dazu Teil-Constraint-Systeme lokal lösen.

Beispiel

let { c = ... }
in let { g = \ f x -> f (if b c x) } in ..

Plan für Compiler

Transformationen/Ziel

• continuation passing (Programmablauf explizit)

• closure conversion (alle Umgebungen explizit)

• lifting (alle Unterprogramme global)

• Registervergabe (alle Argumente in Registern) Ziel: maschinen(nahes) Programm mit

• globalen (Register-)Variablen (keine lokalen)

• Sprüngen (kein return)

• automatischer Speicherbereinigung

– Typeset by FoilTEX – 112

CPS-Transformation

CPS-Transformation: Spezifikation

(als Schritt im Compiler)

• Eingabe: Ausdruck X, Ausgabe: Ausdruck Y

• Semantik: X ≡ Y (λv.v)

• Syntax:

– X ∈ Exp (fast) beliebig,

– Y ∈ Exp/CPSstark eingeschränkt:

∗ keine geschachtelten Applikationen

∗ Argumente von Applikationen und Operationen (+, ∗, >) sind Variablen oder Literale

CPS-Transformation: Zielsyntax

Exp_CPS ==> App Id Exp_Value^*
     | If Exp_Value Exp_CPS Exp_CPS
     | Let Id Exp_Letable Exp_CPS
Exp_Value ==> Literal | Identifier
Exp_Letable ==> Literal
     | Abs Id^* Exp_CPS
     | Exp_Value Op Exp_Value

Übung: Übersetze

(0 - (b * b)) + (4 * (a * c))

Beispiel

(0 - (b * b)) + (4 * (a * c))
==>
let { t.3 = b * b } in
  let { t.2 = 0 - t.3 } in
     let { t.5 = a * c } in
        let { t.4 = 4 * t.5 } in
          let { t.1 = t.2 + t.4 } in
              t.1

Transformation f. Applikation

CPS[ (app f a1 ... an) ] =
(abs (k)
  (app CPS[f] (abs (i_0)
     (app CPS[a1] (abs (i_1)
       ...
         (app CPS[an] (abs (i_n)
             (app i_0 i_1 ... i_n k)))...)))))

dabei sind k, i_0, .. i_n frische Namen (= die im gesamten Ausdruck nicht vorkommen)

Ü: ähnlich für Primop (Unterschied?)

Transformation f. Abstraktion

CPS[ (abs (i_1 ... i_n) b) ] =
(abs (k)
  (let ((i (abs (i_1 .. i_n c)
                (app CPS[b] c))))
     (app k i)))

Ü: Transformation für let

Namen

Bei der Übersetzung werden ”frische“ Variablennamen benötigt (= die im Eingangsprogramm nicht vorkommen).

import Control.Monad.State
data State s a = State ( s -> ( a, s ) )
get :: State s s ; put :: s -> State ()
fresh :: State Int String
fresh = do
     k <- get ; put (k+1)
     return $ "f." ++ show k
type Transform a = State Int a
cps :: Exp -> Transform Exp

Vereinfachungen

um geforderte Syntax (ExpCPS) zu erreichen:

• implicit-let

(app (abs (i_1 .. i_n) b) a_1 .. a_n)
==>
(let ((i_1 a_1)) ( .. (let ((i_n a_n)) b)..))

Umbenennungen von Variablen entfernen:

• copy-prop

(let ((i i')) b) ==> b [i:=i']

aber kein allgemeines Inlining

– Typeset by FoilTEX – 119

Teilweise Auswertung

• Interpreter (bisher): komplette Auswertung (Continuations sind Funktionen, werden angewendet)

• CPS-Transformator (heute): gar keine Auswertung, (Continuations sind Ausdrücke)

• gemischter Transformator: benutzt sowohl

– Continuations als Ausdrücke (der Zielsprache)

– als auch Continuations als Funktionen (der Gastsprache) (compile time evaluation, partial evaluation)

Partial Evaluation

• bisher:

transform  :: Exp -> State ... Exp
transform x = case x of ...
 ConstInt i -> do
  k<-fresh; return $ Abs k (app (Ref k) x)

• jetzt:

type Cont = Exp -> State ... Exp
transform
     :: Exp -> ( Cont -> State ... Exp )
transform x k = case x of ...
   ConstInt i -> k x

Partial Evaluation (II)

CPS[ (app f a1 ... an) ] =
(m-abs (K)
  (m-app CPS[f] (m-abs (i_0)
       ...
         (m-app CPS[an] (m-abs (i_n)
   ???      (app i_0 i_1 ... i_n k)))...)))))

ändere letzte Zeile in

(let ((i (abs (temp) K[temp])))
      (app i_0 .. i_n i))

Erklärung CPS-Transformation

Spezifikation (Vorsicht, enthält Typfehler - welche?):

     eval env x           (\ y -> k2 (k1 y))
=?= eval env (cps x k1) k2

Wiederholung CPS-Interpreter:

type Cont = Val -> Action Val
eval :: Env -> Exp -> Cont -> Action Val
eval env x = \ k -> case x of
     ConstInt i -> ... ; Plus a b -> ...

CPS-Transformator:

type Cont = ExpValue -> Transform Exp
cps :: Exp -> Cont -> Transform Exp
cps x = \ m -> case x of
     ConstInt i -> ... ; Plus a b -> ...

– Typeset by FoilTEX – 123

Übung CPS-Transformation

• Transformationsregeln für Ref, App, Abs, Let nachvollziehen (im Vergleich zu CPS-Interpreter)

• Transformationsregeln für if/then/else, new/put/get hinzufügen

• anwenden auf eine rekursive Funktion (z. B. Fakultät),

wobei Rekursion durch Zeiger auf Abstraktion realisiert wird

Closure Conversion

Motivation

(Literatur: DCPL 17.10) — Beispiel:

let { linear = \ a -> \ x -> a * x + 1
     ; f = linear 2 ; g = linear 3
     }
in  f 4 * g 5

beachte nicht lokale Variablen: (\ x -> .. a .. )

• Semantik-Definition (Interpreter) benutzt Umgebung

• Transformation (closure conversion, environment conversion) (im Compiler) macht Umgebungen explizit.

Spezifikation

closure conversion:

• Eingabe: Programm P

• Ausgabe: äquivalentes Programm P′, bei dem alle Abstraktionen geschlossen sind

• zusätzlich: P in CPS ⇒ P′ in CPS geschlossen: alle Variablen sind lokal Ansatz:

• Werte der benötigten nicht lokalen Variablen ⇒ zusätzliche(s) Argument(e) der Abstraktion

• auch Applikationen entsprechend ändern

– Typeset by FoilTEX – 126

closure passing style

• Umgebung = Tupel der Werte der benötigten nicht lokalen Variablen

• Closure = Paar aus Code und Umgebung

realisiert als Tupel (Code, \underbrace{W_{1}, …, W_{n}}_{Umgebung})

\ x -> a * x + 1
==>
\ clo x ->
  let { a = nth clo 1 } in a * x + 1

Closure-Konstruktion? Komplette Übersetzung des Beispiels?

Transformation

CLC[ \ i_1 .. i_n -> b ] =
   (tuple ( \ clo i_1 .. i_n ->
              let { v_1 = nth 1 clo ; .. }
              in  CLC[b]
           ) v_1 .. )

wobei {v_{1}, …} = freie Variablen in (λi_{1} … i_{n} → b)

CLC[ (f a_1 .. a_n) ] =
  let { clo = CLC[f]
       ; code = nth 0 clo
  } in  code clo CLC[a_1] .. CLC[a_n]

• für alle anderen Fälle: strukturelle Rekursion

• zur Erhaltung der CPS-Form: Spezialfall bei let

Lifting

Spezifikation

(lambda) lifting:

• Eingabe: Programm P

• Ausgabe: äquivalentes Programm P′, bei dem alle Abstraktionen global sind

Motivation: in Maschinencode gibt es nur globale Sprungziele (CPS-Transformation: Unterprogramme kehren nie zurück ⇒ globale Sprünge)

Realisierung

nach closure conversion sind alle Abstraktionen geschlossen, diese müssen nur noch aufgesammelt und eindeutig benannt werden.

let { g1 = \ v1 .. vn -> b1
     ...
     ; gk = \ v1 .. vn -> bk
} in b

dann in b1, .., bk, b keine Abstraktionen gestattet

• Zustandsmonade zur Namenserzeugung (g_{1}, g_{2}, …)

• Ausgabemonade (WriterT) zum Aufsammeln

• g_{1}, …, g_{k} dürften nun sogar rekursiv sein (sich gegenseitig aufrufen)

– Typeset by FoilTEX – 130

Kombinatorische Logik

Motivation

• Lambda-Kalkül zur Modellierung von Abstraktion und Applikation,

wesentliches Merkmal: benutzerdefinierte Funktionen mit gebundene Variablen.

• Kombinatorische Logik ist ein Berechnungsmodell mit einer kleinen, fixierte Menge von (globalen) Funktionen,

diese heißen Kombinatoren.

Beispiele: S = λxyz.xz(yz), K = λxy.x

Beispiele

• vordefinierte Kombinatoren:

I = λx.x, K = λxy.x, S = λxyz.xz(yz) Ü: Berechne Normalform von SKKx, von SIIx

• weitere, z. B.

B = λxyz.x(yz), C = λxyz.xzy, J = λxyzw.xy(xwz) Ü: simuliere B und C durch I und J

Systematische Übersetzung

Spezifikation:

• Eingabe: geschlossener Lambda-Ausdruck P

• Ausgabe: äquivalenter Kombinator-Ausdruck [P] (Applikationen mit S, K, I; sonst keine Variablen und Lambdas)

benutzt [λx.A] = lift_{x}(A) mit Spezifikation: lift_{x}(A)x →^{∗} A • lift_{x}(y) = falls x = y dann I sonst Ky

• lift_{x}(AB) = S lift_{x}(A) lift_{x}(B)

• lift_{x}(λy.A) = lift_{x}(lift_{y}(A)) Beispiele: λx.xx, λxy.y, λxy.yx — Vereinfachungen?

– Typeset by FoilTEX – 133

Kombinator-Basen

Def: Eine Menge M von Kombinatoren heißt Basis, falls es zu jedem Lambda-Ausdruck einen äquivalenten Ausdruck nur aus Applikationen und Kombinatoren aus M gibt.

Satz: {S, K, I} ist Basis. Satz: {S, K} ist Basis. — Beweis? I = … Satz: es gibt eine Basis mit nur einem Element. (Schwer.)

Literatur:

• Henk Barendregt: The Lambda Calculus, its Syntax and

  Semantics, 1984. http://www.cs.ru.nl/~henk/

• Raymond Smullyan: How To Mock a Mockingbird, 1985.

  http://www.raymondsmullyan.com/

Anwendungen

• Übersetzung von λ nach CL entspricht Closure-Conversion und Lifting (beides, gleichzeitig)

• CL: feste Menge (Basis) von Kombinatoren, CC+L: Kombinatoren hängen vom Programmtext ab

• CL als Programmiersprache: http:

  //www.madore.org/~david/programs/unlambda/

Bsp: Berechnung von Fibonacci-Zahlen in Unlambda:

```s``s``sii`ki `k.*``s``s`ks
 ``s`k`s`ks``s``s`ks``s`k`s`kr``s`k`sikk
  `k``s`ksk

– Typeset by FoilTEX – 135

Registervergabe

Motivation

• (klassische) reale CPU/Rechner hat nur globalen Speicher (Register, Hauptspeicher)

• Argumentübergabe (Hauptprogramm → Unterprogramm) muß diesen Speicher benutzen

(Rückgabe brauchen wir nicht wegen CPS)

• Zugriff auf Register schneller als auf Hauptspeicher ⇒ bevorzugt Register benutzen.

Plan (I)

• Modell: Rechner mit beliebig vielen Registern (R_{0}, R_{1}, …)

• Befehle:

– Literal laden (in Register)

– Register laden (kopieren)

– direkt springen (zu literaler Adresse)

– indirekt springen (zu Adresse in Register)

• Unterprogramm-Argumente in Registern:

– für Abstraktionen: (R_{0}, R_{1}, …, R_{k})

(genau diese, genau dieser Reihe nach)

– für primitive Operationen: beliebig

• Transformation: lokale Namen → Registernamen

– Typeset by FoilTEX – 137

Plan (II)

• Modell: Rechner mit begrenzt vielen realen Registern, z. B. (R_{0}, …, R_{7})

• falls diese nicht ausreichen: register spilling virtuelle Register in Hauptspeicher abbilden

• Hauptspeicher (viel) langsamer als Register:

möglichst wenig HS-Operationen: geeignete Auswahl der Spill-Register nötig

Registerbenutzung

Allgemeine Form der Programme:

(let* ((r1 (...))
        (r2 (...))
        (r3 (...)))
        ...
  (r4 ...))

für jeden Zeitpunkt ausrechnen: Menge der freien Register (= deren aktueller Wert nicht (mehr) benötigt wird) nächstes Zuweisungsziel ist niedrigstes freies Register (andere Varianten sind denkbar) vor jedem UP-Aufruf: register shuffle (damit die Argumente in R_{0}, …, R_{k} stehen)

Automatische Speicherverwaltung

Motivation

Speicher-Allokation durch Konstruktion von

• Zellen,Tupel, Closures Modell: Speicherbelegung = gerichteter Graph Knoten lebendig: von Register aus erreichbar. sonst tot ⇒ automatisch freigeben Gliederung:

• mark/sweep (pointer reversal, Schorr/Waite 1967)

• twospace (stop-and-copy, Cheney 1970)

• generational (JVM)

– Typeset by FoilTEX – 140

Mark/Sweep

Plan: wenn Speicher voll, dann:

• alle lebenden Zellen markieren

• alle nicht markierten Zellen in Freispeicherliste

Problem: zum Markieren muß man den Graphen durchqueren, man hat aber keinen Platz (z. B. Stack), um das zu organisieren. Lösung: H. Schorr, W. Waite: An efficient machine-independent procedure for garbage collection in various list structures, Communations of the ACM, 10(8):481-492, August 1967. temporäre Änderungen im Graphen selbst (pointer reversal)

– Typeset by FoilTEX – 141

Pointer Reversal (Invariante)

ursprünglicher Graph G_{0}, aktueller Graph G: Knoten (cons) mit zwei Kindern (head, tail), markiert mit • 0: noch nicht besucht

• 1: head wird besucht (head-Zeiger ist invertiert)

• 2: tail wird besucht (tail-Zeiger ist invertiert)

• 3: fertig globale Variablen p (parent), c (current). Invariante: man erhält G_{0} aus G, wenn man

• head/tail-Zeiger aus 1/2-Zellen (nochmals) invertiert

• und Zeiger von p auf c hinzufügt.

– Typeset by FoilTEX – 142

Pointer Reversal (Ablauf)

• pre: p = null, c = root, ∀z : mark(z) = 0

• post: ∀z : mark(z) = if(root →^{∗} z) then 3 else 0 Schritt (neue Werte immer mit ′): falls mark(c) = …

• 0: c′ = head(c); head′(c) = p; mark′(c) = 1; p′ = c;

• 1,2,3: falls mark(p) = …

– 1: head′(p) = c; tail′(p) = head(p); mark′(p) = 2; c′ = tail(p); p′ = p

– 2: tail′(p) = c; mark′(p) = 3; p′ = tail(p); c′ = p; Knoten werden in Tiefensuch-Reihenfolge betreten.

Eigenschaften Mark/Sweep

• benötigt 2 Bit Markierung pro Zelle, aber keinen weiteren Zusatzspeicher

• Laufzeit für mark ∼ | lebender Speicher |

• Laufzeit für sweep ∼ | gesamter Speicher |

• Fragmentierung (Freispeicherliste springt) Ablegen von Markierungs-Bits:

• in Zeigern/Zellen selbst (Beispiel: Rechner mit Byte-Adressierung, aber Zellen immer auf Adressen ≡ 0 (mod 4): zwei LSB sind frei.)

• in separaten Bitmaps

– Typeset by FoilTEX – 144

Stop-and-copy (Plan)

Plan:

• zwei Speicherbereiche (Fromspace, Tospace)

• Allokation im Fromspace

• wenn Fromspace voll, kopiere lebende Zellen in Tospace und vertausche dann Fromspace ↔ Tospace

auch hier: Verwaltung ohne Zusatzspeicher (Stack) C. J. Cheney: A nonrecursive list compacting algorithm, Communications of the ACM, 13(11):677–678, 1970.

Stop-and-copy (Invariante)

fromspace, tospace : array [ 0 … N ] of cell Variablen: 0 ≤ scan ≤ free ≤ N einige Zellen im fromspace enthalten Weiterleitung (= Adresse im tospace) Invarianten:

• scan ≤ free

• Zellen aus tospace [0 … scan -1] zeigen in tospace

• Zellen aus tospace [scan … free-1] zeigen in fromspace

• wenn man in G (mit Wurzel tospace[0]) allen Weiterleitungen folgt, erhält man isomorphes Abbild von G_{0} (mit Wurzel fromspace[0]).

– Typeset by FoilTEX – 146

Stop-and-copy (Ablauf)

• pre: tospace[0] = Wurzel, scan = 0,free = 1.

• post: scan = free

Schritt: while scan < free:

• für alle Zeiger p in tospace[scan]:

– falls fromspace[p] weitergeleitet auf q, ersetze p durch q.

– falls keine Weiterleitung

∗ kopiere fromspace[p] nach tospace[free],

∗ Weiterleitung fromspace[p] nach free eintragen,

∗ ersetze p durch free, erhöhe free.

• erhöhe scan.

Besucht Knoten in Reihenfolge einer Breitensuche.

– Typeset by FoilTEX – 147

Stop-and-copy (Eigenschaften)

• benötigt ”doppelten“ Speicherplatz

• Laufzeit ∼ | lebender Speicher |

• kompaktierend

• Breitensuch-Reihenfolge zerstört Lokalität.

Breiten- und Tiefensuche

put (Wurzel(G)); while Speicher nicht leer:

u ← get; wenn u nicht markiert: markiere u; für alle v mit u →_{G} v: put(v);

dabei ist Speicher (mit Operationen put/get):

• Stack (LIFO) (push/pop) ⇒ Tiefensuche,

• Queue (FIFO) (enqueue/dequeue) ⇒ Breitensuche.

woran erkennt man, daß eine Knotenreihenfolge eines gerichteten Graphen G bei einer Breiten/Tiefensuche entstanden sein könnte? (wenn man Reihenfolge der Nachfolger eines Knoten jeweils beliebig wählen kann)

– Typeset by FoilTEX – 149

Speicher mit Generationen

Beobachtung: es gibt

• (viele) Zellen, die sehr kurz leben

• Zellen, die sehr lange (ewig) leben Plan:

• bei den kurzlebigen Zellen soll GC-Laufzeit ∼ Leben (und nicht ∼ Leben + Müll) sein

• die langlebigen Zellen möchte man nicht bei jeder GC besuchen/kopieren.

Lösung: benutze Generationen, bei GC in Generation k: betrachte alle Zellen in Generationen > k als lebend.

– Typeset by FoilTEX – 150

Speicherverwaltung in JVM

Speicheraufteilung:

• Generation 0:

– Eden, Survivor 1, Survivor 2

• Generation 1: Tenured Ablauf

• minor collection (Eden voll):

kompaktierend: Eden + Survivor 1/2 → Survivor 2/1 … … falls dabei Überlauf → Tenured

• major collection (Tenured voll):

alles nach Survivor 1 (+ Tenured)

– Typeset by FoilTEX – 151

Speicherverwaltung in JVM (II)

• richtige Benutzung der Generationen:

– bei minor collection (in Gen. 0) gelten Zellen in Tenured (Gen. 1) als lebend (und werden nicht besucht)

– Spezialbehandlung für Zeiger von Gen. 1 nach Gen. 0 nötig (wie können die überhaupt entstehen?)

• Literatur:

http://www.imn.htwk-leipzig.de/~waldmann/
edu/ws09/pps/folien/main/node78.html

• Aufgabe:

http://www.imn.htwk-leipzig.de/~waldmann/
edu/ws09/pps/folien/main/node79.html

Zusammenfassung

Semantik

• dynamische (Programmausführung)

– Interpretation

∗ funktional, • imperativ (Speicher)

∗ Ablaufsteuerung (Continuations)

– Transformation (Kompilation)

∗ CPS transformation

∗ closure passing, lifting, • Registerzuweisung

• statische: Typisierung (Programmanalyse)

– monomorph/polymorph

– deklariert/rekonstruiert

– Typeset by FoilTEX – 153

Monaden zur Programmstrukturierung

class Monad m where { return :: a -> m a ;
     (>>=)  :: m a -> (a -> m b) -> m b }

Anwendungen:

• semantische Bereiche f. Interpreter,

• Parser,

• Unifikation Testfragen (für jede Monad-Instanz):

• Typ (z. B. Action)

• anwendungsspezifische Elemente (z. B. new, put)

• Implementierung der Schnittstelle (return, bind)

– Typeset by FoilTEX – 154

Parser

Ansätze:

• eingebettet: Kombinator-Parser (Parsec)

• separat: lex/yacc (flex/bison), javacc, antlr, …

Unterschiede:

• eingebettet: benutzt Typsystem, Abstraktionsmechanismen, Bibliotheken der Gastsprache (separat: diese Ausdrucksmittel fehlen oder müssen simuliert werden)

• diese Einschränkung der Ausdruckskraft (z. B.

LR(k)-Grammatiken) gestattet effizientere Realisierung (z. B. deterministische Kellerautomaten)

Anhang

Prüfungsvorbereitung

• was ist eine Umgebung (Env), welche Operationen gehören dazu?

• was ist eine Speicher (Store), welche Operationen gehören dazu?

• Gemeinsamkeiten/Unterschiede zw. Env und Store?

• Für (λx.xx)(λx.xx): zeichne den Syntaxbaum, bestimme die Menge der freien und die Menge der gebundenen Variablen. Markiere im Syntaxbaum alle Redexe. Gib die Menge der direkten Nachfolger an (einen Beta-Schritt

– Typeset by FoilTEX – 156

ausführen).

• Definiere Beta-Reduktion und Alpha-Konversion im Lambda-Kalkül. Wozu wird Alpha-Konversion benötigt? (Dafür Beispiel angeben.)

• Wie kann man Records (Paare) durch Funktionen simulieren? (Definiere Lambda-Ausdrücke für

pair, first, second)

• welche semantischen Bereiche wurden in den Interpretern benutzt? (definieren Sie

Val, Action Val, CPS Val)

• welches sind die jeweils hinzukommenden Ausdrucksmöglichkeiten der Quellsprache (Exp)?

– Typeset by FoilTEX – 157

• wie lauten die Monad-Instanzen für Action, CPS, Parser, was bedeutet jeweils das bind

(>>=)?

• warum benötigt man call-by-name für Abstraktionen über den Programmablauf (warum kann man if oder while nicht mit call-by-value implementieren)?

• wie kann man call-by-name simulieren in einer call-by-value-Sprache?

• wie kann man call-by-value simulieren in einer call-by-name-Sprache (Antwort: durch CPS-Transformation)

• Definiere Fakultät mittels Fixpunktoperator (Definiere das

f in fak = fix f )

• Bezüglich welcher Halbordnung ist dieses f monoton? (Definiere die Ordnung, erläutere Monotonie an einem Beispiel.)

• Wie kann man Rekursion durch get/put simulieren? (Programmbeispiel ergänzen)

• Wie kann man Rekursion durch label/jump simulieren? (Programmbeispiel ergänzen)

• Für die Transformationen CPS, Closure Conv., Lifting, Registervergabe: welche Form haben jeweils Eingabeund Ausgabeprogramm? Auf welchem Maschinenmodell

– Typeset by FoilTEX – 159

kann das Zielprogramm ausgeführt werden? (Welche Operationen muß das Laufzeitsystem bereitstellen?)

• Was sind die Bestandteile eines Inferenzsystems (Antwort: Grundbereich, Axiome, Regeln), wie kann man ein Axiom als Spezialfall einer Regel auffassen?

• wie lauten die Inferenzregeln für das Nachschlagen eines Namens in einer Umgebung?

• Inferenzregeln für Applikation, Abstraktion, Let, If/Then/Else im einfach getypten Kalkül

• Geben Sie ein Programm an, das sich nicht einfach (sondern nur polymorph) typisieren läßt. Geben Sie den polymorphen Typ an.

– Typeset by FoilTEX – 160

• Inferenz-Regeln für Typ-Applikation, Typ-Abstraktion im polymorphen Kalkül

• für Typ-Rekonstruktion im einfach getypten Kalkül: Welches ist der Grundbereich des Inferenzsystems?

• geben Sie die Inferenzregel für Typrekonstruktion bei If/Then/Else an

• Geben Sie eine Inferenzregel für Typrekonstruktion an, durch die neue Variablen eingeführt werden.

• Wann ist σ ein Unifikator von zwei Termen s, t?

• Geben Sie zwei verschiedene Unifikatoren von f(a, X) und f(Y, Z) an. Einer davon soll streng allgemeiner als

– Typeset by FoilTEX – 161

der andere sein. Begründen Sie auch diese Beziehung.

• Bestimmen Sie einen Unifikator von f(X_{n}, f(X_{n−1}, …, f(X_{0}, a) …)) und f(f(X_{n−1}, X_{n−1}), f(f(X_{n−2}, X_{n−2}), …, f(a, a) …)).