半可判定（递归可枚举）

上级：logic

"能确认『是』，但对『否』可能永远等下去"这一层——这是可计算性中最重要的一种形态，也是halting-problem所处的层级。

半可判定 / r.e.

一个集合 S 是半可判定的（递归可枚举，recursively enumerable），如果存在某个程序恰好在 S 的成员上停机并接受，而在非成员上则可能永远运行下去。四种等价的刻画：

• 某个偏可计算函数的定义域（它停机的那部分）；
• 某个可计算函数的值域（"可枚举"：存在一台机器恰好列出 S）；
• 可表示为 ∃y. R(x,y)，其中 R 可判定（对一个可验证的证据做一次无界搜索）——即 Σ₁ 类。

那个至关重要的不对称

你可以验证成员资格——搜索证据、运行直到接受——但你永远无法确认非成员资格（搜索也许只是还没跑完）。这种单边性正是不可判定性本身：一个集合可判定，当且仅当它本身和它的补集都是 r.e. 的。

• 是 r.e. 但不是 co-r.e. 的： 停机集（等待即可确认停机；无法确认不停机）。
• 其他不可判定的 r.e. 集合： 一阶逻辑的有效性/可证性（枚举证明即可判定），可解的丢番图方程（MRDP 定理/希尔伯特第十问题），字问题。

为什么这是实用的那一层

整个工程上的诀窍在于：即使寻找/判定很难，验证一个证据也很容易——这正是certificates（一份你可以核验的证明）、Σ₁ 的 ∃-证据，也是为什么harness的gates是在检查一致性而不是判定真值。它也正是乔姆斯基谱系中Type-0 r.e. 层级。