commit cab03d63ec7aa5c56ab5a94573a3ad58781e8091
Author: Tan Kian-ting <chenjt30@gmail.com>
Date:   Wed Dec 25 00:38:19 2024 +0800

    initial

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..0c6117d
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+pkg
\ No newline at end of file
diff --git a/TypeTheoryAndFormalProof第3章.pdf b/TypeTheoryAndFormalProof第3章.pdf
new file mode 100644
index 0000000..e5a2ecd
Binary files /dev/null and b/TypeTheoryAndFormalProof第3章.pdf differ
diff --git a/TypeTheoryAndFormalProof第3章.typ b/TypeTheoryAndFormalProof第3章.typ
new file mode 100644
index 0000000..3fcfde4
--- /dev/null
+++ b/TypeTheoryAndFormalProof第3章.typ
@@ -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
\ No newline at end of file
diff --git a/dated/TypeTheory2第2章part2.pdf b/dated/TypeTheory2第2章part2.pdf
new file mode 100644
index 0000000..e166b2c
Binary files /dev/null and b/dated/TypeTheory2第2章part2.pdf differ
diff --git a/dated/TypeTheory2第2章part2.typ b/dated/TypeTheory2第2章part2.typ
new file mode 100644
index 0000000..df45634
--- /dev/null
+++ b/dated/TypeTheory2第2章part2.typ
@@ -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]$）
\ No newline at end of file
diff --git a/dated/TypeTheoryAndFormalProof第2章.pdf b/dated/TypeTheoryAndFormalProof第2章.pdf
new file mode 100644
index 0000000..5ab69f0
Binary files /dev/null and b/dated/TypeTheoryAndFormalProof第2章.pdf differ
diff --git a/dated/TypeTheoryAndFormalProof第2章.typ b/dated/TypeTheoryAndFormalProof第2章.typ
new file mode 100644
index 0000000..6377f7e
--- /dev/null
+++ b/dated/TypeTheoryAndFormalProof第2章.typ
@@ -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$