Abstract
We present a complete algorithm for the unification of higher-order patterns modulo the associative-commutative theory of some constants +1,...,+nGiven an AC-unification problem over higher-order patterns, the output of the algorithm is a finite set DAG solved forms [9], constrained by some flexible-flexible equations with the same head on both sides. Indeed, in the presence of AC constants, such equations are always solvable, but they have no minimal complete set of unifiers [13]. We prove that the algorithm terminates, is sound, and that any solution of the original unification problem is an instance of one of the computed solutions which satisfies the constraints.
This research was supported in part by the EWG CCL, the HCM Network CONSOLE, and the “GDR de programmation du CNRS”.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Alexandre Boudet. Unification dans les Mélanges de Théories équationnelles. Thése de doctorat, Université Paris-Sud, Orsay, France, February 1990.
Alexandre Boudet. Combining unification algorithms. Journal of Symbolic Computation, 16:597–626, 1993.
Alexandre Boudet. Competing for the AC-unification race. Journal of Automated Reasoning, 11:185–212, 1993.
Alexandre Boudet, Evelyne Contejean, and Hervé Devie. A new AC-unification algorithm with a new algorithm for solving diophantine equations. In Proc. 5 th IEEE Symp. Logic in Computer Science, Philadelphia, pages 289–299. IEEE Computer Society Press, June 1990.
A. Bouhoula, J.-P. Jouannaud, and J. Meseguer. Specification and proof in membership equational logic. In Michel Bidoit and Max Dauchet, editors, Theory and Practice of Software Development, volume 1214 of Lecture Notes in Computer Science, Lille, France, April 1997. Springer-Verlag.
Val Breazu-Tannen. Combining algebra and higher-order types. In Proc. 3rd IEEE Symp. Logic in Computer Science, Edinburgh, July 1988.
R. Hindley and J. Seldin. Introduction to Combinators and λ-calculus. Cambridge University Press, 1986.
Gérard Huet. Résolution déquations dans les langages d'ordre 1, 2... w. Thése d'Etat, Univ. Paris 7, 1976.
Jean-Pierre Jouannaud and Claude Kirchner. Solving equations in abstract algebras: A rule-based survey of unification. In Jean-Louis Lassez and Gordon Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson. MIT-Press, 1991.
Jean-Pierre Jouannaud and Mitsuhiro Okada. Executable higher-order algebraic specification languages. In Proc. 6th IEEE Symp. Logic in Computer Science, Amsterdam, pages 350–361, 1991.
D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. In P. Schroeder-Heister, editor, Extensions of Logic Programming. LNCS 475, Springer Verlag, 1991.
T. Nipkow. Higher order critical pairs. In Proc. IEEE Symp. on Logic in Comp. Science, Amsterdam, 1991.
Zhenyu Qian and Kang Wang. Modular AC-Unification of Higher-Order Patterns. In Jean-Pierre Jouannaud, editor, First International Conference on Constraints in Computational Logics, volume 845 of Lecture Notes in Computer Science, pages 105–120, München, Germany, September 1994. Springer-Verlag.
Jörg H. Siekmann. Unification theory. Journal of Symbolic Computation, 7(3 & 4), 1989. Special issue on unification, part one.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boudet, A., Contejean, E. (1997). AC-unification of higher-order patterns. In: Smolka, G. (eds) Principles and Practice of Constraint Programming-CP97. CP 1997. Lecture Notes in Computer Science, vol 1330. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0017445
Download citation
DOI: https://doi.org/10.1007/BFb0017445
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63753-0
Online ISBN: 978-3-540-69642-1
eBook Packages: Springer Book Archive