发表机构
Universitat Jaume I（海梅一世大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出语义提升算子，证明自修改系统中性质保持的不可判定性，并揭示不可验证性在提升下封闭且攀升算术层级。
AI 中文摘要
程序静态语义性质的不可判定性由 Rice 定理所支配。然而，自修改系统所需的分析并非性质当前是否成立，而是当系统重写自身时该性质是否被保持。我们通过语义提升算子 ${\Lambda}{\Phi}$ 形式化这一转变，它将静态问题“$x$ 是否满足 $P$？”转化为动态问题“在 $x$ 被 ${\Phi}$ 变换后，$P$ 是否被保持？”。我们证明，当 ${\Phi}$ 是内涵的（依赖于源代码，而不仅仅是所计算的函数）时，提升后的性质即使打破了 Rice 定理所要求的外延性，仍然是不可判定的；该证明依赖于 Kleene 递归定理，而非 Rice 定理。因此，不可验证性质类 $U$ 在提升算子下是封闭的。对该算子的无界迭代攀升算术层级——达到 ${\Pi}_2^0$-完全性——将不可验证性巩固为一种结构性事实。我们进一步表明，监督性回归不会终止：不存在有限塔的、能力不断增强的验证器能产生无条件的证书。这些结果在有效拓扑斯中的范畴论解读，其中提升表现为 Lawvere 不动点定理的一个实例，留作未来工作的方向。
英文摘要
We ask whether it can be certified algorithmically that a self-modifying program keeps a behavioural property, a safety property in the motivating case, after its next rewrite (preservation) and along its whole evolution (persistence). When the rewrite depends only on behaviour, preservation is a behavioural property and Rice's theorem applies. When the rewrite reads the code, preservation is no longer behavioural; yet, under a uniform disruption condition, the s-m-n reduction that proves Rice's theorem works inside a single class of behaviourally identical programs, and preservation inherits the degree of the halting problem. One step never exceeds the degree of the property, while persistence can climb one level of the arithmetical hierarchy. We then isolate the mechanism shared by rewriting, supervision and system comparison, the elevation operator, and prove a normal form: the preserving set is determined by a single finite trigger and a polarity, and the Rice-Shapiro theorem restricts the polarity to the arithmetical class of the property. Runtime monitors, consistency supervision, conformance to a reference and observational equivalence are instances, and no sound theory covers the preserving systems.
Commentsv3: journal version. Shortened; neutral terminology; new Proposition 7.12 showing that the class of elevation operators is complete for anchored normal forms; comparison with enforcement by program rewriting (Hamlen, Morrisett and Schneider) added; illustrations moved to an appendix. 35 pages. Companion paper: arXiv:2606.28639 (applied consequences)
