Übung (Haskell)

Wiederholung Haskell
- Interpreter/Compiler: ghci http://haskell.org/
- Funktionsaufruf nicht f(a,b,c+d), sondern f a b (c+d)
- Konstruktor beginnt mit Großbuchstabe und ist auch eine Funktion
Wiederholung funktionale Programmierung/Entwurfsmuster
- rekursiver algebraischer Datentyp (ein Typ, mehrere Konstruktoren)
  
  (OO: Kompositum, ein Interface, mehrere Klassen)
- rekursive Funktion
Wiederholung Pattern Matching:
- beginnt mit case ... of, dann Zweige
- jeder Zweig besteht aus Muster und Folge-Ausdruck
- falls das Muster paßt, werden die Mustervariablen gebunden und der Folge-Ausdruck auswertet

Übung (Interpreter)

Benutzung:
- Beispiel für die Verdeckung von Namen bei geschachtelten Let
- Beispiel dafür, daß der definierte Name während seiner Definition nicht sichtbar ist
Erweiterung:

Verzweigungen mit C-ähnlicher Semantik:

Bedingung ist arithmetischer Ausdruck, verwende 0 als Falsch und alles andere als Wahr.
```
data Exp = ...
         | If Exp Exp Exp
```
Quelltext-Archiv: siehe https://gitlab.imn.htwk-leipzig.de/waldmann/cb-ws15

Motivation

inferieren $=$ ableiten
Inferenzsystem $I$, Objekt $O$,

Eigenschaft $I\vdash O$ (in $I$ gibt es eine Ableitung für $O$)
damit ist $I$ eine Spezifikation einer Menge von Objekten
man ignoriert die Implementierung ($=$ das Finden von Ableitungen)
Anwendungen im Compilerbau:

Auswertung von Programmen, Typisierung von Programmen

Definition

ein Inferenz-System $I$ besteht aus

Regeln (besteht aus Prämissen, Konklusion)

Schreibweise $\frac{P_1, \ldots, P_n}{K}$
Axiomen ($=$ Regeln ohne Prämissen)

eine Ableitung für $F$ bzgl. $I$ ist ein Baum:

jeder Knoten ist mit einer Formel beschriftet
jeder Knoten (mit Vorgängern) entspricht Regel von $I$
Wurzel (Ziel) ist mit $F$ beschriftet

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

Das Ableiten als Hüll-Operation

für Inferenzsystem $I$ über Bereich $O$

und Menge $M \subseteq O$ definiere

$\displaystyle M^\vdash := \{ K \mid \frac{P_1, \ldots, P_n}{K}\in I, P_1\in M,\ldots,P_n\in M\}$.
Übung: beschreibe $\emptyset^\vdash$.
Satz: $\{ F \mid I\vdash F\}$ ist die bzgl. $\subseteq$ kleinste Menge $M$ mit $M^\vdash\subseteq M$

Bemerkung: die kleinste: Existenz? Eindeutigkeit?
Satz: $\displaystyle \{ F \mid I\vdash F\} = \bigcup_{i\ge 0} M_i$ mit $M_0=\emptyset, \forall i: M_{i+1}=M_i^\vdash$

Regel-Schemata

um unendliche Menge zu beschreiben, benötigt man unendliche Regelmengen
diese möchte man endlich notieren
ein Regel-Schema beschreibt eine (mglw. unendliche) Menge von Regeln, Bsp: $\displaystyle\frac{(x,y)}{(x-y,y)}$
Schema wird instantiiert durch Belegung der Schema-Variablen

Bsp: Belegung $x\mapsto 13, y\mapsto 5$

ergibt Regel $\displaystyle\frac{(13,5)}{(8,5)}$

Inferenz-Systeme (Beispiel 1)

Grundbereich $=$ Zahlenpaare $\ZZ\times\ZZ$
Axiom: \[\frac{}{(13,5)}\]
Regel-Schemata: \[\frac{(x,y)}{(x-y,y)},\quad \frac{(x,y)}{(x,y-x)}\]

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

Inferenz-Systeme (Beispiel 2)

Grundbereich: Zeichenketten aus $\{0,1\}^*$
Axiom: \[\frac{}{01}\]
Regel-Schemata (für jedes $u,v$): \[\frac{0u, v0}{u1v}, \quad \frac{1u,v1}{u0v}, \quad \frac{u}{\operatorname{reverse}(u)}\]

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

Inferenz-Systeme (Beispiel 3)

Grundbereich: endliche Folgen von ganzen Zahlen
Axiome: jede konstante Folge (Bsp. $[3,3,3,3]$)
Schlußregeln:
- swap$_k$: $\displaystyle \frac {[\ldots,x_k,x_{k+1},\ldots]} {[\ldots,x_{k+1}+1,x_k-1,\ldots]}$
- rotate: $\displaystyle \frac {[x_1,\ldots,x_n]} {[x_2,\ldots,x_n,x_1]}$

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

jede Folge der Form $[z,0,\ldots,0]$ ist ableitbar
Invarianten, $[5,3,3]$ ist nicht ableitbar

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

Inferenz von Werten

Grundbereich: Aussagen der Form $\operatorname{\mathsf{wert}}(p,z)$ mit $p \in \texttt{Exp}$ , $z\in \ZZ$
```
data Exp = Const Integer
         | Plus Exp Exp
         | Times Exp Exp
```
Axiome: $\operatorname{\mathsf{wert}}(\texttt{Const} z,z)$
Regeln:

$\displaystyle \frac{\operatorname{\mathsf{wert}}(X,a),\operatorname{\mathsf{wert}}(Y,b)} {\operatorname{\mathsf{wert}}(\texttt{Plus} ~ X ~ Y,a+b)}, \quad \frac{\operatorname{\mathsf{wert}}(X,a),\operatorname{\mathsf{wert}}(Y,b)} {\operatorname{\mathsf{wert}}(\texttt{Times} ~ X ~ Y,a\cdot b)}, \dots$

Umgebungen (Spezifikation)

Grundbereich: Aussagen der Form $\operatorname{\mathsf{wert}}(E,p,z)$

(in Umgebung $E$ hat Programm $p$ den Wert $z$)

Umgebungen konstruiert aus $\emptyset$ und $E[v:=b]$
Regeln für Operatoren $\displaystyle \frac{\operatorname{\mathsf{wert}}(E,X,a),\operatorname{\mathsf{wert}}(E,Y,b)} {\operatorname{\mathsf{wert}}(E,\texttt{Plus} X Y,a+b)},\dots$
Regeln für Umgebungen $\displaystyle \frac{}{\operatorname{\mathsf{wert}}(E[v:=b],v,b)}, \quad \frac{\operatorname{\mathsf{wert}}(E,v',b')}{\operatorname{\mathsf{wert}}(E[v:=b],v',b')}$ für $v \neq v'$
Regeln für Bindung: $\displaystyle \frac{\operatorname{\mathsf{wert}}(E,X,b), \operatorname{\mathsf{wert}}(E[v:=b],Y,c)}{\operatorname{\mathsf{wert}}(E,\mathtt{let~} v=X \mathtt{~in~} Y,c)}$

Umgebungen (Implementierung)

Umgebung ist (partielle) Funktion von Name nach Wert

Realisierungen: type Env = String -> Integer

Operationen:

empty :: Env leere Umgebung
lookup :: Env -> String -> Integer

Notation: $e(x)$
extend :: Env -> String -> Integer -> Env

Notation: $e[v := z]$

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:

Axiome: Klauselmenge einer Formel,
Regel:
- Prämissen: Klauseln $K_1, K_2$ mit $v\in K_1, \neg v \in K_2$
- Konklusion: $(K_1\setminus \{v\}) \cup (K_2 \setminus \{\neg v\})$

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:

