2,619
次編輯
「型別理論與形式證明筆記」修訂間的差異
→2.4 Church lambda→演算的推演規則 (derivation rules)
Tankianting（討論 | 貢獻） |
Tankianting（討論 | 貢獻） |
||
| 行 134： | 行 134： | ||
因為我們在conclusion（結論）不需要<math>x</math>在左邊的上下文，所以3.抽象的<math>x:\sigma</math>被移到<math>\vdash</math>右邊的statement去。 | 因為我們在conclusion（結論）不需要<math>x</math>在左邊的上下文，所以3.抽象的<math>x:\sigma</math>被移到<math>\vdash</math>右邊的statement去。 | ||
自然演繹natural deduction的推演範例： | |||
<math> | |||
\cfrac{y:\alpha \rightarrow \beta, z : \alpha \vdash y : \alpha \rightarrow \beta \quad\quad y:\alpha \rightarrow \beta, z : \alpha \vdash z : \alpha}{ | |||
\cfrac{ | |||
y:\alpha \rightarrow \beta, z : \alpha \vdash y~z: \beta} | |||
{\cfrac{y:\alpha \rightarrow \beta \vdash \lambda z : \alpha . y~z:\alpha \rightarrow \beta} | |||
{ \vdash \lambda y : \alpha \rightarrow \beta . \lambda z : \alpha . y~z:(\alpha \rightarrow \beta) \rightarrow \alpha \rightarrow \beta}} | |||
} | |||
</math> | |||
=附註：本筆記使用的邏輯推演排版法= | =附註：本筆記使用的邏輯推演排版法= | ||