Einleitung

Beispiel: C-Compiler

Sprachverarbeitung

Gemeinsamkeit: syntaxgesteuerte Semantik (Ausführung bzw. Übersetzung)

Inhalt der Vorlesung

Konzepte von Programmiersprachen

realisieren durch

Hilfsmittel:

Literatur

Anwendungen von Techniken des Compilerbaus

Organisation der Vorlesung

Beispiel: Interpreter f. arith. 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

das ist syntax-gesteuerte Semantik:

Wert des Terms wird aus Werten der Teilterme kombiniert

Beispiel: 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 )
extend n w e = \ m -> if m == n then w else e m
value :: Env -> Exp -> Integer
value env x = case x of
    Ref n -> env n
    Let n x b -> value (extend n (value env x) env) b
    Const i -> i
    Plus x y -> value env x + value env y
    Times x y -> value env x * value env y
test2 = value (\ _ -> 42) ex2

Übung (Haskell)

Übung (Interpreter)

Inferenz-Systeme

Motivation

Definition

ein Inferenz-System \(I\) besteht aus

eine Ableitung für \(F\) bzgl. \(I\) ist ein Baum:

Def: \(I \vdash F\) \(:\iff\) \(\exists\) \(I\)-Ableitungsbaum mit Wurzel \(F\).

Regel-Schemata

Inferenz-Systeme (Beispiel 1)

kann man \((1,1)\) ableiten? \((-1,5)\)? \((2,4)\)?

Das Ableiten als Hüll-Operation

Aussagenlogische Resolution

Formel \((A\vee \neg B\vee \neg C)\wedge(C\vee D)\) in konjunktiver Normalform

dargestellt als \(\{\{A,\neg B,\neg C\},\{C,D\}\}\)

(Formel \(=\) Menge von Klauseln, Klausel \(=\) Menge von Literalen, Literal \(=\) Variable oder negierte Variable)

folgendes Inferenzsystem heißt Resolution:

Eigenschaft (Korrektheit): wenn \(\displaystyle\frac{K_1,K_2}{K}\), dann \(K_1\wedge K_2\rightarrow K\).

Resolution (Vollständigkeit)

die Formel (Klauselmenge) ist nicht erfüllbar \(\iff\) die leere Klausel ist durch Resolution ableitbar.

Bsp: \(\{ p, q, \neg p\vee\neg q \}\)

Beweispläne:

Die Abtrennungsregel (modus ponens)

…ist das Regelschema \(\displaystyle \frac{P\to Q,P}{Q},\)

Der Hilbert-Kalkül für die Aussagenlogik

ist das Inferenz-System mit modus ponens

und Axiom-Schemata wie z. B.

(es gibt verschiedene Varianten des Kalküls) — Man zeigt:

Inferenz von Werten

Umgebungen (Spezifikation)

Umgebungen (Implementierung)

Umgebung ist (partielle) Funktion von Name nach Wert

Realisierungen: type Env = String -> Integer

Operationen:

Beispiel

lookup (extend  "y" 4 (extend "x" 3 empty)) "x"

entspricht \((\emptyset[x:=3][y:=4]) x\)

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

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 )

Aufgaben

Unterprogramme

Beispiele

Interpreter mit Funktionen

Semantik (mit Funktionen)

Let und Lambda

Mehrstellige Funktionen

…simulieren durch einstellige:

Semantik mit Closures

Closures (Spezifikation)

Rekursion?

Testfall (2)

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

