2,619
次編輯
「型別理論與形式證明筆記」修訂間的差異
→2.4 Church lambda→演算的推演規則 (derivation rules)
Tankianting（討論 | 貢獻） |
Tankianting（討論 | 貢獻） |
||
| 行 105： | 行 105： | ||
# judgement（判斷）形如<math display="inline">\Gamma \vdash M:\sigma</math>，其中左邊的<math display="inline">\Gamma</math>是上下文，右邊的<math display="inline">M:\sigma</math>是statement | # judgement（判斷）形如<math display="inline">\Gamma \vdash M:\sigma</math>，其中左邊的<math display="inline">\Gamma</math>是上下文，右邊的<math display="inline">M:\sigma</math>是statement | ||
;Premiss 前提和Conclusion結論表達式 | |||
表達如： | 表達如： | ||
| 行 118： | 行 118： | ||
derivation scheme（推演規範）是：對於所有premiss都成立，則結論(conclusion)成立。 | derivation scheme（推演規範）是：對於所有premiss都成立，則結論(conclusion)成立。 | ||
這個推演系統(derivation system) | ;這個推演系統(derivation system)的三條規律 | ||
1. (var, 變數) <math display="inline">\Gamma \vdash x:\sigma \quad if \quad x:\sigma \in \Gamma</math> | 1. (var, 變數) <math display="inline">\Gamma \vdash x:\sigma \quad if \quad x:\sigma \in \Gamma</math> | ||
| 行 129： | 行 129： | ||
<math display="inline">\cfrac{\Gamma,x:\sigma \vdash M:\tau}{\Gamma \vdash \lambda x:\sigma . M:\sigma \rightarrow \tau}</math> | <math display="inline">\cfrac{\Gamma,x:\sigma \vdash M:\tau}{\Gamma \vdash \lambda x:\sigma . M:\sigma \rightarrow \tau}</math> | ||
注意上面的符號，逗號,表示連結上下文。上下文 | 注意上面的符號，逗號,表示連結上下文。上下文<math>\Gamma</math>可以為空。 | ||
因為我們在conclusion（結論）不需要<math>x</math>在左邊的上下文，所以3.抽象的<math>x:\sigma</math>被移到<math>\vdash</math>右邊的statement去。 | |||
=附註：本筆記使用的邏輯推演排版法= | =附註：本筆記使用的邏輯推演排版法= | ||