型別理論與形式證明筆記

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

ISBN 9781107036505

原標題：Type Theory and Formal Proof: An Introduction

作者：Rob Nederpelt, Herman Geuvers

編輯格式注意

1. 章節內文太多的時候，拆成新頁面。
2. typst 撰寫 + pandoc 產生貼上於個人維基的內容。

第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. 箭頭型別：${\textstyle \alpha ,\tau \in {\mathbb {T} }\Rightarrow (\alpha \rightarrow \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)}$。

註：在本書中，${\textstyle \mathbb {N} }$ 和 ${\textstyle \mathbb {L} }$ 指數學世界的自然數和列表，而nat和list指電腦程式世界的同樣的型別。

「term ${\textstyle M}$有類型（type、型別）${\textstyle \sigma }$」寫成${\textstyle M:\sigma }$

type有唯一性。比如：若${\textstyle x:\sigma }$且${\textstyle x:\tau }$，則${\textstyle \sigma \equiv \tau }$

簡單型別lambda演算的出現的推演規則：

1. application（代入）：若 ${\textstyle M:\sigma \rightarrow \tau }$ 且 ${\textstyle N:\sigma }$，則 ${\textstyle MN:\tau }$
2. abstration（抽象）：若 ${\textstyle x:\sigma }$ 且 ${\textstyle M:\tau }$，則 ${\textstyle \lambda x.M:\sigma \rightarrow \tau }$

${\textstyle (xx)}$在這種情況下，因為不可能既是${\textstyle x:\alpha \rightarrow \beta }$且${\textstyle x:\alpha }$這種型別存在，所以這種式子不會被構造到。

若${\textstyle \exists \sigma {\text{ such that }}M:\sigma }$，則${\textstyle M}$是可賦予型別的(typable)。