RECURRENCE DOMAINS - THEIR UNIFICATION AND APPLICATION TO LOGIC PROGRAMMING

In this paper we present a formalism for finitely representing infinite sets of terms. This formalism, called rho-terms, enables us to reason finitely about certain recursive types. We present an extension of Horn logic programs, called rho-Prolog, which allows a finite schematization of infinitely many clauses via predicates with rho-terms as arguments. We show that for every rho-Prolog program there is an equivalent Horn logic program. That is, incorporating rho-terms into first order logic programming does not change its denotational semantics. Computationally, however, rho-Prolog has the advantages of (1) representing infinitely many answers finitely, (2) avoiding repetition in computation and thus achieving better efficiency, (3) allowing infinite queries, and (4) avoiding certain kinds of non-termination of Prolog programs. The rho-terms play a similar role to regular-trees and sort-expressions in explicitly defining abstract data types. It differs from the others in that it allows us to define certain non-regular-tree sets such as {(a(n), b(n), c(n)): n epsilon N}. We present a finite and complete algorithm for unification between rho-terms, with which we can also compute the intersections of the sets defined by rho-terms. (C) 1995 Academic Press, Inc.