Übungen

  1. Schreiben und benutzen Sie die Hilfsfunktion with_val, die im Skript an einigen Stellen schon benutzt wurde.

    Realisieren Sie damit die strikte Semantik für Let-Bindung und Funktions-Anwendung.

  2. alternative Implementierung von Umgebungen

    • bisher type Env = String -> Val

    • jetzt type Env = Data.Map.Map String Val

  3. alternative Implementierung von Namen

    der Vergleich von Strings (als Schlüssel im Suchbaum) ist teuer. Ist für diesen Interpreter zeitkritisch!

    • statt data Name = Name T.Text besser

      data Name = 
  Name { hash :: Int, form :: T.Text }
  deriving (Eq, Ord)

    • mit smart constructor name :: String -> Name

      dann Times (Ref (name "x")) (Const 3)

    • und instance IsString Name where ...

      dann (wie früher!) Times (Ref "x") (Const 3)

    • für später: der Compiler benutzt Name und Env nur zur Übersetzungszeit!

      Zur Laufzeit ist Umgebung ein Vektor von Vektoren (siehe VL PPS: Frames, statische Kette),

      die Längen und alle Indizes sind statisch bekannt.

    • recherchieren und beschreiben Sie FastString in GHC (z.B. https://gitlab.haskell.org/ghc/ghc/-/issues/20091, interned strings (symbols) in Ruby (oder ähnlich).

  4. eingebaute primitive Rekursion (Induktion über Peano-Zahlen):

    implementieren Sie die Funktion fold :: r -> (r -> r) -> N -> r

    Testfall: fold 1 (\x -> 2*x) 5 == 32

    durch data Exp = .. | Fold .. und neuen Zweig in value

    Wie kann man damit die Fakultät implementieren?

  5. entwerfen und realisieren Sie einen entsprechenden Operator zur Simulation von while (unbeschränkte Rekursion).

Lambda-Kalkül (Wdhlg.)

Motivation

1. Modellierung von Funktionen:

2. Notation mit gebundenen (lokalen) Variablen, wie in

Der Lambda-Kalkül

Lambda-Terme

Eigenschaften der Reduktion

Beziehung zur Semantik des Interpreters

Daten als Funktionen

Lambda-Kalkül als universelles Modell

Fixpunkt-Kombinatoren (Motivation)

Fixpunkt-Kombinatoren (Implementierung)

Lambda-Berechenbarkeit

Satz: (Church, Turing)

Kodierung von Zahlen nach Church

Übung Lambda-Kalkül (I)

Übung Lambda-Kalkül (II)

folgende Aufgaben aus H. Barendregt: Lambda Calculus

Fixpunkte

Motivation

Das ging bisher gar nicht:

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

Lösung 1: benutze Fixpunktkombinator

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

Lösung 2 (später): realisiere Fixpunktberechnung im Interpreter (neuer AST-Knotentyp)

Existenz von Fixpunkten

Fixpunkt von \(f :: C \to C\) ist \(x :: C\) mit \(f x=x\).

Existenz? Eindeutigkeit? Konstruktion?

Satz: Wenn \(C\) pointed CPO und \(f\) stetig,
dann besitzt \(f\) genau einen kleinsten Fixpunkt.

Beispiele f. Halbordnungen, CPOs

Halbordnung? pointed? complete?

Stetige Funktionen

\(f\) ist stetig \(:=\)

Beispiele: in \((\mathbb{N}\cup\{+\infty\},\le)\)

Satz: Wenn \(C\) pointed CPO und \(f:C\to C\) stetig,
dann besitzt \(f\) genau einen kleinsten Fixpunkt …

…und dieser ist \(\sup [\bot,f(\bot),f^2(\bot),\ldots]\)

Funktionen als CPO

Funktionen als CPO, Beispiel

Welche Funktionale sind stetig?

Fixpunktberechnung im Interpreter

Fixpunkte und Laziness

Fixpunkte existieren in pointed CPOs.

Beispiele in Haskell:

fix f = f (fix f)
xs = fix $ \ zs -> 1 : zs
ys = fix $ \ zs -> 
    0 : 1 : zipWith (+) zs (tail zs)

Arithmetik mit Bedarfsauswertung

Simultane Rekursion: letrec

letrec nach rec (falsch)

letrec nach rec (richtig)

Übung Fixpunkte

  1. Limes der Folge \(F^k(\bot)\) für

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

  2. Ist \(F\) stetig? Gib den kleinsten Fixpunkt von \(F\) an:

    F h =  \ x -> if x >= 2 then 1 + h(x-2) 
    else if x == 1 then 1 else h(4) - 2

    Hat \(F\) weitere Fixpunkte?

  3. \(C=\) Menge der Formalen Sprachen über \(\Sigma=\{a,b\}\), halbgeordnet durch \(\subseteq\). ist CPO? pointed?

    \(g: C\to C: L\mapsto \{\epsilon\}\cup \{a\}\cdot L\cdot\{b\}\) ist stetig? Fixpunkt(e)?

    \(h: C\to C: L\mapsto \{a\}\cup L\cdot \{b\}\cdot (\Sigma^*\setminus L)\)

  4. in der Relation \(\subseteq\) auf \(\{\{A\},\{B\},\{A,B\}\}\): geben Sie eine stetige Funktion an, die zwei verschiedene kleinste Fixpunkte besitzt.

  5. Geben Sie Argumente aus dieser Diskussion wieder: …distinguish bindings that are self-referentially recursive from non-recursive bindings https://github.com/ghc-proposals/ghc-proposals/pull/401 (O. Charles, 8. Febr. 2021)

Verpackung und Verteilung

Haskell-Software-Pakete

Kuratierte Paket-Mengen

Continuous Intergration

Haskell-Module

Modul-Abhängigkeiten

Zustand/Speicher

Motivation

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

Dazu muß semantischer Bereich geändert werden.

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

Speicher (Daten)

Speicher (Operationen)

Auswertung von Ausdrücken

Änderung der Hilfsfunktionen

Variablen?

in unserem Modell haben wir:

\(\Rightarrow\) der Wert eines Namens kann eine Speicherstelle sein, aber dann immer dieselbe.

Imperative Programmierung

es fehlen noch wesentliche Operatoren:

diese kann man:

Rekursion

mehrere Möglichkeiten zur Realisierung

Rekursion (operational)

Speicher—Übung

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

…unter verschiedenen Aspekten

Die Konstruktorklasse Monad

Do-Notation für Monaden

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

do-Notation (explizit geklammert):

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

do-Notation (implizit geklammert):

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

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

Beispiele für Monaden

Die IO-Monade

data IO a -- abstract
instance Monad IO -- eingebaut

readFile :: FilePath -> IO String
putStrLn :: String -> IO ()

Alle Funktionen, deren Resultat von der Außenwelt (Systemzustand) abhängt, haben Resultattyp IO ..., sie sind tatsächlich Aktionen.

Am Typ einer Funktion erkennt man ihre möglichen Wirkungen bzw. deren garantierte Abwesenheit.

main :: IO ()
main = do 
   cs <- readFile "foo.bar" ; putStrLn cs

Grundlagen: Kategorien

Beispiele:

Kategorische Definitionen und Sätze

Beispiel: Isomorphie

weiteres Beispiel

Produkte

Dualität

Funktoren

Die Kleisli-Konstruktion

Diese Komposition ist f >=> g = \ x -> (f x >>= g)

Aus o.g. Forderung (\(K\) ist Kategorie) ergibt sich Spezifikation für return und >>=

Functor, Applicative, Monad

https://wiki.haskell.org/Functor-Applicative-Monad_Proposal

class Functor f where 
  fmap :: (a -> b) -> (f a -> f b)
class Functor f => Applicative f where
  pure :: a -> f a
  (<*>) :: f (a -> b) -> (f a -> f b)
class Applicative m => Monad m where
  (>>=) :: m a -> (a -> m b) -> m b

eine Motivation: effizienterer Code für >>=,
wenn das rechte Argument eine konstante Funktion ist

(d.h. die Folge-Aktion hängt nicht vom Resultat der ersten Aktion ab: dann ist Monad nicht nötig, es reicht Applicative)

Die Maybe-Monade

data Maybe a = Nothing | Just a
instance Monad Maybe where ...

Beispiel-Anwendung:

case ( evaluate e l ) of
    Nothing -> Nothing
    Just a  -> case ( evaluate e r ) of
        Nothing -> Nothing
        Just b  -> Just ( a + b )

mittels der Monad-Instanz von Maybe:

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

Ü: dasselbe mit do-Notation

List als Monade

instance Monad [] where
    return = \ x - > [x]
    m >>= f = case m of 
        []     -> [] 
        x : xs -> f x ++ ( xs >>= f )

Beispiel:

do a <- [ 1 .. 4 ]
   b <- [ 2 .. 3 ]
   return ( a * b )

Anwendung: Ablaufsteuerung für Suchverfahren

Monaden: Zusammenfassung

Monaden-Transformatoren

Der Zustands-Transformator

Der Ausnahme-Transformator MaybeT

Der Ausnahme-Transformator ExceptT

Bibliotheken für Monaden-Transformatoren

Übung

Kombinator-Parser

Datentyp für Parser

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

Definition:

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

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

Anwendungsbeispiel:

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

mit Operatoren aus Control.Applicative:

p = (,) <$> next <*> next

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 = ( \ c ->  fromIntegral 
           $ fromEnum c - fromEnum '0' )
  <$> satisfy Data.Char.isDigit

Kombinatoren für Parser (I)

zahl :: Parser Char Integer = 
  foldl (\ a z -> 10*a+z) 0 <$> some ziffer

Kombinatoren für Parser (II)

(aus Control.Applicative)

Kombinator-Parser und Grammatiken

Parser für Operator-Ausdrücke

Robuste Parser-Bibliotheken

Asymmetrische Komposition

gemeinsam:

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

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

Nichtdeterminismus einschränken

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

Übung Kombinator-Parser

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)

