跳到正文
The Lumenary
探奇小径可选 · 从不评分起点 Repetition and decisions

Can a computer decide?

本页尚未翻译成简体中文,因此以English显示。

帮助翻译 →
1

问题

Some programs stop and some loop forever. Could someone write one clever program that looks at any program, together with its input, and always correctly says whether it will stop?

先动手做实验,再往下读。探索没有错误的方式。

2

实验

对角线机器

这里有一列无穷的 0–1 序列(我们只能显示开头部分)。金色序列 d 把对角线上的数字翻转。

s1…
s2…
s3…
s4…
s5…
s6…
d101001????…

将指针移到某一行(或用 Tab 键切换到该行),看看 d 在哪里与它不同。点击任意数字可以修改列表。

把 d 加入列表,就会出现一个新的 d,它又与列表中的每一项都不同。任何列表——无论多长——都不可能包含所有序列。

3

提示(如果你需要)

    4

    这是怎么回事

    这是怎么回事

    In 1936 Alan Turing proved that no such checker can exist. The argument is short.

    Suppose a program HH could take any program PP and input xx and always answer correctly "PP stops on xx" or "PP runs for ever on xx". Build a new program DD: given a program PP, it asks HH whether PP stops when given its own text as input, and then does the opposite — if HH says "stops", DD loops for ever; if HH says "runs for ever", DD stops.

    Now run DD on its own text. If DD stops, then HH said "DD runs for ever" — wrong. If DD runs for ever, then HH said "DD stops" — wrong again. Either way HH makes a mistake, so the perfect checker HH cannot exist. This is the halting problem, and it is undecidable.

    This is the same diagonal trick Cantor used to show that some infinities are bigger than others, and Gödel used to show that no consistent formal system can prove every true statement about whole numbers. It does not say that we can never tell whether a particular program stops — often we can — only that no single program can do it for all programs. Henry Rice later showed that the same holds for every non-trivial question about what programs compute.

    这是类比,不是形式化构造: The experiment shows Cantor's diagonal argument for 0–1 sequences. The halting proof below uses the same diagonal idea, applied to programs; the experiment is an illustration of the idea, not the halting proof itself.

    已通过计算测试AI 起草 · 等待人工审校
    5

    由此通向何处