diff --git a/documents/Programmierparadigmen/Lambda.tex b/documents/Programmierparadigmen/Lambda.tex index 9eb10d2..feabfeb 100644 --- a/documents/Programmierparadigmen/Lambda.tex +++ b/documents/Programmierparadigmen/Lambda.tex @@ -190,6 +190,12 @@ Auch die gewohnten Operationen lassen sich so darstellen. \texttt{False} wird zu $c_{\text{false}} := \lambda t. \lambda f. f$. \end{definition} +Hiermit lässt sich beispielsweise die Funktion \texttt{is\_zero} definieren, die +\texttt{True} zurückgibt, wenn eine Zahl $0$ repräsentiert und sonst \texttt{False} +zurückgibt: + +\[ \text{\texttt{is\_zero}} = \lambda n.\ n\ (\lambda x.\ c_{\text{False}})\ c_{\text{True}}\] + \section{Weiteres} \begin{satz}[Satz von Curch-Rosser] Wenn zwei unterschiedliche Terme $a$ und $b$ äquivalent sind, d.h. mit Reduktionsschritten beliebiger Richtung ineinander transformiert werden können, dann gibt es einen weiteren Term $c$, zu dem sowohl $a$ als auch $b$ reduziert werden können. diff --git a/documents/Programmierparadigmen/Programmierparadigmen.pdf b/documents/Programmierparadigmen/Programmierparadigmen.pdf index 6e709b6..f96bf23 100644 Binary files a/documents/Programmierparadigmen/Programmierparadigmen.pdf and b/documents/Programmierparadigmen/Programmierparadigmen.pdf differ diff --git a/documents/Programmierparadigmen/Programmierparadigmen.tex b/documents/Programmierparadigmen/Programmierparadigmen.tex index b5f0fe8..fea9ead 100644 --- a/documents/Programmierparadigmen/Programmierparadigmen.tex +++ b/documents/Programmierparadigmen/Programmierparadigmen.tex @@ -46,6 +46,13 @@ \usepackage{tqft} \usepackage{xspace} % for new commands; decides weather I want to insert a space after the command \usepackage[german,nameinlink]{cleveref} % has to be after hyperref, ntheorem, amsthm +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\usepackage{array,xtab,ragged2e} % for symbol table +\newlength\mylengtha +\newlength\mylengthb +\newcolumntype{P}[1]{>{\RaggedRight}p{#1}} +\tabcolsep=3pt % default: 6pt +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \usepackage{acronym} \usepackage{minted} % needed for the inclusion of source code \usemintedstyle{bw} diff --git a/documents/Programmierparadigmen/Symbolverzeichnis.tex b/documents/Programmierparadigmen/Symbolverzeichnis.tex index 32c9ef2..c3a29a4 100644 --- a/documents/Programmierparadigmen/Symbolverzeichnis.tex +++ b/documents/Programmierparadigmen/Symbolverzeichnis.tex @@ -6,29 +6,45 @@ % Reguläre Ausdrücke % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section*{Reguläre Ausdrücke} -$\emptyset\;\;\;$ Leere Menge\\ -$\epsilon\;\;\;$ Das leere Wort\\ -$\alpha, \beta\;\;\;$ Reguläre Ausdrücke\\ -$L(\alpha)\;\;\;$ Die durch $\alpha$ beschriebene Sprache\\ -$\begin{aligned}[t] - L(\alpha | \beta) &= L(\alpha) \cup L(\beta)\\ - L(\alpha \cdot \beta)&= L(\alpha) \cdot L(\beta) -\end{aligned}$\\ -$L^0 := \Set{\varepsilon}\;\;\;$ Die leere Sprache\\ -$L^{n+1} := L^n \circ L \text{ für } n \in \mdn_0\;\;\;$ Potenz einer Sprache\\ -$\begin{aligned}[t] - \alpha^+ &=& L(\alpha)^+ &=& \bigcup_{i \in \mdn} L(\alpha)^i\\ - \alpha^* &=& L(\alpha)^* &=& \bigcup_{i \in \mdn_0} L(\alpha)^i -\end{aligned}$ + +% Set \mylengtha to widest element in first column; adjust +% \mylengthb so that the width of the table is \columnwidth +\settowidth\mylengtha{$\alpha^+ = L(\alpha)^+$} +\setlength\mylengthb{\dimexpr\columnwidth-\mylengtha-2\tabcolsep\relax} + +\begin{xtabular}{@{} p{\mylengtha} P{\mylengthb} @{}} + $\emptyset$ & Leere Menge\\ + $\epsilon$ & Das leere Wort\\ + $\alpha, \beta$ & Reguläre Ausdrücke\\ + $L(\alpha)$ & Die durch $\alpha$ beschriebene Sprache\\ + $L(\alpha | \beta)$& $L(\alpha) \cup L(\beta)$\\ + $L^0$ & Die leere Sprache, also $\Set{\varepsilon}$\\ + $L^{n+1}$ & Potenz einer Sprache. Diese ist definiert als\newline $L^n \circ L \text{ für } n \in \mdn_0$\\ + $\alpha^+ = L(\alpha)^+$ & $\bigcup_{i \in \mdn} L(\alpha)^i$\\ + $\alpha^* = L(\alpha)^*$ & $\bigcup_{i \in \mdn_0} L(\alpha)^i$\\ +\end{xtabular} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Logik % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section*{Logik} -$\mathcal{M} \models \varphi\;\;\;$ Im Modell $\mathcal{M}$ gilt das Prädikat $\varphi$.\\ -$\psi \vdash \varphi\;\;\;$ Die Formel $\varphi$ kann aus der Menge der Formeln $\psi$ hergeleitet werden.\\ + +\settowidth\mylengtha{$\mathcal{M} \models \varphi$} +\setlength\mylengthb{\dimexpr\columnwidth-\mylengtha-2\tabcolsep\relax} + +\begin{xtabular}{@{} p{\mylengtha} P{\mylengthb} @{}} +$\mathcal{M} \models \varphi$& Im Modell $\mathcal{M}$ gilt das Prädikat $\varphi$.\\ +$\psi \vdash \varphi$ & Die Formel $\varphi$ kann aus der Menge der Formeln $\psi$ hergeleitet werden.\\ +\end{xtabular} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Weiteres % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section*{Weiteres} -$\bot\;\;\;$ Bottom\\ \ No newline at end of file + +\settowidth\mylengtha{$\bot$} +\setlength\mylengthb{\dimexpr\columnwidth-\mylengtha-2\tabcolsep\relax} + +\begin{xtabular}{@{} p{\mylengtha} P{\mylengthb} @{}} +$\bot$ & Bottom\\ +$\vdash$& TODO? +\end{xtabular} \ No newline at end of file diff --git a/documents/Programmierparadigmen/Typinferenz.tex b/documents/Programmierparadigmen/Typinferenz.tex index c67ce90..147f9d0 100644 --- a/documents/Programmierparadigmen/Typinferenz.tex +++ b/documents/Programmierparadigmen/Typinferenz.tex @@ -66,15 +66,19 @@ Mit folgenderweise typisiert werden: In der letzten Typisierung stellt $\alpha$ einen beliebigen Typen dar. -Ein Typkontext $\Gamma$ ordnet jeder freien Variable $x$ einen Typ $\Gamma(x)$ -durch folgende Regeln zu: +\begin{definition}[Typsystem $\Gamma \vdash t: T$]\label{def:typsystem-t1} + Ein Typkontext $\Gamma$ ordnet jeder freien Variable $x$ einen Typ $\Gamma(x)$ + durch folgende Regeln zu: + + \begin{align*} + \CONST:&\frac{c \in \text{Const}}{\Gamma \vdash c: \tau_c}\\ + \VAR: &\frac{\Gamma(x) = \tau}{\Gamma \vdash c: \tau}\\ + \ABS: &\frac{\Gamma, x: \tau_1 \vdash t: \tau_2}{\Gamma \vdash \lambda x. t: \tau_1 \rightarrow \tau_2}\\ + \APP: &\frac{\Gamma \vdash t_1, \tau_2 \tau\;\;\; \Gamma \vdash t_2: \tau_2}{\Gamma \vdash t_1 t_2: \tau} + \end{align*} +\end{definition} + -\begin{align*} - \text{\texttt{CONST}}:&\frac{c \in \text{Const}}{\Gamma \vdash c: \tau_c}\\ - \text{\texttt{VAR}}: &\frac{\Gamma(x) = \tau}{\Gamma \vdash c: \tau}\\ - \text{\texttt{ABS}}: &\frac{\Gamma, x: \tau_1 \vdash t: \tau_2}{\Gamma \vdash \lambda x. t: \tau_1 \rightarrow \tau_2}\\ - \text{\texttt{APP}}: &\frac{\Gamma \vdash t_1, \tau_2 \tau\;\;\; \Gamma \vdash t_2: \tau_2}{\Gamma \vdash t_1 t_2: \tau} -\end{align*} Dabei ist der lange Strich kein Bruchstrich, sondern ein Symbol der Logik das als \textbf{Schlussstrich}\xindex{Schlussstrich} bezeichnet wird. Dabei ist der @@ -95,4 +99,19 @@ verwendet. Man schreibt also beispielsweise: $(\sigma, \tau)$ heißt eine Lösung für $(\Gamma, t)$, falls gilt: \[\sigma \Gamma \vdash t : \tau\] -\end{definition} \ No newline at end of file +\end{definition} + +\section{Beispiele} +Im Folgenden wird die Typinferenz für einige $\lambda$-Funktionen durchgeführt. + +\subsection[$\lambda x.\ \lambda y.\ x\ y$]{$\lambda x.\ \lambda y.\ x\ y$\footnote{Lösung von Übungsblatt 6, WS 2013 / 2014}} +Gesucht ist ein Typ $\tau$, sodass sich $\vdash \lambda x.\ \lambda y.\ x\ y: \tau$ +mit einem Ableitungsbaum nachweisen lässt. Es gibt mehrere solche $\tau$, aber +wir suchen das allgemeinste. Die Regeln unseres Typsystems (siehe \cpageref{def:typsystem-t1}) +sind \textit{syntaxgerichtet}, d.~h. zu jedem $\lambda$-(Teil)-Term gibt es genau +eine passende Regel. + +Für $\lambda x.\ \lambda y.\ x\ y$ wissen wir also schon, dass jeder Ableitungsbaum +von folgender Gestalt ist. Dabei sind $\alpha_i$ Platzhalter: + +\[\ABS \frac{}{\vdash}\] \ No newline at end of file diff --git a/documents/Programmierparadigmen/shortcuts.sty b/documents/Programmierparadigmen/shortcuts.sty index a6da775..a1cad29 100644 --- a/documents/Programmierparadigmen/shortcuts.sty +++ b/documents/Programmierparadigmen/shortcuts.sty @@ -76,6 +76,10 @@ \DeclareMathOperator{\pair}{pair} \DeclareMathOperator{\nxt}{next} \DeclareMathOperator{\pred}{pred} +\DeclareMathOperator{\ABS}{ABS} +\DeclareMathOperator{\VAR}{VAR} +\DeclareMathOperator{\CONST}{CONST} +\DeclareMathOperator{\APP}{APP} \let\succ\relax% Set equal to \relax so that LaTeX thinks it's not defined \DeclareMathOperator{\succ}{succ} \newcommand{\iu}{{i\mkern1mu}} % imaginary unit