Theorem. lambda 通過 K1 再編碼 lambda 不能從 lambda 的 identity 得出 [math-A9X1]

2024-07-22 · Lîm Tsú-thuàn
記號繼承自 Higher-Order Computability

標題的描述有點複雜，但其實只是說 κ∘γ⪰̸idΛ0/=β\kappa \circ \gamma \not\succeq id_{\Lambda^0 /_{=_\beta}}，表示 κ∘γ\kappa \circ \gamma 不是 λ\lambda-definable。

Proof [local-0]

兩個 computability model 的等價 ≃\simeq，表示他們可以互相模擬並且兩個模擬的兩種組合都跟模擬自己的函數相似。Kleene's first model K1\mathcal{K}_1 與 closed lambda terms Λ0/=β\Lambda^0 /_{=_\beta} 的模擬細節定義在下面，由於兩者都只有一個 datatype，所以元素的選擇是明顯的。

Definition Λ0/=β\Lambda^0 /_{=_\beta} 模擬 K1\mathcal{K}_1 [local-1]

κ:K1▹Λ0/=β\kappa : \mathcal{K}_1 \triangleright \Lambda^0 /_{=_\beta} 由以下關係定義

M⊩κn iff M=βn~=βλf.λx.fnxM \Vdash^\kappa n \text{ iff } M =_\beta \widetilde{n} =_\beta \lambda f.\lambda x. f^n x

fnf^n 表示重複 ff 剛好 nn 次

Definition K1\mathcal{K}_1 模擬 Λ0/=β\Lambda^0 /_{=_\beta} [local-2]

γ:Λ0/=β▹K1\gamma : \Lambda^0 /_{=_\beta} \triangleright \mathcal{K}_1 由以下關係定義

n⊩γ[M] iff n=⌈M′⌉ for some M′=βMn \Vdash^\gamma [M] \text{ iff } n = \lceil M' \rceil \text{ for some } M' =_\beta M

⌈M′⌉\lceil M' \rceil 是某種 Gödel 編碼

在回答下面兩個問題之前，我們要考慮 γ∘κ:K1▹K1\gamma \circ \kappa : \mathcal{K}_1 \triangleright \mathcal{K}_1 會建立什麼？展開我們可以看到

γ∘κ(n)=γ(κ(n))=γ(n~)=⌈n~⌉\gamma \circ \kappa(n) = \gamma(\kappa(n)) = \gamma(\widetilde{n}) = \lceil \widetilde{n} \rceil

Lemma γ∘κ⪯idK1\gamma \circ \kappa \preceq id_{\mathcal{K}_1} [local-4]

Proof [local-3]

由於 ⌈n~⌉\lceil \widetilde{n} \rceil 確實是自然數，且 Gödel 編碼特性保證了這是獨特的，表示是良好的 tracker。γ∘κ\gamma \circ \kappa 顯然是一個 K1\mathcal{K}_1 對自己的模擬，因此跟某個 idK1id_{\mathcal{K}_1} 在有定義時相等。

Lemma γ∘κ⪰idK1\gamma \circ \kappa \succeq id_{\mathcal{K}_1} [local-6]

Proof [local-5]

同理，只要找到有定義時跟 γ∘κ\gamma \circ \kappa 相等的那個 idK1id_{\mathcal{K}_1} 即可。

反過來就困難得多，κ∘γ:Λ0/=β▹Λ0/=β\kappa \circ \gamma : \Lambda^0 /_{=_\beta} \triangleright \Lambda^0 /_{=\beta} 展開可以得到

κ∘γ(M)=κ(γ(M))=κ(⌈M⌉)=⌈M⌉~\kappa \circ \gamma(M) = \kappa(\gamma(M)) = \kappa(\lceil M \rceil) = \widetilde{\lceil M \rceil}

Lemma κ∘γ⪯idΛ0/=β\kappa \circ \gamma \preceq id_{\Lambda^0 /_{=_\beta}} [local-7]

這裡需要用到 Kleene enumeration theorem，說明存在一個 P∈Λ0P \in \Lambda^0，令式

P(⌈M⌉~)=βM P(\widetilde{\lceil M \rceil}) =_\beta M

對所有 M∈Λ0M \in \Lambda^0 成立。直覺上來說，是因為我們可以從外部看到 ⌈M⌉\lceil M \rceil 的定義之後再找滿足條件的 PP。