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

2024-07-22 · Lîm Tsú-thuàn

所有PCA都沒有decidable equality。

Proof [local-0]

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

d⋅x⋅y={true if x=yfalse otherwised \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 false)v = Y(d\ \text{false}) 就能得到 v=d false vv = d\ \text{false}\ v，其值不可判定，所以 dd 不是decidable equality。