2,619
次編輯
「型別理論與形式證明筆記」修訂間的差異
無編輯摘要
Tankianting（討論 | 貢獻） |
Tankianting（討論 | 貢獻） |
||
| 行 25： | 行 25： | ||
箭頭<math display="inline">\rightarrow</math>是右結合的，和函數的apply代入不同。比較<math display="inline">\alpha \rightarrow \beta \rightarrow \gamma = \left( \alpha \rightarrow (\beta \rightarrow \gamma) \right)</math>和<math display="inline">x_{1}x_{2}x_{3} = \left( \left( x_{1}x_{2} \right)x_{3} \right)</math>。 | 箭頭<math display="inline">\rightarrow</math>是右結合的，和函數的apply代入不同。比較<math display="inline">\alpha \rightarrow \beta \rightarrow \gamma = \left( \alpha \rightarrow (\beta \rightarrow \gamma) \right)</math>和<math display="inline">x_{1}x_{2}x_{3} = \left( \left( x_{1}x_{2} \right)x_{3} \right)</math>。 | ||
註：在本書中，<math display="inline">\mathbb{N}</math> 和 <math display="inline">\mathbb{L}</math> 指數學世界的自然數和列表，而nat和list指電腦程式世界的同樣的型別。 | |||
「term <math display="inline">M</math>有類型（type、型別）<math display="inline">\sigma</math>」寫成<math display="inline">M:\sigma</math> | |||
type有唯一性。比如：若<math display="inline">x:\sigma</math>且<math display="inline">x:\tau</math>，則<math display="inline">\sigma \equiv \tau</math> | |||
簡單型別lambda演算的出現的推演規則： | |||
# application（代入）：若 <math display="inline">M:\sigma \rightarrow \tau</math> 且 <math display="inline">N:\sigma</math>，則 <math display="inline">MN:\tau</math> | |||
# abstration（抽象）：若 <math display="inline">x:\sigma</math> 且 <math display="inline">M:\tau</math>，則 <math display="inline">\lambda x.M:\sigma \rightarrow \tau</math> | |||
<math display="inline">(xx)</math>在這種情況下，因為不可能既是<math display="inline">x:\alpha \rightarrow \beta</math>且<math display="inline">x:\alpha</math>這種型別存在，所以這種式子不會被構造到。 | |||
若<math display="inline">\exists\sigma\text{ such that }M:\sigma</math>，則<math display="inline">M</math>是可賦予型別的(typable)。 | |||
[[category:資訊]] | [[category:資訊]] | ||