438 lines
18 KiB
TeX
438 lines
18 KiB
TeX
\documentclass[11pt,a4paper]{scrartcl}
|
|
\usepackage[a4paper,left=3cm,right=3cm,top=2.5cm,bottom=2.5cm]{geometry}
|
|
\usepackage[ngerman]{babel}
|
|
\usepackage{amssymb}
|
|
\usepackage{amsthm}
|
|
\usepackage{mathrsfs}
|
|
\usepackage{scrextend}
|
|
\usepackage[utf8]{inputenc}
|
|
\usepackage{amsmath}
|
|
\usepackage{enumitem}
|
|
\usepackage{tikz-qtree}
|
|
\usepackage{mathtools}
|
|
\usepackage{latexsym}
|
|
\usepackage{bussproofs}
|
|
\usepackage{csquotes}
|
|
\usepackage{pdfpages}
|
|
\usepackage{pgfplots}
|
|
\usepackage{hyperref}
|
|
\usepackage{upgreek}
|
|
\usepackage{tikz}
|
|
\usetikzlibrary{positioning}
|
|
\usetikzlibrary{arrows.meta}
|
|
|
|
%Anmerkungen am Rand
|
|
\newcommand{\siehe}[1]{\marginpar{\footnotesize \textit{#1}}}
|
|
\newcommand{\satz}[2]{\marginpar{\footnotesize \textit{Satz~#1 (#2)}}}
|
|
\newcommand{\defin}[2]{\marginpar{\footnotesize \textit{Def.~#1 (#2)}}}
|
|
\newcommand{\kor}[2]{\marginpar{\footnotesize \textit{Kor.~#1 (#2)}}}
|
|
\newcommand{\lem}[2]{\marginpar{\footnotesize \textit{Lem.~#1 (#2)}}}
|
|
\newcommand{\bem}[2]{\marginpar{\footnotesize \textit{Bem.~#1 (#2)}}}
|
|
\newcommand{\alg}[2]{\marginpar{\footnotesize \textit{Alg.~#1 (#2)}}}
|
|
|
|
%Abkürzungen für Symbole, Reduktionen, etc.
|
|
\newcommand{\app}{\ensuremath{\rightarrow_a}}
|
|
\newcommand{\norm}{\ensuremath{\rightarrow_n}}
|
|
\newcommand{\pteq}{\ensuremath{\overset{\cdot}{=}}}
|
|
\newcommand{\bred}{\ensuremath{\rightarrow_\beta}}
|
|
\newcommand{\ered}{\ensuremath{\rightarrow_\eta}}
|
|
|
|
\theoremstyle{definition}
|
|
\newtheorem{definition}{Definition}[section]
|
|
|
|
\title{Merkzettel für \enquote{Theorie~der~Programmierung}}
|
|
\author{Marco Ammon}
|
|
\date{\today}
|
|
|
|
\begin{document}
|
|
\maketitle
|
|
\section*{Termersetzungssysteme}
|
|
\subsection*{Terminierung}
|
|
\satz{2.31}{15}
|
|
Sei $>$ Reduktionsordnung, und es gelte: $\forall t,s.t\rightarrow_0 s \Rightarrow t>s$. Dann ist $\rightarrow$ stark normalisierend.
|
|
\subsubsection*{Polynomordnungen}
|
|
\kor{2.44}{18}
|
|
Wir definieren $A \subseteq \mathbb{N}$ und für jede $n$-stellige Operation $f$ ein Polynom $p_f(x_1,\ldots, x_n)$. Wenn die linken Seiten der Umformungsregeln $>_A$ den rechten sind, ist das zugehörige TES stark normalisierend.
|
|
\subsection*{Konfluenz}
|
|
\subsubsection*{Critical Pairs}
|
|
\begin{itemize}
|
|
\item Definition kritisches Paar: \defin{2.55}{22}\\
|
|
Seien $l_1 \rightarrow_0 r_1$ und $l_2 \rightarrow r_2$ zwei Umformungsregeln des TES sowie $FV)(l_1) \cap FV(l_2) = \emptyset$ (ggf. nach Umbenennung). Sei $l_1 = C(t)$, wobei $t$ nicht nur eine Variable ist, so dass $t$ und $l_2$ unifizierbar sind. Sei $\sigma = mgu(t, l_2)$. Dann heißt $(r_1\sigma, C(r_2)\sigma)$ ein kritisches Paar.
|
|
\item Ein TES $T$ ist genau dann lokal konfluent, wenn in $T$ alle kritischen Paare zusammenführbar sind. \satz{2.60}{24}
|
|
\item Ein stark normalisierendes und lokal konfluentes TES ist konfluent. \satz{2.51}{21}
|
|
\end{itemize}
|
|
\section*{$\lambda$-Kalkül}
|
|
\subsection*{Ungetypt}
|
|
\begin{itemize}
|
|
\item $\beta$-Reduktion
|
|
\begin{equation*}
|
|
(\lambda x.t)s \bred t[s/x]
|
|
\end{equation*}
|
|
\item $\eta$-Reduktion
|
|
\begin{equation*}
|
|
\lambda x.yx \ered y
|
|
\end{equation*}
|
|
\item $\alpha$-Äquivalenz: $t_1 =_\alpha t_2$, wenn $t_2$ durch Umbenennung gebundener Variablen aus $t_1$ hervorgeht, formal: \defin{3.6}{31}
|
|
\begin{align*}
|
|
\underbrace{\lambda x.u}_{t_1} =_\alpha \underbrace{\lambda y.u[y/x]}_{t_2} &&\text{wenn } y \notin FV(u)
|
|
\end{align*}
|
|
\end{itemize}
|
|
\subsubsection*{Auswertungsstrategien}
|
|
\begin{itemize}
|
|
\item applikativ (\textit{leftmost-innermost}) \app \defin{3.13}{33}
|
|
\begin{itemize}
|
|
\item $\lambda x.t \app \lambda x.t'$, wenn $t \app t'$
|
|
\item $ts \app t's$, wenn $t \app t'$
|
|
\item $ts \app ts'$, wenn $s\app s'$ und $t$ normal ist
|
|
\item $(\lambda x.t)s \app t\lbrack s/x\rbrack$, wenn $t$ und $s$ normal sind
|
|
\item effizient
|
|
\end{itemize}
|
|
\item normal (\textit{leftmost-outermost}) \norm \defin{3.14}{34}
|
|
\begin{itemize}
|
|
\item $(\lambda x.t) s \norm t\lbrack s/x\rbrack$
|
|
\item $\lambda x.t \norm \lambda x.t'$, wenn $t\norm t'$
|
|
\item $ts \norm t's$ wenn $t\norm t'$ und $t$ keine $\lambda$-Abstraktion ist
|
|
\item $ts \norm ts'$, wenn $s\norm s'$ und $t$ normal und keine $\lambda$-Abstraktion ist
|
|
\item terminiert immer, falls Normalform existiert (nach Standardisierungssatz) \satz{3.17}{35}
|
|
\end{itemize}
|
|
\end{itemize}
|
|
\subsection*{Einfach getypt $(\lambda \rightarrow)$}
|
|
\siehe{S. 39}\begin{itemize}
|
|
\item Church: Annotation der Variablen mit Typen, nur herleitbare Terme hinschreibbar
|
|
\item Curry: Alle Terme hinschreibbar, dann Aussondern der nicht typisierbaren
|
|
\item Typregeln: \siehe{S. 39}
|
|
\begin{prooftree}
|
|
\AxiomC{}
|
|
\LeftLabel{$(Ax)$}
|
|
\RightLabel{$x:\alpha \in \Gamma$}
|
|
\UnaryInfC{$\Gamma \vdash x:\alpha$}
|
|
\end{prooftree}
|
|
\begin{prooftree}
|
|
\AxiomC{$\Gamma \vdash t:\alpha\rightarrow \beta$}
|
|
\AxiomC{$\Gamma \vdash s:\alpha$}
|
|
\LeftLabel{$(\rightarrow_e)$}
|
|
\BinaryInfC{$\Gamma \vdash ts:\beta$}
|
|
\end{prooftree}
|
|
\begin{prooftree}
|
|
\AxiomC{$\Gamma, x:\alpha \vdash t:\beta$}
|
|
\LeftLabel{$(\rightarrow_i)$}
|
|
\UnaryInfC{$\Gamma \vdash \lambda x.t:\alpha\rightarrow\beta$}
|
|
\end{prooftree}
|
|
\item Typisierungsprobleme \siehe{S. 40}
|
|
\begin{itemize}
|
|
\item Typcheck: \enquote{Gilt $\Gamma \vdash t:\alpha$?}
|
|
\item Typinferenz: \enquote{Was ist das beste $\alpha$ / Existiert $\alpha$ mit $\Gamma \vdash t:\alpha$?}
|
|
\item Type inhabitation: \enquote{Existiert $t$ mit $\Gamma t:\alpha$?}
|
|
\end{itemize}
|
|
\item Inversionslemma \lem{3.29}{41}
|
|
\begin{enumerate}
|
|
\item $\Gamma \vdash x:\alpha \Rightarrow x:\alpha\in\Gamma$
|
|
\item $\Gamma \vdash ts:\beta \Rightarrow \exists\alpha$ mit $\Gamma \vdash t:\alpha\rightarrow\beta$ und $\Gamma\vdash s:\alpha$
|
|
\item $\Gamma \vdash\lambda x.t:\gamma \Rightarrow \gamma = \alpha\rightarrow \beta$ mit $\Gamma, x:\alpha \vdash t:\beta$
|
|
\end{enumerate}
|
|
\item Typinferenz \siehe{S. 41}
|
|
\begin{itemize}
|
|
\item Typsubstitution $\sigma$ ist Lösung von $\Gamma \vdash t:\alpha$, wenn $\Gamma\sigma \vdash t:\alpha\sigma$ herleitbar
|
|
\item Substitutionen: $\sigma_1$ allgemeiner als $\sigma_2 \Leftrightarrow \exists \tau. \sigma_1\tau = \sigma_2$ \siehe{GLoIn, S. 38}
|
|
\item Prinzipaltyp von $\Gamma, t$ ist $\sigma(a)$ für allgemeinste Lösung $\sigma$ von $\Gamma\vdash t:a$ ($a$ frisch)
|
|
\item Algorithmus W (Hindley/Milner) \alg{3.31}{42}
|
|
\begin{itemize}
|
|
\item Menge $PT$ von Typgleichungen
|
|
\begin{align*}
|
|
PT(\Gamma;x;\alpha) &= \lbrace \alpha \pteq \beta ~\vert~ x:\beta \in \Gamma\rbrace\\
|
|
PT(\Gamma; \lambda x.t; \alpha) &= PT((\Gamma;x:a);t;b) \cup \lbrace a\rightarrow b \pteq \alpha \rbrace\ \text{mit $a,b$ frisch}\\
|
|
PT(\Gamma;ts;\alpha) &= PT(\Gamma; t; a\rightarrow \alpha ) \cup PT(\Gamma;s;a)\ \text{mit $a$ frisch}
|
|
\end{align*}
|
|
\item Typinferenz des Terms $u$ mit leerem Kontext:
|
|
\begin{equation*}
|
|
\upvarepsilon \coloneqq PT(\emptyset;u;a)
|
|
\end{equation*}
|
|
$\Rightarrow$ Prinzipaltyp von $u$: $\text{mgu}(\upvarepsilon)(a)$
|
|
\end{itemize}
|
|
\end{itemize}
|
|
\item Subjektreduktion: Wenn $\Gamma\vdash t:\alpha$ und $t \rightarrow_\beta^* s$, dann auch $\Gamma \vdash s:\alpha$, aber nicht umgekehrt! \satz{3.38}{45}
|
|
\end{itemize}
|
|
\section*{Induktive Datentypen}
|
|
\subsection*{Mengenkonstruktionen} \defin{4.12}{56}\lem{4.13}{57}
|
|
\begin{align*}
|
|
X_1 \times X_2 &= \left\lbrace \left(x_1, x_2\right)\vert x_i \in X_i\text{ für } i=1,2\right\rbrace &&\text{(\enquote{struct})}\\
|
|
X_1 + X_2 &= \left\lbrace (i,x) \vert i=1,2, x\in X_i\right\rbrace &&\text{(\enquote{union})}\\
|
|
1 &= \left\lbrace * \right\rbrace &&\text{\enquote{()} in Haskell}
|
|
\end{align*}
|
|
|
|
Seien $f_i :X_i \rightarrow Y_i$, $g_i: X_i \rightarrow Z$ und $h_i : Z \rightarrow X_i$ mit $i \in \{1,2\}$.
|
|
\begin{align*}
|
|
f_1 \times f_2 &: X_1 \times X_2 \rightarrow Y_1 \times Y_2, & (f_1\times f_2) (x_1, x_2) &= (f_1(x_1), f_2(x_2))\\
|
|
f_1 + f_2 &: X_1 + X_2 \rightarrow Y_1 + Y_2, & (f_1+f_2)(i,x) &= (i, f_i(x))\\
|
|
[g_1, g_2] &: X_1 + X_2 \rightarrow Z, & [g_1, g_2])(i,x) &= g_i(x)\\
|
|
\langle h_1, h_2\rangle &: Z\rightarrow X_1\times X_2, & \langle h_1, h_2\rangle(z) &= (h_1(z), h_2(z))\\
|
|
in_i &: X_i \rightarrow X_1 + X_2, & in_i(x) &= (i,x)\\
|
|
\pi_i &: X_1\times X_2 \rightarrow X_i, & \pi_i(x_1,x_2) &= x_i\\
|
|
1&: 1\rightarrow 1
|
|
\end{align*}
|
|
|
|
Es gilt
|
|
\begin{align*}
|
|
[g_1, g_2] \circ in_i &= g_i\\
|
|
f_1 + f_2 &= [in_1 \circ f_1, in_2 \circ f_2]\\
|
|
[r\circ in_1, r\circ in_2] &= r \text{ für } r: X_1+X_2 \rightarrow Z\\
|
|
\pi_i \circ \langle h_1, h_2\rangle &= h_i\\
|
|
f_1 \times f_2 &= \langle f_1 \circ\pi_1, f_2\circ\pi_2\rangle\\
|
|
\langle\pi_i \circ f, \pi_2\circ f\rangle &= f \text{ für } f: Z\rightarrow X_1\times X_2
|
|
\end{align*}
|
|
\subsection*{Strukturelle Induktion}
|
|
\begin{itemize}
|
|
\item über einsortige Datentypen \siehe{S. 63}
|
|
\begin{itemize}
|
|
\item Induktionsanfang: \enquote{Anfangs}-Konstruktor (etwa $Nil$)
|
|
\item Induktionsschritt: alle anderen Konstruktoren (etwa $cons$)
|
|
\end{itemize}
|
|
\item über mehrsortige Datentypen \siehe{S. 64}
|
|
\begin{itemize}
|
|
\item Funktionen müssen immer auf allen Datentypen definiert werden
|
|
\end{itemize}
|
|
\end{itemize}
|
|
\subsection*{Kodatentypen}
|
|
\begin{itemize}
|
|
\item Definition über \enquote{Destruktoren} etwa $hd$ und $tl$
|
|
\end{itemize}
|
|
\subsection*{Koinduktion}
|
|
\begin{itemize}
|
|
\item Bisimulation $R\subseteq A^\omega \times A^\omega$, wenn für alle $(s,t) \in R$ gilt: \defin{4.39}{74}
|
|
\begin{align*}
|
|
hd\ s &= hd\ t\\
|
|
(tl\ s)\ &R\ (tl\ t)
|
|
\end{align*}
|
|
\item Wenn $R$ eine Bisimulation ist, gilt $sRt \Rightarrow s=t$ \satz{4.40}{74}
|
|
\end{itemize}
|
|
\section*{System F}
|
|
\subsection*{Curry}
|
|
\begin{itemize}
|
|
\item Typen:\defin{5.1}{84}
|
|
\begin{align*}
|
|
\alpha, \beta \coloneqq a\ \vert\ \alpha \rightarrow \beta\ \vert\ \forall a.\alpha && (a\in V)
|
|
\end{align*}
|
|
\item Typisierung: \defin{5.1}{84}
|
|
\begin{prooftree}
|
|
\AxiomC{}
|
|
\LeftLabel{$(Ax)$}
|
|
\RightLabel{$(x:\alpha \in \Gamma)$}
|
|
\UnaryInfC{$\Gamma \vdash x:\alpha$}
|
|
\end{prooftree}
|
|
\begin{prooftree}
|
|
\AxiomC{$\Gamma \vdash t:\alpha\rightarrow \beta$}
|
|
\AxiomC{$\Gamma \vdash s:\alpha$}
|
|
\LeftLabel{$(\rightarrow_e)$}
|
|
\BinaryInfC{$\Gamma \vdash ts:\beta$}
|
|
\end{prooftree}
|
|
\begin{prooftree}
|
|
\AxiomC{$\Gamma, x:\alpha \vdash t:\beta$}
|
|
\LeftLabel{$(\rightarrow_i)$}
|
|
\UnaryInfC{$\Gamma \vdash \lambda x.t:\alpha\rightarrow\beta$}
|
|
\end{prooftree}
|
|
\begin{prooftree}
|
|
\AxiomC{$\Gamma \vdash s:\alpha$}
|
|
\AxiomC{$a\notin FV(\Gamma)$}
|
|
\LeftLabel{$(\forall_i)$}
|
|
\BinaryInfC{$\Gamma \vdash s:\forall a.\alpha$}
|
|
\end{prooftree}
|
|
\begin{prooftree}
|
|
\AxiomC{$\Gamma \vdash s:\forall a.\alpha$}
|
|
\LeftLabel{$(\forall_e)$}
|
|
\UnaryInfC{$\Gamma \vdash s:(\alpha[\beta/a])$}
|
|
\end{prooftree}
|
|
\end{itemize}
|
|
\subsection*{Church-Kodierung}\siehe{S. 84}
|
|
\begin{itemize}
|
|
\item Natürliche Zahlen
|
|
\begin{align*}
|
|
\mathbb{N}\ &\coloneqq \forall a.(a\rightarrow a) \rightarrow a \rightarrow a\\
|
|
zero\ &: \mathbb{N}\\
|
|
zero\ &= \lambda fx.x\\
|
|
suc\ &: \mathbb{N}\rightarrow\mathbb{N}\\
|
|
suc\ &= \lambda nfx.f(nfx)\\
|
|
fold\ &: \forall a.(a\rightarrow a) \rightarrow a \rightarrow \mathbb{N}\rightarrow a\\
|
|
fold\ &= \lambda fxn.nfx\\
|
|
add &: \mathbb{N}\rightarrow\mathbb{N}\rightarrow\mathbb{N}\\
|
|
add &= \lambda n.fold\ suc\ n
|
|
\end{align*}
|
|
\item Paare
|
|
\begin{align*}
|
|
(a\times b)\ &\coloneqq \forall r.(a\rightarrow b\rightarrow r)\rightarrow r\\
|
|
pair\ &: \forall ab.a\rightarrow b\rightarrow (a\times b)\\
|
|
pair\ &= \lambda xyf.fxy\\
|
|
fst\ &: \forall ab.(a\times b) \rightarrow a\\
|
|
fst\ &= \lambda p.p (\lambda xy.x)\\
|
|
snd\ &: \forall ab.(a\times b) \rightarrow b\\
|
|
snd\ &= \lambda p.p(\lambda xy.y)
|
|
\end{align*}
|
|
\item Summen
|
|
\begin{align*}
|
|
(a+b)\ &\coloneqq \forall r.(a\rightarrow r) \rightarrow (b \rightarrow r)\rightarrow r\\
|
|
inl\ &: \forall ab.a\rightarrow(a+b)\\
|
|
inl\ &= \lambda xfg.fx\\
|
|
inr\ &: \forall ab.b\rightarrow(a+b)\\
|
|
inr\ &= \lambda yfg.gy\\
|
|
case\ &: \forall abs.(a\rightarrow s)\rightarrow (b\rightarrow s) \rightarrow (a+b) \rightarrow s\\
|
|
case\ &= \lambda fgs.sfg
|
|
\end{align*}
|
|
\item Listen
|
|
\begin{align*}
|
|
List\ a\ &\coloneqq \forall r.r\rightarrow (a\rightarrow r\rightarrow r)\rightarrow r\\
|
|
Nil\ &: \forall a.Lista\ a\\
|
|
Nil\ &= \lambda uf.u\\
|
|
Cons\ &: \forall a.a\rightarrow List\ a\rightarrow List\ a\\
|
|
Cons\ &= \lambda xluf.fx(luf)\\
|
|
len\ &: \forall a.List\ a\rightarrow \mathbb{N}\\
|
|
len\ &= \lambda l.l\ zero\ (\lambda xr.suc\ r)
|
|
\end{align*}
|
|
\end{itemize}
|
|
\subsection*{ML-Polymorphie}
|
|
\begin{itemize}
|
|
\item Einschränkung von System F durch $\forall$ nur auf oberster Ebene sowie Mehrfachinstanziierung polymorpher Funktionen nur in $let$-Konstrukt \siehe{S. 88}
|
|
\item Typen
|
|
\begin{equation*}
|
|
\alpha, \beta \coloneqq a\ \vert\ \alpha \rightarrow \beta
|
|
\end{equation*}
|
|
\item Typschemata
|
|
\begin{align*}
|
|
S \coloneqq \forall a_1, \ldots, a_k.\alpha &&(k\geq 0)
|
|
\end{align*}
|
|
\item Terme
|
|
\begin{equation*}
|
|
t,s \coloneqq x\ \vert\ t\ s\ \vert\ \lambda x.t\ \vert\ let\ x = t\ in\ s
|
|
\end{equation*}
|
|
\item Kontexte
|
|
\begin{align*}
|
|
\Gamma &= ( x_1:S_1,\ldots, x_n :S_n )\\
|
|
Cl(\Gamma, \alpha) &= \forall a_1,\ldots,a_k.\alpha &&\text{für $FV(\alpha)\backslash FV(\Gamma) = \lbrace a_1,\ldots,a_k \rbrace$}
|
|
\end{align*}
|
|
\item Typisierungsregeln \siehe{S. 88}
|
|
\begin{prooftree}
|
|
\AxiomC{}
|
|
\LeftLabel{$(\forall_e)$}
|
|
\RightLabel{$(x:\forall a_1,\ldots, \forall a_k .\alpha) \in \Gamma$}
|
|
\UnaryInfC{$\Gamma \vdash x:\alpha[\beta_1/a_1,\ldots, \beta_k/a_k]$}
|
|
\end{prooftree}
|
|
\begin{prooftree}
|
|
\AxiomC{$\Gamma, x:\alpha \vdash t:\beta$}
|
|
\LeftLabel{$(\rightarrow_i)$}
|
|
\UnaryInfC{$\Gamma \vdash \lambda x.t:\alpha\rightarrow\beta$}
|
|
\end{prooftree}
|
|
\begin{prooftree}
|
|
\AxiomC{$\Gamma \vdash t:\alpha\rightarrow \beta$}
|
|
\AxiomC{$\Gamma \vdash s:\alpha$}
|
|
\LeftLabel{$(\rightarrow_e)$}
|
|
\BinaryInfC{$\Gamma \vdash ts:\beta$}
|
|
\end{prooftree}
|
|
\begin{prooftree}
|
|
\AxiomC{$\Gamma \vdash t:\alpha$}
|
|
\AxiomC{$\Gamma, x:Cl(\Gamma, \alpha)\vdash s:\beta$}
|
|
\LeftLabel{(let)}
|
|
\BinaryInfC{$\Gamma \vdash$ let $x = t$ in $s:\beta$}
|
|
\end{prooftree}
|
|
\item Inversionslemma \siehe{S. 89}
|
|
\begin{enumerate}
|
|
\item Wenn $\Gamma \vdash x:\alpha$, dann existieren Typen $\beta_i$ und ein Typschema $S = \forall a_1 \ldots \forall a_k.\gamma$, so dass $(x:S)\in \Gamma$ und $\alpha = \gamma[\beta_1/a_1,\ldots,\beta_k/a_k]$
|
|
\item Wenn $\Gamma \vdash ($ let $x = s$ in $t) : \alpha$, dann existiert ein Typ $\beta$ nut $\Gamma \vdash s:\beta$ und $\Gamma, x:Cl(\Gamma, \beta) \vdash t:\alpha$
|
|
\end{enumerate}
|
|
\item erweiterter Algorithmus W mit Menge $PT$ von Typgleichungen \siehe{S. 90}
|
|
\begin{align*}
|
|
PT(\Gamma;x;\alpha) &= \lbrace \alpha \pteq \gamma [a_1'/a_1,\ldots,a_k'/a_k] \rbrace \text{ mit } (x: \forall a_1,\ldots,\forall a_k .\gamma) \in \Gamma\\
|
|
PT(\Gamma; \lambda x.t; \alpha) &= PT((\Gamma;x:a);t;b) \cup \lbrace a\rightarrow b \pteq \alpha \rbrace\ \text{mit $a,b$ frisch}\\
|
|
PT(\Gamma;ts;\alpha) &= PT(\Gamma; t; a\rightarrow \alpha ) \cup PT(\Gamma;s;a)\ \text{mit $a$ frisch}\\
|
|
PT(\Gamma;(\text{let } x=s\text{ in }t);\alpha) &= PT(\Gamma\sigma, x:Cl(\Gamma\sigma, \sigma(b));t;\alpha\sigma)
|
|
\end{align*}
|
|
wobei $\sigma = mgu(PT(\Gamma;s;b))$ mit $b$ frisch
|
|
\end{itemize}
|
|
\section*{Minimierung von deterministischen endlichen Automaten}
|
|
\begin{enumerate}
|
|
\item Entferne aus $Q$ alle nicht erreichbaren Zustände
|
|
\item Initialisiere $R$ auf $\lbrace (q_1, q_2)\ \vert\ q_1 \in F \Leftrightarrow q_2 \in F\rbrace$
|
|
\item Suche ein Paar $(q_1,q_2) \in R$ und einen Buchstaben $a \in \Sigma$ mit
|
|
\begin{equation*}
|
|
(\delta(a,q_1),\delta(a,q_2)) \notin R
|
|
\end{equation*}
|
|
Wenn kein solches Paar gefunden wird, gehe zu Schritt 4. Andernfalls entferne $(q_1,q_2)$ aus $R$ und fahre bei 3. fort.
|
|
\item Identifiziere alle Zustandspaare in $R$.
|
|
\end{enumerate}
|
|
\section*{Unifikationsalgorithmus (Martelli/Montanari)}
|
|
\begin{align*}
|
|
&S \cup \lbrace x \pteq x\rbrace &&\rightarrow S &&\text{(delete)}\\
|
|
&S \cup \lbrace f(E_1, \ldots, E_n) \pteq f(D_1, \ldots, D_n)\rbrace &&\rightarrow S \cup \lbrace E_1 \pteq D_1, \ldots, E_n \pteq D_n\rbrace &&\text{(decomp)}\\
|
|
&S \cup \lbrace f(E_1, \ldots, E_n) \pteq g(D_1, \ldots, D_k)\rbrace &&\rightarrow \bot \text{ (für $f \not = g$)} &&\text{(conflict)}\\
|
|
&S \cup \lbrace E \pteq x \rbrace &&\rightarrow S \cup \lbrace x \pteq E \rbrace \text{ (für $E$ keine Variable)} &&\text{(orient)}\\
|
|
&S \cup \lbrace x \pteq E \rbrace &&\rightarrow \begin{cases*}
|
|
\bot (\text{für }x \in FV(E), x\not = E) \\
|
|
S\lbrack E/x\rbrack \cup \lbrace x \pteq E\rbrace (\text{für }x\notin FV(E), x\in FV(S))
|
|
\end{cases*} && \text{ (occurs)/(elim)}
|
|
\end{align*}
|
|
\section*{Notation}
|
|
\begin{itemize}
|
|
\item Applikation ist links-assoziativ: $((x(yz))u)v = x(yz)uv$
|
|
\item Abstraktion reicht so weit wie möglich: $\lambda x.(x(\lambda y.(yx))) = \lambda x.x(\lambda y.yx)$
|
|
\item Aufeinanderfolgende Abstraktionen werden zusammengefasst: $\lambda x.\lambda y.\lambda z.yx = \lambda xyz.yz$
|
|
\end{itemize}
|
|
\section*{Definitionen aus der Übung}
|
|
\begin{align*}
|
|
flip\ &= \lambda f\ x\ y.f\ y\ x\\
|
|
const\ &= \lambda x\ y.x\\
|
|
twice\ &= \lambda f\ x.f\ (f\ x)
|
|
\end{align*}
|
|
\begin{align*}
|
|
true\ &= \lambda x\ y.x\\
|
|
false\ &= \lambda x\ y.y\\
|
|
if\_then\_else\ &= \lambda b\ x\ y.b\ x\ y
|
|
\end{align*}
|
|
\begin{align*}
|
|
pair\ a\ b\ &= \lambda select.select\ a\ b\\
|
|
fst\ p\ &= p\ (\lambda x\ y.x)\\
|
|
snd\ p\ &= p\ (\lambda x\ y.y)\\
|
|
swap\ p\ &= p\ (\lambda x\ y\ select.select\ y\ x)
|
|
\end{align*}
|
|
\begin{align*}
|
|
zero\ &= \lambda f\ a.a\\
|
|
succ\ n\ &= \lambda f\ a. f\ (n\ f\ a)\\
|
|
add\ n\ m\ &= \lambda f\ a. n\ f\ (m\ f\ a) = n\ succ\ m\\
|
|
mult\ n\ m\ &= \lambda f\ a.n\ (m\ f)\ a = n\ (add\ m)\ 0\\
|
|
isZero\ n &= n\ (\lambda x.false)\ true\\
|
|
odd\ n\ & if\ (n == 0)\ then\ true\ else\ (not\ (odd\ n-\lceil 1\rceil ))
|
|
\end{align*}
|
|
\begin{align*}
|
|
length\ Nil\ &= 0\\
|
|
length\ (Cons\ x\ xs)\ &= 1 + length(xs)
|
|
\end{align*}
|
|
\begin{align*}
|
|
snoc\ Nil\ x\ &= Cons\ x\ Nil\\
|
|
snoc\ (Cons\ x\ xs)\ y\ &= Cons\ x\ (snoc\ xs\ y)
|
|
\end{align*}
|
|
\begin{align*}
|
|
reverse\ Nil\ &= Nil\\
|
|
reverse\ (Cons\ x\ xs)\ &= snoc\ reverse(xs)\ x
|
|
\end{align*}
|
|
\begin{align*}
|
|
drop\ y\ Nil\ = Nil\\
|
|
drop\ y\ (Cons\ x\ xs) &= \begin{cases*}
|
|
drop\ y\ xs\ \text{, falls } y=x\\
|
|
Cons\ x\ (drop\ y\ xs)\ \text{, sonst}
|
|
\end{cases*}
|
|
\end{align*}
|
|
\begin{align*}
|
|
elem\ y\ Nil\ &= False\\
|
|
elem\ y\ (Cons\ x\ xs) &= \begin{cases*}
|
|
True\ \text{, falls x=y}\\
|
|
elem\ y\ xs\ \text{, sonst}
|
|
\end{cases*}
|
|
\end{align*}
|
|
\begin{align*}
|
|
minimum\ Nil\ &= 0\\
|
|
minimum\ (Cons\ x\ xs)\ &= \begin{cases*}
|
|
x\ \text{, falls $minimum\ xs$ = 0}\\
|
|
min\ x\ (minimum\ xs)\ \text{, sonst}
|
|
\end{cases*}
|
|
\end{align*}
|
|
\begin{align*}
|
|
Nil \oplus ys &= ys\\
|
|
(Cons\ x\ xs) \oplus ys\ &= Cons\ x\ (xs \oplus ys)
|
|
\end{align*}
|
|
\end{document} |