型別理論與形式證明筆記

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

ISBN 9781107036505

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

作者：Rob Nederpelt, Herman Geuvers

編輯格式注意

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

第1章：無型別lambda運算(untyped lambda calculus)

1.6 Substitution(Beta reduction)

1a) x[x:=N]≡N // x:=N 即N代入x

1b) y[x:=N]≡y (if x≢y)

2) (P Q)[x:=N]≡(P[x:=N])(Q[x:=N])

3) (λy.P)[x:=N]≡(λz.P^y→z[x:=N]) // P進行α重名自y到x

若 λz.P^y→z是λy.P的variation，且z∉FV(N)

1.9 Normal form and confluence(合流)

Theorem 1.9.8 Church-Rosser(CR); Confluence 假設有lambda term M，若

${\textstyle M\twoheadrightarrow N_{1}}$且 ${\textstyle M\twoheadrightarrow N_{2}}$

則有${\textstyle N_{3}}$使得

${\textstyle N_{1}\twoheadrightarrow N_{3}}$且 ${\textstyle N_{2}\twoheadrightarrow N_{3}}$

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

若${\textstyle \exists \sigma {\text{ such that }}M:\sigma }$，則${\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的案例：

設${\textstyle M\equiv \left(\left(\lambda x.\lambda y.x\right)(u\ v)\right)}$，如果${\textstyle v:\alpha \rightarrow \alpha }$，${\textstyle u:(\alpha \rightarrow \alpha )\rightarrow \beta }$，${\textstyle x:\beta }$，${\textstyle y:\gamma }$，則${\textstyle M:\gamma \rightarrow \beta }$

implicit typing的案例（需要用推理和類似合一 (unification) 的方法）： ${\textstyle M\equiv \left(\left(\lambda x.\lambda y.x\right)(u\ v)\right)}$，可以推論：

${\textstyle v:\alpha }$

${\textstyle u:\alpha \rightarrow \beta }$

${\textstyle \lambda x.\lambda y.x:\gamma \rightarrow \delta }$

${\textstyle x:\gamma }$

${\textstyle \lambda y.x:\delta =\varepsilon \rightarrow \zeta }$

${\textstyle y:\varepsilon }$

${\textstyle x:\gamma =\zeta }$

${\textstyle \lambda y.x:\delta =\varepsilon \rightarrow \gamma }$

${\textstyle \lambda x.\lambda y.x:\gamma \rightarrow \varepsilon \rightarrow \gamma }$

${\textstyle (u\ v):\beta =\gamma }$

${\textstyle u:\alpha \rightarrow \gamma }$

${\textstyle M:\varepsilon \rightarrow \gamma }$

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

本書常用explicit typing。

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

${\textstyle u:(\alpha \rightarrow \alpha )\rightarrow \beta ,v:(\alpha \rightarrow \alpha )}$ 可以推論到

${\textstyle \left(\left(\lambda x.\lambda y.x\right)(u\ v)\right):\beta \rightarrow \gamma }$，

則可以寫成：

在上下文${\textstyle u:(\alpha \rightarrow \alpha )\rightarrow \beta ,v:(\alpha \rightarrow \alpha )}$下，${\textstyle \left(\left(\lambda x:\beta .\lambda y:\gamma .x\right)(u\ v)\right):\gamma \rightarrow \beta }$

用形式語言的方式寫出來如下： ${\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

Premiss 前提和Conclusion結論表達式

表達如：

${\cfrac {premiss_{1}\quad premiss_{2}\quad ...\quad premiss_{n}}{conclusion}}$

其中前提(premiss)可以0個以上。

derivation scheme（推演規範）是：對於所有premiss都成立，則結論(conclusion)成立。

這個推演系統(derivation system)的三條規律

1. (var, 變數) ${\textstyle \Gamma \vdash x:\sigma \quad if\quad x:\sigma \in \Gamma }$

2. (appl, 應用) ${\cfrac {\Gamma \vdash M:\sigma \rightarrow \tau \quad \Gamma \vdash N:\tau }{\Gamma \vdash M\ N:\tau }}$

3. (abst, 抽象) ${\textstyle {\cfrac {\Gamma ,x:\sigma \vdash M:\tau }{\Gamma \vdash \lambda x:\sigma .M:\sigma \rightarrow \tau }}}$

注意上面的符號，逗號,表示連結上下文。上下文$\Gamma$可以為空。

推論可以由上到下讀，或是下到上讀推到目標。

推論不只是建構judgement，更是一種justify的方式。

1.變數沒有前提，只有conclusion，可以用在推演開頭，意思是在上下文內的變數可以從這個上下文推演出來。

因為我們在conclusion（結論）不需要$x$在左邊的上下文，所以3.抽象的$x:\sigma$被移到$\vdash$右邊的statement去。

自然演繹natural deduction的推演範例：

${\cfrac {y:\alpha \rightarrow \beta ,z:\alpha \vdash y:\alpha \rightarrow \beta \quad \quad y:\alpha \rightarrow \beta ,z:\alpha \vdash z:\alpha }{\cfrac {y:\alpha \rightarrow \beta ,z:\alpha \vdash y~z:\beta }{\cfrac {y:\alpha \rightarrow \beta \vdash \lambda z:\alpha .y~z:\alpha \rightarrow \beta }{\vdash \lambda y:\alpha \rightarrow \beta .\lambda z:\alpha .y~z:(\alpha \rightarrow \beta )\rightarrow \alpha \rightarrow \beta }}}}$

比較數學和邏輯學：

1. 數學： $(func-appl){\cfrac {f:A\rightarrow Band~c\in A}{f(c)\in B}}$

$(func-abst){\cfrac {\forall x\in A,f(x)~\in ~B}{f:~A\rightarrow B}}$

2. 邏輯學：

• (⇒-elim 消去)${\textstyle {\cfrac {A\Rightarrow B\quad A}{B}}}$
• (⇒-intro 引入)（參考附錄的表記法）

*Assume : A*
| ...
| B
------
A⇒B

旗標flag（本筆記用雙星號**夾起來的地方表示變數定義或assumption假設）

旗杆（本筆記用串聯的豎線|標記）表示定義假設的範圍(scope)。

若∃上下文Γ, ∃型別ρ s.t.(such that) Γ⊢M:ρ（且M是pre-typed），則M是legal。

2.5 不同的推演格式

型別推論如natural deduction是樹狀。

但是推演過程會發散，使讀者無法專注其中。

linear format 比較可以省略，如下：

(1) y:α→β, z:α⊢y:α→β
(2) y:α→β, z:α⊢z:α
(3) y:α→β, z:α⊢y z:β
(4) y:α→β⊢λ z :α. (y z):α→β
(5) y:α→β⊢λ y:α→β. λ z :α.(y z):(α→β)→(α→β)

排序有時不一定照順序也可。

judgement之間的相依性，是一個嚴格偏序(strict partial order)關係：

• 非自反性 irreflexive：J ⇏ J
• 非對稱性 asymmetric：(J1 ⇒ J2) ⇏ (J2⇒ J1)
• 遞移性 transitive：(J1 ⇒ J2) ∧ (J2 ⇒ J3) ⇒ (J1 ⇒ J3)

可是還會出現一堆重複的上下文。所以就用 flag format 的標記法（類似Fitcher式），見附註

2.6 型別論要解決的問題

1. well-typedness (viz Ch 2.7) aka typability
   • ? ⊢term:? #找到一個上下文和type，使term legal。
     • 型別指派是變體：context ⊢term:?，推得term型別，aka inhabitation（term construction)
   • 型別檢查：「context ⊢term:type」是否能推導出？
   • 尋找term：context ⊢?:type，找到符合type的term。

這些問題在lambda→係可決定的，有演算法可以產出，但更後面的系統的term finding，是無固定演算法且非決定型別。

2.7 well-typedness 於lambda→

找上下文和term的type，範例：

M = λ y:α→β. λ z :α.(y z):？，求型別和上下文。

因為這裡沒有自由變數，所以可以假設上下文是∅。

所以我們可以找上下文。

因為有引入y 和z，所以：

*y : α → β*
| ??
| λ z :α.(y z):??
λ y:α→β. λ z :α.(y z):？

接續

*y : α → β*
| *z : α*
| | ??
| | (y z):??
| | λ z :α.(y z):??
λ y:α→β. λ z :α.(y z):？

接續

*y : α → β*
| *z : α*
| | (y z):β
| | λ z :α.(y z):??
λ y:α→β. λ z :α.(y z):？

接續

*y : α → β*
| *z : α*
| | (y z):β
| | λ z :α.(y z):α→β
λ y:α→β. λ z :α.(y z):(α→β)→(α→β)

所以可以得知型別。

但是若是z是β，則無法得知其型別，換言之，是illegal的。這種well-typedness推論有不同的推論方法。

2.8-2.10

參此pdf。

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

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

假設A

假設B C ⋮ D

E

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

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

範例：

*y : α → β*
| *z : α*
| | y : α → β
| | z : α
| | y z: β
| λz.(y z): α → β
λy.λz.(y z): (α → β) → α → β

書中把變數引入(var)省略，所以變成：

*y : α → β*
| *z : α*
| | y z: β
| λz.(y z): α → β
λy.λz.(y z): (α → β) → α → β