2
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) 未定义

但这意味着不同意与它自己的存在相矛盾。由于我们采取的每一步都是建设性的,除了最初的假设,我们必须假设最初的假设是错误的。因此,停机问题是无法解决的。

4

0 回答 0