型別理論與形式證明筆記

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

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：解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle {\mathbb{V}} = \left\{ \alpha,\beta,\gamma,\ldots \right\}} 用希臘字母表示。

解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\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 (x\ x)}$在這種情況下，因為不可能既是${\textstyle x:\alpha \rightarrow \beta }$且解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle x:\alpha} 這種型別存在，所以這種式子不會被構造到。

若解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle \exists\sigma\text{ such that }M:\sigma} ，則解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle M} 是可賦予型別的(typable)。

2.3 Church-typing (explicit typing) 和 Curry-typing (implicit typing)

1. typing à la Church（explicit typing，外顯型別）：先給定型別予變數，再推出其他表達式的型別。
2. typing à la Curry（implicit typing，隱藏型別）：先給定一個表達式，再推論其內變數可能的型別。

explicit typing的案例：

設解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle M \equiv \left( \left( \lambda x.\lambda y.x \right)(u\ v) \right)} ，如果解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle v:\alpha \rightarrow \alpha} ，解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle u:(\alpha \rightarrow \alpha) \rightarrow \beta} ，解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle x:\beta} ，解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle y:\gamma} ，則解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle M:\gamma \rightarrow \beta}

implicit typing的案例（需要用推理和類似合一 (unification) 的方法）： 解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle M \equiv \left( \left( \lambda x.\lambda y.x \right)(u\ v) \right)} ，可以推論：

解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle v:\alpha}

解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle u:\alpha \rightarrow \beta}

解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle \lambda x.\lambda y.x:\gamma \rightarrow \delta}

解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle x:\gamma}

解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle \lambda y.x:\delta = \varepsilon \rightarrow \zeta}

解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle y:\varepsilon}

解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle x:\gamma = \zeta}

解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle \lambda y.x:\delta = \varepsilon \rightarrow \gamma}

解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle \lambda x.\lambda y.x:\gamma \rightarrow \varepsilon \rightarrow \gamma}

解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle (u\ v):\beta = \gamma}

解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle u:\alpha \rightarrow \gamma}

解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle M:\varepsilon \rightarrow \gamma}

但是implicit typing的型別變數，只是一種示例，可以把β用「ω→ω」這種形式取代。

本書常用explicit typing。

我們用上面的explicit typing的範例，

解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle u:(\alpha \rightarrow \alpha) \rightarrow \beta,v:(\alpha \rightarrow \alpha)} 可以推論到

解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle \left( \left( \lambda x.\lambda y.x \right)(u\ v) \right):\beta \rightarrow \gamma} ，

則可以寫成：

在上下文解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle u:(\alpha \rightarrow \alpha) \rightarrow \beta,v:(\alpha \rightarrow \alpha)} 下，解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle \left( \left( \lambda x: \beta.\lambda y: \gamma.x \right)(u\ v) \right):\gamma \rightarrow \beta}

用形式語言的方式寫出來如下： 解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle u:(\alpha \rightarrow \alpha) \rightarrow \beta,v:(\alpha \rightarrow \alpha) \vdash \left( \left( \lambda x: \beta.\lambda y: \gamma.x \right)(u\ v) \right):\gamma \rightarrow \beta}

2.4 Church lambda→演算的推演規則 (derivation rules)

先賦予型別的lambda term，其名為${\textstyle \Lambda _{\left\{{\mathbb {T} }\right\}}}$，定義如下:

${\textstyle \Lambda _{\mathbb {T} }=V\left|\left(\Lambda _{\mathbb {T} }\ \Lambda _{\mathbb {T} }\right)\right|\left(\lambda V:{\mathbb {T} }.\Lambda _{\mathbb {T} }\right)}$，其中${\textstyle V}$表變數的集合。

定義

1. statement形如${\textstyle M:\sigma }$，其中${\textstyle M\in \Lambda _{\mathbb {T} }}$且${\textstyle \sigma \in {\mathbb {T} }}$（${\textstyle \sigma }$是型別）。${\textstyle M}$稱為主體(subject)，${\textstyle \sigma }$稱為類型(type)。
2. declaration（宣告）是有變數當主體的statement
3. context（上下文）是一系列不同主體（不同變數）的宣告列表（註：context可為空）
4. judgement（判斷）形如${\textstyle \Gamma \vdash M:\sigma }$，其中左邊的${\textstyle \Gamma }$是上下文，右邊的${\textstyle M:\sigma }$是statement