Abstract
Unification in the presence of an equational theory is an important problem in theorem-proving and in the integration of functional and logic programming languages. This paper presents an improvement of the proposed lazy unification methods by incorporating simplification into the unification process. Since simplification is a deterministic computation process, more efficient unification algorithms can be achieved. Moreover, simplification reduces the search space so that in some case infinite search spaces are reduced to finite ones. We show soundness and completeness of our method for equational theories represented by ground confluent and terminating rewrite systems which is a reasonable class w.r.t. functional logic programming.
Chapter PDF
Similar content being viewed by others
References
S. Antoy, R. Echahed, and M. Hanus. A Needed Narrowing Strategy. In Proc. 21st ACM Symp. on Principles of Programming Languages, pp. 268–279, Portland, 1994.
D. Bert and R. Echahed. Design and Implementation of a Generic, Logic and Functional Programming Language. In Proc. ESOP'86, pp. 119–132. Springer LNCS 213, 1986.
J. Darlington and Y. Guo. Narrowing and unification in functional programming — an evaluation mechanism for absolute set abstraction. In Proc. of the Conference on Rewriting Techniques and Applications, pp. 92–108. Springer LNCS 355, 1989.
N. Dershowitz. Termination of Rewriting. J. Symbolic Computation, Vol. 3, pp. 69–116, 1987.
N. Dershowitz and J.-P. Jouannaud. Rewrite Systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Vol. B, pp. 243–320. Elsevier, 1990.
N. Dershowitz, S. Mitra, and G. Sivakumar. Equation Solving in Conditional AC-Theories. In Proc. ALP'90, pp. 283–297. Springer LNCS 463, 1990.
R. Echahed. Uniform Narrowing Strategies. In Proc. of the 3rd International Conference on Algebraic and Logic Programming, pp. 259–275. Springer LNCS 632, 1992.
M.J. Fay. First-Order Unification in an Equational Theory. In Proc. 4th Workshop on Automated Deduction, pp. 161–167, Austin (Texas), 1979. Academic Press.
L. Fribourg. SLOG: A Logic Programming Language Interpreter Based on Clausal Superposition and Rewriting. In Proc. IEEE Internat. Symposium on Logic Programming, pp. 172–184, Boston, 1985.
J.H. Gallier and S. Raatz. Extending SLD-Resolution to Equational Horn Clauses Using E-Unification. Journal of Logic Programming (6), pp. 3–43, 1989.
J.H. Gallier and W. Snyder. Complete Sets of Transformations for General E-Unification. Theoretical Computer Science, Vol. 67, pp. 203–260, 1989.
A. Geser and H. Hussmann. Experiences with the RAP system — a specification interpreter combining term rewriting and resolution. In Proc. ESOP 86, pp. 339–350. Springer LNCS 213, 1986.
E. Giovannetti, G. Levi, C. Moiso, and C. Palamidessi. Kernel LEAF: A Logic plus Functional Language. Journal of Computer and System Sciences, Vol. 42, No. 2, pp. 139–185, 1991.
W. Hans, R. Loogen, and S. Winkler. On the Interaction of Lazy Evaluation and Backtracking. In Proc. PLILP'92, pp. 355–369. Springer LNCS 631, 1992.
M. Hanus. Compiling Logic Programs with Equality. In Proc. PLILP'90, pp. 387–401. Springer LNCS 456, 1990.
M. Hanus. Improving Control of Logic Programs by Using Functional Logic Languages. In Proc. PLILP'92, pp. 1–23. Springer LNCS 631, 1992.
M. Hanus. Lazy Unification with Inductive Simplification. Technical Report MPI-I-93-215, Max-Planck-Institut für Informatik, Saarbrücken, 1993.
M. Hanus. The Integration of Functions into Logic Programming: From Theory to Practice. To appear in Journal of Logic Programming, 1994.
S. Hölldobler. Foundations of Equational Logic Programming. Springer LNCS 353, 1989.
J.-P. Jouannaud and H. Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal on Computing, Vol. 15, No. 4, pp. 1155–1194, 1986.
A. Martelli and U. Montanari. An Efficient Unification Algorithm. ACM Transactions on Programming Languages and Systems, Vol. 4, No. 2, pp. 258–282, 1982.
A. Martelli, G.F. Rossi, and C. Moiso. Lazy Unification Algorithms for Canonical Rewrite Systems. In Hassan Aït-Kaci and Maurice Nivat, editors, Resolution of Equations in Algebraic Structures, Volume 2, Rewriting Techniques, chapter 8, pp. 245–274. Academic Press, New York, 1989.
J.J. Moreno-Navarro and M. Rodríguez-Artalejo. Logic Programming with Functions and Predicates: The Language BABEL. Journal of Logic Programming, Vol. 12, pp. 191–223, 1992.
W. Nutt, P. Réty, and G. Smolka. Basic Narrowing Revisited. Journal of Symbolic Computation, Vol. 7, pp. 295–317, 1989.
P. Padawitz. Computing in Horn Clause Theories, volume 16 of EATCS Monographs on Theoretical Computer Science. Springer, 1988.
G.D. Plotkin. Building-in Equational Theories. In B. Meltzer and D. Michie, editors, Machine Intelligence 7, pp. 73–90, 1972.
U.S. Reddy. Narrowing as the Operational Semantics of Functional Languages. In Proc. IEEE Internat. Symposium on Logic Programming, pp. 138–151, Boston, 1985.
P. Réty. Improving basic narrowing techniques. In Proc. of the Conference on Rewriting Techniques and Applications, pp. 228–241. Springer LNCS 256, 1987.
J.H. Siekmann. An Introduction to Unification Theory. In Formal Techniques in Artificial Intelligence, pp. 369–425. Elsevier Science Publishers, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hanus, M. (1994). Lazy unification with simplification. In: Sannella, D. (eds) Programming Languages and Systems — ESOP '94. ESOP 1994. Lecture Notes in Computer Science, vol 788. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57880-3_18
Download citation
DOI: https://doi.org/10.1007/3-540-57880-3_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57880-2
Online ISBN: 978-3-540-48376-2
eBook Packages: Springer Book Archive