$\Rightarrow$ : Gegeben ist die nicht erfüllbare Formel. Gesucht ist eine Ableitung für die leere Klausel. Methode: Induktion nach Anzahl der in der Formel vorkommenden Variablen.
$\Leftarrow$ : Gegeben ist die Ableitung der leeren Klausel. Zu zeigen ist die Nichterfüllbarkeit der Formel. Methode: Induktion nach Höhe des Ableitungsbaumes.

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.

$A \to (B \to A)$
$(A \to (B \to C)) \to ((A \to B) \to (A \to C))$
$(\neg A \to \neg B) \to ((\neg A \to B) \to A)$

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

Korrektheit: jede ableitbare Aussage ist allgemeingültig
Vollständigkeit: jede allgemeing. Aussage ist ableitbar

Semantische Bereiche

bisher: Wert eines Ausdrucks ist Zahl.

jetzt erweitern (Motivation: if-then-else mit richtigem Typ):

data Val = ValInt Int
         | ValBool Bool

Dann brauchen wir auch

data Val = ... | ValErr String
vernünftige Notation (Kombinatoren) zur Einsparung von Fallunterscheidungen bei Verkettung von Rechnungen
```
with_int  :: Val -> (Int  -> Val) -> Val
```

Continuations

Programmablauf-Abstraktion durch Continuations:

Definition:

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

Benutzung:

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

Aufgaben: if/then/else mit with_bool, relationale Operatoren (==, <, o.ä.), Boolesche Konstanten.

Beispiele

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

Prozedur, sog. Funktion, Methode, Operator, Delegate, anonymes Unterprogramm
allgemeinstes Modell: Kalkül der anonymen Funktionen (Lambda-Kalkül),

Interpreter mit Funktionen

abstrakte Syntax:

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

konkrete Syntax:

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

let { x = A } in Q

kann übersetzt werden in

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

wird übersetzt in …
beachte: das ist nicht das let aus Haskell

Mehrstellige Funktionen

…simulieren durch einstellige:

mehrstellige Abstraktion:

\ x y z -> B := \x -> (\y -> (\z -> B ))

mehrstellige Applikation:
```
f P Q R    :=   ((f P) Q) R
```
(die Applikation ist links-assoziativ)
der Typ einer mehrstelligen Funktion:
```
T1 -> T2 -> T3 -> T4   :=
   T1 -> (T2 -> (T3 -> T4))
```
(der Typ-Pfeil ist rechts-assoziativ)

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:

Closure konstruieren:

$\displaystyle \frac{ }{\operatorname{\mathsf{wert}}(E,\lambda n.b,\operatorname{\mathsf{Clos}}(E,n,b)) }$
Closure benutzen:

$\displaystyle \frac{ \begin{array}{c} \operatorname{\mathsf{wert}}(E_1,f,\operatorname{\mathsf{Clos}}(E_2,n,b)), \operatorname{\mathsf{wert}}(E_1,a,w), \\ \operatorname{\mathsf{wert}}(E_2[n:=w],b,r) \end{array} } {\operatorname{\mathsf{wert}}(E_1,f a,r)}$

Rekursion?

Das geht nicht, und soll auch nicht gehen:
```
let { x = 1 + x } in x
```

aber das hätten wir doch gern:

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

(nächste Woche)

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

Testfall (2)

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

auf dem Papier den Wert bestimmen
mit Haskell ausrechnen
mit selbstgebautem Interpreter ausrechnen

Motivation

1. intensionale Modellierung von Funktionen,

intensional: Fkt. ist Berechnungsvorschrift, Programm
(extensional: Fkt. ist Menge v. geordneten Paaren)

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

Analysis: $\int x^2 \operatorname{d}x, \sum_{k=0}^n k^2$
Logik: $\forall x \in A: \forall y\in B: P(x,y)$
Programmierung: static int foo (int x) { ... }

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

(Variable) wenn $x \in V$, dann $x\in \Lambda$
(Applikation) wenn $F\in \Lambda, A\in \Lambda$, dann $(F A)\in\Lambda$
(Abstraktion) wenn $x\in V,B\in\Lambda$, dann $(\lambda x.B)\in\Lambda$

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

Applikation als links-assoziativ auffassen:

\[(\dots ((F A_1) A_2) \dots A_n) \sim F A_1 A_2 \dots A_n\]

Beispiel: $((x z)(y z)) \sim x z (y z)$
geschachtelte Abstraktionen unter ein Lambda schreiben:

\[\lambda x_1.(\lambda x_2. \dots (\lambda x_n.B)\dots) \sim \lambda x_1 x_2 \dots x_n . B\]

Beispiel: $\lambda x.\lambda y.\lambda z.B \sim \lambda x y z.B$
die vorigen Abkürzungen sind sinnvoll, denn $(\lambda x_1 \dots x_n.B)A_1 \dots A_n$ verhält sich wie eine Anwendung einer mehrstelligen Funktion.

Gebundene Variablen

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

$\operatorname{FV}(x)= \{x\}$
$\operatorname{FV}(F A)= \operatorname{FV}(F) \cup \operatorname{FV}(A)$
$\operatorname{FV}(\lambda x.B) = \operatorname{FV}(B) \setminus \{x\}$

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

$\operatorname{BV}(x)= \emptyset$

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

$A$ ist Variable (2 Fälle)
$A$ ist Applikation
$A$ ist Abstraktion
- $(\lambda x.B)[x := N] = \lambda x.B$
- $(\lambda y.B)[x := N] = \lambda y. (B[x:=N])$,
  
  falls $x\neq y$ und $\operatorname{BV}(\lambda y.B)\cap\operatorname{FV}(N)=\emptyset$

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

Axiom: $(\lambda x.B)\to_\alpha(\lambda y. B[x:=y])$ falls $y\notin V(B)$.

und Substitution erlaubt
Abschluß unter Kontext:

$\displaystyle\frac{F\to_\alphaF'}{(F A)\to_\alpha(F' A)}$, $\displaystyle\frac{A\to_\alphaA'}{(F A)\to_\alpha(F A')}$, $\displaystyle\frac{B\to_\alphaB'}{\lambda x.B\to_\alpha\lambda x.B'}$

$\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$,

dann $[x]_R$ (die $R$-Äquivalenzklasse von $x$)

$[x]_R:= \{ y \mid R(x,y) \}$.
$M/R$ (die Menge der $R$-Klassen von $M$)

$M/R := \{ [x]_R \mid x\in M \}$.

Beispiele:

$\QQ = \ZZ^2/R$ mit $R((x_1,x_2),(y_1,y_2)))= \dots$
$\ZZ = \NN^2/R$ mit …
Nerode-Kongruenz einer formalen Sprache

Ableitungen

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

Axiom: $(\lambda x.B)A \to_\betaB[x:=A]$

ein Term der Form $(\lambda x.B)A$ heißt Redex ($=$ reducible expression)
Abschluß unter Kontext:

$\displaystyle\frac{F\to_\betaF'}{(F A)\to_\beta(F' A)}$, $\displaystyle\frac{A\to_\betaA'}{(F A)\to_\beta(F A')}$, $\displaystyle\frac{B\to_\betaB'}{\lambda x.B\to_\beta\lambda x.B'}$

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

konfluent

$\forall A,B,C\in\Lambda: A\to_\beta^*B \wedge A\to_\beta^* C \Rightarrow \exists D\in\Lambda: B\to_\beta^*D \wedge C\to_\beta^* D$
(Folgerung: jeder Term hat höchstens eine Normalform)
aber nicht terminierend (es gibt Terme mit unendlichen Ableitungen)

$W=\lambda x.xx, \Omega = WW$.
es gibt Terme mit Normalform und unendlichen Ableitungen, $KI\Omega$ mit $K=\lambda xy.x, I=\lambda x.x$

Daten als Funktionen

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

