\section{Der $\lambda$-Kalkül}
\inhalta{8-14}

--- nicht  behandelt ---
% \newcommand{\LD}{$\lambda$}
% 
% 
% \begin{frame}
% Historie:
% \begin{itemize}
% \item 
% ca. 1930: Alonzo Church entwickelt $\lambda$-Kalk"ul als Methode zur Beschreibung (beliebiger) Funktionen
% 
% \item 
% 1960: Listenverarbeitungssprache
% \texttt{Lisp}, die an $\lambda$-Kalk"ul erinnert
% 
% \item 
% \texttt{Lisp} f"uhrt z.B. zu funktionalen Sprachen \texttt{ML} und \texttt{Haskell}
% 
% \item 
% \texttt{OCaml} als \texttt{ML}-Dialekt kombiniert funktionale und objektorientierte Ansätze
% \end{itemize}
% 
% \end{frame}
% \begin{frame}[fragile]
% 
% \begin{itemize}
% \item 
% $\lambda$-Kalk"ul: Definition von $\lambda$-Termen, die oft als 
% Funktionen interpretiert werden können 
% \item 
% Ausdr"ucke im $\lambda$-Kalk"ul in strikter Pr"afix-Form, d.h es
% gibt weder Infix- noch Postfixoperatoren wie bei $x+y$ oder $x^2$
% \item weitgehender Verzicht auf Klammerung, soweit möglich
% \item 
% Funktionen und ihre Argumente werden einfach nebeneinander
% geschrieben:
% \[
% \begin{tabular}{|c|c|}\hline
% klassisch: &$\lambda$-Term\\\hline
% $f(x)$ & \texttt{f x} \\
% $g (x,y)$& \texttt{g x y}\\
% $x + 3$ & \texttt{+ 3 x}\\ 
% $\sin(x)+4$&
% \texttt{+ (sin x) 4}\\\hline
% \end{tabular}
% \]
% \item Konstruktion ist nicht assoziativ, daher Festlegung einer Auswertungsreihenfolge
% \item 
% Klammern nur für Abweichungen von Präzendenzregeln notwendig
% \end{itemize}
% \end{frame}
% \begin{frame}
% im $\lambda$-Kalkül gibt es weder Schleifen noch Verzweigungen, aber 
% einen sehr mächtigen Konstruktor für (anonyme) Funktionen:
% \begin{itemize}\item
% aus DSL gewohnt:
% ``Funktion $f$ mit 
%  $f (x) = 3\cdot x$'' oder
% ``$x \mapsto 3\cdot x$''
% \item Schreibweise im
% $\lambda$-Kalkül:
% \[\mbox{\texttt{\LD x.*3x}}\]
% \item Bei \texttt{\LD x.t} ist \texttt{x} formaler Parameter und 
% \texttt{t} der Prozedurrumpf, der i.d.R. \texttt{x} verwendet.
% \item
% keine Festlegung von
% Parametertypen 
% (``untypisierter'' $\lambda$-Kalkül)
% \item es gibt nur einstellige Funktionen 
% \end{itemize}
% \end{frame}
% 
% \begin{frame}
% mehrstellige Funktionen über ``Currying'' (oder ``Schönfinkeln''):
% Fixiert man bei einer $n$-stelligen Funktion einen Parameter, so entsteht eine $n{-}1$-stellige Funktion.
% 
% Beispiel: Beim zweistelliger Funktion $f:\nat\times\nat\to \nat$, $(x,y)\mapsto f(x,y)$ ist z.B. die  
% Funktion $g:\nat\to \nat$, $x\mapsto f(2,x)$ einstellig. 
% 
% Verwendung anderer Werte $z$ statt fixiertem Wert $2$: Jedem $z$ wird eine Funktion zugeordnet!
% 
% Als $\lambda$-Term: \texttt{\LD x.f z x} ist (höhere) Funktion, die jedem
% $z$ die Funktion $x\mapsto f(z,x)$ zuordnet.
% 
% \texttt{(\LD x.f z x) 3} ist die Funktion  $x\mapsto f(3,x)$   
% 
% \texttt{((\LD x.f z x) 3) 2} ist der Wert   $f(3,2)$   
% 
% Hintergrund:
% $\nat\times\nat\to \nat$ ist isomorph zu $\nat\to(\nat\to \nat)$
% 
% \end{frame}
% 
% \begin{frame}
% \begin{itemize}
% \item Bei $\mathtt{f x}$ ist \texttt{x} aktueller Parameter, mit dem die
% Funktion \texttt{f} ausgewertet wird.
% \item Beispiel: \texttt{(\LD x.*3x)4} ist Anwendung der Funktion \texttt{(\LD x.*3x)} auf 
% den Parameter \texttt{4}. 
% 
% Werden die Konstanten \texttt{*}, \texttt{3} und \texttt{4} wie `üblich' interpretiert,
% ergibt sich die Zahl $12$ als Wert. 
% \item Im Folgenden Abk"urzungen f"ur Bequemlichkeit: Ist \texttt{F := \LD x.*3x}, kann
% man \texttt{F 4} schreiben anstelle von \texttt{(\LD x.*3x)4}
% 
% In realen funktionalen Programmiersprachen oft formuliert wie \texttt{let F := \LD x.*3x in  F 4}
% \item Terme wie \texttt{\LD x f} dürfen als Parameter oder im Rumpf von Funktionen eingesetzt werden!
% 
% Beispiel: Wird die Funktion \texttt{G := \LD y.(\LD x.*yx)} auf den Parameter \texttt{y=3} angewendet
% also \texttt{G 3} , entsteht als Wert(!) die Funktion \texttt{\LD x.*3x}, d.h. \texttt{F} wird ist der Wert bei Parameter, dann ist \texttt{N 3} wieder \texttt{\LD x. * 3 x},
% d.h. \texttt{N 3} verh"alt sich wie \texttt{F}
% 
% \item Mehrdeutigkeit von Ausdrücken wie \texttt{\LD x.\LD y.xyz}:
% \texttt{\LD x.(\LD y.xy)z}
% \texttt{\LD x.(\LD y.x(yz))}
% \texttt{\LD x.(\LD y.(xy)z))}
% $\leadsto$ Präzedenzregeln, Auswertungsreihenfolgen und Klammern notwendig!
% 
% Dabei: Applikation bindet stärker als Abstraktion, d.h.
% \texttt{\LD x.\LD y.xyz} wird gelesen als \texttt{\LD x.\LD y.((xy)z)}
% \end{itemize}
% \end{frame}
% 
% \begin{frame}
% \begin{definition}[Lambda-Terme] 
% $C$ sei eine Menge von Konstanten und $V$ eine (abzählbar unendliche) 
% Menge von Variablen. Die Menge der Lambda-Terme $\Lambda$ ist definiert als
% die kleinste Menge, so dass:
% \begin{itemize}
% \item $C\subseteq \Lambda$,
% \item $V\subseteq \Lambda$,
% \item $(t_1\  t_2 ) \in \Lambda$ für alle $t_1, t_2 \in \Lambda$ und 
% \item $(\lambda x.t) \in \Lambda$ für alle $x\in V$ und $t\in \Lambda$.
% \end{itemize}
% \end{definition}
% \begin{itemize}
% \item $\Lambda$ ist also eine (i.W. kontextfreie) Sprache über dem Alphabet $C\cup V \cup\{~~'(',~~ ')',~~ '.', ~~'\lambda'\}$
%  \item Terme der Form $(t_1~~t_2)$ nennt man {\em Anwendungen} oder {\em Applikationen}.
% 
%  \item Idee: Der Algorithmus(?) $t_1$ wird auf die Daten(?) $t_2$ angewendet.
% 
% \item Terme der Form $(\lambda x.t)$ heißen {\em (Lambda-)Abstraktionen}.
% 
%  \item Idee:  $(\lambda x.t)$ ist eine Funktion, die Werte von $x$ auf Werte von $t$ abbildet.
% Lambda-Abstraktionen repräsentieren anonyme Funktionen.
% \end{itemize}
% 
% \end{frame}
% 
% \begin{frame}
% Regeln zur Klammerersparnis beim Aufschreiben:
% \begin{itemize}
% \item Anwendungen assoziieren nach links.\\
% Damit steht also $t_1~~t_2~~t_3$ für $((t_1~~t_2)~~t_3 )$.
% \item Der Wirkungsbereich eines Lambdas erstreckt sich so weit wie möglich nach rechts.
% Daher steht $\lambda x.t_1~t_2$ für $(\lambda x.(t_1~t_2))$.
% \item  Wir schreiben $\lambda x y.t$ statt $\lambda x.\lambda y.t$.
% \end{itemize}
% \end{frame}
% 
% \begin{frame}Beispiele mit Konstanten $3$ ($\in\nat$) und Variablen $x, q$  (`quadrieren');
% \begin{itemize}
% \item  Der Term
% \[ 
% \lambda x. q~x\equiv (\lambda x. (q~x))\]
% beschreibt die Funktion, die ihr Argument quadriert, also z.B. $(\lambda x. q~ x)~3 \equiv 9$ 
% \item Der Term
% \[ 
% \lambda x. q~(q~x)\equiv (\lambda x. (q~(q~x)))\]
% beschreibt die Funktion, die ihr Argument zweifach quadriert, also z.B. $\lambda x. q~(q~x))~3 \equiv 81$.
% \item Bei \[ 
% \lambda x. q~q~x\equiv (\lambda x. ((q~q)~x))\]
% müsste allerdings $q$ auf sich selbst angewendet werden... 
% \end{itemize}
% Eine Interpretation von $q$ als Funktion im herkömmlichen Sinne ist also nicht immer möglich.
% \end{frame}
% 
% 
% \begin{frame}
% \begin{definition}[(Freie Variablen eines Lambda-Terms)]
% Für jeden Lambda-Term
% $t \in  \Lambda$  definieren wir $\mathrm{free}(t)\subseteq  V$, die Menge seiner freien Variablen, wie folgt:
% \begin{itemize}
% \item $ \mathrm{free}(c) = \emptyset$ für alle $c \in  C$,
% \item $ \mathrm{free}(x) = \{x\}$ für alle $x \in  V$,
% \item $ \mathrm{free}(t_1 t_2) = \mathrm{free}(t_1 ) \cup \mathrm{free}(t_2)$ für alle $t_1 , t_2 \in  \Lambda$,
% \item $ \mathrm{free}(\lambda x.t) = \mathrm{free}(t) \setminus  \{x\}$ für alle $x \in  V, t \in  \Lambda$.
% \end{itemize}
% Ein Term $t$ heißt geschlossen, falls $\mathrm{free}(t) = \emptyset$. Man bezeichnet geschlossene Lambda-Terme
% auch als Kombinatoren.
% \end{definition}
% 
% \end{frame}
% 
% 
% 
% 
% 
% 
% 
% 
% 
% 
% 
% 
% 
% 
% 
% 
% 
% 
% 
% 
% 
% \begin{frame}
% \begin{definition}
% Ein $\lambda$-Term wird konstruiert durch die folgende Grammatik:
% \[
% \texttt{M ::= c | x | M M | {\LD}x.M}
% \]
% wobei \texttt{c} Konstanten sind wie z.B. \texttt{1}, \texttt{2},... \texttt{*}, \texttt{*} und \texttt{x} eine (von
% unendlich vielen) Variablen.
% 
% Ein Ausdruck ohne Konstanten heisst reiner $\lambda$-Term.
% \end{definition}
% \end{frame}
% 
% \begin{frame}
% 
% 
% 
% 
% 
% 
% Grammatik ist nicht eindeutig
% 
% M ::= c|x |M M|*x .M
% Der Term *x.x y kann auf zwei Arten gelesen werden:
% 
% *x
% 
% app
% 
% x y
% 
% app
% *x
% 
% x
% 
% y
% 
% *x.(x y ) (*x .x) y,,,,,XXXXX(*x .x) y
% Applikation ist linksassoziativ, d.h.
% 
% E1E2E3 . . . En wird ausgewertet als (. . . (E1E2)E3) . . . En)
% Abstraktion ist rechtsassoziativ, d.h.
% 
% \texttt{\LD x .\LD y .\LD z. x y z} wird ausgewertet als 
% \texttt{\LD x.(\LD y .(\LD z. x y z))}
% 
% 
% \end{frame}
% \begin{frame}
% 
% Reduktion
% 
% einzige Rechenregel ist Reduktion($\beta$-Reduktion)
% beschreibt, wie formale Parameter durch tats"achliche ersetzt
% werden
% 
% wird nur gebraucht, wenn ein Term auf einen anderen
% angewendet wird
% 
% \texttt{
% (\LD x. \LD  3 x) 4 !fi \LD 3 4
% (\LD y .y 5)(\LD x . \LD 3 x) !fi (\LD x. \LD 3 x)5 !fi \LD 3 5
% }
% 
% mit manchen Ausdr"ucken kann man das unendlich oft machen:
% 
% \texttt{$\Omega$  = (\LD x.x x)(\LD x .x x )}
% ein Term ist in Normalform, falls keine weiteren Reduktionen
% m"oglich sind
% 
% nicht jeder Term hat eine Normalform(z.B. \texttt{$\Omega$} )
% 
% \end{frame}
% \begin{frame}
% 
% Konfluenz
% 
% in manchen F"allen gibt es mehrere M"oglichkeiten f"ur eine
% Reduktion
% 
% damit der Kalk"ul sinnvoll ist, sollte die Reihenfolge der
% Reduktionen keine Rolle spielen
% 
% Satz (Church-Rosser)
% Falls ein Term M in einer endlichen Anzahl von Schritten zu einem
% Term N oder zu einem Term P reduziert werden kann, dann
% existiert ein Term Q zu dem sowohl N als auch P reduziert werden
% k"onnen.
% 
% Warnung: Nicht jede Auswertungsstrategie f"uhrt zur Normalform!
% Siehe Aufgabe 3.1.1.
% 
% 
% \end{frame}
% \begin{frame}
% 
% 
% "Aquivalenz von $\lambda$-Termen
% 
% Folgerung
% Jeder Term hat h"ochstens eine Normalform.
% 
% Beweis: Seien N und P zwei Normalformen zum Term M. Nach
% Church-Rosser existiert ein Q mit P !\LD fi Q und N !\LD fi Q. Da P
% und N in NF folgt P j N j Q. $\Lambda$ 
% 
% Terme s und t, die sich nur durch Namen der Variablen
% unterscheiden werden als "aquivalent betrachtet: s j t
% 
% Terme s und t, die durch Umbenennung(ff-Konversion) der
% Variablen und fi-Reduktion auseinander hervorgehen, heissen
% $\lambda$-gleich: s ss t.
% 
% 
% \end{frame}
% \begin{frame}
% 
% Beispiele
% 
% I = \LD x .x Identit"at
% K = \LD x.\LD y .x Kc = \LD y .c Konstante
% B = \LD x.\LD y .\LD z.x(y (z)) B f g = \LD z.f (g (z)) Komposition
% S = \LD x.\LD y .\LD z.(xz)(yz) Substitution
% 
% SKK =[\LD x.\LD y .\LD z.(xz)(yz)]KK
% 
% =[\LD y .\LD z.(Kz)(yz)]K
% =\LD z.[(Kz)(Kz)] K = \LD x .\LD y .x, Kz = \LD y .z
% =\LD z.[(\LD y .z)(\LD y .z)]
% =\LD z.z
% 
% 
% \end{frame}
% \begin{frame}
% 
% Freie Variablen
% 
% alle Namen sind lokale Definitionen
% Variable x in \LD x.x heisst gebunden, da sie im K"orper der
% Funktionsdefinition, die mit \LD x beginnt, steht
% 
% eine Variable, der kein zugeh"origes \LD  vorangeht, heisst frei,
% z.B. y in \LD x.xy
% 
% in (\LD x.x)(\LD y .yx) ist das x im linken Ausdruck gebunden, im
% zweiten Teil ist y gebunden und x ist frei, es ist vollkommen
% unabh"angig von dem x im linken Teil
% 
% Definition
% Eine Variable x ist frei in folgenden F"allen:
% 
% 1 x ist frei im Ausdruck x
% 2 x ist frei in \LD y .E falls x frei im Ausdruck E vorkommt und
% 
% y 6= x
% 3 x ist frei in E1E2, falls x frei in E1 oder E2
% 
% 
% \end{frame}
% \begin{frame}
% 
% Gebundene Variablen und Substitution
% 
% Definition
% Eine Variable x ist in folgenden F"allen gebunden
% 
% 1 x ist gebunden in \LD x.E und x ist frei in E
% 2 x ist gebunden in E1E2, falls x gebunden in E1 oder gebunden
% 
% in E2.
% 
% Eine Variable kann also in einem Ausdruck sowohl frei als auch
% gebunden sein!
% 
% 1 F"ur Identit"atsfunktion I ergibt II j (\LD x .x)(\LD x.x ). Man kann
% 
% auch II j (\LD x .x)(\LD z.z) schreiben und reduziert durch
% [\LD z.z/x]x zu \LD z.z j I
% 
% 2 Vorsicht beim Substituieren, freie und gebundene Vorkommen
% 
% d"urfen nicht verwechselt werden
% 
% \end{frame}
% \begin{frame}
% 
% Beispiel Substitution in (\LD x .(\LD y .xy ))y
% 
% das linke y ist gebunden, das rechte ist frei
% 
% falsch: ,,,XXX\LD y .yy
% richtig benenne gebundenes y in t um:
% 
% \LD x.(\LD t.tx)y !fi \LD t.yt
% 
% wird \LD x.E1 auf E2 angewendet, werden alle freien Vorkommen
% von x in E1 durch E2 ersetzt
% 
% k"ame dabei eine freie Variable aus E2 in einen Ausdruck, wo
% diese Variable gebunden ist, wird die gebundene Variable
% vorher umbenannt
% 
% in
% 
% (\LD x.(\LD y .(x (\LD x.xy ))))y
% 
% ersetzt man y im Innern durch t zu
% 
% (\LD x.(\LD t.(x (\LD x.xt))))y !fi (\LD t.(y (\LD x .xt)))
% 
% \end{frame}
% \begin{frame}
% 
% Nat"urliche Zahlen-Church Numerals
% 
% k"onnen durch 0 und Nachfolgerfunktion dargestellt werden:
% zero, suc(zero), suc(suc(zero)) . . .
% 
% Null wird definiert als 0 j \LD s.(\LD z.z)
% weitere Zahlen:
% 1 j \LD s.\LD z.s(z), 2 j \LD s.\LD z.s(s(z)), 3 j \LD s.\LD z.s(s(s(z))) usw.
% 
% Nachfolgerfunktion S j \LD w .\LD y .\LD x.y (wyx) angewendet auf
% zero:
% 
% \LD w \LD y .\LD x .(y ( w yx)) (\LD s.(\LD z.z)) !
% 
% \LD y .\LD x .(y ( \LD s .(\LD z.z)) y x ) !
% \LD y .\LD x .(y ( \LD z.z ) x ) ! \LD y .\LD x .(y (x)) j 1
% (\LD w .\LD y .\LD x.y (wyx))(\LD s.\LD z.s(z)) !
% (\LD y .\LD x.y ((\LD s.\LD z.s(z))yx)) !
% (\LD y .\LD x.y (\LD z.y (z))x ) ! (\LD y .\LD x.y (y (x )))
% 
% 
% \end{frame}
% \begin{frame}
% 
% Addition
% 
% gr"uner Teil in 1 j \LD s.\LD z. s(z) ist Anwendung von s auf z
% 2 + 3 bedeutet 2-malige Anwendung der Nachfolgerfunktion S
% 
% 2S3 = {\LD s.\LD z.s(s(z))}{\LD wyx .y (wyx )}{\LD a.\LD b.a3(b)} !
% 
% !{\LD z.[\LD w .\LD y .\LD x .y (wyx )]([\LD w \LD y .\LD x.y (wyx)](z))}{\LD a.\LD b.a3(b)}
% ![\LD w \LD y .\LD x.y (wyx)]([\LD w .\LD y \LD .x.y (wyx)](\LD a.\LD b.a3(b))) j SS3
% 
% SS3 ! S4 ! 5
% 
% \end{frame}
% \begin{frame}
% Multiplikation
% 
% zwei Zahlen m und n multipliziert man durch \LD m.\LD n.\LD z.m(nz)
% Produkt von 2 mit 2 ist dann (\LD m.\LD n.\LD z.m(nz))2 2
% reduziert zu \LD z.2(2z), weitere Reduktion ergibt 4.
% 
% \end{frame}
% \begin{frame}
% Logische Konstanten und Funktionen
% 
% logische Konstanten T j \LD x\LD y .x und F j \LD x\LD y .y
% logische Funktionen: $^ j$ \LD x \LD y .xy F, . j \LD x\LD y .x(\LD u\LD v .u)y
% und $~ j$ \LD x.xFT
% 
% Die Negationsfunktion angewendet auf T ist
% 
% (\LD x .xFT)(\LD a\LD b.a) j (\LD x.x(\LD c\LD d .d )
%     (\LD e\LD f .e))(\LD a\LD b.a)
% was reduziert werden kann zu:
% 
% TFT j (\LD a\LD b.a)(\LD c\LD d .d )(\LD e\LD f .e) !$\beta$ 
% (\LD c\LD d.d) j F
% 
% \end{frame}
% \begin{frame}
% Konditionale
% 
% hilfreich bei Programmierung ist eine Test-auf-Null-Funktion f
% mit $f (0) = T$ und $f (n) = F$ f"ur $n \neq 0$
% 
% ein $\lambda$-Term f"ur eine solche Funktion ist:
% 
% Z j \LD n.nF~F
% f"ur jedes f ist nullfache Anwendung von f auf a gerade a
% 
% 0fa j (\LD s.\LD z.z)fa j a
% ausserdem Fa j \LD y .y = I f"ur beliebiges a
% 
% Z 0 j (\LD n.nF~F)0 = 0F~F = ~F = T
% 
% Z n j (\LD x .xF~F)n j nF~F = I F = F
% 
% \end{frame}
% \begin{frame}
% Vorg"angerfunktion $P$
% 
% f"ur den Vorg"anger von $n$ konstruiert man das Paar $(n, n {-} 1)$
% und nimmt das zweite Element
% 
% ein Paar $(a, b)$ wird als \texttt{\LD z.zab} dargestellt
% 
% \texttt{(\LD z.zab)T = Tab = a} und \texttt{(\LD z.zab)F = Fab = b}
% 
% $\lambda$-Ausdruck f"ur $\Phi$  mit: $\Phi  : (n, n - 1) \mapsto (n + 1, n - 1)$
% 
% \texttt{$\Phi$  j (\LD p.\LD z.z(S(pT))(pT))}
% 
% \texttt{pT} ergibt das erste Element des Paares \texttt{p}
% wende $\Phi$  $n$-mal auf das Paar \texttt{(\LD z.z00)} an, bilde zweite
% Projektion
% 
% \texttt{P j (\LD n.n$\Phi$ (\LD z.z00)F )}
% 
% beachte: der Vorg"anger von $0$ ist $0$.
% 
% \end{frame}
% \begin{frame}
% Funktionen h"oherer Ordnung
% 
% kein Unterschied zwischen einfachen Objekten z.B. Zahlen
% und komplexen Objekten wie Funktionen von Funktionen
% 
% was sich als $\lambda$-Term formulieren l"asst, kann durch andere
% $\lambda$-Terme manipuliert werden
% 
% \texttt{Q := \LD x. \LD  x x} ist Term f"ur Quadrieren
% 
% \texttt{P8 := \LD x.Q(Q(Q x ))} ist Term f"ur 8. Potenz
% Term, f"ur dreimalige Funktionsanwendung
% \texttt{T : \LD f .(\LD x .f (f (f x)))}, damit gilt \texttt{P8 j T Q} und \texttt{58 ist T Q 5}
% 
% \texttt{T T} angewendet auf eine Funktion \texttt{f} ergibt \texttt{f 27}
% Operatoren wie \texttt{T} heissen Funktionen h"oherer Ordnung
% 
% \end{frame}
% \begin{frame}
% Iterationen und Rekursion
% 
% wiederholte Funktionsanw. als Kombination von $\lambda$-Termen
% wollen Verhalten einer FOR-Schleife darstellen, bei der die
% Anzahl der Wiederholungen durch Z"ahler kontrolliert wird
% 
% haben Z j \LD n.nF~F mit Z 0xy = x und Z nxy = y f"ur n 6= 0,
% sowie Vorg"anger P und Nachfolger S
% 
% suchen I mit I n f x = f (f (f . . . (f x) . . .)) und I 0 f x = x
% probiere: I = \LD n.\LD f .\LD x .Z n x (I(P n)f (f x))
% I steht sowohl rechts als auch links, keine echte Definition
% man kann I aber als Fixpunkt des rechten Terms auffassen
% 
% A := \LD M.(\LD n.\LD f .\LD x.Z n x(M(P n)f (f x))))
% F"ur welches I ist I = A I ? Wie findet man Fixpunkte von A?
% 
% \end{frame}
% \begin{frame}
% Fixpunktkombinator
% 
% suchen Fixpunkt für einen Term
% man kann $\lambda$-Terme Y angeben, die einen Fixpunkt für einen
% beliebigen Term angeben, d.h.
% 
% 9Y .8M. Y M = M (Y M)
% mit diesem Y l"osen wir I = A I durch I := Y A
% 
% Y := (\LD y .(\LD x.y (xx))(\LD x.y (xx)))
% 
% YR = (\LD y .(\LD x.y (xx))(\LD x .y (xx)))R!
% 
% $\beta$ (\LD x.R(xx))(\LD x .R(xx))!
% $\beta$ R((\LD x.R(xx))(\LD x.R(xx)))j
% 
% R(YR)
% 
% R wird ausgewertet durch rekursiven Aufruf von YR als erstes
% Argument.
% 
% \end{frame}
% \begin{frame}
% Fixpunktkombinator am Beispiel
% 
% Berechne
% 
% f (n) =
% 
% nX
% 
% i=0
% 
% i = n +
% 
% n-1X
% 
% i=0
% 
% i
% 
% Sei R = (\LD r \LD n.Zn0(nS(r (Pn)))) wende S n-mal an, falls n 6= 0)
% 
% YR3 = R(YR)3 ! Z 30(3S(YR(P3)))!
% 
% 3S(YR2) (weil 3 6= 0)!
% . . . ! 3S2S1S0 j 6
% 
% Rekursion bricht ab, wenn Argument 0 wird.
% 
% \end{frame}
% \begin{frame}
% $\lambda$-Kalk"ul als Berechnungsmodell
% 
% es gibt eine Vielzahl von $\lambda$-Kalk"ulvarianten
% ein Kalk"ul heisst Turing-m"achtig oder Turing-vollst"andig, wenn
% in ihm alle berechenbaren Funktionen auf N ausgedr"uckt
% werden k"onnen
% 
% fi-Regel ist wohldefiniert und kann von einem Programm
% ausgef"uhrt werden
% 
% $\lambda$-Kalk"ul angereichert mit Z , P, S und mit Konstanten f"ur
% alle Zahlen ist Turing-m"achtig
% 
% reiner $\lambda$-Kalk"ul ohne Konstanten ist Turing-m"achtig
% 
% \end{frame}
% \begin{frame}
% 
% Bonusmaterial
% 
% \end{frame}
% \begin{frame}
% 
% Vermeidung schlechter Terme durch Typisierung
% 
% wir haben Verwendung f"ur seltsame Terme wie
% Y := (\LD y .(\LD x.y (xx))(\LD x.y (xx)))
% 
% niemand hindert uns sin log zu bilden, obwohl sin nur auf
% Zahlen angewendet werden sollte, Compiler einer vern"unftigen
% Programmiersprache sollte ablehnen
% 
% Typisieren der Terme: welche Arten von Argumenten
% akzeptiert ein Term, welche Art Ergebnis produziert er
% 
% Beispiel sin : R ! R
% einfaches Typsystem o/ = c | o/ ! o/ besteht aus Basistypen c
% und Funktionentypen o/ ! o/
% 
% \end{frame}
% \begin{frame}
% Wohlgetypte $\lambda$-Terme
% 
% Definition
% 
% Basisfall f"ur jeden Typ oe und Variable x ist der Term x : oe
% 
% wohlgetypt und hat Typ oe
% 
% Abstraktion f"ur M : o/ und Variable x : oe ist \LD x : oe.M wohlgetypt
% 
% und hat Typ oe ! o/
% 
% Applikation falls M wohlgetypt vom Typ oe ! o/ und N
% 
% wohlgetypt vom Typ oe, dann ist M N wohlgetypt
% vom Typ o/
% 
% Beispiele:
% 
% 1 \LD x : oe.x : oe hat Typ oe ! oe
% 2 \LD x : oe.\LD y : o/.x : oe hat den Typ oe ! (o/ ! oe)
% 3 sin log ist nicht wohlgetypt, M M l"asst sich niemals typisieren,
% 
% egal f"ur welches M
% 
% \end{frame}
% \begin{frame}
% R"uckgewinnung der Turing-M"achtigkeit
% 
% Satz
% Jeder wohlgetypte Term hat eine Normalform.
% 
% Y ist also nicht wohlgetypt, geh"ort nicht zum einfach
% getypten $\lambda$-Kalk"ul
% 
% einfach getypter $\lambda$-Kalk"ul ist nicht Turing-m"achtig
% man kann ihn anreichern mit
% Fixpunkt-Kombinator-Konstanten
% 
% System PCF (programming computable functions), eingef"uhrt
% von Scott und Plotkin, ist Turing-m"achtig.
% 
% \end{frame}
% \begin{frame}
% System PCF
% 
% besteht aus $\lambda$-Termen f"ur ein einfaches Typsystem mit Basistyp
% int und folgenden Konstanten:
% 
% 1 n vom Typ int f"ur jede nat"urliche Zahl n
% 2 Konditional Zoe vom Typ int ! (oe ! (oe ! oe))
% 3 P und S vom Typ int!int f"ur Vorg"anger- und
% 
% Nachfolgerfunktion
% 4 je ein Yoe vom Typ (oe ! oe) ! oe
% 
% \end{frame}
% 
%