檢視型別理論與形式證明筆記的原始碼

{{Nav|程式語言、邏輯學}}


= 第2章：簡單型別lambda運算(simple typed lambda calculus) =

== 2.2 simple type 簡單型別 ==

型別變數 type variable：<math display="inline">{\mathbb{V}} = \left\{ \alpha,\beta,\gamma,\ldots \right\}</math>用希臘字母表示。

<math display="inline">\mathbb{T}</math>：所有簡單型別，定義如下：

# 型別變數：<math display="inline">\alpha \in {\mathbb{V}} \Rightarrow  \alpha \in {\mathbb{T}}</math>，表達基本型別，比如list, nat等
# 箭頭型別：<math display="inline">\alpha,\tau \in {\mathbb{T}} \Rightarrow  (\alpha \rightarrow \tau) \in {\mathbb{T}}</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>。

[[category:資訊]]