檢視型別理論與形式證明筆記的原始碼

{{Nav|程式語言、邏輯學}}

{{isbn|9781107036505}}

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

作者：Rob Nederpelt, Herman Geuvers

'''編輯格式注意'''
# 章節內文太多的時候，拆成新頁面。
# typst 撰寫 + pandoc 產生貼上於個人維基的內容。

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

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

== 2.2 simple type 簡單型別 ==

型別變數 type variable：<math display="inline">{\mathbb{V}} = \left\{ \alpha,\beta,\gamma,\ldots \right\}</math>用希臘字母表示。

<math display="inline">\mathbb{T}</math>：所有簡單型別，定義如下：

# 型別變數：<math display="inline">\alpha \in {\mathbb{V}} \Rightarrow  \alpha \in {\mathbb{T}}</math>，表達基本型別，比如list, nat等
# 箭頭型別：<math display="inline">\alpha,\tau \in {\mathbb{T}} \Rightarrow  (\alpha \rightarrow \tau) \in {\mathbb{T}}</math>

箭頭<math display="inline">\rightarrow</math>是右結合的，和函數的apply代入不同。比較<math display="inline">\alpha \rightarrow \beta \rightarrow \gamma = \left( \alpha \rightarrow (\beta \rightarrow \gamma) \right)</math>和<math display="inline">x_{1}x_{2}x_{3} = \left( \left( x_{1}x_{2} \right)x_{3} \right)</math>。

註：在本書中，<math display="inline">\mathbb{N}</math> 和 <math display="inline">\mathbb{L}</math> 指數學世界的自然數和列表，而nat和list指電腦程式世界的同樣的型別。

「term <math display="inline">M</math>有類型（type、型別）<math display="inline">\sigma</math>」寫成<math display="inline">M:\sigma</math>

type有唯一性。比如：若<math display="inline">x:\sigma</math>且<math display="inline">x:\tau</math>，則<math display="inline">\sigma \equiv \tau</math>

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

# application（代入）：若 <math display="inline">M:\sigma \rightarrow \tau</math> 且 <math display="inline">N:\sigma</math>，則 <math display="inline">MN:\tau</math>
# abstration（抽象）：若 <math display="inline">x:\sigma</math> 且 <math display="inline">M:\tau</math>，則 <math display="inline">\lambda x.M:\sigma \rightarrow \tau</math>

<math display="inline">(x\ x)</math>在這種情況下，因為不可能既是<math display="inline">x:\alpha \rightarrow \beta</math>且<math display="inline">x:\alpha</math>這種型別存在，所以這種式子不會被構造到。

若<math display="inline">\exists\sigma\text{ such that }M:\sigma</math>，則<math display="inline">M</math>是可賦予型別的(typable)。

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

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

explicit typing的案例：

設<math display="inline">M \equiv \left( \left( \lambda x.\lambda y.x \right)(u\ v) \right)</math>，如果<math display="inline">v:\alpha \rightarrow \alpha</math>，<math display="inline">u:(\alpha \rightarrow \alpha) \rightarrow \beta</math>，<math display="inline">x:\beta</math>，<math display="inline">y:\gamma</math>，則<math display="inline">M:\gamma \rightarrow \beta</math>

implicit typing的案例（需要用推理和類似合一 (unification) 的方法）： <math display="inline">M \equiv \left( \left( \lambda x.\lambda y.x \right)(u\ v) \right)</math>，可以推論：

<math display="inline">v:\alpha</math>

<math display="inline">u:\alpha \rightarrow \beta</math>

<math display="inline">\lambda x.\lambda y.x:\gamma \rightarrow \delta</math>

<math display="inline">x:\gamma</math>

<math display="inline">\lambda y.x:\delta = \varepsilon \rightarrow \zeta</math>

<math display="inline">y:\varepsilon</math>

<math display="inline">x:\gamma = \zeta</math>

<math display="inline">\lambda y.x:\delta = \varepsilon \rightarrow \gamma</math>

<math display="inline">\lambda x.\lambda y.x:\gamma \rightarrow \varepsilon \rightarrow \gamma</math>

<math display="inline">(u\ v):\beta = \gamma</math>

<math display="inline">u:\alpha \rightarrow \gamma</math>

<math display="inline">M:\varepsilon \rightarrow \gamma</math>

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

本書常用explicit typing。

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

<math display="inline">u:(\alpha \rightarrow \alpha) \rightarrow \beta,v:(\alpha \rightarrow \alpha)</math> 可以推論到

<math display="inline">\left( \left( \lambda x.\lambda y.x \right)(u\ v) \right):\beta \rightarrow \gamma</math>，

則可以寫成：

在上下文<math display="inline">u:(\alpha \rightarrow \alpha) \rightarrow \beta,v:(\alpha \rightarrow \alpha)</math>下，<math display="inline">\left( \left( \lambda x: \beta.\lambda y: \gamma.x \right)(u\ v) \right):\gamma \rightarrow \beta</math>

用形式語言的方式寫出來如下： <math display="inline">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</math>

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

先賦予型別的lambda term，其名為<math display="inline">\Lambda_{\left\{ {\mathbb{T}} \right\}}</math>，定義如下:

