2,619
次編輯
「型別理論與形式證明筆記」修訂間的差異
跳至導覽
跳至搜尋
→2.3 Church-typing (explicit typing) 和 Curry-typing (implicit typing)
Tankianting（討論 | 貢獻） |
Tankianting（討論 | 貢獻） |
||
| 行 78： | 行 78： | ||
但是implicit typing的型別變數，只是一種示例，可以把β用「ω→ω」這種形式取代。 | 但是implicit typing的型別變數，只是一種示例，可以把β用「ω→ω」這種形式取代。 | ||
本書常用explicit typing。 | |||
我們用上面的explicit typing的範例， | |||
<math display="inline">u:(\alpha \rightarrow \alpha) \rightarrow \beta,v:(\alpha \rightarrow \alpha)</math> 可以推論到 | |||
<math display="inline">\left( \left( \lambda x.\lambda y.x \right)(u\ v) \right):\beta \rightarrow \gamma</math>， | |||
則可以寫成： | |||
在上下文<math display="inline">u:(\alpha \rightarrow \alpha) \rightarrow \beta,v:(\alpha \rightarrow \alpha)</math>下，<math display="inline">\left( \left( \lambda x: \beta.\lambda y: \gamma.x \right)(u\ v) \right):\gamma \rightarrow \beta</math> | |||
用形式語言的方式寫出來如下： <math display="inline">u:(\alpha \rightarrow \alpha) \rightarrow \beta,v:(\alpha \rightarrow \alpha) \vdash \left( \left( \lambda x: \beta.\lambda y: \gamma.x \right)(u\ v) \right):\gamma \rightarrow \beta</math> | |||
[[category:資訊]] | [[category:資訊]] | ||