:: Reduction Relations :: by Grzegorz Bancerek :: :: Received November 14, 1995 :: Copyright (c) 1995-2017 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, FINSEQ_1, ORDINAL4, XBOOLE_0, SUBSET_1, ARYTM_3, RELAT_1, XXREAL_0, CARD_1, NAT_1, FUNCT_1, FINSEQ_5, ARYTM_1, TARSKI, WELLORD1, PBOOLE, RELAT_2, FUNCOP_1, EQREL_1, REWRITE1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, FUNCT_1, RELAT_1, RELAT_2, WELLORD1, EQREL_1, FINSEQ_1, FUNCOP_1, PBOOLE, FINSEQ_5; constructors SETFAM_1, WELLORD1, XXREAL_0, XREAL_0, NAT_1, EQREL_1, PBOOLE, FINSEQ_5, RELSET_1, NUMBERS; registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1, NAT_1, XXREAL_0, XREAL_0, FINSEQ_1, CARD_1; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin :: Forgetting concatenation and reduction sequence definition let p,q be FinSequence; func p\$^q -> FinSequence means :: REWRITE1:def 1 it = p^q if p = {} or q = {} otherwise ex i being Nat, r being FinSequence st len p = i+1 & r = p|Seg i & it = r^q; end; reserve p,q,r for FinSequence, x,y for object; theorem :: REWRITE1:1 {}\$^p = p & p\$^{} = p; theorem :: REWRITE1:2 q <> {} implies (p^<*x*>)\$^q = p^q; theorem :: REWRITE1:3 (p^<*x*>)\$^(<*y*>^q) = p^<*y*>^q; theorem :: REWRITE1:4 q <> {} implies <*x*>\$^q = q; theorem :: REWRITE1:5 p <> {} implies ex x,q st p = <*x*>^q & len p = len q+1; scheme :: REWRITE1:sch 1 PathCatenation {P[set,set], p,q() -> FinSequence}: for i being Nat st i in dom (p()\$^q()) & i+1 in dom (p()\$^q()) for x,y being set st x = (p( )\$^q()).i & y = (p()\$^q()).(i+1) holds P[x,y] provided for i being Nat st i in dom p() & i+1 in dom p() holds P[ p().i, p().(i+1)] and for i being Nat st i in dom q() & i+1 in dom q() holds P[ q().i, q().(i+1)] and len p() > 0 & len q() > 0 & p().len p() = q().1; definition let R be Relation; mode RedSequence of R -> FinSequence means :: REWRITE1:def 2 len it > 0 & for i being Nat st i in dom it & i+1 in dom it holds [it.i, it.(i+1)] in R; end; registration let R be Relation; cluster -> non empty for RedSequence of R; end; theorem :: REWRITE1:6 for R being Relation, a being object holds <*a*> is RedSequence of R; theorem :: REWRITE1:7 for R being Relation, a,b being object st [a,b] in R holds <*a,b*> is RedSequence of R; theorem :: REWRITE1:8 for R being Relation, p,q being RedSequence of R st p.len p = q.1 holds p\$^q is RedSequence of R; theorem :: REWRITE1:9 for R being Relation, p being RedSequence of R holds Rev p is RedSequence of R~; theorem :: REWRITE1:10 for R,Q being Relation st R c= Q for p being RedSequence of R holds p is RedSequence of Q; begin :: Reducibility, convertibility, and normal forms definition let R be Relation; let a,b be object; pred R reduces a,b means :: REWRITE1:def 3 ex p being RedSequence of R st p.1 = a & p. len p = b; end; definition let R be Relation; let a,b be object; pred a,b are_convertible_wrt R means :: REWRITE1:def 4 R \/ R~ reduces a,b; end; theorem :: REWRITE1:11 for R being Relation, a,b being object holds R reduces a,b iff ex p being FinSequence st len p > 0 & p.1 = a & p.len p = b & for i being Nat st i in dom p & i+1 in dom p holds [p.i, p.(i+1)] in R; theorem :: REWRITE1:12 for R being Relation, a being object holds R reduces a,a; theorem :: REWRITE1:13 for a,b being object st {} reduces a,b holds a = b; theorem :: REWRITE1:14 for R being Relation, a,b being object st R reduces a,b & not a in field R holds a = b; theorem :: REWRITE1:15 for R being Relation, a,b being object st [a,b] in R holds R reduces a,b; theorem :: REWRITE1:16 for R being Relation, a,b,c being object st R reduces a,b & R reduces b,c holds R reduces a,c; theorem :: REWRITE1:17 for R being Relation, p being RedSequence of R, i,j being Nat st i in dom p & j in dom p & i <= j holds R reduces p.i,p.j; theorem :: REWRITE1:18 for R being Relation, a,b being object st R reduces a,b & a <> b holds a in field R & b in field R; theorem :: REWRITE1:19 for R being Relation, a,b being object st R reduces a,b holds a in field R iff b in field R; theorem :: REWRITE1:20 for R being Relation, a,b being object holds R reduces a,b iff a = b or [a,b] in R[*]; theorem :: REWRITE1:21 for R being Relation, a,b being object holds R reduces a,b iff R[*] reduces a,b; theorem :: REWRITE1:22 for R,Q being Relation st R c= Q for a,b being object st R reduces a,b holds Q reduces a,b; theorem :: REWRITE1:23 for R being Relation, X being set, a,b being object holds R reduces a,b iff R \/ id X reduces a,b; theorem :: REWRITE1:24 for R being Relation, a,b being object st R reduces a,b holds R~ reduces b,a; theorem :: REWRITE1:25 for R being Relation, a,b being object st R reduces a,b holds a,b are_convertible_wrt R & b,a are_convertible_wrt R; theorem :: REWRITE1:26 for R being Relation, a being object holds a,a are_convertible_wrt R; theorem :: REWRITE1:27 for a,b being object st a,b are_convertible_wrt {} holds a = b; theorem :: REWRITE1:28 for R being Relation, a,b being object st a,b are_convertible_wrt R & not a in field R holds a = b; theorem :: REWRITE1:29 for R being Relation, a,b being object st [a,b] in R holds a,b are_convertible_wrt R; theorem :: REWRITE1:30 for R being Relation, a,b,c being object st a,b are_convertible_wrt R & b,c are_convertible_wrt R holds a,c are_convertible_wrt R; theorem :: REWRITE1:31 for R being Relation, a,b being object st a,b are_convertible_wrt R holds b,a are_convertible_wrt R; theorem :: REWRITE1:32 for R being Relation, a,b being object st a,b are_convertible_wrt R & a <> b holds a in field R & b in field R; definition let R be Relation; let a be object; pred a is_a_normal_form_wrt R means :: REWRITE1:def 5 not ex b being object st [a,b] in R; end; theorem :: REWRITE1:33 for R being Relation, a,b being object st a is_a_normal_form_wrt R & R reduces a,b holds a = b; theorem :: REWRITE1:34 for R being Relation, a being object st not a in field R holds a is_a_normal_form_wrt R; definition let R be Relation; let a,b be object; pred b is_a_normal_form_of a,R means :: REWRITE1:def 6 b is_a_normal_form_wrt R & R reduces a,b; pred a,b are_convergent_wrt R means :: REWRITE1:def 7 ex c being object st R reduces a,c & R reduces b,c; pred a,b are_divergent_wrt R means :: REWRITE1:def 8 ex c being object st R reduces c,a & R reduces c,b; pred a,b are_convergent<=1_wrt R means :: REWRITE1:def 9 ex c being object st ([a,c] in R or a = c) & ([b,c] in R or b = c); pred a,b are_divergent<=1_wrt R means :: REWRITE1:def 10 ex c being object st ([c,a] in R or a = c) & ([c,b] in R or b = c); end; theorem :: REWRITE1:35 for R being Relation, a being object st not a in field R holds a is_a_normal_form_of a,R; theorem :: REWRITE1:36 for R being Relation, a,b being object st R reduces a,b holds a,b are_convergent_wrt R & a,b are_divergent_wrt R & b,a are_convergent_wrt R & b,a are_divergent_wrt R; theorem :: REWRITE1:37 for R being Relation, a,b being object st a,b are_convergent_wrt R or a,b are_divergent_wrt R holds a,b are_convertible_wrt R; theorem :: REWRITE1:38 for R being Relation, a being object holds a,a are_convergent_wrt R & a,a are_divergent_wrt R; theorem :: REWRITE1:39 for a,b being object st a,b are_convergent_wrt {} or a,b are_divergent_wrt {} holds a = b; theorem :: REWRITE1:40 for R being Relation, a,b being object st a,b are_convergent_wrt R holds b,a are_convergent_wrt R; theorem :: REWRITE1:41 for R being Relation, a,b being object st a,b are_divergent_wrt R holds b ,a are_divergent_wrt R; theorem :: REWRITE1:42 for R being Relation, a,b,c being object st R reduces a,b & b,c are_convergent_wrt R or a,b are_convergent_wrt R & R reduces c,b holds a,c are_convergent_wrt R; theorem :: REWRITE1:43 for R being Relation, a,b,c being object st R reduces b,a & b,c are_divergent_wrt R or a,b are_divergent_wrt R & R reduces b,c holds a,c are_divergent_wrt R; theorem :: REWRITE1:44 for R being Relation, a,b being object st a,b are_convergent<=1_wrt R holds a,b are_convergent_wrt R; theorem :: REWRITE1:45 for R being Relation, a,b being object st a,b are_divergent<=1_wrt R holds a,b are_divergent_wrt R; definition let R be Relation; let a be object; pred a has_a_normal_form_wrt R means :: REWRITE1:def 11 ex b being object st b is_a_normal_form_of a,R; end; theorem :: REWRITE1:46 for R being Relation, a being object st not a in field R holds a has_a_normal_form_wrt R; definition let R be Relation, a be object; assume that a has_a_normal_form_wrt R and for b,c being object st b is_a_normal_form_of a,R & c is_a_normal_form_of a,R holds b = c; func nf(a,R) -> set means :: REWRITE1:def 12 it is_a_normal_form_of a,R; end; begin :: Terminating reductions definition let R be Relation; attr R is co-well_founded means :: REWRITE1:def 13 R~ is well_founded; attr R is weakly-normalizing means :: REWRITE1:def 14 for a being object st a in field R holds a has_a_normal_form_wrt R; attr R is strongly-normalizing means :: REWRITE1:def 15 :: terminating, Noetherian for f being ManySortedSet of NAT ex i being Nat st not [f.i,f.(i+1)] in R; end; definition let R be Relation; redefine attr R is co-well_founded means :: REWRITE1:def 16 for Y being set st Y c= field R & Y <> {} ex a being object st a in Y & for b being object st b in Y & a <> b holds not [a,b] in R; end; scheme :: REWRITE1:sch 2 coNoetherianInduction{R() -> Relation, P[object]}: for a being object st a in field R() holds P[a] provided R() is co-well_founded and for a being object st for b being object st [a,b] in R() & a <> b holds P[b] holds P[a]; registration cluster strongly-normalizing -> irreflexive co-well_founded for Relation; cluster co-well_founded irreflexive -> strongly-normalizing for Relation; end; registration cluster empty -> weakly-normalizing strongly-normalizing for Relation; end; theorem :: REWRITE1:47 for Q being co-well_founded Relation, R being Relation st R c= Q holds R is co-well_founded; registration cluster strongly-normalizing -> weakly-normalizing for Relation; end; begin :: Church-Rosser property definition let R,Q be Relation; pred R commutes-weakly_with Q means :: REWRITE1:def 17 for a,b,c being object st [a,b] in R & [a,c ] in Q ex d being object st Q reduces b,d & R reduces c,d; symmetry; pred R commutes_with Q means :: REWRITE1:def 18 for a,b,c being object st R reduces a,b & Q reduces a,c ex d being object st Q reduces b,d & R reduces c,d; symmetry; end; theorem :: REWRITE1:48 for R,Q being Relation st R commutes_with Q holds R commutes-weakly_with Q; definition let R be Relation; attr R is with_UN_property means :: REWRITE1:def 19 for a,b being object st a is_a_normal_form_wrt R & b is_a_normal_form_wrt R & a,b are_convertible_wrt R holds a = b; attr R is with_NF_property means :: REWRITE1:def 20 for a,b being object st a is_a_normal_form_wrt R & a,b are_convertible_wrt R holds R reduces b,a; attr R is subcommutative means :: REWRITE1:def 21 for a,b,c being object st [a,b] in R & [a,c] in R holds b,c are_convergent<=1_wrt R; attr R is confluent means :: REWRITE1:def 22 for a,b being object st a,b are_divergent_wrt R holds a,b are_convergent_wrt R; attr R is with_Church-Rosser_property means :: REWRITE1:def 23 for a,b being object st a,b are_convertible_wrt R holds a,b are_convergent_wrt R; attr R is locally-confluent means :: REWRITE1:def 24 for a,b,c being object st [a,b] in R & [a,c] in R holds b,c are_convergent_wrt R; end; theorem :: REWRITE1:49 for R being Relation st R is subcommutative for a,b,c being object st R reduces a,b & [a,c] in R holds b,c are_convergent_wrt R; theorem :: REWRITE1:50 for R being Relation holds R is confluent iff R commutes_with R; theorem :: REWRITE1:51 for R being Relation holds R is confluent iff for a,b,c being object st R reduces a,b & [a,c] in R holds b,c are_convergent_wrt R; theorem :: REWRITE1:52 for R being Relation holds R is locally-confluent iff R commutes-weakly_with R; registration cluster with_Church-Rosser_property -> confluent for Relation; cluster confluent -> locally-confluent with_Church-Rosser_property for Relation; cluster subcommutative -> confluent for Relation; cluster with_Church-Rosser_property -> with_NF_property for Relation; cluster with_NF_property -> with_UN_property for Relation; cluster with_UN_property weakly-normalizing -> with_Church-Rosser_property for Relation; end; registration cluster empty -> subcommutative for Relation; end; theorem :: REWRITE1:53 for R being with_UN_property Relation for a,b,c being object st b is_a_normal_form_of a,R & c is_a_normal_form_of a,R holds b = c; theorem :: REWRITE1:54 for R being with_UN_property weakly-normalizing Relation for a being object holds nf(a,R) is_a_normal_form_of a,R; theorem :: REWRITE1:55 for R being with_UN_property weakly-normalizing Relation for a,b being object st a,b are_convertible_wrt R holds nf(a,R) = nf(b,R); registration cluster strongly-normalizing locally-confluent -> confluent for Relation; end; definition let R be Relation; attr R is complete means :: REWRITE1:def 25 R is confluent strongly-normalizing; end; registration cluster complete -> confluent strongly-normalizing for Relation; cluster confluent strongly-normalizing -> complete for Relation; end; registration cluster complete for non empty Relation; end; theorem :: REWRITE1:56 for R,Q being with_Church-Rosser_property Relation st R commutes_with Q holds R \/ Q is with_Church-Rosser_property; theorem :: REWRITE1:57 for R being Relation holds R is confluent iff R[*] is locally-confluent; theorem :: REWRITE1:58 for R being Relation holds R is confluent iff R[*] is subcommutative; begin :: Completion method definition let R,Q be Relation; pred R,Q are_equivalent means :: REWRITE1:def 26 for a,b being object holds a,b are_convertible_wrt R iff a,b are_convertible_wrt Q; symmetry; end; definition let R be Relation; let a,b be object; pred a,b are_critical_wrt R means :: REWRITE1:def 27 a,b are_divergent<=1_wrt R & not a,b are_convergent_wrt R; end; theorem :: REWRITE1:59 for R being Relation, a,b being object st a,b are_critical_wrt R holds a,b are_convertible_wrt R; theorem :: REWRITE1:60 for R being Relation st not ex a,b being object st a,b are_critical_wrt R holds R is locally-confluent; theorem :: REWRITE1:61 for R,Q being Relation st for a,b being object st [a,b] in Q holds a,b are_critical_wrt R holds R, R \/ Q are_equivalent; theorem :: REWRITE1:62 for R being Relation ex Q being complete Relation st field Q c= field R & for a,b being object holds a,b are_convertible_wrt R iff a,b are_convergent_wrt Q; definition let R be Relation; mode Completion of R -> complete Relation means :: REWRITE1:def 28 for a,b being object holds a,b are_convertible_wrt R iff a,b are_convergent_wrt it; end; theorem :: REWRITE1:63 for R being Relation, C being Completion of R holds R,C are_equivalent; theorem :: REWRITE1:64 for R being Relation, Q being complete Relation st R,Q are_equivalent holds Q is Completion of R; theorem :: REWRITE1:65 for R being Relation, C being Completion of R, a,b being object holds a,b are_convertible_wrt R iff nf(a,C) = nf(b,C);