Konstruktor: $\langle D_1,\ldots,D_k\rangle \Rightarrow \lambda s. s D_1 \ldots D_k$
Selektoren: $s_i \Rightarrow \lambda t . t (\lambda d_1 \ldots d_k.d_i)$

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

Anwendungen:

Auflösung simultaner Rekursion
Modellierung von Zahlen

Lambda-Kalkül als universelles Modell

Wahrheitswerte:

$\operatorname{\sf True}= \lambda x y.x, \operatorname{\sf False}= \lambda x y .y$

(damit läßt sich if-then-else leicht aufschreiben)
natürliche Zahlen:

$0 = \lambda x.x; (n+1) = \langle\operatorname{\sf False},n\rangle$

(damit kann man leicht $x > 0$ testen)
Rekursion?

Fixpunkt-Kombinatoren

Definition: $\Theta =(\lambda x y. (y (x x y))) (\lambda x y. (y (x x y)))$
Satz: $\Theta f \to_\beta^* f(\Theta f)$, d. h. $\Theta f$ ist Fixpunkt von $f$
d.h. $\Theta$ ist Fixpunkt-Kombinator, (T wegen Turing)
Folgerung: im Lambda-Kalkül kann man beliebige Wiederholung (Schachtelung) von Rechnungen beschreiben

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)

Menge der Turing-berechenbaren Funktionen

(Zahlen als Wörter auf Band)

Alan Turing: On Computable Numbers, with an Application to the Entscheidungsproblem, Proc. LMS, 2 (1937) 42 (1) 230–265 https://dx.doi.org/10.1112/plms/s2-42.1.230
Menge der Lambda-berechenbaren Funktionen

(Zahlen als Lambda-Ausdrücke)

Alonzo Church: A Note on the Entscheidungsproblem, J. Symbolic Logic 1 (1936) 1, 40–41
Menge der while-berechenbaren Funktionen

(Zahlen als Registerinhalte)

Übung Lambda-Kalkül

Konstruktor und Selektoren für Paare
Test, ob der Nachfolger von 0 gleich 0 ist

(mit $\lambda$-kodierten Zahlen)
Fakultät mittels $\Theta$

(mit echten Zahlen und Operationen)

folgende Aufgaben aus Barendregt: Lambda Calculus, 1984:

(Aufg. 6.8.2) Konstruiere $K^\infty \in\Lambda^0$ (ohne freie Variablen) mit $K^\infty x = K^\infty$ (hier und in im folgenden hat $=$ die Bedeutung $\equiv_\beta$)

Konstruiere $A\in\Lambda^0$ mit $A x = x A$
beweise den Doppelfixpunktsatz (Kap. 6.5)

$\forall F,G : \exists A,B: A = FAB \wedge B = GAB$
(Aufg. 6.8.14, J.W.Klop) \[\begin{aligned} &&X = \lambda abcdefghijklmnopqstuvvxyzr. \\ && \qquad r(thisisafixedpointcombinator) \\ &&Y = X^{27}=\underbrace{X\dots X}_{27}\end{aligned}\] Zeige, daß $Y$ ein Fixpunktkombinator ist.

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.

CPO $=$ complete partial order $=$ vollständige Halbordnung
complete $=$ jede monotone Folge besitzt Supremum ($=$ kleinste obere Schranke)
pointed: $C$ hat kleinstes Element $\bot$

Beispiele f. Halbordnungen, CPOs

Halbordnung? pointed? complete?

$\le$ auf $\NN$
$\le$ auf $\NN\cup \{+\infty\}$
$\le$ auf $\{ x \mid x\in \RR, 0\le x \le 1 \}$
$\le$ auf $\{ x \mid x\in \QQ, 0\le x \le 1 \}$
Teilbarkeit auf $\NN$
Präfix-Relation auf $\Sigma^*$
$\{((x_1,y_1),(x_2,y_2)) \mid (x_1\le x_2) \vee (y_1\le y_2) \}$ auf $\RR^2$
$\{((x_1,y_1),(x_2,y_2)) \mid (x_1\le x_2) \wedge (y_1\le y_2) \}$ auf $\RR^2$
identische Relation $\operatorname{id}_M$ auf einer beliebigen Menge $M$
$\{(\bot,x)\mid x\in M_\bot\}\cup \operatorname{id}_M$ auf $M_\bot := \{\bot\}\cup M$

Stetige Funktionen

$f$ ist stetig $:=$

$f$ ist monoton: $x\le y\Rightarrow f(x)\le f(y)$
und für monotone Folgen $[x_0,x_1,\ldots]$ gilt: $f (\sup [x_0,x_1,\ldots])=\sup [f(x_0),f(x_1),\ldots]$

Beispiele: in $(\NN\cup\{+\infty\},\le)$

$x\mapsto 42$ ist stetig
$x\mapsto$ if $x<+\infty$ then $x+1$ else $+\infty$
$x\mapsto$ if $x<+\infty$ then $42$ else $+\infty$

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

Menge der partiellen Funktionen von $B$ nach $B$:

$C = (B\hookrightarrow B)$
partielle Funktion $f:B\hookrightarrow B$
entspricht totaler Funktion $f: B\rightarrow B_\bot$
$C$ geordnet durch $f\le g \iff \forall x\in B: f(x) \le g(x)$,

wobei $\le$ die vorhin definierte CPO auf $B_\bot$
$f\le g$ bedeutet: $g$ ist Verfeinerung von $f$
Das Bottom-Element von $C$ ist die überall undefinierte Funktion. (diese heißt auch $\bot$)

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.

Zahlen: nicht pointed

(arithmetische Operatoren sind strikt)
Funktionen: partiell $\Rightarrow$ pointed

($\bot$ ist überall undefinierte Funktion)
Daten (Listen, Bäume usw.): pointed:

(Konstruktoren sind nicht strikt)

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

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

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

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?

$C=$ Menge der Formalen Sprachen über $\Sigma$, halbgeordnet durch $\subseteq$. ist CPO? pointed?

$h: C\to C: L\mapsto \{\epsilon\}\cup L\cdot \{ab\}$ ist stetig?

Fixpunkt(e) von $h$?

Motivation

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

direktes Rechnen auf von-Neumann-Maschine: Änderungen im Hauptspeicher
direkte Modellierung von Prozessen mit Zustandsänderungen ((endl.) Automaten)

Dazu muß semantischer Bereich geändert werden.

bisher: Val, jetzt: State -> (State, Val)
(dabei ist (A,B) die Notation für $A\times B$)

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

Speicher

import qualified Data.Map as M

http://hackage.haskell.org/packages/archive/containers/0.5.0.0/doc/html/Data-Map-Lazy.html

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

spezifische Aktionen:

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

Aktion ausführen, Resultat liefern:

run :: Store -> Action a -> a

Auswertung von Ausdrücken

Ausdrücke (mit Nebenwirkungen):

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

Resultattyp des Interpreters ändern:

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

semantischen Bereich erweitern:

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

Aufruf des Interpreters:

run Store.empty $ evaluate undefined $ ...

Änderung der Hilfsfunktionen

bisher:

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

jetzt:

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

Hauptprogramm muß kaum geändert werden (!)

Speicher-Aktionen als Monade

generische Aktionen/Verknüpfungen:

nichts tun (return), $\bullet$ nacheinander (bind, >>=)

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

Variablen?

in unserem Modell haben wir:

veränderliche Speicherstellen,
aber immer noch unveränderliche Variablen (lokale Namen)

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

Imperative Programmierung

es fehlen noch wesentliche Operatoren:

Nacheinanderausführung (Sequenz)
Wiederholung (Schleife)

diese kann man:

simulieren (durch let)
als neue AST-Knoten realisieren (Übung)

Rekursion

mehrere Möglichkeiten zur Realisierung

mit Fixpunkt-Kombinator (bekannt)
in der Gastsprache des Interpreters

(dabei neu: Fixpunkte von Aktionen)
(neu:) simulieren (in der interpretierten Sprache)

