A Framework for Computing Finite SLD Trees

Abstract

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, called closed SLD 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.