tex-projects/LaTeX-examples
2
0
Fork 0
mirror of https://github.com/MartinThoma/LaTeX-examples.git synced 2025-04-26 06:48:04 +02:00
Code Activity

Fehler korrigiert - danke an Vincent Schnitzbauer

Browse source
This commit is contained in:
Martin Thoma 2014-09-18 12:08:55 +02:00
parent 20994f6cc3
commit 42486c92a4
9 changed files with 44 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

12
documents/Programmierparadigmen/Typinferenz.tex
View file

@ -58,15 +58,15 @@ Bei solchen Ableitungen sind häufig viele Typen möglich. So kann der Ausdruck
\[\lambda x.\ 2\]
folgenderweise typisiert werden:
\begin{itemize}
\item $\vdash(\lambda x.\ 2): \text{bool} \rightarrow int$
\item $\vdash(\lambda x.\ 2): \text{int} \rightarrow int$
\item $\vdash(\lambda x.\ 2): \text{Char} \rightarrow int$
\item $\vdash(\lambda x.\ 2): \alpha \rightarrow int$
\item $\vdash(\lambda x.\ 2): \text{bool} \rightarrow \text{int}$
\item $\vdash(\lambda x.\ 2): \text{int} \rightarrow \text{int}$
\item $\vdash(\lambda x.\ 2): \text{Char} \rightarrow \text{int}$
\item $\vdash(\lambda x.\ 2): \alpha \rightarrow \text{int}$
\end{itemize}
In der letzten Typisierung stellt $\alpha$ einen beliebigen Typen dar.
Wichtig ist , dass man sich von unten nach oben arbeitet.
Wichtig ist, dass man sich von unten nach oben vorarbeitet.
\begin{beispiel}[Typinferenz\footnotemark]
Typisieren Sie den Term
@ -90,6 +90,8 @@ Wichtig ist , dass man sich von unten nach oben arbeitet.
&\\
\APP: &\frac{\Gamma \vdash t_1: \tau_2 \rightarrow \tau\;\;\; \Gamma \vdash t_2: \tau_2}{\Gamma \vdash t_1 t_2: \tau} \\
\end{align*}
wobei $t_1, t_2$ immer $\lambda$-Terme bezeichnet.
\end{definition}
\footnotetext{WS 2013 / 2014, Folie 192}