Unification of infinite sets of terms schematized by primal grammars

AbstractInfinite sets of terms appear frequently at different places in computer science. On the other hand, several practically oriented parts of logic and computer science require the manipulated objects to be finite or finitely representable. Schematizations present a suitable formalism to manipulate finitely infinite sets of terms. Since schematizations provide a different approach to solve the same kind of problems as constraints do, they can be viewed as a new type of constraints.The paper presents a new recurrent schematization called primal grammars. The main idea behind the primal grammars is to use primitive recursion as the generating engine of infinite sets. The evaluation of primal grammars is based on substitution and rewriting, hence no particular semantics for them is necessary. This fact allows also a natural integration of primal grammars into Prolog, into functional languages or into other rewrite-based applications.Primal grammars have a decidable unification problem and the paper presents a unification algorithm for them that produces finite results. This unification algorithm is proved sound and complete, and it terminates for every input