Einleitung

Beispiel

Eingabe (\(\approx\) 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:

Sprachverarbeitung

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

(weitere) Methoden und Modelle

Inhalt der Vorlesung

Konzepte von Programmiersprachen

realisieren durch

Hilfsmittel:

Literatur

Anwendungen von Techniken des Compilerbaus

Organisation der Vorlesung

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)

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

Das Ableiten als Hüll-Operation

Regel-Schemata

Inferenz-Systeme (Beispiel 1)

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

Inferenz-Systeme (Beispiel 2)

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

Inferenz-Systeme (Beispiel 3)

Aufgaben: \(\bullet\) Ableitungen für \([5,3,1,3], [7,7,1]\)

praktische Realisierung: http://www.siteswap.org/ und HTWK-Hochschulsport

Inferenz von Werten

Umgebungen (Spezifikation)

Umgebungen (Implementierung)

Umgebung ist (partielle) Funktion von Name nach Wert

Realisierungen: type Env = String -> Integer

Operationen:

Beispiel

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

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

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:

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: if/then/else mit with_bool, relationale Operatoren (==, <, o.ä.), Boolesche Konstanten.

Unterprogramme

Beispiele

Interpreter mit Funktionen

abstrakte Syntax:

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

konkrete Syntax:

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

konkrete Syntax (Alternative):

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

Let und Lambda

Mehrstellige Funktionen

…simulieren durch einstellige:

Closures (I)

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

Closures (II)

Spezifikation der Semantik durch Inferenz-System:

Rekursion?

Testfall (2)

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

Lambda-Kalkül (Wdhlg.)

Motivation

1. intensionale Modellierung von Funktionen,

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

Der Lambda-Kalkül

(Alonzo Church, 1936 …Henk Barendregt, 1984 …)

ist der Kalkül für Funktionen mit benannten Variablen

die wesentliche Operation ist das Anwenden einer Funktion:

\[(\lambda x . B) A \to B[x:=A]\]

Beispiel: \((\lambda x.x*x)(3+2) \to (3+2)*(3+2)\)

Im reinen Lambda-Kalkül gibt es nur Funktionen—keine Zahlen

Lambda-Terme

Menge \(\Lambda\) der Lambda-Terme (mit Variablen aus einer Menge \(V\)):

das sind also Lambda-Terme: \(x, (\lambda x.x), ((x z) (y z)), (\lambda x.(\lambda y.(\lambda z.((x z) (y z)))))\)

verkürzte Notation

Gebundene Variablen

Def: Menge \(\operatorname{FV}(t)\) der freien Variablen von \(t\in\Lambda\)

Def: Menge \(\operatorname{BV}(t)\) der gebundenen Variablen von \(t\in\Lambda\)

Substitution

\(A[x:= N]\) ist (eine Kopie von) \(A\), wobei jedes freie Vorkommen von \(x\) durch \(N\) ersetzt ist…

…und keine in \(N\) frei vorkommende Variable hierdurch gebunden wird

Definition durch strukturelle Induktion

falls… hat zur Folge: Substitution ist partielle Fkt.

Das falsche Binden von Variablen

Diese Programme sind nicht äquivalent:

int f (int y) {
  int x = y + 3; int sum = 0;
  for (int y = 0; y<4; y++) 
        { sum = sum + x   ; }
  return sum;
}
int g (int y) {
                 int sum = 0;
  for (int y = 0; y<4; y++) 
        { sum = sum + (y+3); }
  return sum;
}

Gebundene Umbenennungen

Relation \(\to_\alpha\) auf \(\Lambda\):

\(\equiv_\alpha\) ist die durch \(\to_\alpha\) definierte Äquivalenzrelation

(die transitive, reflexive und symmetrische Hülle von \(\to_\alpha\))

Bsp. \(\lambda x.\lambda x.x \equiv_\alpha \lambda y.\lambda x.x\), \(\lambda x.\lambda x.x \not\equiv_\alpha \lambda y.\lambda x.y\)

\(\alpha\)-Äquivalenzklassen

wir wollen bei Bedarf gebunden umbenennen, aber das nicht immer explizit hinschreiben: betrachten \(\Lambda/\equiv_\alpha\) statt \(\Lambda\)

Wdhlg (1. Sem) wenn \(R\) eine Äquivalenz-Relation auf \(M\),

Beispiele:

Ableitungen

Absicht: Relation \(\to_\beta\) auf \(\Lambda/\equiv_\alpha\) (Ein-Schritt-Ersetzung):

Vorsicht:

\((\lambda x.(\lambda y.xyx))(y y) \to_\beta(\lambda y.yx)[x:=(y y)] \stackrel{?}{=} \lambda y.y(yy)\)

das freie \(y\) wird fälschlich gebunden

die Substitution ist nicht ausführbar, man muß vorher lokal umbenennen

Eigenschaften der Reduktion

\(\to\) auf \(\Lambda\) ist

Lambda-Kalkül (Universalität)

Daten als Funktionen

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

dann gilt \(s_i \langle D_1, \ldots, D_k\rangle \to_{\beta}^* D_i\)

Anwendungen:

Lambda-Kalkül als universelles Modell

Fixpunkt-Kombinatoren

Anwendung:

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

Beispiel: \(f (\lambda z.z) 7 = 7\cdot (\lambda z.z) 6=7\cdot 6\), \(f (\lambda z.z) 0 = 1\);

