Definitionen aus Übung

This commit is contained in:
Marco Ammon 2018-10-08 16:53:31 +02:00
parent 18acfc5469
commit 34cca3fd19
2 changed files with 66 additions and 0 deletions

Binary file not shown.

View File

@ -72,6 +72,7 @@ Wir definieren $A \subseteq \mathbb{N}$ und für jede $n$-stellige Operation $f$
\begin{equation*} \begin{equation*}
\lambda x.yx \ered y \lambda x.yx \ered y
\end{equation*} \end{equation*}
\item \textbf{TODO} $\alpha$-Äquivalenz
\end{itemize} \end{itemize}
\subsubsection*{Auswertungsstrategien} \subsubsection*{Auswertungsstrategien}
\begin{itemize} \begin{itemize}
@ -363,4 +364,69 @@ f_1 \times f_2 &= \langle f_1 \circ\pi_1, f_2\circ\pi_2\rangle\\
S\lbrack E/x\rbrack \cup \lbrace x \pteq E\rbrace (\text{für }x\notin FV(E), x\in FV(S)) 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{cases*} && \text{ (occurs)/(elim)}
\end{align*} \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*}
\subsection*{Church-Kodierung}
\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*}
\end{document} \end{document}