A comprehensive setting for matching and unification over iterative terms

Terms finitely representing infinite sequences of finite first-order terms have received attention by several authors. In this paper, we consider the class of recurrent terms proposed by H. Chen and J. Hsiang, and we extend it to allow infinite terms. This extension helps in clarifying the relationships between matching and unification over the class of terms we consider, that we call iterative terms. In fact, it holds that if a term s matches a term t by a substitution G, then the limit of iterations of the matching G, if it exists, is a most general unifier of s and t. A crucial feature of iterative terms is the notion of maximally-folded normal form that allows for a comprehensive treatment of both finite and infinite iterative terms. In this setting, infinite terms can be simply characterized as limits of sequences of finite terms. For finite terms we positively settle an open problem of H. Chen and J. Hsiang on the number of most general unifiers for a pair of terms.