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