Abstract
Semi-unification is a generalization of both matching and ordinary unification: for a given pair of terms s and t, two substitutions ρ and σ are sought such that ρ(σ(s))=σ(t). Semi-unifiability can be used as a check for non-termination of a rewrite rule, but constructing a correct semi-unification algorithm has been an elusive goal; for example, an algorithm given by Purdom in his RTA-87 paper was incorrect. This paper presents a decision procedure for semi-unification based on techniques similar to those used in the Knuth-Bendix completion procedure. When its inputs are semi-unifiable, the procedure yields a canonical term-rewriting system from which substitutions ρ and σ are easily extracted. Though exponential in its computing time, the decision procedure can be improved to a polynomial time algorithm, as will be shown.
Some of the results reported here are a partial fulfillment of the Ph.D. requirements of the last author, and will be part of his dissertation.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
De Champeaux, D., “About the Paterson-Wegman Linear Unification Algorithm,” in J. of Computer and System Sciences 32, 1986, pp. 79–90.
Dershowitz, N., “Orderings for term-rewriting systems,” in Theoretical Computer Science 17, 1982, pp. 279–301.
Dershowitz, N., “Termination,” in Rewriting Techniques and Applications, Jean-Pierre Jouannaud, ed., Springer Verlag, Berlin, 1985, pp. 180–224.
Henglein, F., “Type Inference and Semi-Unification,” in Proceedings, ACM Conference on LISP and Functional Programming, ACM, ACM Press, June 1988.
Hsiang, J., and Dershowitz, N., “Rewrite methods for clausal and non-clausal theorem proving,” in Proc. 10th EATCS Intl. Colloq. on Automata, Languages, and Programming, Barcelona, Spain, 1983.
Huet, G., and Lankford, D.S., “On the Uniform Halting Problem for Term Rewriting Systems,” Rapport Laboria 283, INRIA, Paris, 1978.
Huet, G., and Oppen, D., “Equations and rewrite rules: a survey,” in Formal Languages: Perspectives and Open Problems (R. Book, ed.), Academic Press, New York, 1980.
Kapur, D., and Narendran, P., “An equational approach to theorem proving in first-order predicate calculus,” in 9th Intl. Joint Conference on Artificial Intelligence, Los Angeles, California, 1985.
Kapur, D., Sivakumar, G., and Zhang, H., “RRL: a rewrite rule laboratory,” in Proceedings of the 8th Intl. Conference on Automated Deduction, Oxford, U.K., 1986, LNCS 230, Springer-Verlag.
Knuth, D.E., and Bendix, P.B., “Simple word problems in universal algebras,” in Computational Problems in Abstract Algebra (J. Leech, ed.), Pergamon Press, Oxford, 1970, pp. 263–297.
Kruskal, J.B., “Well-quasi-ordering, the Tree Theorem, and Vazsonyi's conjecture,” in Transactions of the American Mathematical Society 95, 1960, pp. 210–225.
Lankford, D.S., and Musser, D.R. “A finite termination criterion,” Unpublished Draft, USC Information Sciences Institute, Marina Del Rey, California, 1978.
Paterson, M.S., and Wegman, M.N., “Linear Unification,” in J. of Computer and System Sciences 16, 1978, pp. 158–167. (see also [1]).
Plaisted, D.A., “A simple non-termination test for the Knuth-Bendix method,” in Proceedings of the 8th Intl. Conf. on Automated Deduction, Oxford, U.K., 1986, LNCS 230, Springer Verlag, NY, 79–88.
Purdom, P.W., Jr., “Detecting Looping Simplifications,” in Proc. 2nd Conference on Rewrite Rule Theory and Applications (RTA), Bordeaux, France, May 1987, LNCS 250, Springer-Verlag, 54–62.
Thompson, D.H., and Erickson, R.W. (eds.), AFFIRM Reference Manual, USC Information Sciences Institute, Marina Del Rey, California, 1981.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1988 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kapur, D., Musser, D., Narendran, P., Stillman, J. (1988). Semi-unification. In: Nori, K.V., Kumar, S. (eds) Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1988. Lecture Notes in Computer Science, vol 338. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-50517-2_95
Download citation
DOI: https://doi.org/10.1007/3-540-50517-2_95
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-50517-4
Online ISBN: 978-3-540-46030-5
eBook Packages: Springer Book Archive