151 lines
6.3 KiB
TeX
151 lines
6.3 KiB
TeX
\documentclass[11pt,a4paper]{scrartcl}
|
|
\usepackage[a4paper,left=1.5cm,right=3.0cm,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{algorithmicx}
|
|
\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}{=}}}
|
|
|
|
\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}
|
|
\subsubsection*{Polynomordnungen}
|
|
\subsection*{Konfluenz}
|
|
\subsection*{Critical Pairs}
|
|
|
|
\section*{$\lambda$-Kalkül}
|
|
\subsection*{Ungetypt}
|
|
\subsubsection*{Rekursion}
|
|
\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$m 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{itemize}
|
|
\item \textbf{TODO}
|
|
\end{itemize}
|
|
\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} \textbf{TODO}
|
|
\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 a\pteq b \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*{Mehrsortigkeit}
|
|
\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}
|
|
\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}
|
|
\subsection*{Kodatentypen mit Alternativen}
|
|
\section*{System F}
|
|
\section*{Polymorphie}
|
|
\subsection*{ML-Polymorphie}
|
|
\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*}
|
|
\end{document} |