Affiliations: Dipartimento di Matematica pura ed applicata, University of L'Aquila, L'Aquila, Italy. intrigila@univaq.it | Dipartimento di Matematica pura ed applicata, University of L'Aquila, L'Aquila, Italy. inverard@univaq.it | Dipartimento di Scienze dell'informazione, University of Rome ‘La Sapienza’ Rome, Italy. zilli@dsi.uniroma1.it
Note: [] Address for correspondence: Dipartimento di Matematica pura ed applicata, University of L'Aquila, L'Aquila, Italy
Note: [] Address for correspondence: Dipartimento di Matematica pura ed applicata, University of L'Aquila, L'Aquila, Italy
Note: [] Address for correspondence: Dipartimento di Scienze dell'informazione, University of Rome ‘La Sapienza’, Rome, Italy
Abstract: 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 Γ, then the limit of iterations of the matching Γ, 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.
Keywords: Infinite sequences of terms, infinite terms, normal forms, matching, unification, most general unifiers
