可计算性理论可视化实验室

通过交互式动画探索可计算性的核心概念：图灵机、停机问题、递归函数、丘奇-图灵论题、归约、莱斯定理与算术层级。纯 HTML/CSS/JS + SVG 构建，零依赖。

Turing Machine Halting Problem λ-Calculus Undecidability Arithmetical Hierarchy

MODULE 01

图灵机 Turing Machine

由无限纸带、读写头、有限状态控制器与转移规则组成的抽象计算模型。下图演示二进制递增机：从最低位开始执行 +1 并传播进位。

输入: 速度

点击运行开始模拟。当前转移规则将根据纸带符号与状态决定读写头的动作。

状态

步数

磁头位置

纸带内容

1011

MODULE 02

通用图灵机 Universal Turing Machine

通用图灵机 U 能够模拟任意图灵机 M：将 M 的转移函数编码为符号串，连同输入一起放在纸带上，U 解码并逐步模拟。这正是"程序即数据"的思想。

选择机器:

选择一台图灵机后点击编码，将其转移函数编码为一进制串（状态 qk 编码为 1^k+1，符号 sk 编码为 1^k+1，用 0 分隔）。再点击模拟观察通用机如何解码并执行。

编码长度

—

转移数

—

模拟步数

U 的状态

idle

MODULE 03

停机问题 Halting Problem

不存在能判定任意程序是否停机的算法。通过对角线论证：假设存在判定机 H，构造反例机 D(i) = "若 H(i,i)=停机则死循环，否则停机"，令 D 以自身编码 d 为输入即得矛盾。

表格中行代表程序 M_i，列代表输入 j。H=停机，L=死循环。对角线 M_i(i) 的取值定义了反例机 D，D 与自身矛盾。

程序数

对角矛盾

—

H 的判定

—

结论

待推演

MODULE 04

递归函数 Recursive Functions

从初始函数（零函数 Z、后继 S、投影 P）出发，通过组合、原始递归与最小化（μ）算子构造可计算函数。前三类构成原始递归函数，加入 μ 得到部分递归函数。

构建方式: 参数 n:

选择构建方式并输入参数。原始递归可定义加法 add(x,y)、乘法、阶乘等；最小化算子 μ 搜索使谓词成立的最小值，可能发散。

函数类型

初始

输入 n

输出 f(n)

—

是否全定义

是

MODULE 05

丘奇-图灵论题 Church-Turing Thesis

一切"直觉上可计算"的函数，均可用图灵机（等价地：λ 演算、递归函数、寄存器机等）计算。论题无法被证明，但三个独立模型的等价性提供了强有力的证据。

展示:

三个圆分别代表 λ 演算、递归函数、图灵机。流动粒子表示可计算函数在模型间的双向翻译——任一模型可计算的函数，其余两者亦可计算。

模型数

等价性

成立

论题性质

猜想

超越者

无

MODULE 06

归约 Reduction

若问题 A 可通过可计算函数映射为问题 B（多一归约 A ≤_m B），则 B 可判定蕴含 A 可判定。利用归约可将停机问题的不可判定性传递给其他问题，形成不可判定类。

归约类型:

左侧问题 A（如停机问题）通过映射函数 f 归约到右侧问题 B。若 B 可判定，则 A 亦可判定——与 A 不可判定矛盾，故 B 不可判定。

源问题 A

HALT

目标 B

—

归约强度

—

B 可判定?

否

MODULE 07

莱斯定理 Rice's Theorem

图灵机计算的任何非平凡语义性质（即依赖于函数行为而非程序文本的性质）均不可判定。例如"是否计算全函数""是否在某输入上停机"等都不可判定。

语义性质 P:

将图灵机集合划分为满足性质 P 与不满足两部分。因 P 非平凡，存在满足 P 的机器 M_P 与不满足的 M_¬P。从停机问题归约：构造 M'(x) = if H(x) then M_P(x) else M_¬P(x)，则判定 P 等价于判定停机。

性质 P

计算全函数

是否平凡

否

可判定?

否

归约来源

HALT

MODULE 08

算术层级 Arithmetical Hierarchy

按公式中量词交替次数对判定性问题分类：Σ_n（存在量词在前）、Π_n（全称量词在前）、Δ_n = Σ_n ∩ Π_n。层级严格递增，覆盖递归可枚举集到高阶不可判定问题。

层级:

Δ₀：可判定（如 x+y=z）。Σ₁：递归可枚举，如停机问题 ∃t Halts(M,x,t)。Π₁：补递归可枚举，如 ∀t ¬Halts(M,x,t)（非停机）。层级严格包含，每层增加一次量词交替。

当前层级

Σ₁/Π₁

量词交替

代表问题

停机问题