型別理論與形式證明筆記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的過程不會用到)