Abstract
The purpose of this paper is to describe a decision algorithm for unifiability of equations w.r.t. the equational theory of two distributive axioms: x*(y+z)=x*y+x*z and (x+y)*z=x*z + y*z. The algorithm is described as a set of non-deterministic transformation rules. The equations given as input are eventually transformed into a conjunction of two further problems: One is an AC 1-unification-problem with linear constant restrictions. The other one is a second-order unification problem that can be transformed into a word-unification problem and then can be decided using Makanin's decision algorithm. Since the algorithm terminates, this is a solution for an open problem in the field of unification.
One spin-off is an algorithm that decides the word-problem w.r.t. D in polynomial time. This is the basis for an NP-algorithm for D-matching, hence D-matching is NP-complete.
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., Algebra of communicating processes with abstraction. J. theoretical computer science 37, 77–121, (1985)
Baader, F., Schulz, K.U., General A-and AX-Unification via Optimised Combination Procedures, Proc. Second International Workshop on Word Equations and Related Topics 1991, LNCS 677, pp. 23–42, (1992)
Baader, F., Schulz, K.U., Unification in the union of disjoint equational theories: Combining decision procedures, Proc. 11th CADE, LNCS 607, Springer-Verlag, pp. 50–65, (1992)
Baader, F, Siekmann, J., Unification Theory, in D.M. Gabbay, C.J. Hogger, J.A: Robinson (eds.), Handbook of Logic in Artificial Intelligence and Logic Programming, Oxford University Press, (1994)
Baeten, J.C.M., Weijland, W.P., Process Algebra, Cambridge tracts in theoretical computer science, Cambridge university press, (1990)
Contejean, E., Solving *-problems modulo Distributivity by a reduction to ACl-Unification, J. of Symbolic Computation 16, pp. 493–521. (1993)
Farmer, W., Farmer, A., Simple second-order languages for which unification is undecidable. Theoretical Computer Science 87, pp. 173–214, (1991)
Goldfarb, W. The undecidability of the second-order unification problem, J. TCS 13, pp. 225–230, (1981)
Jaffar, J., Minimal and complete word unification, J. of the ACM, 37, 47–85, (1990)
Kapur, D., Narendran, Complexity of AC1-unification, JAR 92: pp 261–288, (1992)
Kirchner, C. (ed.), Unification, reprint from J. of Symbolic Computation, Academic Press, (1989)
Makanin, G.S:, The problem of solvability od equations in a free semigroup. Math. Sbornik, 103, 147–236, (1977), english translation in Math USSR Sbornik 32, (1977)
Narendran, P., Pfenning, F., Statman, R., On the unification problem in cartesian closed categories, Proc. Logic in Computer Science, 57–63, (1993)
Rittri, M., Retrieving library identifiers via equational matching of types, Proc. 10th CADE, Springer Lecture Notes in Computer Science 449, 603–617, (1990)
Schmidt-Schauß, M., Unification in a combination of arbitrary disjoint equational theories, J. Symbolic computation 8, 51–99, (1989)
Schmidt-Schauß, M., Some results on unification in distributive equational theories, Internal report 7/92. J.W. Goethe-Universität, Frankfurt am Main, (1992)
Schmidt-Schauß, M., Unification under one-sided distributivity with a multiplicative unit, Proc. LPAR 93, Springer LNCS 698, pp. 289–300, (1993)
Schmidt-Schauß, M., Unification of Stratified Second-Order Terms, Internal report 12/94, Fachbereich Informatik, Johann Wolfgang Goethe-Universität Frankfurt, (1994)
Schmidt-Schauß, M., An Algorithm for Distributive Unification, Internal report 13/94, Fachbereich Informatik, Johann Wolfgang Goethe-Universität Frankfurt, (1994)
Schmidt-Schauß, M., Unification of Stratified Second-Order Terms, improved version of Sch94a, submitted for publication, 1995
Schulz, K.U., Word unification and transformation of generalized equations, J. Automated Reasoning 11, pp. 149–184, (1993)
Siekmann, J., Unification theory: a survey, in C. Kirchner (ed.), Special issue on unification, Journal of symbolic computation 7, (1989)
Szabó, P., Unifikationstheorie erster Ordnung, Dissertation, Karlsruhe, (1982)
Tiden, E., Arnborg, S., Unification problems with one-sided distributivity, J. Symbolic Computation 3, pp. 183–202, (1987)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schmidt-Schauß, M. (1996). An algorithm for distributive unification. In: Ganzinger, H. (eds) Rewriting Techniques and Applications. RTA 1996. Lecture Notes in Computer Science, vol 1103. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61464-8_60
Download citation
DOI: https://doi.org/10.1007/3-540-61464-8_60
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61464-7
Online ISBN: 978-3-540-68596-8
eBook Packages: Springer Book Archive