durch Benutzung des Speichers

Rekursion (semantisch)

bisher:

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

jetzt:

import Control.Monad.Fix
class MonadFix m where
    mfix :: ( a -> m a ) -> m a

instance MonadFix Action where
mfix f = Action $ \ s0 -> 
    let Action a = f v
        ( s1, v ) = a s0
    in  ( s1, v )

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

Schleife durch Rekursion ersetzen und Sequenz durch let:
```
fak = let { a = new 1 }
      in  Rec f ( \ n -> ... )
```
Syntaxbaumtyp erweitern um Knoten für Sequenz und Schleife

…unter verschiedenen Aspekten

unsere Motivation: semantischer Bereich,

return :: a -> m a als leere Aktion,

Operator (>>=) :: m a -> (a -> m b) -> m b zum Verknüpfen von Aktionen
auch nützlich: do-Notation (anstatt Ketten von >>=)
die Wahrheit: a monad in X is just a monoid
in the category of endofunctors of X
die ganze Wahrheit:

Functor m => Applicative m => Monad m
weitere Anwendungen: IO, Parser-Kombinatoren

Die Konstruktorklasse Monad

Definition:

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

Benutzung der Methoden:

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

Do-Notation für Monaden

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

do-Notation (explizit geklammert):

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

do-Notation (implizit geklammert):

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

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

Beispiele für Monaden

Aktionen mit Speicheränderung (vorige Woche)

Action (Store -> (Store, a))
Aktionen mit Welt-Änderung: IO a
Transaktionen (Software Transactional Memory) STM a
Aktionen, die möglicherweise fehlschlagen:

data Maybe a = Nothing | Just a
Nichtdeterminismus (eine Liste von Resultaten): [a]
Parser-Monade (nächste Woche)

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

Kategorie $C$ hat Objekte $\operatorname{\text{Obj}}_C$ und Morphismen $\operatorname{\text{Mor}}_C$,

jeder Morphismus $m$ hat als Start ($S$) und Ziel ($T$) ein Objekt, Schreibweise: $m:S\to T$ oder $m\in\operatorname{\text{Mor}}_C(S,T)$
für jedes $O\in\operatorname{\text{Obj}}_C$ gibt es $\operatorname{\text{id}}_O:O\to O$
für $f:S\to M$ und $f:M\to T$ gibt es $f\circ g:S\to T$.

es gilt immer $f\circ \operatorname{\text{id}}=f$, $\operatorname{\text{id}}\circ g=g$, $f\circ(g\circ h)=(f\circ g)\circ h$

Beispiele:

Set: $\operatorname{\text{Obj}}_{\operatorname{\text{Set}}}$ = Mengen, $\operatorname{\text{Mor}}_{\operatorname{\text{Set}}}$ = totale Funktionen
Grp: $\operatorname{\text{Obj}}_{\operatorname{\text{Grp}}}$ = Gruppen, $\operatorname{\text{Mor}}_{\operatorname{\text{Set}}}$ = Homomorphismen
für jede Halbordnung $(M,\le)$: $\operatorname{\text{Obj}}=M,\operatorname{\text{Mor}}=(\le)$
Hask: $\operatorname{\text{Obj}}_{\operatorname{\text{Hask}}}$ = Typen, $\operatorname{\text{Mor}}_{\operatorname{\text{Hask}}}$ = Funktionen

Kategorische Definitionen

Beispiel: Isomorphie

eigentlich: Abbildung, die die Struktur (der abgebildeten Objekte) erhält
Struktur von $O\in \operatorname{\text{Obj}}(C)$ ist aber unsichtbar
Eigenschaften von Objekten werden beschrieben
durch Eigenschaften ihrer Morphismen
(vgl. abstrakter Datentyp, API)

Bsp: $f:A\to B$ ist Isomorphie (kurz: ist iso),
falls es ein $g:B\to A$ gibt mit ${f\circ g=\operatorname{\text{id}}_A }\wedge {g\circ f=\operatorname{\text{id}}_B}$

weiteres Beispiel

$m:a\to b$ monomorph: $\forall f,g: f\circ m=g\circ m\Rightarrow f=g$

Produkte

Def: $P$ ist Produkt von $A_1$ und $A_2$
mit Projektionen $\operatorname{\text{proj}}_1:P\to A_1, \operatorname{\text{proj}}_2:P\to A_2$,

wenn für jedes $B$ und Morphismen $f_1:B\to A_1, f_2:B\to A_2$

es existiert genau ein $g:B\to P$
mit $g\circ\operatorname{\text{proj}}_1=f_1$ und $g\circ\operatorname{\text{proj}}_2=f_2$
für Set ist das wirklich das Kreuzprodukt
für die Kategorie einer Halbordnung?
für Gruppen? (Beispiel?)

Dualität

Wenn ein Begriff kategorisch definiert ist,

erhält man den dazu dualen Begriff
durch Spiegeln aller Pfeile
Bsp: dualer Begriff zu Produkt:

Definition hinschreiben, Beispiele angeben
Bsp: dualer Begriff zu: monomorph
entsprechend: die duale Aussage

diese gilt gdw. die originale (primale) Aussage gilt

Übung (1)

der identische Morphismus jedes Objektes ist eindeutig bestimmt
Def. epi, mono, Dualität, Beispiele
Schubert Satz 6.4.2 (prismatisches Diagramm)
…die dazu duale Aussage
Kategorie der Graphen (was sind die Morphismen?)

Funktoren

Def: Funktor $F$ von Kategorie $C$ nach Kategorie $D$:
- einer Wirkung auf Objekte: ${F_{\operatorname{\text{Obj}}}}:\operatorname{\text{Obj}}(C)\to\operatorname{\text{Obj}}(D)$
- einer Wirkung auf Pfeile: ${F_{\operatorname{\text{Mor}}}}: (g:s\to t)\mapsto (g':{F_{\operatorname{\text{Obj}}}}(S)\to{F_{\operatorname{\text{Obj}}}}(T))$
mit den Eigenschaften:
- ${F_{\operatorname{\text{Mor}}}}(\operatorname{\text{id}}_o)=\operatorname{\text{id}}_{{F_{\operatorname{\text{Obj}}}}(o)}$
- ${F_{\operatorname{\text{Mor}}}}(g\circ_C h)={F_{\operatorname{\text{Mor}}}}(g)\circ_D{F_{\operatorname{\text{Mor}}}}(h)$
Bsp: Funktoren zw. Kategorien von Halbordnungnen?

class Functor f where 
  fmap :: (a -> b) -> (f a -> f b)

Beispiele: List, Maybe, Action

Die Kleisli-Konstruktion

Plan: für Kategorie $C$, Endo-Funktor $F :C\to C$

definiere sinnvolle Struktur auf Pfeilen $s \to F t$
Durchführung: die Kleisli-Kategorie $K$ von $F$:

$\operatorname{\text{Obj}}(K)=\operatorname{\text{Obj}}(C)$, Pfeile: $s\to F t$
…$K$ ist tatsächlich eine Kategorie, wenn:
- identische Morphismen (return), Komposition (>=>)
- mit passenden Eigenschaften
$(F,\verb|return|,\verb|(>=>)|)$ heißt dann Monade

Diese Komposition ist

f >=> g  =  \ x -> (f x >>= g)

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 konstant ist

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

Übung (2)

Funktor- und Monadengesetze ausprobieren (ghci)
falsche Functor- und Monad-Instanzen für Maybe, List, Tree

(d.h. typkorrekt, aber semantisch falsch)
optional: inverse Zustandsmonade

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 )

Monaden: Zusammenfassung

verwendet zur Definition semantischer Bereiche,
Monade $=$ Monoid über Endofunktoren in Hask,

(Axiome für return, >=> bzw. >>=)
Notation do { x <- foo ; bar ; .. }

