Transformations of CLP modules
Transformations of CLP modules
复制标题
DOI：
10.1016/0304-3975(95)00148-4
复制
发表时间：
1996-10-20
影响因子：
1.1
通讯作者：
Gabbrielli, M
中科院分区：
文献类型：
--
作者：
Etalle, S;Gabbrielli, M
提出了一种约束逻辑规划（CLP）程序和模块的转换系统。该框架的灵感来自Tamaki和Sate（1984）的纯逻辑程序。然而，CLP的使用允许我们引入一些新的操作，比如拆分和约束替换。我们提供了两组适用条件。第一个保证原始程序和转换后的程序在答案约束方面具有相同的计算行为。第二组包含了更多保证组合性的约束条件：我们证明了在这些条件下，原模块和变换后的模块在与其他模块组合时具有相同的答案约束。这个结果是通过首先引入CLP结果语义的树的新公式来证明的。作为推论，我们得到了模系统和非模系统w.r.t的正确性，即最小模型语义。
We propose a transformation system for Constraint Logic Programming (CLP) programs and modules. The framework is inspired by the one of Tamaki and Sate (1984) for pure logic programs. However, the use of CLP allows us to introduce some new operations such as splitting and constraint replacement. We provide two sets of applicability conditions. The first one guarantees that the original and the transformed programs have the same computational behaviour, in terms of answer constraints. The second set contains more restrictive conditions that ensure compositionality: we prove that under these conditions the original and the transformed modules have the same answer constraints also when they are composed with other modules. This result is proved by first introducing a new formulation, in terms of trees, of a resultants semantics for CLP. As corollaries we obtain the correctness of both the modular and the nonmodular system w.r.t, the least model semantics.