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

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

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 f-cps 3 2 g-cps

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 -> 
  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:

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

Der CPS-Transformator

Beispiele/Übung KW 50: Parser

Beispiele/Übung KW 50: CPS

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 (Wiederholung/Nachtrag)

  1. Pretty-Printer für Exp,

  2. Pretty-Printer und Parser für Type

  3. ExceptT in Sem verwenden, bessere Fehlermeldungen in module With

  4. ContT aus Transformers-Bibliothek, damit Nachnutzung der dort definierten Instanzen

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? Implementierung? — Testfall:

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

Inferenzregeln f. Rekonstrukion

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

\(\operatorname{mgu}(s, t)\) nach Fallunterscheidung

mgu :: Term -> Term -> Maybe Substitution

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

Übung Rekonstruktion

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-Argumente (Inferenz-Regeln)

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 s -> t t s 0 ) 
  ( \ f x -> f (f x) ) (\ x -> x+1)

Implementierung

Luis Damas, Roger Milner: Principal Type Schemes for Functional Programs 1982,

Jones 1999 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.134.7274 Grabmüller 2006 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.65.7733,

Dependent Types

Funktionen zwischen Typen und Daten

Implementierung

Anwendung: Peano-Zahlen, Fold

Übung: Tupel

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 …

Automatische Speicherverwaltung

Motivation

Speicher-Allokation durch Konstruktion von

Modell: Speicherbelegung \(=\) gerichteter Graph

Knoten lebendig: von Register aus erreichbar.

sonst tot \(\Rightarrow\) automatisch freigeben

Gliederung:

Mark/Sweep

Plan: wenn Speicher voll, dann:

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)

Pointer Reversal (Invariante)

ursprünglicher Graph \(G_0\), aktueller Graph \(G\):

Knoten (cons) mit zwei Kindern (head, tail), markiert mit

globale Variablen \(p\) (parent), \(c\) (current).

Invariante: man erhält \(G_0\) aus \(G\), wenn man

Pointer Reversal (Ablauf)

Schritt (neue Werte immer mit \('\)): falls \(\operatorname{mark}(c)=\) …

Knoten werden in Tiefensuch-Reihenfolge betreten.

Eigenschaften Mark/Sweep

Ablegen von Markierungs-Bits:

Stop-and-copy (Plan)

Plan:

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 \le \text{scan} \le \text{free} \le N\)

einige Zellen im fromspace enthalten Weiterleitung (\(=\) Adresse im tospace)

Invarianten:

Stop-and-copy (Ablauf)

Schritt: while scan \(<\) free:

Besucht Knoten in Reihenfolge einer Breitensuche.

Stop-and-copy (Eigenschaften)

Speicher mit Generationen

Beobachtung: es gibt

Plan:

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

Speicherverwaltung in JVM

Speicheraufteilung:

Ablauf

Speicherverwaltung in JVM (II)

Ausblick

Informative Typen

in \(X::T\), der deklarierte Typ \(T\) kann eine schärfere Aussage treffen als aus \(X\) (Implementierung) ableitbar.

data T a = C a -- C :: a -> T a
data T a where C :: Bool -> T Bool

das ist u.a. nützlich bei der Definition und Implementierung von (eingebetteten) domainspezifischen Sprachen

GADT

Higher Order Abstract Syntax

data Exp a  where
  Var :: a -> Exp a
  Abs :: (a -> Exp b) -> Exp (a -> b)
  App :: Exp (a -> b) -> Exp a -> Exp b

App (Abs $ \x -> Plus (C 1) (Var x)) (C 2) 

value :: Exp a -> a
value e = case e of
  App f a -> value f ( value a )

Ü: vervollständige Interpreter

Quelle: Frank Pfenning, Conal Elliott: HOAS, PLDI 1988 http://conal.net/papers/

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/