Abstract
A description of the completion of a set of identities by a set of inference rules has allowed recent progresses in proving its completeness. But there existed no attempt to use this description in an actual implementation. This paper shows that this is feasible using a functional programming language namely CAML. The implementation uses a toolkit, a set of transition rules and a short procedure for describing the control. A major role is played by the data structure on which both the transition rules and the control operate. Three versions of the classical Knuth-Bendix completion and two versions of the unfailing completion are proposed.
The research was sponsored by PRC “programmation avancée et outils de l'intelligence artificielle”, CNRS and INRIA
Chapter PDF
References
L. Bachmair. Proof methods for equational theories. PhD thesis, University of Illinois, Urbana-Champaign, 1987.
L. Bachmair and N. Dershowitz. Completion for rewriting modulo a congruence. In Proceedings Second Conference on Rewriting Techniques and Applications, Springer Verlag, Bordeaux (France), May 1987.
L. Bachmair, N. Dershowitz, and J. Hsiang. Orderings for equational proofs. In Proc. Symp. Logic in Computer Science, pages 346–357, Boston (Massachusetts USA), 1986.
J. L. Bentley. Writing Efficient Programs. Prentice Hall, 1982.
F. Bellegarde and P. Lescanne. Transformation orderings. In 12th Coll. on Trees in Algebra and Programming, TAPSOFT, pages 69–80, Springer Verlag, 1987.
A. BenCherifa and P. Lescanne. Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming, 9(2):137–160, October 1987.
N. Dershowitz. Completion and its applications. In Proc. Colloquium on Resolution of Equations in Algebraic Structures, MCC, 3500 West Balconies Center Drive, Austin, Texas 78759-6509, May 4–6 1987.
A.J.J. Dick. ERIL equational reasoning: an interactive laboratory. In B. Buchberger, editor, Proceedings of the EUROCAL Conference, Springer-Verlag, Linz (Austria), 1985.
N. Dershowitz, L. Marcus, and A. Tarlecki. Existence, uniqueness and construction of rewrite systems. SIAM J. Comput., 17(4):629–639, August 1988.
F. Fages. Le système KB. Manuel de référence, présentation et bibliographie, mise en œuvre. Technical Report, Greco de Programmation, Bordeaux, 1984.
R. Forgaard and J. Guttag. REVE: A term rewriting system generator with failure-resistant Knuth-Bendix. Technical Report, MIT-LCS, 1984.
R. Forgaard. A program for generating and analyzing term rewriting systems. Technical Report 343, Laboratory for Computer Science, Massachusetts Institute of Technology, 1984. Master's Thesis.
Projet FORMEL. The CAML Primer. Technical Report, INRIA LIENS, 1987.
Projet FORMEL. CAML: the reference Manuel. Technical Report, INRIA-ENS, March 1987.
Projet FORMEL. The CAML Anthology. July 1987. Internal Document.
B. Galabertier. Implémentation de l'ordre de terminaison par transformation. Technical Report, CRIN, Septembre 1988.
H. Ganzinger. A completion procedure for conditional equations. In Proc. 1st International Workshop on Conditional Term Rewriting Systems, pages 62–83, Springer-Verlag, 1987. Extended version to appear in Journal of Symbolic Computation.
S. Garland and J. Guttag. An Overview of LP, The Larch Prover. Technical Report, MIT, 1988.
I. Gnaedig, C. Kirchner, and H. Kirchner. Equational completion in order-sorted algebras. In M. Dauchet and M. Nivat, editors, Proceedings of the 13th Colloquium on Trees in Algebra and Programming, pages 165–184, Springer-Verlag, Nancy (France), 1988.
J. Gallier and W. Snyder. Complete sets of transformations for general E-unification. Journal of Theorical Computer Science, 1988.
J. Hsiang and J-P. Jouannaud. General e-unification revisited. In Proceedings of 2nd Workshop on Unification, 1988.
J. Hsiang and J. Mzali. Algorithme de Complétion SKB. Technical Report, LRI, Orsay, France, 1988. Submitted.
J. Hsiang and M. Rusinowitch. On word problem in equational theories. In Proceedings of 14th International Colloquium on Automata, Languages and Programming, Springer-Verlag, Karlsruhe (West Germany), 1987.
G. Huet. A complete proof of correctness of the Knuth-Bendix completion algorithm. Technical Report 25, INRIA, August 1980.
G. Huet. A complete proof of correctness of the Knuth and Bendix completion algorithm. Journal of Computer Systems and Sciences, 23:11–21, 1981.
D. Knuth and P. Bendix. Simple Word Problems in Universal Algebra, pages 263–297. Pergamon Press, 1970.
H. Kirchner. A general inductive completion algorithm and application to abstract data types. In R. Shostak, editor, Proceedings 7th international Conference on Automated Deduction, pages 282–302, Springer-Verlag, Napa Valley (California, USA), 1984.
K. Kapur and G. Sivakumar. Experiments with an architecture of RRL, a rewrite rule laboratory. In Proc. of an NSF Workshop on the Rewrite Rule Laboratory, pages 33–56, 1983.
P. Lescanne. Computer Experiments with the REVE Term Rewriting Systems Generator. In Proceedings, 10th ACM Symposium on Principles of Programming Languages, ACM, 1983.
F. Orejas. Good food considered helpful. Bulletin of EATCS, 20:14–22, June 1983.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lescanne, P. (1989). Completion procedures as transition rules + control. In: Díaz, J., Orejas, F. (eds) TAPSOFT '89. CAAP 1989. Lecture Notes in Computer Science, vol 351. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-50939-9_123
Download citation
DOI: https://doi.org/10.1007/3-540-50939-9_123
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-50939-4
Online ISBN: 978-3-540-46116-6
eBook Packages: Springer Book Archive