Unverified Commit a169a5bf authored by Philip K.'s avatar Philip K. 🌝

miscellaneous fixes

parent ace9f2bc
......@@ -30,12 +30,12 @@ right (slant s) = slant s
\end{multicols}
\begin{enumerate}
\item \points{3} Zeigen Sie, dass folgende Aussagen gelten:
\item Zeigen\points{3} Sie, dass folgende Aussagen gelten:
\begin{verbatim}
genl (slant s) = s
genr (slant s) = const (hd s)
\end{verbatim}
\item \points{3} Definieren Sie eine korekursive Funktion
\item Definieren\points{3} Sie eine korekursive Funktion
\texttt{layers: S a -> IT a}, die einen Baum erzeugt, in dem das
Wurzelelement den Wert des ersten Elements des Parameters hat. Die
Kinder der Wurzel, den Wert des zweiten Elements. Die Kinder der
......
\section{System F \hfill 8 Punkte}
In Funktionalen Programmiersprachen werden Maybe Datentypen benutzt um
eine Berechnung mit Fehlermöglichkeit darzustellen. Dieses kann in
System F mit dem Typen \[ \mathbb{M}a := \forall r \,.\, (a \rightarrow r)
\rightarrow r \rightarrow r \] kodiert werden. Nehmen Sie zudem an,
dass Listen den Typ \[ \mathbb{L}a := \forall r \,.\, r \rightarrow (a
\rightarrow r \rightarrow r) \rightarrow r \] besitzt.
In funktionalen Programmiersprachen werden \emph{Maybe} Datentypen
benutzt um eine Berechnung mit Fehlermöglichkeit zu beschreiben. Dieses
kann in System F mit dem Typen
\[ \mathbb{M}a := \forall r \,.\, (a \rightarrow r) \rightarrow r
\rightarrow r \] kodiert werden. Nehmen Sie zudem an, dass Listen den
Typ
\[ \mathbb{L}a := \forall r \,.\, r \rightarrow (a \rightarrow r
\rightarrow r) \rightarrow r \] besitzen.
\begin{enumerate}
\item Definieren \points{2} Sie die Konstruktoren für
\item Definieren\points{2} Sie die Konstruktoren für
"`$\mathrm{some} : \forall a \,.\, a \rightarrow \mathbb{M}a$"' und
"`$\mathrm{none} : \forall a \,.\, \mathbb{M}a$"' (d.h. geben sie die
Lambda-Terme an).
\item Sei \points{5}
\item Sei\points{5}
$t : \forall a \,.\, \mathbb{L}a \rightarrow \mathbb{M}a$ definiert
als
\[ t = \lambda l \,.\, l \; \mathrm{none}\;(\lambda xq\,.\,
\mathrm{some}\;x) \] Geben Sie die Typeherleitung in System F für
\[ \{ \mathrm{some} : \forall a \,.\, a \rightarrow \mathbb{M}a,
\mathrm{none} : \forall a \,.\, \mathbb{M}a \} \vdash t : \forall a
\[ \{ \; \mathrm{some} : \forall a \,.\, a \rightarrow \mathbb{M}a,\,
\mathrm{none} : \forall a \,.\, \mathbb{M}a \; \} \vdash t : \forall a
\,.\, \mathbb{L}a \rightarrow \mathbb{M}a \]
\item Welche \points{1} bekannte Funktion auf Listen stellt $t$ dar?
\item Welche\points{1} bekannte Funktion auf Listen stellt $t$ dar?
\end{enumerate}
%%% Local Variables:
......
......@@ -13,12 +13,12 @@ $x^{\ast}$) und einem binärem, infix Operator $x \vdash y$:
\tag{1.3}\label{tes13}
\end{align}
\begin{enumerate}
\item Zeigen \points{3} Sie, dass das TES nicht stark normalisierend
\item Zeigen\points{3} Sie, dass das TES nicht stark normalisierend
ist.
\item Gehen \points{3} sie im Folgenden davon aus, dass Regel (1.2)
\item Gehen\points{3} Sie im Folgenden davon aus, dass Regel (1.2)
entfernt wird. Zeigen Sie mithilfe von geeigneten Polynomordnungen,
dass das TES jetzt stark normalisierend ist.
\item Es \points{3} gibt nur ein einziges kritisches Paar. Bestimmen Sie
\item Es\points{3} gibt nur ein einziges kritisches Paar. Bestimmen Sie
dieses und prüfen Sie, ob das TES konfluent ist.
\end{enumerate}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment