Abstract
We consider terms in which some patterns can be repeatedn times.n is an integer variable which is part of the syntax of the terms (and hence may occur more than once in them). We show that unification of such terms is decidable and finitary, extending Chen and Hsiang's result onp-term unification. Finally, extending slightly the syntax yields an undecidable unification problem.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
H. Chen and J. Hsiang. Logic programming with recurrence domains.Proc. 18th International Colloquium on Automata, Languages, and Programming, Madrid. Lecture Notes in Computer Science, Vol. 510. Springer-Verlag, Berlin, 1991.
H. Chen, J. Hsiang, and H.-C. Kong. On finite representations of infinite sequences of terms.Proc. CTRS 90, Montreal, 1990.
H. Comon Completion of rewrite systems with membership constraints.Proc. 19th International Colloquium on Automata, Languages, and Programming, Vienna. Lecture Notes in Computer Science, Vol. 623. Springer-Verlag, 1992.
E. Contejean. Elements pour la decidabilite de l'unification modulo la distributivité. Thèse de Doctorat, Universite de Paris-Sud, France, April 1992.
J. -P. Jouannaud and C. Kirchner. Solving equations in abstract algebras: A rule-based survey of unification. In J. -L. Lassez and G. Plotkin, editors,Computational Logic: Essays in Honor of Alan Robinson. MIT Press, Cambridge, MA, 1991.
G. Salzer. On unification of infinite sets of terms and its applications.Proc. LPAR 92. Lecture Notes in Computer Science, Vol. 624. Springer-Verlag, Berlin, 1992, pp. 409–421.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Comon, H. On unification of terms with integer exponents. Math. Systems Theory 28, 67–88 (1995). https://doi.org/10.1007/BF01294596
Received:
Accepted:
Issue Date:
DOI: https://doi.org/10.1007/BF01294596