「型別理論與形式證明筆記」修訂間的差異

型別理論與形式證明筆記 (檢視原始碼)

於 2024年7月8日 (一) 22:35 的修訂

增加 1,856 位元組、 2024年7月8日 (一) 22:35

無編輯摘要

Tankianting

行政員、管理員

2,732

次編輯

@@ 行 40： / 行 40： @@
 若<math display="inline">\exists\sigma\text{ such that }M:\sigma</math>，則<math display="inline">M</math>是可賦予型別的(typable)。
+=== 2.3 Church-typing (explicit typing) 和 Curry-typing (implicit typing) ===
+# typing à la Church（explicit typing，外顯型別）：先給定型別予變數，再推出其他表達式的型別。
+# typing à la Curry（implicit typing，隱藏型別）：先給定一個表達式，再推論其內變數可能的型別。
+explicit typing的案例：
+設<math display="inline">M \equiv \left( \left( \lambda x.\lambda y.x \right)(u\ v) \right)</math>，如果<math display="inline">v:\alpha \rightarrow \alpha</math>，<math display="inline">u:(\alpha \rightarrow \alpha) \rightarrow \beta</math>，<math display="inline">x:\beta</math>，<math display="inline">y:\gamma</math>，則<math display="inline">M:\gamma \rightarrow \beta</math>
+implicit typing的案例（需要用推理和類似合一 (unification) 的方法）： <math display="inline">M \equiv \left( \left( \lambda x.\lambda y.x \right)(u\ v) \right)</math>，可以推論：
+<math display="inline">v:\alpha</math>
+<math display="inline">u:\alpha \rightarrow \beta</math>
+<math display="inline">\lambda x.\lambda y.x:\gamma \rightarrow \delta</math>
+<math display="inline">x:\gamma</math>
+<math display="inline">\lambda y.x:\delta = \varepsilon \rightarrow \zeta</math>
+<math display="inline">y:\varepsilon</math>
+<math display="inline">x:\gamma = \zeta</math>
+<math display="inline">\lambda y.x:\delta = \varepsilon \rightarrow \gamma</math>
+<math display="inline">\lambda x.\lambda y.x:\gamma \rightarrow \varepsilon \rightarrow \gamma</math>
+<math display="inline">(u\ v):\beta = \gamma</math>
+<math display="inline">u:\alpha \rightarrow \gamma</math>
+<math display="inline">M:\varepsilon \rightarrow \gamma</math>
+但是implicit typing的型別變數，只是一種示例，可以把β用「ω→ω」這種形式取代。
+但是本書常用explicit typing。
 [[category:資訊]]