some haskell / chruch numbers

documents/Programmierparadigmen/Haskell.tex

@@ -209,9 +209,13 @@ \subsection{Fibonacci}\xindex{Fibonacci}
 \inputminted[linenos, numbersep=5pt, tabsize=4, frame=lines, label=fibonacci-pattern-matching.hs]{haskell}{scripts/haskell/fibonacci-pattern-matching.hs}
 
 \subsection{Quicksort}
+TODO
+
 \subsection{Funktionen höherer Ordnung}\xindex{Folds}\xindex{foldl}\xindex{foldr}\label{bsp:foldl-und-foldr}
 \inputminted[linenos, numbersep=5pt, tabsize=4, frame=lines, label=folds.hs]{haskell}{scripts/haskell/folds.hs}
 
+\subsection{Chruch-Zahlen}
+\inputminted[linenos, numbersep=5pt, tabsize=4, frame=lines, label=church.hs]{haskell}{scripts/haskell/church.hs}
 
 \subsection{Standard Prelude}
 Hier sind die Definitionen eininger wichtiger Funktionen:

documents/Programmierparadigmen/Programmiersprachen.tex

@@ -133,9 +133,52 @@ \section{Dies und das}
 \begin{definition}[Unifikation]\xindex{Unifikation}%
     Die Unifikation ist eine Operation in der Logik und dient zur Vereinfachung
     prädikatenlogischer Ausdrücke.
-    \todo[inline]{Das ist keine formale Definition!}
+    Der Unifikator ist also eine Abbildung, die in einem Schritt dafür sorgt, dass
+    auf beiden Seiten der Gleichung das selbe steht.
 \end{definition}
 
-\begin{beispiel}[Unifikation]
-
+\begin{beispiel}[Unifikation\footnotemark]
+    Gegeben seien die Ausdrücke
+    \begin{align*}
+        A_1 &= \left(X, Y, f(b) \right)\\
+        A_2 &= \left(a, b, Z \right)
+    \end{align*}
+    Großbuchstaben stehen dabei für Variablen und Kleinbuchstaben für atomare 
+    Ausdrücke.
+
+    Ersetzt man in $A_1$ nun $X$ durch $a$, $Y$ durch $b$ und in $A_2$ 
+    die Variable $Z$ durch $f\left(b\right)$, so sind sie gleich oder 
+    \enquote{unifiziert}. Man erhält
+
+    \begin{align*}
+        \sigma(A_1) &= \left(a, b, f(b) \right)\\
+        \sigma(A_2) &= \left(a, b, f(b) \right)
+    \end{align*}
+
+    mit
+    \[\sigma = \{X \mapsto a, Y \mapsto b, Z \mapsto f(b)\}\]
 \end{beispiel}
+
+\begin{definition}[Allgemeinster Unifikator]\xindex{Unifikator!allgemeinster}%
+    Ein Unifikator $\sigma$ heißt \textit{allgemeinster Unifikator}, wenn 
+    es für jeden Unifikator $\gamma$ eine Substitution $\delta$ mit
+    \[\gamma = \delta \circ \sigma\]
+    gibt.
+\end{definition}
+
+\begin{beispiel}[Allgemeinster Unifikator\footnotemark]
+    Sei
+    \[C = \Set{f(a,D) = Y, X = g(b), g(Z) = X}\]
+    eine Menge von Gleichungen über Terme.
+
+    Dann ist 
+    \[\gamma = [Y \text{\pointer} f(a,b), D \text{\pointer} b, X \text{\pointer} g(b), Z \text{\pointer} b]\]
+    ein Unifikator für $C$. Jedoch ist
+    \[\sigma = [Y \text{\pointer} f(a,D), X \text{\pointer} g(b), Z \text{\pointer} b]\]
+    der allgemeinste Unifikator. Mit
+    \[\delta = [D \text{\pointer} b]\]
+    gilt $\gamma = \delta \circ \sigma$.
+\end{beispiel}
+\footnotetext{Folie 268 von Prof. Snelting}
+
+\footnotetext{\url{https://de.wikipedia.org/w/index.php?title=Unifikation\_(Logik)&oldid=116848554\#Beispiel}}

documents/Programmierparadigmen/scripts/haskell/church.hs

@@ -0,0 +1,8 @@
+type Church t = (t -> t) -> t -> t
+
+int2church :: Integer -> Church t
+int2church 0 s z = z
+int2church n s z = int2church (n - 1) s (s z)
+
+church2int :: Church Integer -> Integer
+church2int n = n (+1) 0