diff --git a/merkzettel.pdf b/merkzettel.pdf index e9d5164..01221af 100644 Binary files a/merkzettel.pdf and b/merkzettel.pdf differ diff --git a/merkzettel.tex b/merkzettel.tex index b317cec..b982fe6 100644 --- a/merkzettel.tex +++ b/merkzettel.tex @@ -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 ($ 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} - \item erweiterter Algorithmus W mit Menge $PT$ von Typgleichungen + \item erweiterter Algorithmus W mit Menge $PT$ von Typgleichungen \siehe{S. 90} \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;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)