AI 中文总结
从递归理论角度研究抽象解释的局部完备性与不完备性，刻画静态和动态程序分析区别，证明诱导局部完备谓词变换器的程序类难以捉摸但有可判定覆盖，可通过程序转换构造有效枚举。
AI 中文摘要
我们从递归理论的角度研究抽象解释的局部完备性和不完备性。局部完备性弱化了全局完备性，捕捉了特定前置条件下精度损失的不存在：抽象计算产生的结果恰好是通过抽象相应具体计算得到的。这支持组合推理并排除验证中的误报。我们根据一致可判定操作来刻画静态和动态程序分析的区别，并观察到动态程序分析仅对平凡抽象是一致可判定的。然后我们证明，对于给定的非平凡抽象域，诱导局部完备谓词变换器的程序类在精确的递归理论意义上是难以捉摸的：它是一个产生集，因此不是可计算枚举的，并且在温和假设下，其补集也是如此。特别地，第一类属于$\Pi^0_2$，第二类属于$\Sigma^0_2$。与通常的$\Pi^0_2$属性示例不同，我们表明局部完备程序类允许可判定覆盖。这使得通过程序转换能够构造一个有效枚举，该枚举完全覆盖此类的程序代表子集——从外部捕捉一个从内部难以枚举的类。
英文摘要
We study local completeness and incompleteness of abstract interpretations from a recursion-theoretic perspective. Local completeness weakens global completeness and captures the absence of precision loss for a specific precondition: abstract computation yields exactly what is obtained by abstracting the corresponding concrete computation. This enables compositional reasoning and rules out false positives in verification. We characterize the distinction between static and dynamic program analysis in terms of uniformly decidable operations and observe that the latter is uniformly decidable only for trivial abstractions. We then prove that the class of programs inducing a predicate transformer that is locally complete for a given non-trivial abstract domain is elusive in a precise recursion-theoretic sense: it is a productive set, hence not computably enumerable, and, under mild hypotheses, the same holds for its complement. In particular, the first class lies in $Π^0_2$ and the second in $Σ^0_2$. Unlike the usual examples of $Π^0_2$ properties, we show that the classes of locally complete programs admit decidable coverings. This makes it possible to construct, via program transformation, an effective enumeration of a representative subset of programs that entirely covers this class -- capturing from the outside a class that eludes enumeration from within.
