Towards a Categorical Calculus for Critical-Pair/Completion

  • Karel Stokkermans
Part of the Texts and Monographs in Symbolic Computation book series (TEXTSMONOGR)


The ultimate aim of the research reported here is to provide a general framework for algorithms that show the following two characteristics: critical pairs and completion. Here completion means extending a certain set of reductions (given by, e.g., rewrite rules, or polynomials from an ideal) until that set fulfills some completeness property. Critical pairs are used for the selection of elements for which the reduction relation to be completed is not yet confluent. The selection is essentially done by superposing left hand sides of basic reduction rules, and testing whether applying the applicable reduction rules yield the same reducts. If not, one forces confluence by adding a reduction rule between the differing reducts (if possible without violating certain conditions on the reduction relation).


Normal Form Reduction Relation Universal Property Reduction Rule Critical Pair 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Becker, T., Weispfenning, V. (1993): Gröbner bases. Springer, Berlin Heidelberg New York Tokyo (Graduate texts in mathematics, vol. 141).MATHCrossRefGoogle Scholar
  2. Benson, D. (1975): The basic algebraic structures in the categories of derivations. Inf. Control 28: 1–29.MathSciNetMATHCrossRefGoogle Scholar
  3. Buchberger, B. (1983): A critical-pair/completion algorithm in reduction rings. Tech. Rep. RISC Linz 83-21.Google Scholar
  4. Buchberger, B. (1985a): Gröbner bases: an algorithmic method in polynomial ideal theory. In: Bose, N. (ed.): Multidimensional systems theory. Reidel, Dordrecht, pp. 184–232.CrossRefGoogle Scholar
  5. Buchberger, B. (1985b): Basic features and development of the critical-pair/completion procedure. In: Jouannaud, J.-P. (ed.): Rewriting techniques and applications. Springer, Berlin Heidelberg New York Tokyo, pp. 1–45 (Lecture notes in computer science, vol. 202).CrossRefGoogle Scholar
  6. Buchberger, B., Loos, R. (1982): Algebraic simplification. Computing [Suppl.] 4: 11–43.CrossRefGoogle Scholar
  7. Cox, D., Little, J., O’Shea, D. (1992): Ideals, varieties, and algorithms. Springer, Berlin Heidelberg New York Tokyo (Undergraduate texts in mathematics).MATHGoogle Scholar
  8. Dershowitz, N. (1983): Applications of the Knuth-Bendix completion procedure. Tech. Rep. The Aerospace Corporation El Segundo, California ATR-83(8478)-2.Google Scholar
  9. Dershowitz, N., Jouannaud, J.-P. (1990): Rewriting systems. In: Van Leeuwen, J. (ed.): Handbook of theoretical computer science. Elsevier, Amsterdam, pp. 243–320.Google Scholar
  10. Freyd, P., Ćčedrov, A. (1990): Categories, allegories. North-Holland, Amsterdam.MATHGoogle Scholar
  11. Goldblatt, R. (1984): Topoi. The categorial analysis of logic. North-Holland, Amsterdam.MATHGoogle Scholar
  12. Huet, G. (1980): Confluent reductions: abstract properties and applications to term rewriting systems. J. ACM 27: 797–821.MathSciNetMATHCrossRefGoogle Scholar
  13. Huet, G. (1986): Formal structures for computation and deduction. Working material for lectures at the International Summer School on Logic of Programming and Calculi of Discrete Design in Marktoberdorf, Germany, 1986.Google Scholar
  14. Huet, G., Lévy, J.-J. (1979): Call by need computations in non-ambiguous linear term rewriting systems. Techn. Rep. IRIA 359.Google Scholar
  15. Jay, C. B. (1991): Modelling reduction in confluent categories. Tech. Rep. Department of Computer Science, University of Edinburgh ECS-LFCS-91-187.Google Scholar
  16. Johnson, M. (1987): Pasting diagrams in n-categories with applications to coherence theorems and categories of paths. Ph.D. thesis, University of Sydney, Sydney, N.S.W., Australia.Google Scholar
  17. Johnson, M. (1991): Linear term rewriting systems are higher dimensional string rewriting systems. In: Rattray, C., Clark, R. (eds.): The unified computation laboratory. Oxford University Press, Oxford, pp. 3–12.Google Scholar
  18. Kandri-Rody, A., Kapur, D., Winkler, F. (1989): Knuth-Bendix procedure and Buchberger algorithm — a synthesis. In: Proceedings of the ACM-SIGSAM International Symposium on Symbolic and Algebraic Computation, ISSAC’ 89, Portland, Oregon. ACM Press, New York, pp. 55–67.Google Scholar
  19. Klop, J. W. (1980): Combinatory reduction systems. Ph.D. thesis, Mathematisch Centrum, Amsterdam, The Netherlands.MATHGoogle Scholar
  20. Klop, J. W. (1990): Term rewriting systems. Tech. Rep. Centrum voor Wiskunde en Informatica Amsterdam CS-R9073.Google Scholar
  21. Klop, J. W., Middeldorp, A. (1988): An introduction to Knuth-Bendix completion. Tech. Rep. Vrije Universiteit Amsterdam IR-162.Google Scholar
  22. Knuth, D., Bendix, P. (1967): Simple word problems in universal algebras. In: Leech, J. (ed.): Proceedings of the Conference on Computational Problems in Abstract Algebra, Oxford, 1967. Pergamon Press, Oxford, pp. 263–298.Google Scholar
  23. Lambek, J., Scott, P. (1986): Introduction to higher-order categorical logic. Cambridge University Press, Cambridge (Studies in advanced mathematics, vol. 7).MATHGoogle Scholar
  24. Lévy, J.-J. (1978): Réductions correctes et optimales dans le λ-calcul. Thèse d’Etat, Université de Paris VII, Paris, France.Google Scholar
  25. MacLane, S. (1971): Categories for the working mathematician. Springer, Berlin Heidelberg New York Tokyo (Graduate texts in mathematics, vol. 5).Google Scholar
  26. MacLane, S., Moerdijk, I. (1992): Sheaves in geometry and logic. Springer, Berlin Heidelberg New York Tokyo.CrossRefGoogle Scholar
  27. MEDLAR Consortium (1989): Mechanizing deduction in the logics of practical reasoning. Technical Annex of ESPRIT BRA 3125. Tech. Rep. RISC Linz 89-49.0.Google Scholar
  28. Power, A. J. (1989): An abstract formulation for rewrite systems. In: Pitt, D. H., Rydeheard, D. E., Dybjer, P., Pitts, A. M., Poigne, A. (eds.): Category theory and computer science. Springer, Berlin Heidelberg New York Tokyo, pp. 300–312 (Lecture notes in computer science, vol. 389).CrossRefGoogle Scholar
  29. Power, A. J. (1990): A 2-categorical pasting theorem. J. Algebra 129: 439–445.MathSciNetMATHCrossRefGoogle Scholar
  30. Reichel, H. (1990): A 2-category approach to critical pair completion. In: Ehrig, H., Jantke, K. P., Orejas, F., Reichel, H. (eds.): Recent trends in data type specification. Springer, Berlin Heidelberg New York Tokyo, pp. 266–273 (Lecture notes in computer science, vol. 534).Google Scholar
  31. Rydeheard, D., Burstall, R. (1985): A categorical unification algorithm. In: Pitt, D. H., Abramsky, S., Poigne, A., Rydeheard, D. E. (eds.): Category theory and computer programming. Springer, Berlin Heidelberg New York Tokyo, pp. 493–505 (Lecture notes in computer science, vol. 240).Google Scholar
  32. Rydeheard, D., Stell, J. (1987): Foundations of equational deduction: a categorical treatment of equational proofs and unification algorithms. In: Pitt, D. H., Poigne, A., Rydeheard, D. E. (eds.): Category theory and computer science. Springer, Berlin Heidelberg New York Tokyo, pp. 114–139 (Lecture notes in computer science, vol. 283).CrossRefGoogle Scholar
  33. Stell, J. (1992): Categorical aspects of unification and rewriting. Ph.D. thesis, University of Manchester, Manchester, U.K.Google Scholar
  34. Stokkermans, K. (1991): A categorical approach to critical-pair/completion procedures. Techn. Rep. RISC Linz 91-58.Google Scholar
  35. Stokkermans, K. (1992): A categorical formulation for critical-pair/completion procedures. In: Rusinowitch, M., Rémy, J.-L. (eds.): Conditional term rewriting systems. Springer, Berlin Heidelberg New York Tokyo, pp. 328–342 (Lecture notes in computer science, vol. 656).Google Scholar

Copyright information

© Springer-Verlag Wien 1995

Authors and Affiliations

  • Karel Stokkermans

There are no affiliations available

Personalised recommendations