A comprehensive setting for matching and unification over iterative terms

• Autorzy: Intrigila B. , Inverardi P. , Zilli M.V.
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

infinite sequences of terms; infinite terms; normal forms; matching; unification; most general unifiers

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 1999
• Tom: Vol. 39, Nr 3
• Strony: 273--304
• Opis fizyczny: bibliogr. 19 poz.

Twórcy

autor

Intrigila B.

autor

Inverardi P.

autor

Zilli M.V.

• Dipartimento di Matematica Pura ed Applicata, University of L'Aquila, L'Aquila, Italy,