抽象域的压缩化

本文展示了在抽象解释中对逻辑语言进行可逆分析时，如何通过系统性地细化抽象域而不牺牲精度。其核心思想是将语义结构纳入抽象域，使得细化后的抽象域富足以容纳自下而下和自上而下的语义近似值相互一致。此类抽象域称为压缩抽象域。实质上，若目标驱动分析与独立于目标的分析一致，则抽象域即为压缩的，即在独立于目标的分析中对查询的近似不会引入精度损失。我们证明了压缩是抽象域的属性，问题在于使抽象域压缩化归结为使该域相对于统一性完备的问题。在一般的抽象解释框架下，我们展示当具体域和运算导致量块（即命题线性逻辑的模型）时，完善后的抽象域中的对象可由基于线性逻辑的表述式明确 characterize。这是一种用于近似计算答案置换的抽象域，其中统一在量块中充当乘积联合的角色。因此，压缩抽象域可通过简单的域细化算子对任何通常非压缩域进行最小化扩展来系统地推导。