mirror of
https://gitlab.cs.fau.de/ik15ydit/latexandmore.git
synced 2024-11-22 19:59:31 +01:00
147 lines
5.0 KiB
TeX
147 lines
5.0 KiB
TeX
\documentclass{article}
|
|
\usepackage{amsmath}
|
|
\usepackage{nccmath}
|
|
%\usepackage{bussproofs}
|
|
%dieses Paket koennte man fuer die typherleitung verwenden wenn man wollte
|
|
\DeclareMathSizes{10}{10}{10}{10}
|
|
\setlength{\parindent}{0pt}
|
|
\title{System F und Reduktionsreihenfolge}
|
|
\date{ }
|
|
\begin{document}
|
|
\section{Generelles}
|
|
\subsection{Normale-/Lazy-Reduktion}
|
|
- pre-order durch Baum ("von unten nach oben auswerten") \\
|
|
- leftmost-outermost\\
|
|
- Argumente zum Schluss auswerten
|
|
\begin{align*}
|
|
pow(a,pow(c,b))\:\: & mit\;linkem\;pow\;anfangen\\
|
|
& dann\;a\\
|
|
& dann\;rechtes\;pow\\
|
|
& dann\;c\\
|
|
& dann\;d
|
|
\end{align*}
|
|
\subsection{Applikative Reduktion:}
|
|
- post-order durch Baum ("von oben nach unten")\\
|
|
- leftmost-innermost\\
|
|
- als erstes die Argumente auswerten
|
|
\begin{align*}
|
|
pow(a,pow(c,b))\:\: & mit\;c\;anfangen
|
|
\enspace\;\;\;\;\;\;\;\;\;\enspace\;\;\;\;
|
|
\\
|
|
& dann\;b\\
|
|
& dann\;a\\
|
|
& dann\;rechtes\;pow\\
|
|
& dann\;linkes\;pow
|
|
\end{align*}
|
|
\subsection{How to work with Lambda}
|
|
- Buchstabe hinter $\lambda $ wegnehmen\\
|
|
- Term von der respektiven Stelle hinten entfernen\\
|
|
- alle Vorkommen des Buchstabens mit dem Term ersetzen\\
|
|
- idealerweise bei mehreren $\lambda$ in einem Term \textbf{immer} verschiedene Buchstaben verwenden\\
|
|
- wenn nicht genug Terme zum Aufl\"osen von $\lambda$ vorhanden sind, nicht damit anfangen, also z.B. bei $pred\;\lambda\,f\,a\,.\,fa\;one$ nicht one f\"ur f einsetzen sondern $pred$ aufl\"osen
|
|
\section{SS15Probeklausur Beispielaufgabe}
|
|
\subsection*{1) Reduktion}
|
|
\subsubsection*{a) Normal/Lazy}
|
|
\begin{align*}
|
|
pow2\;three\; &=\; three\;(mult\;two)\;one\\
|
|
&=\; \lambda f\,a\, .\,f\,(\,f\,(\,f\;a\,)(\,mult\;two)\;one\\
|
|
&=\; \lambda a\, .\, (mult\;two)\,((mult\;two)\,((mult\;two)\;a\,)\;one\\
|
|
&=\; (mult\;two)\,((mult\;two)\,((mult\;two)\;one\,)
|
|
\end{align*}
|
|
\subsubsection*{b) Aplikativer Reihenfolge}
|
|
\begin{align*}
|
|
pow2\;three\; &=\; pow2\; (\, \lambda f\,a\, .\,f\,(\,f\,(\,f\;a\,) \,)\\
|
|
&=\; (\, \lambda f\,a\, .\,f\,(\,f\,(\,f\;a\,) \,)(mult\;two)\;one\\
|
|
&=\; (\, \lambda f\,a\, .\,f\,(\,f\,(\,f\;a\,) \,)(mult\;\lambda g\,b\, .\,g\,(\,g\;b\,))\;one\\
|
|
&=\; (\, \lambda f\,a\, .\,f\,(\,f\,(\,f\;a\,) \,)(mult\;\lambda g\,b\, .\,g\,(\,g\;b\,))\;(\lambda h\,c\, .\,h\;c)
|
|
\end{align*}
|
|
kleine Anmerkung hierzu noch:
|
|
\[
|
|
\underbrace{(\, \lambda f\,a\, .\,f\,(\,f\,(\,f\;a\,) \,)}_{oberste\;Funktion}
|
|
\underbrace{(mult\;\lambda g\,b\, .\,g\,(\,g\;b\,))}_{erstes\;Argument}
|
|
\;
|
|
\underbrace{(\lambda h\,c\, .\,h\;c)}_{zweites\;argument}
|
|
\]
|
|
d.h. wir w\"urden hier beim ersten Argument weitermachen und "mult" aufl\"osen
|
|
(beim zweiten g\"abe es gerade auch gar nichts mehr zu machen)
|
|
|
|
\subsection*{2) Typherleitung}
|
|
\textbf{Typherleitung f\"ur:}
|
|
\[
|
|
\{
|
|
\,mult\;:\;
|
|
\mathrm{N}\rightarrow\mathrm{N}\rightarrow\mathrm{N},\;
|
|
one\; : \; \mathrm{N},\,two\;\mathrm{N}\,
|
|
\vdash \; \lambda n.\,n\,(\, mult \; two\,)\;one\,:\mathrm{N}\rightarrow
|
|
\mathrm{N}
|
|
\}
|
|
\]
|
|
\textbf{mit Sonderhinweis, dass die Chruch-Numerale in System F den folgenden Typ besitzen:}
|
|
\[
|
|
\mathrm{N}\; := \; \forall a.(a\,\rightarrow \, a)\, \rightarrow \, a \, \rightarrow \,a
|
|
\]
|
|
\textbf{Herleitung:}\\
|
|
|
|
%Zeile 5
|
|
\underline{
|
|
$(5)\;
|
|
\Gamma \;\cup \{\,n:\mathrm{N}\,\} \vdash
|
|
\overbrace{
|
|
n\,:\,\forall a\,.\,(\,a\,\rightarrow\,a\,)\rightarrow (\,a\,\rightarrow \,a\,)
|
|
}^{per\;Definition\; =\;\mathrm{N}}
|
|
\hspace{8mm}
|
|
\overbrace{
|
|
mult:\;\mathrm{N}\rightarrow \mathrm{N}\rightarrow \mathrm{N}
|
|
}^{Ax}
|
|
\hspace{5mm}
|
|
\overbrace{
|
|
two:\;\mathrm{N}
|
|
}^{Ax}
|
|
$
|
|
}\\
|
|
%Zeile 4
|
|
\underline{
|
|
$(4)\;
|
|
\Gamma \;\cup \{\,n:\mathrm{N}\,\} \vdash
|
|
n\,:\,(\,\mathrm{N}\rightarrow \mathrm{N}\,)
|
|
\rightarrow (\,\mathrm{N}\rightarrow \mathrm{N}\,)
|
|
\hspace{25mm}
|
|
mult\;two\;\mathrm{N}\rightarrow \mathrm{N}
|
|
$
|
|
}\\
|
|
%Zeile 3
|
|
\underline{
|
|
$ (3)\;
|
|
\Gamma \; \cup \{\,n:\mathrm{N}\,\}\,
|
|
\vdash \, n\,(\,mult\;two\,)\,: \mathrm{N}\rightarrow\,\mathrm{N}
|
|
\hspace{6cm}
|
|
\;one\; : \mathrm{N}
|
|
$
|
|
}\\
|
|
%Zeile 2
|
|
\underline{
|
|
$(2)\;
|
|
\Gamma \; \cup \{\,n:\mathrm{N}\,\}\,
|
|
\vdash \, n\,(\,mult\;two\,)\;one\; : \mathrm{N}
|
|
$\hspace{48mm}}
|
|
\\
|
|
%Zeile 1
|
|
$ (1)\;
|
|
\{
|
|
\underbrace{
|
|
\,mult\;:\;
|
|
\mathrm{N}\rightarrow\mathrm{N}\rightarrow\mathrm{N},\;
|
|
one\; : \; \mathrm{N},\,two\;\mathrm{N}\,
|
|
}_{:=\Gamma}
|
|
\vdash \; \lambda n.\,n\,(\, mult \; two\,)\;one\,:\mathrm{N}\rightarrow\mathrm{N}
|
|
$
|
|
\\
|
|
\textbf{Erkl\"arungen:}\\
|
|
(1) $\rightarrow_{i}$\\
|
|
(2)(3) $\rightarrow_e$\\
|
|
(3)(rechts)$[\,one:\mathrm{N}\,]$ mit Ax fertig\\
|
|
(4) $\forall _e$ (wir wissen, dass N : $(a->a)->a->a$ ist, und dass \{n : N ist\}; damit n hinten also mit dem Kontex aufgeht muss es von der Form $(a->a)->a->a$ sein)\\
|
|
(4)(links) $\forall_{e}$ (rechts) $\rightarrow_e$\\\\
|
|
\textbf{Eine \"Ubersicht der Regeln findet sich in den \"Ubungsfolien oder dem SS14 Spickzettel!}
|
|
|
|
\end{document} |