Witnessability of Undecidable Problems
Witnessability of Undecidable Problems
复制标题
不可判定问题的可见证性
DOI：
10.1145/3571227
复制
发表时间：
2023
影响因子：
--
通讯作者：
Zhang, Qirun
中科院分区：
文献类型：
--
作者：
Ding, Shuo;Zhang, Qirun
编程语言理论和形式化方法中的许多问题是不可判定的，因此无法精确解决。处理不可判定问题的实用技术通常基于可判定的近似。不确定性意味着这些近似值总是不精确的。通常，从业者使用启发式和临时推理来识别不精确问题并改进近似值，但是缺乏关于这些努力是否能够成功的可计算性理论基础。本文展示了不可判定性和可判定近似值之间令人惊讶的相互作用：存在一类不可判定问题，因此可以计算将任何可判定近似值转换为证明其不精确性的见证输入。我们将那些不可判定的问题称为可见证的问题。例如，如果程序属性Pi是可见证的，则存在可计算函数fP，使得fP将任何程序分析器针对P的代码作为输入，并产生程序分析器不精确的输入程序w。更令人惊讶的事实是，可见证问题类别几乎包括编程语言理论和形式方法中所有不可判定的问题。具体来说，我们证明对角停止问题K是可见证的，并且可见证问题的类别在补集和多一约简下是封闭的。特别是，赖斯定理中提到的所有“程序的非平凡语义属性”都是可见的。我们还明确地构造了不可见证（和不可判定）类中的问题，并表明这两个类的基数都是 2ℵ0。我们的结果为理解不可判定性提供了新的视角：对于可见证的问题，尽管不可能精确地解决它们，但总是可以改进任何可判定的近似，使其更接近精确的解决方案。这一事实正式表明，对此类近似的研究工作是有前途的，并表明存在识别程序分析器、程序验证器、SMT求解器等精度问题的通用方法，因为它们的本质是可见证问题的可判定近似。
Many problems in programming language theory and formal methods are undecidable, so they cannot be solved precisely. Practical techniques for dealing with undecidable problems are often based on decidable approximations. Undecidability implies that those approximations are always imprecise. Typically, practitioners use heuristics andad hocreasoning to identify imprecision issues and improve approximations, but there is a lack of computability-theoretic foundations about whether those efforts can succeed.This paper shows a surprising interplay between undecidability and decidable approximations: there exists a class of undecidable problems, such that it is computable to transform any decidable approximation to a witness input demonstrating its imprecision. We call those undecidable problemswitnessable problems. For example, if a program propertyPis witnessable, then there exists a computable functionfP, such thatfPtakes as input the code of any program analyzer targetingPand produces an input programwon which the program analyzer is imprecise. An even more surprising fact is that the class of witnessable problems includes almost all undecidable problems in programming language theory and formal methods. Specifically, we prove the diagonal halting problemKis witnessable, and the class of witnessable problems is closed under complements and many-one reductions. In particular, all “non-trivial semantic properties of programs” mentioned in Rice’s theorem are witnessable. We also explicitly construct a problem in the non-witnessable (and undecidable) class and show that both classes have cardinality 2ℵ0.Our results offer a new perspective on the understanding of undecidability: for witnessable problems, although it is impossible to solve them precisely, it is always possible to improve any decidable approximation to make it closer to the precise solution. This fact formally demonstrates that research efforts on such approximations are promising and shows there exist universal ways to identify precision issues of program analyzers, program verifiers, SMT solvers, etc., because their essences are decidable approximations of witnessable problems.
登录
查看更多内容
通过抽象解释进行形式语言、语法和基于集合约束的程序分析
DOI：
10.1145/224164.224199
发表时间：
1995
期刊：
ACM Trans. Program. Lang. Syst.
影响因子：
--
作者：
P. Cousot;R. Cousot
通讯作者：
R. Cousot
NP 困难问题的近似性
DOI：
10.1145/276698.276784
发表时间：
1998
期刊：
--
影响因子：
--
作者：
Sanjeev Arora
通讯作者：
Sanjeev Arora
DOI：
10.1007/978-3-030-00250-3_2
发表时间：
2018-09
期刊：
--
影响因子：
--
作者：
Joel D. Day;Vijay Ganesh;Paul He;F. Manea;Dirk Nowotka
通讯作者：
Joel D. Day;Vijay Ganesh;Paul He;F. Manea;Dirk Nowotka
DOI：
--
发表时间：
--
期刊：
影响因子：
--
作者：
R. Bruni;R. Giacobazzi;R. Gori;I. Garcia;Dusko Pavlovic
通讯作者：
Dusko Pavlovic
Nelson-Oppen 和基于重写的决策程序的可判定性和不可判定性结果
DOI：
10.1007/11814771_42
发表时间：
2006
期刊：
--
影响因子：
--
作者：
M. P. Bonacina;S. Ghilardi;Enrica Nicolini;Silvio Ranise;D. Zucchelli
通讯作者：
D. Zucchelli