Journal of Formalized Mathematics
Volume 7, 1995
University of Bialystok
Copyright (c) 1995 Association of Mizar Users

Reduction Relations


Grzegorz Bancerek
Institute of Mathematics, Polish Academy of Sciences

Summary.

The goal of the article is to start the formalization of Knuth-Bendix completion method (see [2], [10] or [1]; see also [11],[9]), i.e. to formalize the concept of the completion of a reduction relation. The completion of a reduction relation $R$ is a complete reduction relation equivalent to $R$ such that convertible elements have the same normal forms. The theory formalized in the article includes concepts and facts concerning normal forms, terminating reductions, Church-Rosser property, and equivalence of reduction relations.

MML Identifier: REWRITE1

The terminology and notation used in this paper have been introduced in the following articles [12] [15] [14] [3] [6] [16] [4] [5] [13] [7] [8]

Contents (PDF format)

  1. Forgetting concatenation and reduction sequence
  2. Reducibility, convertibility and normal forms
  3. Terminating reductions
  4. Church-Rosser property
  5. Completion method

Bibliography

[1] S. Abramsky, D. M. Gabbay, and S. E. Maibaum, editors. \em Handbook of Logic in Computer Science, vol. 2: Computational structures. Clarendon Press, Oxford, 1992.
[2] Leo Bachmair and Nachum Dershowitz. Critical pair criteria for completion. \em Journal of Symbolic Computation, 6(1):1--18, 1988.
[3] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.
[4] Grzegorz Bancerek. The well ordering relations. Journal of Formalized Mathematics, 1, 1989.
[5] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.
[6] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[7] Czeslaw Bylinski. Some properties of restrictions of finite sequences. Journal of Formalized Mathematics, 7, 1995.
[8] Patricia L. Carlson and Grzegorz Bancerek. Context-free grammar --- part I. Journal of Formalized Mathematics, 4, 1992.
[9] Gerard Huet. A complete proof of correctness of the Knuth-Bendix completion. \em Journal of Computer and System Sciences, 23(1):3--57, 1981.
[10] Jan Willem Klop and Aart Middeldorp. An introduction to Knuth-Bendix completion. \em CWI Quarterly, 1(3):31--52, 1988.
[11] Donald E. Knuth and Peter B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, \em Computational Problems in Abstract Algebras, pages 263--297, Oxford, 1970. Pergamon.
[12] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[13] Andrzej Trybulec. Many-sorted sets. Journal of Formalized Mathematics, 5, 1993.
[14] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[15] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[16] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

Received November 14, 1995


[ Download a postscript version, MML identifier index, Mizar home page]