(>>= ist das benutzer-definierte Semikolon)
Grundlagen: Kategorien-Theorie (ca. 1960),

in Funktl. Prog. seit ca. 1990 http://homepages.inf.ed.ac.uk/wadler/topics/monads.html
in anderen Sprachen: F#: Workflows, C#: LINQ-Syntax
GHC ab 7.10: Control.Applicative: pure und <*>

($=$ return und eingeschränktes >>=)

Datentyp für Parser

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

über Eingabestrom von Zeichen (Token) $c$,
mit Resultattyp $a$,
nichtdeterministisch (List).

Beispiel-Parser, Aufrufen mit:

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

Elementare Parser (I)

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

Monadisches Verketten von Parsern

Definition:

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

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

Anwendungsbeispiel:

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

Elementare Parser (II)

satisfy :: ( c -> Bool ) -> Parser c c
satisfy p = do 
    x <- next 
    if p x then return x else reject

expect :: Eq c => c -> Parser c c
expect c = satisfy ( == c )

ziffer :: Parser Char Integer
ziffer = do 
    c <- satisfy Data.Char.isDigit
    return $ fromIntegral 
           $ fromEnum c - fromEnum '0'

Kombinatoren für Parser (I)

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

Auswahl (or)

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

Wiederholung (beliebig viele)

many, many1 :: Parser c a -> Parser c [a]
many p = many1 p <|> return [] 
many1 p = do x <- p; xs <- many p; return $ x : xs

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

Kombinator-Parser und Grammatiken

Grammatik mit Regeln $S \to a S b S, S \to \epsilon$ entspricht

s :: Parser Char ()
s =   do { expect 'a' ; s ; expect 'b' ; s } 
  <|> return ()

Anwendung: exec "abab" $ do s ; eof

Robuste Parser-Bibliotheken

Designfragen:

asymmetrisches <|>
Nichtdeterminismus einschränken
Fehlermeldungen (Quelltextposition)

Beispiel: Parsec (Autor: Daan Leijen) http://www.haskell.org/haskellwiki/Parsec

Asymmetrische Komposition

gemeinsam:

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

symmetrisch: p s ++ q s
asymmetrisch: if null p s then q s else p s

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

Nichtdeterminismus einschränken

Nichtdeterminismus $=$ Berechnungsbaum $=$ Backtracking
asymmetrisches p <|> q : probiere erst p, dann q
häufiger Fall: p lehnt sofort ab

Festlegung (in Parsec): wenn p wenigstens ein Zeichen verbraucht, dann wird q nicht benutzt (d. h. p muß erfolgreich sein)

Backtracking dann nur durch try p <|> q

Fehlermeldungen

Fehler $=$ Position im Eingabestrom, bei der es nicht weitergeht
und auch durch Backtracking keine Fortsetzung gefunden wird
Fehlermeldung enthält:
- Position
- Inhalt (Zeichen) der Position
- Menge der Zeichen mit Fortsetzung

Pretty-Printing (I)

John Hughes’s and Simon Peyton Jones’s Pretty Printer Combinators

Based on The Design of a Pretty-printing Library in Advanced Functional Programming, Johan Jeuring and Erik Meijer (eds), LNCS 925

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

Pretty-Printing (II)

data Doc abstrakter Dokumententyp, repräsentiert Textblöcke
Konstruktoren:
```
text :: String -> Doc
```

Kombinatoren:

vcat       :: [ Doc ] -> Doc -- vertikal
hcat, hsep :: [ Doc ] -> Doc -- horizontal

Ausgabe: render :: Doc -> String

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

original: Funktion gibt Wert zurück
```
f == (abs (x y) (let ( ... ) v))
```
cps: Funktion erhält zusätzliches Argument, das ist eine Fortsetzung (continuation), die den Wert verarbeitet:
```
f-cps == (abs (x y k) (let ( ... ) (k v))
```

aus g (f 3 2) wird f-cps 3 2 g-cps

Motivation

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

CPS als einheitlicher Mechanismus für

Linearisierung (sequentielle Anordnung von primitiven Operationen)
Ablaufsteuerung (Schleifen, nicht lokale Sprünge)
Unterprogramme (Übergabe von Argumenten und Resultat)
Unterprogramme mit mehreren Resultaten

CPS für Linearisierung

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

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

plus x y k = k (x + y)
mal  x y k = k (x * y)

später tatsächlich als Programmtransformation (Kompilation)

CPS für Resultat-Tupel

wie modelliert man Funktion mit mehreren Rückgabewerten?

benutze Datentyp Tupel (Paar):
```
f : A -> (B, C)
```
benutze Continuation:
```
f/cps : A -> (B -> C -> D) -> D
```

CPS/Tupel-Beispiel

erweiterter Euklidischer Algorithmus:

prop_egcd x y = 
    let (p,q) = egcd x y
    in  (p*x + q*y) == gcd x y

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

vervollständige, übersetze in CPS

CPS für Ablaufsteuerung

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:

Syntax: Label, Jump, Parser
Semantik:
- Verkettung durch >>= aus instance Monad CPS
- Einbetten von Action Val durch lift
- evaluate für bestehende Sprache (CBV)
- evaluate für label und jump

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

Parser für \x y z -> ..., benutze foldr
Parser für let { f x y = ... } in ...
Parser für let { a = b ; c = d ; ... } in ..
Text.Parsec.Combinator.notFollowedBy zur Erkennung von Schlüsselwörtern
Ziffern in Bezeichnern

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

Beschreibe die Auswertung (Datei ex4.hs)

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

jump (label x x) (label y y)

Ersetze undefined, so daß f x = x! (Datei ex5.hs)

let { triple x y z = \ s -> s x y z 
    ; fst t = t ( \ x y z -> x )
    ; snd t = t ( \ x y z -> y )
    ; thd t = t ( \ x y z -> z )
    ; f x = let { p = label start undefined
                ; loop = fst p ; n = snd p ; a = thd p
                } in if  0 == n then a 
                     else loop (triple loop (n - 1) (n * a))
    } in f 5

Grundlagen

Typ $=$ statische Semantik

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

formale Beschreibung:

$P$: Menge der Ausdrücke (Programme)
$T$: Menge der Typen
Aussagen $p :: t$ (für $p\in P$, $t\in T$)
- prüfen oder
- herleiten (inferieren)

Inferenzsystem für Typen (Syntax)

Grundbereich: Aussagen der Form $E \vdash X : T$

(in Umgebung $E$ hat Ausdruck $X$ den Typ $T$)
Menge der Typen:
- primitiv: Int, Bool
- zusammengesetzt:
  - Funktion $T_1 \to T_2$
  - Verweistyp $\operatorname{Ref}T$
  - Tupel $(T_1, \ldots, T_n)$, einschl. $n=0$
Umgebung bildet Namen auf Typen ab

Inferenzsystem für Typen (Semantik)

Axiome f. Literale: $E \vdash \text{Zahl-Literal} : \text{Int}$, …
Regel für prim. Operationen: $\displaystyle \frac{E\vdash X : \text{Int},E\vdash Y : \text{Int}} {E \vdash (X+Y) : \text{Int}}$, …
Abstraktion/Applikation: …
Binden/Benutzen von Bindungen: …

hierbei (vorläufige) Design-Entscheidungen:

Typ eines Ausdrucks wird inferiert
Typ eines Bezeichners wird …
- in Abstraktion: deklariert
- in Let: inferiert

Inferenz für Let

(alles ganz analog zu Auswertung von Ausdrücken)

Regeln für Umgebungen
- $\displaystyle E[v:=t] \vdash v : t$
- $\displaystyle \frac{E \vdash v' : t'}{E[v:=t] \vdash v' : t'}$ für $v \neq v'$
Regeln für Bindung: \[\frac{E\vdash X : s, \quad E [v:=s] \vdash Y : t} {E \vdash \mathtt{let~} v=X \mathtt{~in~} Y : t}\]

