型別理論與形式證明筆記

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

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. 型別變數：解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\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 \rightarrow \tau) \in {\mathbb{T}}}

箭頭解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle \rightarrow} 是右結合的，和函數的apply代入不同。比較解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle \alpha \rightarrow \beta \rightarrow \gamma = \left( \alpha \rightarrow (\beta \rightarrow \gamma) \right)} 和解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle x_{1}x_{2}x_{3} = \left( \left( x_{1}x_{2} \right)x_{3} \right)} 。

註：在本書中，解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle \mathbb{N}} 和 解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle \mathbb{L}} 指數學世界的自然數和列表，而nat和list指電腦程式世界的同樣的型別。

「term 解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle M} 有類型（type、型別）解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle \sigma} 」寫成解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle M:\sigma}

type有唯一性。比如：若解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle x:\sigma} 且解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle x:\tau} ，則解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle \sigma \equiv \tau}

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

1. application（代入）：若 解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle M:\sigma \rightarrow \tau} 且 解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle N:\sigma} ，則 解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle MN:\tau}
2. abstration（抽象）：若 解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle x:\sigma} 且 解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle M:\tau} ，則 解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle \lambda x.M:\sigma \rightarrow \tau}

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

附註：本筆記使用的邏輯推演排版法

原本的書使用的排版法如下，類似Fitch的表示法(Fitch notation)，雖然可以用HTML硬畫，但是很不好當筆記使用：

假設A

假設B C ⋮ D

E

所以姑且改編Fitch表示法，變如下：

(a) *假設A*
(b)   | *假設B*
(1)   | | C
      | | ⋮
(n)   | | D
(n+1) | E