Proof [local-0]

我們從 If two computability models are equivalent, then decidable equality exists for one iff another has one 跟兩個 lemma 得知 $\mathcal{K}_1 \not\simeq \Lambda^0 /_{=\beta}$ 。

Lemma Partial combinatory algebra沒有decidable equality [math-BF7A]

2024-07-22

所有PCA都沒有decidable equality。

Proof [local-0]

考慮一個PCA $A$ ，假定有元素 $d \in A^\#$ 是一個decidable equality，這表示對任意 $x, y \in A$

d \cdot x \cdot y = \begin{aligned} \begin{cases} \text{true} &\text{ if } x = y \\ \text{false} &\text{ otherwise} \end{cases} \end{aligned}

只要定義 $v = Y(d\ \text{false})$ 就能得到 $v = d\ \text{false}\ v$ ，其值不可判定，所以 $d$ 不是decidable equality。

Lemma $\mathcal{K}_1$ 有 decidable equality [local-2]

Proof [local-1]

比較任意兩個自然數是可判定的。

Proposition If two computability models are equivalent, then decidable equality exists for one iff another has one [math-0L0G]

2024-07-22

若 $A$ 跟 $B$ model 等價 $A \simeq B$ ，則 $A$ 有 decidable equality 若且唯若 $B$ 也有 decidable equality。

Proof [local-0]

先假設 $A$ 中有一 decidable equality $=_A$ ，這表示

=_A \cdot a_1 \cdot a_2 = \begin{cases} \text{true}_A \quad a_1 = a_2 \\ \text{false}_A \quad \text{otherwise} \end{cases}

對所有 $a_1, a_2 \in A$ 成立。由於 $A \simeq B$ ，所以對每個元素 $a \in A$ 必有一個 $b \in B$ 追蹤 $a$ ，所以我們用 $=_B, b_1, b_2, \text{true}_B, \text{false}_B$ 對應地表示這個關係。那麼我們有

=_B \cdot b_1 \cdot b_2 = \begin{cases} \text{true}_B \quad b_1 = b_2 \\ \text{false}_B \quad \text{otherwise} \end{cases}

顯然 $B$ 也有一個 decidable equality $=_B$ 。由於論證對 $A,B$ 沒有特別要求，這個證明是對稱的，因此兩個方向都證明完畢。

Theorem. Kleene's first model 與 Closed lambda terms 不等價 [math-I098]

Proof [local-0]

Lemma Partial combinatory algebra沒有decidable equality [math-BF7A]

Proof [local-0]

Lemma K1\mathcal{K}_1K1​ 有 decidable equality [local-2]

Proof [local-1]

Proposition If two computability models are equivalent, then decidable equality exists for one iff another has one [math-0L0G]

Proof [local-0]

Lemma $\mathcal{K}_1$ 有 decidable equality [local-2]