Bidirektionale Programme

Motivation: parse und (pretty-)print aus einem gemeinsamen Quelltext

Tillmann Rendel and Klaus Ostermann: Invertible Syntax Descriptions, Haskell Symposium 2010

http://lambda-the-ultimate.org/node/4191

Datentyp

data PP a = PP
  { parse :: String -> [(a,String)]
  , print :: a -> Maybe String
  }

Spezifikation, elementare Objekte, Kombinatoren?

Ablaufsteuerung/Continuations

Definition

(alles nach: Turbak/Gifford Ch. 17.9)

CPS-Transformation (continuation passing style):

aus g (f 3 2)

wird \ k -> f_cps 3 2 $ \ v -> g_cps v k

Motivation

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

CPS als einheitlicher Mechanismus für

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?

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

Wdhlg: CPS-Transformation von 1+(2*(3-(4+5))) ist

\ top -> plus 4 5 $ \ a ->
         minus 3 a $ \ b ->
         mal 2 b $ \ c ->
         plus 1 c top

Neu: label und jump

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

Semantik: durch label wird die aktuelle Continuation benannt: foo = \ c -> plus 1 c top

und durch jump benutzt:

\ top -> plus 4 5 $ \ a -> foo a

Vergleiche: label: Exception-Handler deklarieren,
jump: Exception auslösen

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 -> 
  ( \ k0 -> k0 k0 ) $ \ k' -> 
  value (E, label y y) k'
