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

{{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

[[category:資訊]]