Abstract
The goal of this paper is both to give a E-unification procedure that always terminates, and to decide unifiability. For this, we assume that the equational theory is specified by a confluent and constructor-based rewrite system, and that four additional restrictions are satisfied. We give a procedure that represents the (possibly infinite) set of solutions thanks to a new kind of grammar, called tree tuple synchronized grammar, and that can decide unifiability thanks to an emptiness test. Moreover we show that if only three of the four additional restrictions are satisfied then unifiability is undecidable.
Missing formal definitions and proofs are given in [10].
Chapter PDF
References
J. Christian. Some Termination Criteria for Narrowing and E-Unification. In Saragota Springs, editor, CADE, Albany (NY, USA), volume 607 of LNAI, pages 582–588. Springer-Verlag, 1992.
H. Comon, M. Haberstrau, and J.-P. Jouannaud. Syntacticness, Cycle-Syntacticness and Shallow Theories. Information and Computation, 111(1):154–191, 1994.
N. Dershowitz and J.-P. Jouannaud. Rewrite Systems. In J. Van Leuven, editor, Handbook of Theoretical Computer Science. Elsevier Science Publishers, 1990.
H. Faßbender and S. Maneth. A strict border for the decidability of E-unification for recursive functions. In proceedings of the intern. Conf. on Algebraic and Logic Programming. To appear., 1996.
R. Gilleron, S. Tison, and M. Tommasi. Some new decidability results on positive and negative set constraints. In LNCS, volume 845, pages 336–351, 1994. First International Conference on Constraints in Computational Logics.
Y. Guan, G. Hotz, and A. Reichert. Tree Grammars with Multilinear Interpretation. Technical Report FB14-S2-01, Fachbereich 14, 1992.
J.-M. Hullot. Canonical Forms and Unification. In W. Bibel and R. Kowalski, editors, CADE, Les Arcs (France), volume 87 of LNCS, pages 318–334. Springer-Verlag, 1980.
Y. Kaji, T. Fujiwara, and T. Kasami. Solving a Unification Problem under Constrained Substitutions Using Tree Automata. In Proc. Fourteenth Conference on FST & TCS, Madras, India, volume 880 of LNCS, pages 276–287. Springer-Verlag, 1994.
D. Kapur and P. Narendran. Matching, unification and complexity. Sigsam Bulletin, 21(4):6–9, November 1987.
S. Limet and P. Réty. E-Unification by Means of Tree Tuple Synchronized Grammars. Technical Report 96-16, Laboratoire d'Informatique Fondamentale d'Orléans, 1996. Available by anonymous ftp at ftp-lifo.univ-orleans.fr.
S. Mitra. Semantic Unification for Convergent Rewrite Systems. Phd thesis, Univ. Illinois at Urbana-Champaign, 1994.
R. Nieuwenhuis. Basic Paramodulation and Decidable Theories. In procedings of the 11th Annual IEEE Symposium on Logic in Computer Science, to appear, 1996.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Limet, S., Réty, P. (1997). E-unification by means of tree tuple synchronized grammars. In: Bidoit, M., Dauchet, M. (eds) TAPSOFT '97: Theory and Practice of Software Development. CAAP 1997. Lecture Notes in Computer Science, vol 1214. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0030616
Download citation
DOI: https://doi.org/10.1007/BFb0030616
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62781-4
Online ISBN: 978-3-540-68517-3
eBook Packages: Springer Book Archive