2,619
次編輯
「型別理論與形式證明筆記」修訂間的差異
跳至導覽
跳至搜尋
無編輯摘要
Tankianting（討論 | 貢獻） |
Tankianting（討論 | 貢獻） |
||
| 行 41： | 行 41： | ||
若<math display="inline">\exists\sigma\text{ such that }M:\sigma</math>，則<math display="inline">M</math>是可賦予型別的(typable)。 | 若<math display="inline">\exists\sigma\text{ such that }M:\sigma</math>，則<math display="inline">M</math>是可賦予型別的(typable)。 | ||
== 2.3 Church-typing (explicit typing) 和 Curry-typing (implicit typing) == | |||
# typing à la Church（explicit typing，外顯型別）：先給定型別予變數，再推出其他表達式的型別。 | # typing à la Church（explicit typing，外顯型別）：先給定型別予變數，再推出其他表達式的型別。 | ||
| 行 91： | 行 91： | ||
用形式語言的方式寫出來如下： <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>，定義如下: | |||
<math display="inline">\Lambda_{\mathbb{T}} = V\left| \left( \Lambda_{\mathbb{T}}\ \Lambda_{\mathbb{T}} \right) \right|\left( \lambda V:{\mathbb{T}}.\Lambda_{\mathbb{T}} \right)</math>，其中<math display="inline">V</math>表變數的集合。 | |||
'''定義''' | |||
# statement形如<math display="inline">M:\sigma</math>，其中<math display="inline">M \in \Lambda_{\mathbb{T}}</math>且<math display="inline">\sigma \in {\mathbb{T}}</math>（<math display="inline">\sigma</math>是型別）。<math display="inline">M</math>稱為主體(subject)，<math display="inline">\sigma</math>稱為類型(type)。 | |||
# declaration（宣告）是有變數當主體的statement | |||
# context（上下文）是一系列不同主體（不同變數）的宣告列表（註：context可為空） | |||
# judgement（判斷）形如<math display="inline">\Gamma \vdash M:\sigma</math>，其中左邊的<math display="inline">\Gamma</math>是上下文，右邊的<math display="inline">M:\sigma</math>是statement | |||
[[category:資訊]] | [[category:資訊]] | ||