Marco
/
ThProg-Merkzettel
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

fixed hindley/milner algorithm

This commit is contained in:
Alexander Schroth 2018-10-08 19:04:09 +02:00
parent 6c07176b97
commit b30e3466cd
2 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

BIN
merkzettel.pdf
View File

Binary file not shown.

4
merkzettel.tex
View File

@ -336,9 +336,9 @@ f_1 \times f_2 &= \langle f_1 \circ\pi_1, f_2\circ\pi_2\rangle\\
\item Wenn $\Gamma \vdash x:\alpha$, dann existieren Typen $\beta_i$ und ein Typschema $S = \forall a_1 \ldots \forall a_k.\gamma$, so dass $(x:S)\in \Gamma$ und $\alpha = \gamma[\beta_1/a_1,\ldots,\beta_k/a_k]$ \item Wenn $\Gamma \vdash x:\alpha$, dann existieren Typen $\beta_i$ und ein Typschema $S = \forall a_1 \ldots \forall a_k.\gamma$, so dass $(x:S)\in \Gamma$ und $\alpha = \gamma[\beta_1/a_1,\ldots,\beta_k/a_k]$
\item Wenn $\Gamma \vdash ($ let $x = s$ in $t) : \alpha$, dann existiert ein Typ $\beta$ nut $\Gamma \vdash s:\beta$ und $\Gamma, x:Cl(\Gamma, \beta) \vdash t:\alpha$ \item Wenn $\Gamma \vdash ($ let $x = s$ in $t) : \alpha$, dann existiert ein Typ $\beta$ nut $\Gamma \vdash s:\beta$ und $\Gamma, x:Cl(\Gamma, \beta) \vdash t:\alpha$
\end{enumerate} \end{enumerate}
\item erweiterter Algorithmus W mit Menge $PT$ von Typgleichungen \item erweiterter Algorithmus W mit Menge $PT$ von Typgleichungen \siehe{S. 90}
\begin{align*} \begin{align*}
PT(\Gamma;x;\alpha) &= \lbrace a\pteq \gamma [a_1'/a_1,\ldots,a_k'/a_k] \vert (x: \forall a_1,\ldots,\forall a_k .\gamma) \in \Gamma\rbrace\\ PT(\Gamma;x;\alpha) &= \lbrace \alpha \pteq \gamma [a_1'/a_1,\ldots,a_k'/a_k] \rbrace \text{ mit } (x: \forall a_1,\ldots,\forall a_k .\gamma) \in \Gamma\\
PT(\Gamma; \lambda x.t; \alpha) &= PT((\Gamma;x:a);t;b) \cup \lbrace a\rightarrow b \pteq \alpha \rbrace\ \text{mit $a,b$ frisch}\\ PT(\Gamma; \lambda x.t; \alpha) &= PT((\Gamma;x:a);t;b) \cup \lbrace a\rightarrow b \pteq \alpha \rbrace\ \text{mit $a,b$ frisch}\\
PT(\Gamma;ts;\alpha) &= PT(\Gamma; t; a\rightarrow \alpha ) \cup PT(\Gamma;s;a)\ \text{mit $a$ frisch}\\ PT(\Gamma;ts;\alpha) &= PT(\Gamma; t; a\rightarrow \alpha ) \cup PT(\Gamma;s;a)\ \text{mit $a$ frisch}\\
PT(\Gamma;(\text{let } x=s\text{ in }t);\alpha) &= PT(\Gamma\sigma, x:Cl(\Gamma\sigma, \sigma(b));t;\alpha\sigma) PT(\Gamma;(\text{let } x=s\text{ in }t);\alpha) &= PT(\Gamma\sigma, x:Cl(\Gamma\sigma, \sigma(b));t;\alpha\sigma)