2,728
次編輯
「型別理論與形式證明筆記」修訂間的差異
跳至導覽
跳至搜尋
→2.4 Church lambda→演算的推演規則 (derivation rules)
Tankianting（討論 | 貢獻） |
Tankianting（討論 | 貢獻） |
||
| 行 104： | 行 104： | ||
# context（上下文）是一系列不同主體（不同變數）的宣告列表（註：context可為空） | # context（上下文）是一系列不同主體（不同變數）的宣告列表（註：context可為空） | ||
# 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結論表達式''' | |||
表達如： | |||
<math> | |||
\cfrac{premiss_1\quad premiss_2\quad ...\quad premiss_n}{conclusion} | |||
</math> | |||
其中前提(premiss)可以0個以上。 | |||
derivation scheme（推演規範）是：對於所有premiss都成立，則結論(conclusion)成立。 | |||
這個推演系統(derivation system)的三條規律： | |||
1. (var, 變數) <math display="inline">\Gamma \vdash x:\sigma \quad if \quad x:\sigma \in \Gamma</math> | |||
2. (appl, 應用) | |||
<math>\cfrac{\Gamma \vdash M:\sigma \rightarrow \tau\quad\Gamma \vdash N:\tau}{\Gamma \vdash M\ N:\tau} | |||
</math> | |||
3. (abst, 抽象) | |||
<math display="inline">\cfrac{\Gamma,x:\sigma \vdash M:\tau}{\Gamma \vdash \lambda x:\sigma . M:\sigma \rightarrow \tau}</math> | |||
注意上面的符號，逗號,表示連結上下文。上下文$\Gamma$可以為空。 | |||
因為我們在結論不需要x在左邊，所以3.抽象的$x:\sigma$被移到$\vdash$右邊的statement去。 | |||
=附註：本筆記使用的邏輯推演排版法= | =附註：本筆記使用的邏輯推演排版法= | ||