Recurrence Domains: Their Unification and Application to Logic Programming

AbstractIn this paper we present a formalism for finitely representing infinite sets of terms. This formalism, called ρ-terms, enables us to reason finitely about certain recursive types. We present an extension of Horn logic programs, called ρ-Prolog, which allows a finite schematization of infinitely many clauses via predicates with ρ-terms as arguments. We show that for every ρ-Prolog program there is an equivalent Horn logic program. That is, incorporating ρ-terms into first order logic programming does not change its denotational semantics. Computationally, however, ρ-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 ρ-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 {(an, bn, cn): nϵN}. We present a finite and complete algorithm for unification between ρ-terms, with which we can also compute the intersections of the sets defined by ρ-terms