Applikation und Abstraktion

Applikation: \[\frac{E\vdash F : T_1 \to T_2, \quad E \vdash A : T_1} {E \vdash (F A) : T_2}\]

vergleiche mit modus ponens
Abstraktion (mit deklariertem Typ der Variablen)

\[\frac{E[v:=T_1] \vdash X : T_2} {E\vdash (\lambda (v :: T_1) X) : T_1 \to T_2}\]

Eigenschaften des Typsystems

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

jedes Programm hat höchstens einen Typ
nicht jedes Programm hat einen Typ.

Der $Y$-Kombinator $(\lambda x.xx)(\lambda x.xx)$ hat keinen Typ
jedes getypte Programm terminiert

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

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

Motivation

ungetypt:

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

einfach getypt nur so möglich:

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

wie besser?

Typ-Argumente (Beispiel)

Typ-Abstraktion, Typ-Applikation:

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

zur Laufzeit werden die Abstraktionen und Typ-Applikationen ignoriert

Typ-Argumente (Regeln)

neuer Typ $\forall t.T$,

neue Ausdrücke mit Inferenz-Regeln:

Typ-Abstraktion: erzeugt parametrischen Typ

\[\frac{E \vdash \dots } {E \vdash \Lambda t\to X : \dots}\]
Typ-Applikation: instantiiert param. Typ

\[\frac{E \vdash F : \dots}{E \vdash F\langle T_2\rangle : \dots}\]

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

Inferenz allgemeingültige Formeln

Grundbereich: aussagenlogische Formeln (mit Variablen und Implikation)

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:

Übung (autotool): Leite $p\to p$ ab.
(Korrektheit): jede ableitbare Formel ist allgemeingültig
(Vollständigkeit): sind alle allgemeingültigen Formeln (in dieser Signatur) ableitbar?

Typen und Daten

bisher: Funktionen von Daten nach Daten

\ (x :: Int) -> x + 1
heute: Funktionen von Typ nach Daten

