initial
This commit is contained in:
commit
cab03d63ec
7 changed files with 387 additions and 0 deletions
1
.gitignore
vendored
Normal file
1
.gitignore
vendored
Normal file
|
|
@ -0,0 +1 @@
|
|||
pkg
|
||||
BIN
TypeTheoryAndFormalProof第3章.pdf
Normal file
BIN
TypeTheoryAndFormalProof第3章.pdf
Normal file
Binary file not shown.
50
TypeTheoryAndFormalProof第3章.typ
Normal file
50
TypeTheoryAndFormalProof第3章.typ
Normal file
|
|
@ -0,0 +1,50 @@
|
|||
#import "pkg/prooftrees.typ"
|
||||
#import "pkg/internal.typ"
|
||||
|
||||
#show regex("\p{sc=Hani}+"): set text(font: ("Noto Serif CJK SC"), lang: "zh", region: "tw")
|
||||
|
||||
= Type Theory And Formal Proof
|
||||
== 3. Second order typed lambda calculus 二階有型別lambda運算
|
||||
=== 3.1 型別抽象與型別套用
|
||||
$x -> lambda x \. M$，$M$中所有裡面的$x$變成bound variable（約束變數）。
|
||||
|
||||
$lambda x : sigma : M$ 取決於(depends on)term $x$ => $lambda_arrow.r$可以terms depends on the terms
|
||||
|
||||
$M N$是型別的應用
|
||||
|
||||
如此可說是一階(first order)抽象
|
||||
|
||||
本章討論terms depend on types (second order operation/second order dependency) 可以理解成依型別值（？）
|
||||
|
||||
本章討論$lambda 2$：二階具型別lambda演算
|
||||
|
||||
範例：$id(x)=x$函數
|
||||
|
||||
若是自然數，則有$lambda x : \n\a\t . space x : \n\a\t -> \n\a\t $
|
||||
|
||||
若是布林值，則有$lambda x : italic("bool") . space x : \b\o\o\l -> \b\o\o\l $
|
||||
|
||||
還有函數$lambda x : (\n\a\t->\b\o\o\l) . space x : (\n\a\t->\b\o\o\l) -> (\n\a\t->\b\o\o\l) $
|
||||
|
||||
可是這樣函數要每個型別就重複定義一次，有無更好的方法？
|
||||
|
||||
我們需要定義一個任意型別$alpha$，變成：$f equiv lambda x : alpha space . x$
|
||||
|
||||
但是對於$M in \n\a\t$，$f space M$是invalid，因為$alpha equiv.not \n\a\t$。所以要進行抽象化：
|
||||
|
||||
$lambda alpha : ast . lambda x : alpha . x$
|
||||
|
||||
其中$alpha$ 是type，$ast$是kind。
|
||||
|
||||
所以
|
||||
|
||||
$(lambda alpha : ast . lambda x : alpha . x ) \n\a\t $
|
||||
|
||||
$arrow.twohead.r_beta lambda x : \n\a\t . space x$
|
||||
|
||||
且
|
||||
$(lambda alpha : ast . lambda x : alpha . x ) (\b\o\o\l->\n\a\t) $
|
||||
|
||||
$arrow.twohead.r_beta lambda x : (\b\o\o\l->\n\a\t) . space x$
|
||||
|
||||
然而我們需要$beta$-reduction
|
||||
BIN
dated/TypeTheory2第2章part2.pdf
Normal file
BIN
dated/TypeTheory2第2章part2.pdf
Normal file
Binary file not shown.
223
dated/TypeTheory2第2章part2.typ
Normal file
223
dated/TypeTheory2第2章part2.typ
Normal file
|
|
@ -0,0 +1,223 @@
|
|||
#show regex("\p{sc=Hani}+"): set text(font: ("Noto Serif CJK TC"), lang: "zh", region: "tw")
|
||||
#set par(leading: 1.25em) // 行距
|
||||
|
||||
=== 2.8 型別檢查於$lambda arrow.r$
|
||||
$x : alpha arrow.r alpha, space y : (alpha arrow.r alpha) arrow.r beta tack.r (lambda z : beta . lambda u : gamma .z)(y space x): gamma arrow.r beta $
|
||||
|
||||
```(a)| ``` \*$x : alpha arrow.r alpha$\*
|
||||
|
||||
```(b)||``` \*$y : (alpha arrow.r alpha) arrow.r beta$\*
|
||||
|
||||
``` || ...```
|
||||
|
||||
```(n)||```$(lambda z : beta . lambda u : gamma .z)(y space x): gamma arrow.r beta$
|
||||
|
||||
appl 拆解
|
||||
|
||||
```(a) | ``` \*$x : alpha arrow.r alpha$\*
|
||||
|
||||
```(b) ||``` \*$y : (alpha arrow.r alpha) arrow.r beta$\*
|
||||
|
||||
``` (m1)|| ``` $lambda z : beta . lambda u : gamma .z:?_1$
|
||||
|
||||
``` (m2)|| ``` $y space x:?_2$
|
||||
|
||||
```(n) ||```$(lambda z : beta . lambda u : gamma .z)(y space x): gamma arrow.r beta$
|
||||
|
||||
繼續反推
|
||||
|
||||
```(a) | ``` \*$x : alpha arrow.r alpha$\*
|
||||
|
||||
```(b) ||``` \*$y : (alpha arrow.r alpha) arrow.r beta$\*
|
||||
|
||||
``` ||| ``` \*$z : beta$\*
|
||||
|
||||
``` |||| ``` \*$u : gamma$\*
|
||||
|
||||
``` |||| ``` $lambda u.z : gamma -> beta$
|
||||
|
||||
``` (m1)|| ``` $lambda z : beta . lambda u : gamma .z:beta->(gamma->beta)$
|
||||
|
||||
``` (m2)|| ``` $y space x:beta$
|
||||
|
||||
```(n) ||```$(lambda z : beta . lambda u : gamma .z)(y space x): gamma arrow.r beta$
|
||||
|
||||
就可以得到一串推論過程。
|
||||
|
||||
但是，$(lambda z: beta lambda u : gamma .z )(y space x)$
|
||||
|
||||
用beta-reduction處理可得：
|
||||
|
||||
$(lambda u : gamma .(y space x))$
|
||||
|
||||
型別是：$gamma arrow.r beta$，也和剛才的推論出來的(n)的型別相同。
|
||||
|
||||
=== 2.9 找term於$lambda ->$
|
||||
|
||||
$a in T =>$ a 是 T 的inhabitant（居民）
|
||||
|
||||
type 是邏輯表達式(proposition)
|
||||
|
||||
term構築型別的證明
|
||||
|
||||
證明有一個term，滿足
|
||||
|
||||
$?:A->B->A$
|
||||
|
||||
證明法：逆著回推，箭頭$->$型別表示abst抽象。
|
||||
#pagebreak()
|
||||
|
||||
```|```\*$x:A$\*
|
||||
|
||||
```||```\*$y:B$\*
|
||||
|
||||
```||``` $x : A$
|
||||
|
||||
```|``` $lambda y. x : B->A$
|
||||
|
||||
$lambda x.lambda y.x : A->B->A$
|
||||
|
||||
PAT-interpretation
|
||||
- proposition as types命題即型別
|
||||
- proof as terms證明即term
|
||||
|
||||
=== 2.10 $lambda -> $的一般性質
|
||||
dom、$harpoon.tr$投影(projection)、$subset.eq$次上下文(subcontext)
|
||||
|
||||
定義
|
||||
1. 上下文：$Gamma equiv x_1 : sigma_1, ..., x_n: sigma_n=>$即上下文的定義域(domain)是$(x_1, x_2, ..., x_n)$
|
||||
2. 若所有的宣告變數一樣，且排序一致，則$Gamma' subset.eq Gamma$，即$Gamma'$是$Gamma$的次上下文
|
||||
3. $Gamma'$是$Gamma$上下文的permutation(排列)，若$Gamma'$的變數宣告於$Gamma$有，且反之亦然。
|
||||
4. 若$Gamma$是上下文，$Phi$是變數集合，$Gamma$在$Phi$上的投影(projection)，即$Gamma harpoon.tr Phi$是$Gamma'$，滿足$d o m ( Gamma')= d o m(Gamma) sect Phi$.
|
||||
|
||||
定理2.10.3自由變數公理
|
||||
|
||||
$Gamma tack.r L:sigma => F V(L) subset.eq d o m(Gamma)$
|
||||
|
||||
任何自由變數x在L出現，則在$Gamma$有$x:sigma$這個宣告。
|
||||
|
||||
任何變數的型別不會搞混。
|
||||
|
||||
Lemma 2.10.5
|
||||
1. thinning(厚化): 令$Gamma'$和$Gamma''$是滿足$Gamma' subset.eq Gamma''$的上下文，$Gamma' tack.r M : sigma => Gamma'' tack.r M : sigma$
|
||||
2. condensing(濃縮): $Gamma tack.r M: sigma => Gamma harpoon.tr F V\(M\) tack.r M : sigma $. 意思是可以移除$x:sigma$，若是x不是M的自由變數，所以保持這些和M有關的宣告。
|
||||
3. Permutation(排列): 若$Gamma tack.r M:sigma $且 $Gamma'$是$Gamma$的permutation，則$Gamma'$是上下文，滿足$Gamma' tack.r M : sigma$. 指context的變數順序不影響推演能力（變數宣告互相獨立）
|
||||
|
||||
一個人可以加減junk變數到上下文，而不影響衍推能力(derivibility)。
|
||||
|
||||
junk包含於M中不自由的變數（typing的過程不會用到）
|
||||
|
||||
Lemma 2.10.7 - Generation Lemma
|
||||
|
||||
1. $Gamma tack.r x : sigma => x : sigma in Gamma$
|
||||
2. if $Gamma tack.r M space N:tau$, then $exists sigma, space s.t. space Gamma tack.r M : sigma -> tau $ and $Gamma tack.r N : sigma $
|
||||
3. $Gamma tack.r lambda x : sigma . M : rho => exists tau space s.t. space Gamma, x : sigma tack.r M : tau and rho equiv sigma -> tau$
|
||||
|
||||
Lemma 2.10.8 subterm Lemma
|
||||
|
||||
若M是legal$=>$任何M的subterm也legal。
|
||||
|
||||
if $exists Gamma_1, space sigma_1 space s.t. space Gamma_1 tack.r M:sigma_1$ 且L為M的subterm$=> exists Gamma_2, sigma_2 space s.t. space Gamma_2 tack.r L : sigma_2$
|
||||
|
||||
在一個上下文F，一個term至多有一個type，也就是：
|
||||
|
||||
$Gamma tack.r M : sigma and Gamma tack.r M : tau => gamma equiv tau$
|
||||
|
||||
我們可以分出4種求型別或term的類型：
|
||||
|
||||
1. well-typeness
|
||||
|
||||
? $tack.r $ term: $ ?$
|
||||
|
||||
1a. type assignment
|
||||
|
||||
context $tack.r$ term : ?
|
||||
|
||||
2. type checking
|
||||
|
||||
#set math.vec(delim: none)
|
||||
context $vec( ?, tack.r)$ term: type
|
||||
#set math.vec(delim: "(")
|
||||
|
||||
3. term finding
|
||||
context $tack.r ? :$ type
|
||||
|
||||
|
||||
以上4種皆為decidible（可決定的）。
|
||||
|
||||
=== Sec.2.11 歸約與 $lambda arrow.r$
|
||||
Ch1.6有beta-reduction（$beta$歸約）的公式：
|
||||
|
||||
|
||||
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]≡($lambda z.P^(y→z)$[x:=N])若 $lambda z.P^(y→z)$是λy.P的variation，且z∉FV(N)
|
||||
|
||||
為了型別系統的改變，所以我們把3)改為：
|
||||
|
||||
***3)(λ$y:sigma$.P)[x:=N]≡($lambda z:sigma . P^(y→z)$[x:=N])*** 若$lambda z: sigma . P ^(y arrow.r z)$是$lambda y : sigma . P$的alpha variant，且滿足$z in.not F V (N)$
|
||||
|
||||
Lemma 2.11.1替換Lemma
|
||||
|
||||
假設$Gamma', x:sigma,Gamma'' tack.r M:tau$且$Gamma' tack.r N : sigma$
|
||||
|
||||
則$Gamma', Gamma'' tack.r M[x:=N]:tau$
|
||||
|
||||
==== Def 定義 One-step reduction$arrow.r_(beta)$ for $Lambda_(𝕋)$
|
||||
|
||||
1. (Basis)
|
||||
|
||||
$(lambda x : sigma . M) N arrow.r_(beta)M[x:=N]$
|
||||
|
||||
(compatibility)見定義1.8.1。
|
||||
|
||||
Theorem 2.11.3
|
||||
|
||||
Church-Rosser Theorem ( Theorem 1.9.8)在 $lambda arrow.r$也成立。
|
||||
|
||||
Corollary 推論 2.11.4
|
||||
|
||||
假設有 $M =_(beta) N$則$exists L space s.t. M arrow.twohead.r_(beta) L$且$N arrow.twohead.r_(beta) L$
|
||||
|
||||
Lemma 2.11.5 Subject Reduction:
|
||||
|
||||
$Gamma tack.r L : rho$且$L arrow.twohead.r L'$ 則$Gamma tack.r L' : rho$
|
||||
|
||||
beta歸約不改變typability和其型別。
|
||||
|
||||
Reduction是一種形式的calculation。
|
||||
|
||||
$x : alpha arrow.r alpha, y : (alpha arrow.r alpha) arrow.r beta tack.r lambda u : gamma. y space x : gamma arrow.r beta$
|
||||
|
||||
任何計算皆為finite（有限的）！
|
||||
|
||||
Theorem 2.11.6
|
||||
|
||||
strong normalization theorem (Termination theorem)
|
||||
|
||||
任何合法的M是strongly normalizing（強正規化的）。
|
||||
|
||||
strong normalizing 保證運算有結果
|
||||
|
||||
因為$lambda arrow.r$的能力有限，有足夠能力的運算系統會有無法終止的情況發生。雖然能終止的系統也可能要很久（雖然是有限久）才能算出結果。
|
||||
|
||||
== 2.12結果
|
||||
|
||||
untyped lambda運算的缺點會消失：
|
||||
- 沒有自我代入(self-application)
|
||||
- 保證有 beta-normal forms
|
||||
- 不是所有的legal lambda term 都有不動點
|
||||
|
||||
|
||||
== 2.13 結論
|
||||
positive points of untyped lambda calculation 擴展到簡單型別 lambda 運算
|
||||
system$lambda arrow.r$太弱，不能封裝所有運算的函數，不能作為數學的形式化。
|
||||
|
||||
- call-by-value
|
||||
$(lambda x : sigma . M) N$先求出N再代入
|
||||
- call-by-name
|
||||
$(lambda x : sigma . M) N$直接將N代入M中的各個x（$M[x:=N]$）
|
||||
BIN
dated/TypeTheoryAndFormalProof第2章.pdf
Normal file
BIN
dated/TypeTheoryAndFormalProof第2章.pdf
Normal file
Binary file not shown.
113
dated/TypeTheoryAndFormalProof第2章.typ
Normal file
113
dated/TypeTheoryAndFormalProof第2章.typ
Normal file
|
|
@ -0,0 +1,113 @@
|
|||
#import "pkg/prooftrees.typ"
|
||||
#import "pkg/internal.typ"
|
||||
|
||||
#show regex("\p{sc=Hani}+"): set text(font: ("Noto Serif CJK SC"), lang: "zh", region: "tw")
|
||||
|
||||
= Type Theory And Formal Proof
|
||||
|
||||
== 第2章：簡單型別lambda運算(simple typed lambda calculus)
|
||||
|
||||
=== 2.2 simple type 簡單型別
|
||||
型別變數 type variable：$VV = {alpha, beta, gamma, dots.h}$用希臘字母表示。
|
||||
|
||||
$TT$：所有簡單型別，定義如下：
|
||||
|
||||
+ 型別變數：$alpha in VV arrow.double alpha in TT $，表達基本型別，比如list, nat等
|
||||
+ 箭頭型別：$alpha, tau in TT arrow.double (alpha arrow tau ) in TT$
|
||||
箭頭$arrow$是右結合的，和函數的apply代入不同。比較$alpha arrow beta arrow gamma=(alpha arrow (beta arrow gamma))$和$x_1 x_2 x_3 = ((x_1 x_2) x_3)$。
|
||||
|
||||
註：在本書中，$NN$ 和 $LL$ 指數學世界的自然數和列表，而nat和list指電腦程式世界的同樣的型別。
|
||||
|
||||
「term $M$有類型（type、型別）$sigma$」寫成$M : sigma$
|
||||
|
||||
type有唯一性。比如：若$x : sigma$且$x : tau$，則$sigma ≡ tau$
|
||||
|
||||
簡單型別lambda演算的出現的推演規則：
|
||||
|
||||
1. application（代入）：若 $M:sigma arrow.r tau$ 且 $N:sigma$，則 $M N : tau$
|
||||
2. abstration（抽象）：若 $x:sigma$ 且 $M:tau$，則 $lambda x.M : sigma arrow.r tau$
|
||||
|
||||
$(x space x)$在這種情況下，因為不可能既是$x:alpha->beta$且$x:alpha$這種型別存在，所以這種式子不會被構造到。
|
||||
|
||||
若$exists sigma "滿足" M:sigma$，則$M$是可賦予型別的(typable)。
|
||||
|
||||
=== 2.3 Church-typing (explicit typing) 和 Curry-typing (implicit typing)
|
||||
|
||||
+ typing à la Church（explicit typing，外顯型別）：先給定型別予變數，再推出其他表達式的型別。
|
||||
+ typing à la Curry（implicit typing，隱藏型別）：先給定一個表達式，再推論其內變數可能的型別。
|
||||
|
||||
explicit typing的案例：
|
||||
|
||||
設$M≡((lambda x .lambda y. x) (u space v))$，如果$v:alpha -> alpha$，$u:(alpha->alpha)->beta$，$x : beta$，$y:gamma$，則$M: gamma->beta$
|
||||
|
||||
implicit typing的案例（需要用推理和類似合一 (unification) 的方法）：
|
||||
$M≡((lambda x .lambda y. x) (u space v))$，可以推論：
|
||||
|
||||
$v : alpha$
|
||||
|
||||
$u : alpha -> beta $
|
||||
|
||||
$lambda x .lambda y. x : gamma->delta$
|
||||
|
||||
$x : gamma$
|
||||
|
||||
$lambda y.x : delta = epsilon -> zeta$
|
||||
|
||||
$y : epsilon$
|
||||
|
||||
$x : gamma = zeta$
|
||||
|
||||
$ lambda y.x : delta = epsilon -> gamma$
|
||||
|
||||
$lambda x .lambda y. x : gamma-> epsilon -> gamma$
|
||||
|
||||
$(u space v) : beta = gamma $
|
||||
|
||||
$u :alpha -> gamma $
|
||||
|
||||
$M: epsilon -> gamma$
|
||||
|
||||
|
||||
但是implicit typing的型別變數，只是一種示例，可以把$beta$用「$omega -> omega$」這種形式取代。
|
||||
|
||||
本書常用explicit typing。
|
||||
|
||||
我們用上面的explicit typing的範例，
|
||||
|
||||
$u : (alpha arrow.r alpha) arrow.r beta, v: (alpha arrow.r alpha)$ 可以推論到
|
||||
|
||||
$((lambda x . lambda y . x) (u space v)) : beta -> gamma$，
|
||||
|
||||
則可以寫成：
|
||||
|
||||
在上下文$u colon (alpha->alpha)->beta, v colon (alpha->alpha)$下，$((lambda x . lambda y . x) (u space v)) : beta -> gamma$
|
||||
|
||||
用形式語言的方式寫出來如下：
|
||||
$u colon (alpha->alpha)->beta, v colon (alpha->alpha) tack.r ((lambda x .lambda y . x) (u space v)) : beta -> gamma$
|
||||
|
||||
$tack.r$ 表示左邊的可以推論到右邊的能力(derivibility)。（註：可以參考弗雷格的著作）
|
||||
|
||||
== 2.4 Church lambda→演算的推演規則 (derivation rules)
|
||||
|
||||
先賦予型別的lambda term，其名為$Lambda_{TT}$，定義如下:
|
||||
|
||||
$Lambda_TT = V|(Lambda_𝕋 space Lambda_𝕋)|(λ V : 𝕋 . Lambda_𝕋)$，其中$V$表變數的集合。
|
||||
|
||||
*定義*
|
||||
|
||||
+ statement形如$M:sigma$，其中$M in Lambda_𝕋$且$sigma in 𝕋$（$sigma$是型別）。$M$稱為主體(subject)，$sigma$稱為類型(type)。
|
||||
+ declaration（宣告）是有變數當主體的statement
|
||||
+ context（上下文）是一系列不同主體（不同變數）的宣告列表（註：context可為空）
|
||||
+ judgement（判斷）形如$Gamma tack.r M : sigma$，其中左邊的$Gamma$是上下文，右邊的$M:sigma$是statement
|
||||
|
||||
|
||||
*Premiss 前提和Conclusion表達式：*
|
||||
|
||||
$gamma tack.r x : sigma 若 x : sigma in Gamma$
|
||||
|
||||
$Gamma tack.r M : sigma arrow.r tau quad Gamma tack.r N : tau$
|
||||
$Gamma tack.r M space N : tau$
|
||||
|
||||
$Gamma, x : sigma tack.r M : tau$
|
||||
|
||||
$Gamma tack.r lambda x : sigma M : sigma arrow.r tau$
|
||||
Loading…
Reference in a new issue