Halt = { f,x | f(x)↓ } is re (semi-decidable) but undecidable
Total = { f | ∀x f(x)↓ } is non-re (not even semi-decidable)
我需要一些帮助来证明Total问题不是递归的(可判定的)。
我知道Halting问题的对角化证明,我只需要Total问题的相同证明。我发布了停止问题证明以供参考:
停止问题证明
假设我们可以决定停机问题。那么存在一些总函数 Halt 使得
1 if [x] (y) is defined
Halt(x,y) =
0 if [x] (y) is not defined
在这里,我们对所有程序进行了编号,[x] 指的是此顺序中的第 x 个程序。我们可以将 Halt 视为从 ℵ 到 ℵ 的映射,将其输入视为一个数字,表示通过 one-one on 函数配对两个数字
pair(x,y) = <x,y> = 2^x (2y + 1) – 1
with inverses
<z>1 = exp(z+1,1)
<z>2 = ((( z + 1 ) // 2^<z>1) – 1 ) // 2
现在,如果 Halt 存在,那么 Disagree 也存在,其中
0 if Halt(x,x) = 0, i.e, if Φx (x) is not defined
Disagree(x) =
µy (y == y+1) if Halt(x,x) = 1, i.e, if Φx (x) is defined
由于不同意是从 ℵ 到 ℵ 的程序,因此可以通过 Halt 来推断不同意。令 d 满足 Disagree = Φd,则
Disagree(d) 已定义 ⇔ Halt(d,d) = 0 ⇔ Φd (d) 未定义 ⇔ Disagree(d) 未定义
但这意味着不同意与它自己的存在相矛盾。由于我们采取的每一步都是建设性的,除了最初的假设,我们必须假设最初的假设是错误的。因此,停机问题是无法解决的。