\(\Theta f 7 \to_\beta^* 7 \cdot (f (\Theta f) 6) \to_\beta^* 7 \cdot (6 \cdot (f (\Theta f) 5)) \to_\beta^*\dots\)

Lambda-Berechenbarkeit

Satz: (Church, Turing)

Übung Lambda-Kalkül

folgende Aufgaben aus Barendregt: Lambda Calculus, 1984:

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 \((\NN\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

der Operator \(F =\)

\ g -> ( \ x -> if (x==0) then 0
                else 2 + g (x - 1) )

ist stetig auf \((\NN\hookrightarrow \NN)\) (Beispiele nachrechnen!)

Iterative Berechnung des Fixpunktes: \[\begin{aligned} \bot &=& \emptyset \quad \text{überall undefiniert} \\ F \bot &=& \{ (0,0) \} \quad \text{sonst $\bot$} \\ F (F \bot) &=& \{ (0,0),(1,2) \} \quad \text{sonst $\bot$} \\ F^3 \bot &=& \{ (0,0),(1,2),(2,4) \} \quad \text{sonst $\bot$} \end{aligned}\]

Fixpunktberechnung im Interpreter

Erweiterung der abstrakten Syntax:

data Exp = ... | Rec Name Exp

Beispiel

App 
  (Rec g (Abs v (if v==0 then 0 else 2 + g(v-1))))
  5

Bedeutung: Rec x B bezeichnet den Fixpunkt von \((\lambda x.B)\)

Definition der Semantik:

value (E, (\x.B)(Rec x B), v)
-----------------------------
value (E, Rec x B, v)

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)

Simultane Rekursion: letrec

Beispiel (aus: D. Hofstadter, Gödel Escher Bach)

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)\neq g(x)\)?

weitere Beispiele:

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

letrec nach rec

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

Übung Fixpunkte

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

Ausdrücke (mit Nebenwirkungen):

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

Resultattyp des Interpreters ändern:

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

semantischen Bereich erweitern:

data Val = ... | ValAddr Addr

Aufruf des Interpreters:

run Store.empty $ value undefined $ ...

Änderung der Hilfsfunktionen

bisher:

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

jetzt:

with_int :: Action Val 
  -> ( Int -> Action Val ) -> Action Val
with_int a k = bind a $ \ v -> case v of
    ValInt i -> k i

Hauptprogramm muß kaum geändert werden (!)

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)

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

Rec n (Abs x b)  ==> 
    a := new 42
    put a ( \ x -> let { n = get a } in b )
    get a

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

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

Übung

Kombinator-Parser

Datentyp für Parser

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

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

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

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)

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

Inferenz allgemeingültige Formeln

Grundbereich: aussagenlog. Formeln mit Variablen und Implikationen, Axiom-Schemata: \(\displaystyle \frac{}{X \to(Y \to X)}, \frac{}{(X\to(Y\to Z)) \to ((X \to Y)\to(X\to Z))}\) Regel-Schema (modus ponens): \(\displaystyle \frac{X\to Y, X}{Y}\)

Beobachtungen/Fragen:

Ausblick: Typen und Daten

Übung: Tupel

Tupel

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 \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]{\)\(}\sigma_2 \iff \exists \tau : \sigma_1 \circ \tau = \sigma_2\)

Beispiele:

Eigenschaften

Unifikation—Definition

Unifikationsproblem

(allgemeinst: infimum bzgl. \(\raisebox{-8pt}[0pt][0pt]{\)\(}\))

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

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

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,

Übung Rekonstruktion

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

Namen

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

module Control.Monad.State where
data State s a = State ( s -> ( a, s ) ) 
get :: State s s ; put :: s -> State ()
evalState :: State s a -> s -> a

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

Teilweise Auswertung

Partial Evaluation

Umrechnung zw. Continuations (I)

id2mc :: Name -> ExpValue -> Transform ExpCPS
id2mc c = \ v-> return $ MultiApp (Ref c) [v] 

Anwendung bei Abstraktion

 Abs x b -> \ k -> do
     c <- fresh "k"
     b' <- cps b ( id2mc c )
     k $ MultiAbs [ x, c ] b' -- Ansatz

tatsächlich statt letzter Zeile:

     fresh_let (return $ MultiAbs [f,c] b') k

mit Hilfsfunktion

fresh_let t k  = do 
     f <- fresh "l" ; a <- t
     b <- k ( Ref f ) ; return $ Let f a b

Umrechnung zw. Continuations (II)

mc2exp :: Cont -> Transform ExpCPS
mc2exp k = do
    e <- fresh "e" ; out <- k (Ref e)
    return $ MultiAbs [e] out

Anwendung:

App f a -> \ k ->
  cps f $ \ f' -> 
  cps a $ \ a' -> do -- Ansatz:
    x <- mc2exp k;return $ MultiApp f'[a',x]

tatsächlich statt Ansatz:

    fresh_let ( mc2exp k ) $ \ x -> 
        return $ MultiApp f' [ a', x ]

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 -> Transform ExpCPS
cps :: Exp -> Cont -> Transform 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 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,\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{lift}(\lambda x.\lambda y.y x) = \operatorname{lift}_x(\operatorname{lift}_y(y x)) = \operatorname{lift}_x(S I (K x)) = S (K( S I )) (S (K K) I)\)

Registervergabe

Motivation

Plan (I)

Plan (II)

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,\ldots,R_k\) stehen)

Compiler-Übungen

(ist gleichzeitig Wiederholung Rekursion)

1. implementiere 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

2. ergänze das Programm, so daß \(5!\) ausgerechnet wird

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