A framework for computing finite SLD trees
A framework for computing finite SLD trees
复制标题
计算有限 SLD 树的框架
DOI：
10.1016/j.jlamp.2014.11.006
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
G. Vidal
中科院分区：
文献类型：
--
作者：
Naoki Nishida;G. Vidal
SLD分解的搜索空间通常由所谓的SLD树表示，通常是无限的。然而，有许多应用程序必须处理可能无限的SLD树，如部分求值或某些静态分析。在这种情况下，能够构建一个有限表示的无限SLD树变得useful.In这项工作中，我们引入了一个框架来构建一个有限的数据结构表示（可能是无限的）SLD派生的目标。这个数据结构称为closedSLD树，使用四个基本操作构建：展开、展平、拆分和包容。我们证明了封闭的SLD树的一些基本性质，即计算的答案和调用被保存。我们提出了几个简单的策略，用于构建不同抽象级别的封闭SLD树，以及它的应用程序的一些例子。最后，我们通过引入一个基于探索封闭SLD树的测试用例生成器来说明我们的方法的可行性。
The search space of SLD resolution, usually represented by means of a so-called SLD tree, is often infinite. However, there are many applications that must deal with possibly infinite SLD trees, like partial evaluation or some static analyses. In this context, being able to construct a finite representation of an infinite SLD tree becomes useful.In this work, we introduce a framework to construct a finite data structure representing the (possibly infinite) SLD derivations for a goal. This data structure, calledclosedSLD tree, is built using four basic operations: unfolding, flattening, splitting, and subsumption. We prove some basic properties for closed SLD trees, namely that both computed answers and calls are preserved. We present a couple of simple strategies for constructing closed SLD trees with different levels of abstraction, together with some examples of its application. Finally, we illustrate the viability of our approach by introducing a test case generator based on exploring closed SLD trees.