= \ k -> 
  ( \ k0 -> k0 k0 ) $ \ k' -> 
  ( \ k1 -> k1 k1 ) k'

Semantik

semantischer Bereich:

type Continuation a = a -> Action Val
newtype CPS a 
   = CPS ( Continuation a -> Action Val )
value :: Env -> Exp -> CPS Val

Plan:

CPS als Monade

Der CPS-Transformator

Übungsaufgaben

Rekursion (bzw. Schleifen) mittels Label/Jump

(und ohne Rec oder Fixpunkt-Kombinator)

folgende Beispiele sind aus Turbak/Gifford, DCPL, 9.4.2

Typen

Grundlagen

Typ \(=\) statische Semantik

(Information über mögliches Programm-Verhalten, erhalten ohne Programm-Ausführung)

formale Beschreibung:

Inferenzsystem für Typen (Syntax)

Inferenzsystem für Typen (Semantik)

hierbei (vorläufige) Design-Entscheidungen:

Inferenz für Let

(alles ganz analog zu Auswertung von Ausdrücken)

Applikation und Abstraktion

Eigenschaften des Typsystems

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

Übung: typisiere t t t t succ 0 mit succ = \ x -> x + 1 und t = \ f x -> f (f x)

Übung

  1. Typisierung für Vergleichs-Operatoren, If-Then-Else, New/Get/Put

  2. Tupel: abstrakte Syntax, dynamische Semantik, statische Semantik

  3. konkrete Syntax (Parser): Let, Abs, App, Tupel (Syntax immer wie in Haskell)

  4. konkrete Syntax: AbsTyped (dazu brauchen wir Parser für Typ-Ausdrücke)

