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

{{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>可以為空。

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

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

=附註：本筆記使用的邏輯推演排版法=
原本的書使用的排版法如下，類似[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>
[[category:資訊]]