型別理論與形式證明筆記

導航：首頁 > 程式語言、邏輯學> 型別理論與形式證明筆記

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

2.2 simple type 簡單型別

型別變數 type variable：${\textstyle {\mathbb {V} }=\left\{\alpha ,\beta ,\gamma ,\ldots \right\}}$用希臘字母表示。

${\textstyle \mathbb {T} }$：所有簡單型別，定義如下：

1. 型別變數：${\textstyle \alpha \in {\mathbb {V} }\Rightarrow \alpha \in {\mathbb {T} }}$，表達基本型別，比如list, nat等
2. 箭頭型別：解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle \alpha,\tau \in {\mathbb{T}} \Rightarrow (\alpha \arrow \tau) \in {\mathbb{T}}}

箭頭${\textstyle \rightarrow }$是右結合的，和函數的apply代入不同。比較${\textstyle \alpha \rightarrow \beta \rightarrow \gamma =\left(\alpha \rightarrow (\beta \rightarrow \gamma )\right)}$和${\textstyle x_{1}x_{2}x_{3}=\left(\left(x_{1}x_{2}\right)x_{3}\right)}$。