\ (t :: Type) -> \ (x :: t) -> x
Funktionen von Typ nach Typ (ML, Haskell, Java, C#)

\ (t :: Type) -> List t
Funktionen von Daten nach Typ (dependent types)

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

Sprachen: Cayenne, Coq, Agda

Eigenschaften: Typkorrektheit i. A. nicht entscheidbar,

d. h. Programmierer muß Beweis hinschreiben.

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

$E$: Umgebung (Name $\to$ Typ)
$X$: Ausdruck (Exp)
$T$: Typ
$C$: Menge von Typ-Constraints

wobei

Menge der Typen $T$ erweitert um Variablen
Constraint: Paar von Typen $(T_1, T_2)$
Lösung eines Constraints: Substitution $\sigma$ mit $T_1 \sigma = T_2 \sigma$

Inferenzregeln f. Rekonstruktion (Plan)

Plan:

Aussage $E \vdash X : (T, C)$ ableiten,
dann $C$ lösen (allgemeinsten Unifikator $\sigma$ bestimmen)
dann ist $T \sigma$ der (allgemeinste) Typ von $X$ (in Umgebung $E$)

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

Inferenzregeln? Implementierung? — Testfall:

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

Inferenzregeln f. Rekonstrukion

primitive Operationen (Beispiel)

\[\frac {E \vdash X_1:(T_1,C_1), \quad E \vdash X_2:(T_2,C_2)} {E \vdash X_1 + X_2 : (\text{Int}, \{ T_1=\text{Int},T_2=\text{Int}\}\cup C_1 \cup C_2) }\]
Applikation \[\frac {E \vdash F : (T_1, C_1), \quad E \vdash A : (T_2,C_2)} {E \vdash (F A): \ldots}\]
Abstraktion \[\frac{\ldots}{E\vdash \lambda x.B : \ldots}\]
(Ü) Konstanten, Variablen, if/then/else

Substitutionen (Definition)

Signatur $\Sigma=\Sigma_0\cup\ldots\Sigma_k$,
$\operatorname{Term}(\Sigma,V)$ ist kleinste Menge $T$ mit $V\subseteq T$ und $\forall 0\le i\le k, f\in\Sigma_i, t_1\in T,\ldots,t_i\in T: f(t_1,\ldots,t_i)\in T$.

(hier Anwendung für Terme, die Typen beschreiben)
Substitution: partielle Abbildung $\sigma:V\to\operatorname{Term}(\Sigma,V)$,

Definitionsbereich: $\operatorname{dom}\sigma$, Bildbereich: $\operatorname{img}\sigma$.
Substitution $\sigma$ auf Term $t$ anwenden: $t\sigma$
$\sigma$ heißt pur, wenn kein $v\in\operatorname{dom}\sigma$ als Teilterm in $\operatorname{img}\sigma$ vorkommt.

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:

$\sigma$ pur $\Rightarrow$ $\sigma$ idempotent: $\sigma \circ \sigma= \sigma$
$\sigma_1$ pur $\wedge$ $\sigma_2$ pur impliziert nicht $\sigma_1\circ \sigma_2$ pur

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:

$\{X\mapsto Y\} \raisebox{-8pt}[0pt][0pt]{$$}\{X\mapsto a,Y\mapsto a\}$,
$\{X\mapsto Y\}\raisebox{-8pt}[0pt][0pt]{$$}\{Y\mapsto X\}$,
$\{Y\mapsto X\}\raisebox{-8pt}[0pt][0pt]{$$}\{X\mapsto Y\}.$

Eigenschaften

Relation $\raisebox{-8pt}[0pt][0pt]{$$}$ ist Prä-Ordnung (…, …, aber nicht …)
Die durch $\raisebox{-8pt}[0pt][0pt]{$$}$ erzeugte Äquivalenzrelation ist die …

Unifikation—Definition

Unifikationsproblem

Eingabe: Terme $t_1,t_2\in\operatorname{Term}(\Sigma,V)$
Ausgabe: ein allgemeinster Unifikator (mgu): Substitution $\sigma$ mit $t_1\sigma = t_2\sigma$.

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

Satz: jedes Unifikationsproblem ist

entweder gar nicht
oder bis auf Umbenennung eindeutig

lösbar.

Unifikation—Algorithmus

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

$s$ ist Variable: …
$t$ ist Variable: symmetrisch
$s=(s_1 \to s_2)$ und $t=(t_1 \to t_2)$: …

mgu :: Term -> Term -> Maybe Substitution

Unifikation—Komplexität

Bemerkungen:

gegebene Implementierung ist korrekt, übersichtlich, aber nicht effizient,
(Ü) es gibt Unif.-Probl. mit exponentiell großer Lösung,
eine komprimierte Darstellung davon kann man aber in Polynomialzeit ausrechnen.

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,

Inferenzsystem ähnlich zu Rekonstruktion monomorpher Typen mit Aussagen der Form $E \vdash X : (T, C)$
Umgebung $E$ ist jetzt partielle Abbildung von Name nach Typschema (nicht wie bisher: nach Typ).
Bei Typinferenz für let-gebundene Bezeichner wird über die freien Typvariablen generalisiert.
Dazu Teil-Constraint-Systeme lokal lösen.

Grabmüller 2006

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.65.7733,

Jones 1999

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.134.7274

Tupel

abstrakte Syntax

data Exp = .. | Tuple [Exp] | Nth Exp Int

konkrete Syntax (runde Klammern, Kommas, keine 1-Tupel)
dynamische Semantik: data Val = .. , Interpreter.value
statische Semantik (Typen)
- abstrakte Syntax
- konkrete Syntax (für Typrekonstruktion nicht nötig)
- Typisierung (Inferenzregeln, Implementierung)

Transformationen/Ziel

continuation passing (Programmablauf explizit)
closure conversion (alle Umgebungen explizit)
lifting (alle Unterprogramme global)
Registervergabe (alle Argumente in Registern)

Ziel: maschinen(nahes) Programm mit

globalen (Register-)Variablen (keine lokalen)
Sprüngen (kein return)
automatischer Speicherbereinigung

CPS-Transformation: Spezifikation

(als Schritt im Compiler)

Eingabe: Ausdruck $X$, Ausgabe: Ausdruck $Y$
Semantik: Wert von $X$ $=$ Wert von $Y (\lambda v.v)$
Syntax:
- $X \in\text{Exp}$ (fast) beliebig,
- $Y\in\text{Exp/CPS}$ stark eingeschränkt:
  - keine geschachtelten Applikationen
  - Argumente von Applikationen und Operationen $(+,*,>)$ sind Variablen oder Literale

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/

$\operatorname{CPS}(v)=\lambda k.k v$
$\operatorname{CPS}(F A) = \lambda k.(\operatorname{CPS}(F) (\lambda f. \operatorname{CPS}(A) (\lambda a.f a k) ) )$
$\operatorname{CPS}(\lambda x.B)=\lambda k.k (\lambda x.\operatorname{CPS}(B))$

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

Interpreter (bisher): komplette Auswertung

(Continuations sind Funktionen, werden angewendet)
CPS-Transformator (heute): gar keine Auswertung,

(Continuations sind Ausdrücke)
gemischter Transformator: benutzt sowohl
- Continuations als Ausdrücke (der Zielsprache)
- als auch Continuations als Funktionen (der Gastsprache)
(compile time evaluation, partial evaluation)

Partial Evaluation

bisher: Applikation zur Laufzeit

(Continuation bezeichnet durch Ref k::Exp)

transform  :: Exp -> Transform ExpCPS
transform x = case x of 
 ConstInteger i -> do 
  k<-fresh; return $ Abs k (App (Ref k) x)

jetzt: Applikation während der Transformation

(Continuation bezeichnet durch k::Cont)

type Cont = ExpValue -> Transform ExpCPS
transform :: Exp -> (Cont->Transform ExpCPS)
transform x = case x of 
   ConstInteger i -> \ k -> k x

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

Transformationsregeln für Ref, App, Abs, Let nachvollziehen (im Vergleich zu CPS-Interpreter)
Transformationsregeln für if/then/else, new/put/get hinzufügen
anwenden auf eine rekursive Funktion (z. B. Fakultät),

wobei Rekursion durch Zeiger auf Abstraktion realisiert wird

Motivation

(Literatur: DCPL 17.10) — Beispiel:

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

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

Semantik-Definition (Interpreter) benutzt Umgebung
Transformation (closure conversion, environment conversion) (im Compiler) macht Umgebungen explizit.

Spezifikation

closure conversion:

Eingabe: Programm $P$
Ausgabe: äquivalentes Programm $P'$, bei dem alle Abstraktionen geschlossen sind
zusätzlich: $P$ in CPS $\Rightarrow$ $P'$ in CPS

geschlossen: alle Variablen sind lokal

Ansatz:

Werte der benötigten nicht lokalen Variablen
$\Rightarrow$ zusätzliche(s) Argument(e) der Abstraktion
auch Applikationen entsprechend ändern

closure passing style

Umgebung $=$ Tupel der Werte der benötigten nicht lokalen Variablen
Closure $=$ Paar aus Code und Umgebung

realisiert als Tupel (Code, $\underbrace{W_1, \dots, W_n}_\text{Umgebung}$)

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

Closure-Konstruktion?
Komplette Übersetzung des Beispiels?

Transformation

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

wobei $\{v_1,\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]

für alle anderen Fälle: strukturelle Rekursion
zur Erhaltung der CPS-Form: Spezialfall bei let

Spezifikation

(lambda) lifting:

Eingabe: Programm $P$, bei dem alle Abstraktionen geschlossen sind
Ausgabe: äquivalentes Programm $P'$,
bei dem alle Abstraktionen (geschlossen und) global sind

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

Zustandsmonade zur Namenserzeugung ($g_1, g_2,\ldots)$
Ausgabemonade (WriterT) zum Aufsammeln
$g_1,\ldots, g_k$ dürften nun sogar rekursiv sein (sich gegenseitig aufrufen)

Lambda-Lifting (Plan)

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

bisher: closure conversion $+$ lifting:

(verwendet Tupel)
Alternative: lambda lifting

(reiner $\lambda$-Kalkül, keine zusätzlichen Datenstrukturen)

Lambda-Lifting (Realisierung)

verwendet Kombinatoren (globale Funktionen)

$I=\lambda x.x, S=\lambda x y z.xz(yz), K=\lambda xy.x$
und Transformationsregeln

$\operatorname{lift}(FA)=\operatorname{lift}(F) \operatorname{lift}(A), \operatorname{lift}(\lambda x.B)=\operatorname{lift}_x(B);$
Spezifikation: $\operatorname{lift}_x(B) x \to_\beta^* B$
Implementierung:

falls $x\notin\operatorname{FV}(B)$, dann $\operatorname{lift}_x(B)=KB$;

sonst $\operatorname{lift}_x(x)=I, \operatorname{lift}_x(FA)=S\operatorname{lift}_x(F) \operatorname{lift}_x(A)$

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

Motivation

(klassische) reale CPU/Rechner hat nur globalen Speicher (Register, Hauptspeicher)
Argumentübergabe (Hauptprogramm $\to$ Unterprogramm) muß diesen Speicher benutzen

(Rückgabe brauchen wir nicht wegen CPS)
Zugriff auf Register schneller als auf Hauptspeicher $\Rightarrow$ bevorzugt Register benutzen.

Plan (I)

Modell: Rechner mit beliebig vielen Registern $(R_0, R_1, \ldots)$
Befehle:
- Literal laden (in Register)
- Register laden (kopieren)
- direkt springen (zu literaler Adresse)
- indirekt springen (zu Adresse in Register)
Unterprogramm-Argumente in Registern:
- für Abstraktionen: $(R_0, R_1,\ldots, R_k)$
  
  (genau diese, genau dieser Reihe nach)
- für primitive Operationen: beliebig
Transformation: lokale Namen $\to$ Registernamen

Plan (II)

Modell: Rechner mit begrenzt vielen realen Registern,

z. B. $(R_0,\ldots, R_7)$
falls diese nicht ausreichen: register spilling

virtuelle Register in Hauptspeicher abbilden
Hauptspeicher (viel) langsamer als Register:

möglichst wenig HS-Operationen:

geeignete Auswahl der Spill-Register nötig

Registerbenutzung

Allgemeine Form der Programme:

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

für jeden Zeitpunkt ausrechnen: Menge der freien Register ($=$ deren aktueller Wert nicht (mehr) benötigt wird)

nächstes Zuweisungsziel ist niedrigstes freies Register (andere Varianten sind denkbar)

vor jedem UP-Aufruf: register shuffle (damit die Argumente in $R_0,\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 ... ... ...)

Informative Typen

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

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

generalized algebraic data types GADTs
(parametric) higher order abstract syntax (P)HOAS
Dependent Types (in Haskell)

Typen für Listen

das ist klar:

data List a = Nil | Cons a (List a)
Cons False (Cons True Nil) :: List Bool

nach welcher Deklaration ist
```
Cons True (Cons "foo" Nil)
```
statisch korrekt?
Hinweis:
```
data List a b = ...
```

Übung: Vollständige Binärbäume

data Tree a = Leaf a | Branch (Tree (a,a))

deklariere einen Baum t :: Tree Int mit 4 Schlüsseln
implementiere leaves :: Tree a -> [a]

GADT

üblich (algebraischer Datentyp, ADT)

data Tree a = 
  Leaf a | Branch (Tree a) (Tree a)

äquivalente Schreibweise:

data Tree a where
  Leaf :: a -> Tree a
  Branch :: Tree a -> Tree a -> Tree a

Verallgemeinerung (generalized ADT)

data Exp a where
  ConsInt :: Int -> Exp Int
  Greater :: Exp Int -> Exp Int -> Exp Bool

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

Dependent Types (I)

{-# language DataKinds #-}
data Nat = Z | S Nat

data Vec n a where
   Nil :: Vec Z a
   Cons :: a -> Vec n a -> Vec (S n) a

Cons False (Cons True Nil) :: Vec (S (S Z)) Bool

type family Plus a b where
  Plus Z b = b ; Plus (S a) b = S (Plus a b)

Typ von append, reverse?

Dependent Types (II)


{-# OPTIONS_GHC 
     -fplugin GHC.TypeLits.Normalise #-}
import GHC.TypeLits

data Vec l a where
  Nil :: Vec 0 a
  Cons :: a -> Vec l a -> Vec (1 + l) a

app :: Vec p a -> Vec q a -> Vec (q + p) a

Methoden

Inferenzsysteme
Lambda-Kalkül
(algebraischen Datentypen, Pattern Matching, Funktionen höherer Ordnung)
Monaden

Semantik

dynamische (Programmausführung)
- Interpretation
  - funktional, $\bullet$ imperativ (Speicher)
  - Ablaufsteuerung (Continuations)
- Transformation (Kompilation)
  - CPS transformation
  - closure passing, lifting, $\bullet$ Registerzuweisung
statische: Typisierung (Programmanalyse)
- monomorph/polymorph
- deklariert/rekonstruiert

Monaden zur Programmstrukturierung

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

Anwendungen:

semantische Bereiche f. Interpreter,
Parser,
Unifikation

Testfragen (für jede Monad-Instanz):

Typ (z. B. Action)
anwendungsspezifische Elemente (z. B. new, put)
Implementierung der Schnittstelle (return, bind)

Prüfungsvorbereitung

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

was ist eine Umgebung (Env), welche Operationen gehören dazu?
was ist eine Speicher (Store), welche Operationen gehören dazu?
Gemeinsamkeiten/Unterschiede zw. Env und Store?
Für $(\lambda x.xx) (\lambda x.xx)$: zeichne den Syntaxbaum, bestimme die Menge der freien und die Menge der gebundenen Variablen. Markiere im Syntaxbaum alle Redexe. Gib die Menge der direkten Nachfolger an (einen Beta-Schritt ausführen).
Definiere Beta-Reduktion und Alpha-Konversion im Lambda-Kalkül. Wozu wird Alpha-Konversion benötigt? (Dafür Beispiel angeben.)
Wie kann man Records (Paare) durch Funktionen simulieren? (Definiere Lambda-Ausdrücke für pair, first, second)
welche semantischen Bereiche wurden in den Interpretern benutzt? (definieren Sie Val, Action Val, CPS Val)
welches sind die jeweils hinzukommenden Ausdrucksmöglichkeiten der Quellsprache (Exp)?
wie lauten die Monad-Instanzen für Action, CPS, Parser, was bedeutet jeweils das bind (>>=)?
warum benötigt man call-by-name für Abstraktionen über den Programmablauf (warum kann man if oder while nicht mit call-by-value implementieren)?
wie kann man call-by-name simulieren in einer call-by-value-Sprache?
wie kann man call-by-value simulieren in einer call-by-name-Sprache (Antwort: durch CPS-Transformation)
Definiere Fakultät mittels Fixpunktoperator (Definiere das f in fak = fix f )
Bezüglich welcher Halbordnung ist dieses f monoton? (Definiere die Ordnung, erläutere Monotonie an einem Beispiel.)
Wie kann man Rekursion durch get/put simulieren? (Programmbeispiel ergänzen)
Wie kann man Rekursion durch label/jump simulieren? (Programmbeispiel ergänzen)
Für die Transformationen CPS, Closure Conv., Lifting, Registervergabe: welche Form haben jeweils Eingabe- und Ausgabeprogramm? Auf welchem Maschinenmodell kann das Zielprogramm ausgeführt werden? (Welche Operationen muß das Laufzeitsystem bereitstellen?)
Was sind die Bestandteile eines Inferenzsystems (Antwort: Grundbereich, Axiome, Regeln), wie kann man ein Axiom als Spezialfall einer Regel auffassen?
wie lauten die Inferenzregeln für das Nachschlagen eines Namens in einer Umgebung?
Inferenzregeln für Applikation, Abstraktion, Let, If/Then/Else im einfach getypten Kalkül
Geben Sie ein Programm an, das sich nicht einfach (sondern nur polymorph) typisieren läßt. Geben Sie den polymorphen Typ an.
Inferenz-Regeln für Typ-Applikation, Typ-Abstraktion im polymorphen Kalkül
für Typ-Rekonstruktion im einfach getypten Kalkül: Welches ist der Grundbereich des Inferenzsystems?
geben Sie die Inferenzregel für Typrekonstruktion bei If/Then/Else an
Geben Sie eine Inferenzregel für Typrekonstruktion an, durch die neue Variablen eingeführt werden.
Wann ist $\sigma$ ein Unifikator von zwei Termen $s, t$?
Geben Sie zwei verschiedene Unifikatoren von $f(a,X)$ und $f(Y,Z)$ an. Einer davon soll streng allgemeiner als der andere sein. Begründen Sie auch diese Beziehung.
Bestimmen Sie einen Unifikator von $f(X_n, f(X_{n-1}, \ldots, f(X_0, a) \ldots))$ und $f(f(X_{n-1},X_{n-1}),f(f(X_{n-2},X_{n-2}),\ldots,f(a,a)\ldots))$.

Einleitung

Beispiel

Sprachverarbeitung

(weitere) Methoden und Modelle

Inhalt der Vorlesung

Literatur

Anwendungen von Techniken des Compilerbaus

Organisation der Vorlesung

Beispiel: Interpreter (I)

Beispiel: Interpreter (II)

Übung (Haskell)

Übung (Interpreter)

Inferenz-Systeme

Motivation

Definition

Das Ableiten als Hüll-Operation

Regel-Schemata

Inferenz-Systeme (Beispiel 1)

Inferenz-Systeme (Beispiel 2)

Inferenz-Systeme (Beispiel 3)

Inferenz von Werten

Umgebungen (Spezifikation)

Umgebungen (Implementierung)

Aussagenlogische Resolution

Resolution (Vollständigkeit)

Die Abtrennungsregel (modus ponens)

Semantische Bereiche

Continuations

Unterprogramme

Beispiele

Interpreter mit Funktionen

Semantik

Testfall (1)

Let und Lambda

Mehrstellige Funktionen

Closures (I)

Closures (II)

Rekursion?

Testfall (2)

Lambda-Kalkül

Motivation

Der Lambda-Kalkül

Lambda-Terme

verkürzte Notation

Gebundene Variablen

Substitution

Das falsche Binden von Variablen

Gebundene Umbenennungen

\(\alpha\)-Äquivalenzklassen

Ableitungen

Eigenschaften der Reduktion

Daten als Funktionen

Lambda-Kalkül als universelles Modell

Fixpunkt-Kombinatoren

Lambda-Berechenbarkeit

Übung Lambda-Kalkül

Fixpunkte

Motivation

Existenz von Fixpunkten

Beispiele f. Halbordnungen, CPOs

Stetige Funktionen

Funktionen als CPO

Funktionen als CPO, Beispiel

Fixpunktberechnung im Interpreter

Fixpunkte und Laziness

Simultane Rekursion: letrec

letrec nach rec

Übung Fixpunkte

Zustand/Speicher

Motivation

Speicher

Auswertung von Ausdrücken

Änderung der Hilfsfunktionen

Speicher-Aktionen als Monade

Variablen?

Imperative Programmierung

Rekursion

Rekursion (semantisch)

Rekursion (operational)

Speicher—Übung