<math display="inline">\Lambda_{\mathbb{T}} = V\left| \left( \Lambda_{\mathbb{T}}\ \Lambda_{\mathbb{T}} \right) \right|\left( \lambda V:{\mathbb{T}}.\Lambda_{\mathbb{T}} \right)</math>，其中<math display="inline">V</math>表變數的集合。

'''定義'''

# statement形如<math display="inline">M:\sigma</math>，其中<math display="inline">M \in \Lambda_{\mathbb{T}}</math>且<math display="inline">\sigma \in {\mathbb{T}}</math>（<math display="inline">\sigma</math>是型別）。<math display="inline">M</math>稱為主體(subject)，<math display="inline">\sigma</math>稱為類型(type)。
# declaration（宣告）是有變數當主體的statement
# context（上下文）是一系列不同主體（不同變數）的宣告列表（註：context可為空）
# judgement（判斷）形如<math display="inline">\Gamma \vdash M:\sigma</math>，其中左邊的<math display="inline">\Gamma</math>是上下文，右邊的<math display="inline">M:\sigma</math>是statement

;Premiss 前提和Conclusion結論表達式

表達如：


<math>
\cfrac{premiss_1\quad premiss_2\quad ...\quad premiss_n}{conclusion}
</math>

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

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

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

1. (var, 變數) <math display="inline">\Gamma \vdash x:\sigma \quad if \quad x:\sigma \in \Gamma</math>

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

3. (abst, 抽象)
<math display="inline">\cfrac{\Gamma,x:\sigma \vdash M:\tau}{\Gamma \vdash \lambda x:\sigma . M:\sigma \rightarrow \tau}</math>

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

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

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

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

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

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

<math>
\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}}


}
</math>

;比較數學和邏輯學：

1. 數學：
<math> (func-appl)\cfrac{f : A \rightarrow B and ~c \in A}{f(c)\in B}</math>


<math> (func-abst)\cfrac{\forall x \in A, f(x)~\in~B}{f:~A\rightarrow B}</math>



2. 邏輯學：

*(⇒-elim 消去)<math display="inline">\cfrac{A \Rightarrow B\quad A}{B}</math>
*(⇒-intro 引入)（參考附錄的表記法）

<pre>
*Assume : A*
| ...
| B
------
A⇒B
</pre>

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

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

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

== 2.5 不同的推演格式 ==

型別推論如natural deduction是樹狀。

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

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

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

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

judgement之間的相依性，是一個嚴格偏序(strict partial order)關係：
* 非自反性 irreflexive：J ⇏ J
* 非對稱性 asymmetric：(J1 ⇒ J2) ⇏ (J2⇒ J1)
* 遞移性 transitive：(J1 ⇒ J2) ∧ (J2 ⇒ J3) ⇒ (J1 ⇒ J3)



可是還會出現一堆重複的上下文。所以就用 flag format 的標記法（類似Fitcher式），見[[#附註：本筆記使用的邏輯推演排版法|附註]]

==2.6 型別論要解決的問題==
# 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，所以：

<pre>
*y : α → β*
| ??
| λ z :α.(y z):??
λ y:α→β. λ z :α.(y z):？
</pre>
接續
<pre>
*y : α → β*
| *z : α*
| | ??
| | (y z):??
| | λ z :α.(y z):??
λ y:α→β. λ z :α.(y z):？
</pre>
接續
<pre>
*y : α → β*
| *z : α*
| | (y z):β
| | λ z :α.(y z):??
λ y:α→β. λ z :α.(y z):？
</pre>
接續
<pre>
*y : α → β*
| *z : α*
| | (y z):β
| | λ z :α.(y z):α→β
λ y:α→β. λ z :α.(y z):(α→β)→(α→β)
</pre>
所以可以得知型別。

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

== 2.8-2.10 ==
參[[:檔案:型別理論與形式證明筆記Sec2.8-2.10.pdf|此pdf]]。

=附註：本筆記使用的邏輯推演排版法=
原本的書使用的排版法如下，類似[https://en.wikipedia.org/wiki/Fitch_notation Fitch的表示法(Fitch notation)]，雖然可以用HTML硬畫，但是很不好當筆記使用：
<div>
<table style="margin-bottom:1em;">
<tr>
<td style="border:1px solid black;padding:0.5em;">假設A</td></tr><tr>
<td style="border-left:1px solid black; padding:1em;" ><table style="margin-bottom:0.5em;">
<tr>
<td style="border:1px solid black;padding:0.5em;">假設B</td></tr><tr>
<td style="border-left:1px solid black; padding:1em;" >C</td>
</tr><tr>
<td style="border-left:1px solid black; padding:1em;" >⋮</td>
</tr><tr><td>D</td></tr>
</table></td>
</tr><tr><td>E</td></tr>
</table>
</div>

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

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


</pre>

範例：

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

</pre>

書中把變數引入(var)省略，所以變成：
<pre>
*y : α → β*
| *z : α*
| | y z: β
| λz.(y z): α → β
λy.λz.(y z): (α → β) → α → β

</pre>


[[category:資訊]]
[[分類:邏輯學]]