无法用安全Agda编写的终止程序示例及构造性证明需求

启用--safe选项的Agda强制所有函数通过结构化递归或良基递归证明终止性，因此无法编写非终止程序。但根据停机问题的结论：所有终止函数的集合是不可判定的，而安全Agda的终止检查器是可判定的，因此必然存在可证终止但无法在安全Agda中写出逐点等价版本的函数。以下给出有限输出和无限输出的具体示例，并提供易于理解的证明。

1. 有限输出示例：安全Agda终止函数的特征函数 #

函数定义 #

定义全函数F : ℕ → Bool，其中：

• F e = true，当且仅当编码为e的函数能通过安全Agda的终止检查（即可以在--safe模式下定义）
• F e = false，否则

这里的编码e是将Agda函数映射为自然数的哥德尔编码（所有可计算函数都可被编码为自然数）。

终止性证明 #

安全Agda的终止检查器是一个可判定程序：对于任意编码e，我们可以运行终止检查器，它必然在有限步内返回“通过”或“不通过”的结果。因此F对所有输入e都能在有限步内给出结果，是严格终止的全函数。

无法在安全Agda中实现的证明 #

假设存在安全Agda中的函数F' : ℕ → Bool与F逐点等价。我们构造函数G : ℕ → ℕ：

G : ℕ → ℕ
G n = if F' ⌜G⌝ then G n else 0

其中⌜G⌝是G的哥德尔编码。

现在分析F ⌜G⌝的取值：

• 若F ⌜G⌝ = true：说明G能通过安全Agda的终止检查，但根据G的定义，当F' ⌜G⌝ = true时会无限递归，矛盾。
• 若F ⌜G⌝ = false：说明G无法通过安全Agda的终止检查，但此时F' ⌜G⌝ = false，G n = 0是明显终止的函数，理应通过检查，矛盾。

由此可知假设不成立，F无法在安全Agda中实现。

2. 无限输出示例：基于停机信息的无限流生成函数 #

函数定义 #

定义全函数streamFromHalt : ℕ → Stream ℕ，其中Stream ℕ是无限自然数序列的coinductive类型，函数行为：

• 若编码为e的函数在输入0时停机，则streamFromHalt e是无限重复序列0, 0, 0, ...
• 否则，streamFromHalt e是递增序列1, 2, 3, ...

终止性（良定义性）证明 #

从元理论角度看，每个可计算函数要么在输入0时停机，要么不停机，二者必居其一。因此对于任意e，streamFromHalt e的每一位都有明确的取值：要么全为0，要么从1开始递增。该函数在coinductive意义下是良定义的（即可以生成合法的无限流，无矛盾）。

无法在安全Agda中实现的证明 #

假设安全Agda中存在streamFromHalt' : ℕ → Stream ℕ与原函数逐点等价。我们可以构造一个停机判定器：

haltsOn0 : ℕ → Bool
haltsOn0 e = head (streamFromHalt' e) == 0

其中head : Stream ℕ → ℕ是取无限流第一个元素的投影函数（安全Agda中允许定义此类coinductive类型的操作）。

但停机问题的核心结论是：不存在可计算的停机判定器。而安全Agda中的所有函数都是可计算的（构造性逻辑保证了这一点），因此haltsOn0不可能存在，进而streamFromHalt'也无法存在。

内容的提问来源于stack exchange，提问作者zamfofex