型別理論與形式證明筆記Sec2.8-2.10.pdf/原始碼

檔案:型別理論與形式證明筆記Sec2.8-2.10.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的過程不會用到）