Abstract
We show that unification in the equational theory defined by the one-sided distributivity law x × (y+z)=x×y+x×z is decidable and that unification is undecidable if the laws of associativity x+(y+z)=(x+y)+z and unit element 1×x=x× 1=x are added. Unification under one-sided distributivity with unit element is shown to be as hard as Markov's problem, whereas unification under two-sided distributivity, with or without unit element, is NP-hard. A quadratic time unification algorithm for one-sided distributivity, which may prove interesting since available universal unification procedures fail to provide a decision procedure for this theory, is outlined. The study of these problems is motivated by possible applications in circuit synthesis and by the need for gaining insight in the problem of combining theories with overlapping sets of operator symbols.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Bergstra, J.A. and Klop, J.W.: The Algebra of Recursively defined Processes and the Algebra of Regular Processes, ICALP 84, LNCS 172, 82–94, Springer, 1984.
Davis, M.: Hilberts tenth problem is unsolvable, Amer. Math. Monthly, vol 80, 1973.
Garey, M.R. and Johnson, D.S.: Computers and Intractability, W.H. Freeman and Company, 1979.
Huet, G.: Résolution d'équations dans des languages d'ordre 1, 2, ..., ω. Thèse de doctorat d'état, Université Paris VII, 1976.
Huet, G. and Oppen, D.C.: Equations and Rewrite Rules: A Survey, in Formal Languages: Perspectives and Open Problems, Ed. R. Book, Academic Press, 1980.
Hullot, J.M.: Canonical Forms and Unification, Proc. 5th Workshop on Automated Deduction, LNCS 87, 318–334, Springer, 1980.
Kirchner, C.: A New Equational Unification Method: A Generalisation of Martelli-Montanari's Algorithm, 7th Int. Conf. on Automated Deduction, LNCS 170, 224–247, Springer, 1984.
Makanin, G.S.: The Problem of Solvability of Equations in a Free Semigroup, Soviet Akad., Nauk SSSR, Tom 233, no 2, 1977.
Martelli, A. and Montanari, U.: An Efficient Unification Algorithm, ACM Trans. Programming Languages and Systems 4(2), 258–282, 1982.
Siekmann, J.: Universal Unification, 7th Int. Conf. on Automated Deduction, LNCS 170, 1–42, Springer, 1984.
Szabó, P.: Unifikationstheorie erster Ordnung. Thesis, Univ. Karlsruhe, 1982.
Tarjan, R.E.: Efficiency of a Good but not Linear Set Union Algorithm, JACM 22(2), 215–225.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1985 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Arnborg, S., Tidén, E. (1985). Unification problems with one-sided distributivity. In: Jouannaud, JP. (eds) Rewriting Techniques and Applications. RTA 1985. Lecture Notes in Computer Science, vol 202. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-15976-2_20
Download citation
DOI: https://doi.org/10.1007/3-540-15976-2_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-15976-6
Online ISBN: 978-3-540-39679-6
eBook Packages: Springer Book Archive