型別理論與形式證明筆記Sec2.8-2.13.pdf/原始碼
檔案:型別理論與形式證明筆記Sec2.8-2.13.pdf的Typst原始碼。
#show regex("\p{sc=Hani}+"): set text(font: ("Noto Serif CJK TC"), lang: "zh", region: "tw")
=== 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的過程不會用到）