On finite representations of infinite sequences of terms

Abstract

In this paper we introduce a notion of recurrence-terms for finitely representing infinite sequences of terms. A recurrence-term utilizes the structural similarities among terms and expresses them explicitly using recurrence relations. Its formalism is natural and simple, and based on which algebraic operations such as unification, matching, and reductions can be defined. Recurrence-rewrite rules, defined respectively, also yield finite representation of certain divergent term rewriting systems. Recurrence-rules do not only play a passive role in detecting divergence, they can also be incorporated as part of the completion process. In addition to giving the formalism, we present methods of inferring recurrence-terms from finite sets of regular terms, and a matching algorithm between a recurrence-term and a regular term. Recurrence-term rewriting systems are also defined, and we prove the equivalence between a recurrence-system and the (infinite) term rewriting system it schematizes, as well as the preservation of desirable properties such as termination and confluence.