Normalizable Horn Clauses, Strongly Recognizable Relations, and Spi
Normalizable Horn Clauses, Strongly Recognizable Relations, and Spi
复制标题
可规范化的霍恩子句、强可识别关系和 Spi
DOI：
10.1007/3-540-45789-5_5
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
H. Seidl
中科院分区：
文献类型：
--
作者：
F. Nielson;H. R. Nielson;H. Seidl
我们展示了一类丰富的角子句，我们称之为H1，他们的模型虽然可能是无限的，但可以有效地计算出最小的模型。我们表明，H1子句的最小模型由所谓的强烈可识别的关系组成，并提出了计算它的指数正常化程序。为了获得用于程序分析的实用工具，我们确定了H1子句的限制，我们称之为H2，其中最少的模型可以在多项式时间内计算。该片段仍然可以表达，例如笛卡尔产品和关系的及时封闭。在H2内部，我们表现出一个碎片H3，其中归一化甚至是立方体。我们通过得出[14]中介绍的SPI微积分[1]的立方控制流分析来证明我们的方法的有用性。
We exhibit a rich class of Horn clauses, which we call H1, whose least models, though possibly infinite, can be computed effectively. We show that the least model of an H1 clause consists of so-called strongly recognizable relations and present an exponential normalization procedure to compute it. In order to obtain a practical tool for program analysis, we identify a restriction of H1 clauses, which we call H2, where the least models can be computed in polynomial time. This fragment still allows to express, e.g., Cartesian product and transitive closure of relations. Inside H2, we exhibit a fragment H3 where normalization is even cubic. We demonstrate the usefulness of our approach by deriving a cubic control-flow analysis for the Spi calculus [1] as presented in [14].