Typ-Rekonstruktion

Motivation

Realisierung mit Constraints

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

wobei

Bsp: \(U=\{u,v,w\}, C=\{(u,\textsf{Int}\to v),(w\to \textsf{Bool}, u)\0\}\),

\(\sigma=\{(u,\textsf{Int}\to\textsf{Bool}),(v,\textsf{Bool}),(w,\textsf{Int})\}\)

Inferenzregeln f. Rekonstruktion (Plan)

Plan:

Für (fast) jeden Teilausdruck eine eigene (frische) Typvariable ansetzen, Beziehungen zwischen Typen durch Constraints ausdrücken.

Inferenzregeln? Lösbarkeit? Implementierung? — Testfall:

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

Inferenzregeln f. Rekonstrukion

Implementierung Constraint-Erzeugung

Substitutionen (Definition)

Substitutionen: Produkt

Produkt von Substitutionen: \(t (\sigma_1 \circ \sigma_2) = (t \sigma_1) \sigma_2\)

Beispiel 1:

\(\sigma_1=\{X\mapsto Y\}, \sigma_2 = \{Y\mapsto a\}, \sigma_1 \circ \sigma_2 = \{ X\mapsto a, Y\mapsto a\}\).

Beispiel 2 (nachrechnen!):

\(\sigma_1 = \{X\mapsto Y\}, \sigma_2=\{Y \mapsto X\}, \sigma_1\circ\sigma_2 = \sigma_2\)

Eigenschaften:

Implementierung:

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

Substitutionen: Ordnung

Substitution \(\sigma_1\) ist allgemeiner als Substitution \(\sigma_2\):

\(\sigma_1 \raisebox{-8pt}[0pt][0pt]{$\stackrel{\displaystyle <}{\sim}$}\sigma_2 \iff \exists \tau : \sigma_1 \circ \tau = \sigma_2\)

Beispiele:

Eigenschaften

Unifikation—Definition

Unifikationsproblem

(allgemeinst: infimum bzgl. \(\raisebox{-8pt}[0pt][0pt]{$\stackrel{\displaystyle <}{\sim}$}\))

Satz: jedes Unifikationsproblem ist

lösbar.

Unifikation—Algorithmus

Unifikation—Komplexität

Bemerkungen:

Bsp: Signatur \(\{f/2, a/0\}\),

unifiziere \(f(X_1,f(X_2,f(X_3,f(X_4,a))))\) mit \(f(f(X_2,X_2),f(f(X_3,X_3),f(f(X_4,X_4),f(a,a))))\)

Hausaufgaben

Plan für Compiler

Transformationen/Ziel

Ziel: maschinen(nahes) Programm mit

CPS-Transformation

CPS-Transformation: Spezifikation

(als Schritt im Compiler)

CPS-Transformation: Zielsyntax

drei Teilmengen von data Exp:

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

Übung 1: Übersetze von Exp nach Exp_CPS:

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

Übung 2: wegen CPS brauchen wir tatsächlich:

\ k -> k ((0 - (b * b)) + (4 * (a * c))

Beispiel

Lösung 1:

(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

Lösung 2:

\ k -> let  ... in k t.1

CPS-Transf. f. Abstraktion, Applikation

vgl. Sect. 6 in: Gordon Plotkin: Call-by-name, call-by-value and the \(\lambda\)-calculus,

Th. Comp. Sci. 1(2) 1975, 125–159 http://dx.doi.org/10.1016/0304-3975(75)90017-1 , http://homepages.inf.ed.ac.uk/gdp/

dabei sind \(k,f,a\) frische Namen.

Bsp. \(\operatorname{CPS}(\lambda x.9)=\lambda k_2.k_2(\lambda x.\operatorname{CPS}(9)) =\lambda k_2.k_2(\lambda x k_1.k_1 9),\)

\(\operatorname{CPS}((\lambda x.9) 8) = \lambda k_4.(\lambda k_2.k_2(\lambda x k_1.k_1 9)) (\lambda f.((\lambda k_3.k_3 8) (\lambda a.f a k_4)))\)

Ü: Normalform von \(\operatorname{CPS}((\lambda x.9)8) (\lambda z.z)\)

Realisierung der CPS-Transformation

Namen

Anwendung der Namens-Erzeugung

Kompilation des If

Kompilation des Let

Umrechnung zw. Continuations (App)

Umrechnung zw. Continuations (Abs)

Vergleich CPS-Interpreter/Transformator

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 -> Fresh ExpCPS
cps :: Exp -> Cont -> Fresh ExpCPS
cps x = \ m -> case x of
    ConstInt i -> ... 
    Plus a b -> ...

Übung CPS-Transformation

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 .. )

Spezifikation

closure conversion:

geschlossen: alle Variablen sind lokal

Ansatz:

closure passing style

\ x -> a * x + 1
==>
\ clo x -> 
  let { a = nth 1 clo } 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,\ldots\}=\) freie Variablen in \((\lambda i_1 \ldots i_n \to b)\)

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

Lifting

Spezifikation

(lambda) lifting:

Motivation: in Maschinencode gibt es nur globale Sprungziele

(CPS-Transformation: Unterprogramme kehren nie zurück \(\Rightarrow\) 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

Lambda-Lifting (Plan)

um ein Programm zu erhalten, bei dem alle Abstraktionen global sind:

Lambda-Lifting (Realisierung)

Beispiel: \(\operatorname{\textsf{lift}}(\lambda x.\lambda y.y x) = \operatorname{\textsf{lift}}_x(\operatorname{\textsf{lift}}_y(y x)) = \operatorname{\textsf{lift}}_x(S I (K x)) = S (K( S I )) (S (K K) I)\)

Registervergabe

Motivation

Plan (I)

Plan (II)

Registerbenutzung

Compiler-Übungen

  1. Testen Sie die richtige Kompilation von

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

  2. implementieren Sie fehlende Codegenerierung/Runtime für

    let { p = new 42 
    ; f = \ x -> if (x == 0) then 1 
                 else  (x * (get p) (x-1)) 
    ; foo = put p f 
    } in f 5

  3. ergänzen Sie das Programm, so daß \(5!\) ausgerechnet wird

    let { f = label x (x, 5, 1) } 
in  if ( 0 == nth 1 f ) 
    then nth 2 f  
    else jump ...
              (..., ..., ...)

    Kompilieren Sie das Programm. Dazu muß für label, jump, tuple, nth die CPS-Transformation implementiert werden.

  4. Bei der CPS-Transformation von If wird die Continuation \(k\) kopiert:

          If b' <$> cps j k <*> cps n k

    Geben Sie ein Beispiel dafür an, daß dadurch der Ausgabetext groß werden kann.

    Geben Sie eine andere Übersetzung für If an, bei der \(k\) nur einmal angewendet wird. (Benutzen Sie cont2exp.)

    Überprüfen Sie für das eben angegebene Beispiel.

  5. Alle Tests bis hier kompilieren konstante Ausdrücke. Diese könnte man auch sofort auswerten.

    Ändern Sie Compiler und Laufzeitsystem, so daß Funktionen kompiliert werden, die zur Laufzeit Argumente (Zahlen) von der Kommandozeile bekommen.

  6. Register Allocator in GCC: siehe https://gcc.gnu.org/onlinedocs/gccint/RTL-passes.html.

    Suchen Sie die entsprechende Beschreibung/Implementierung in clang (llvm).

    Vergleichen Sie an Beispielen die Anzahl der Register in dem von unserem Compiler erzeugten Code und dem daraus durch GCC (clang) erzeugten Assemblercode.

    Wo findet die Register-Allokation für Java-Programme statt?

und wer Zeit hat …

Zusammenfassung

Methoden

Semantik

Monaden zur Programmstrukturierung

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

Anwendungen:

Testfragen (für jede Monad-Instanz):

Wozu braucht man den Compilerbau?

Prüfungsvorbereitung

Beispielklausur http://www.imn.htwk-leipzig.de/~waldmann/edu/ws11/cb/klausur/