2,619
次編輯
「型別理論與形式證明筆記」修訂間的差異
跳至導覽
跳至搜尋
→2.2 simple type 簡單型別
Tankianting（討論 | 貢獻） |
Tankianting（討論 | 貢獻） |
||
| 行 37： | 行 37： | ||
# abstration（抽象）：若 <math display="inline">x:\sigma</math> 且 <math display="inline">M:\tau</math>，則 <math display="inline">\lambda x.M:\sigma \rightarrow \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">( | <math display="inline">(x\ x)</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)。 | 若<math display="inline">\exists\sigma\text{ such that }M:\sigma</math>，則<math display="inline">M</math>是可賦予型別的(typable)。 | ||
[[category:資訊]] | [[category:資訊]] | ||