2,619
次編輯
「型別理論與形式證明筆記」修訂間的差異
跳至導覽
跳至搜尋
→2.4 Church lambda→演算的推演規則 (derivation rules)
Tankianting（討論 | 貢獻） |
Tankianting（討論 | 貢獻） |
||
| 行 92： | 行 92： | ||
用形式語言的方式寫出來如下： <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> | 用形式語言的方式寫出來如下： <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> | ||
== 2.4 Church lambda→演算的推演規則 (derivation rules) == | |||
先賦予型別的lambda term，其名為<math display="inline">\Lambda_{\left\{ {\mathbb{T}} \right\}}</math>，定義如下: | 先賦予型別的lambda term，其名為<math display="inline">\Lambda_{\left\{ {\mathbb{T}} \right\}}</math>，定義如下: | ||