Warsaw University- Bialystok Reduction Relations.pdf

FORMALIZED MATHEMATICS Volume 5, Number 4, 1996 Warsaw University - Bia lystok 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,11] or [1]; see also [12,10]), i.e. to formalize the concept of the completion of a reduction relation. The completion of a reduction relation R is a complete reduction rela- tion 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 prop- erty, and equivalence of reduction relations. MML Identifier: REWRITE1. The terminology and notation used here are introduced in the following articles: [16], [17], [9], [3], [6], [18], [19], [4], [13], [14], [5], [15], [7], and [8]. 1. Forgetting concatenation and reduction sequence Let p, q be finite sequences. The functor p $
q yielding a finite sequence is defined as follows: (Def. 1) (i) p $
q = p
q if p = ε or q = ε, (ii) there exists a natural number i and there exists a finite sequence r such that len p = i + 1 and r = p Seg i and p $
q = r
q, otherwise. In the sequel p, q are finite sequences and x, y are sets. We now state several propositions: (1) ε $
p = p and p $
ε = p. (2) If q 6= ε, then (p
〈x〉) $
q = p
q. (3) (p
〈x〉) $
(〈y〉
q) = p
〈y〉
q. (4) If q 6= ε, then 〈x〉 $
q = q. (5) If p 6= ε, then there exist x, q such that p = 〈x〉
q and len p = len q+1. 469 c? 1996 Warsaw University - Bia lystok ISSN 1426–2630 470 grzegorz bancerek The scheme PathCatenation concerns finite sequences A, B and a binary predicate P, and states that: Let i be a natural number. Suppose i ∈ dom(A $
B) and i + 1 ∈ dom(A $
B). Let x, y be sets. If x = (A $
B)(i) and y = (A $
B)(i + 1), then P[x, y] provided the parameters satisfy the following conditions: ? For every natural number i such