:: String Rewriting Systems
:: by Micha{\l} Trybulec
::
:: Received July 17, 2007
:: Copyright (c) 2007-2021 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, NAT_1, FINSEQ_1, RELAT_1, ARYTM_3, CARD_1, XXREAL_0,
ORDINAL4, REWRITE1, TARSKI, SUBSET_1, FUNCT_1, AFINSQ_1, XBOOLE_0,
ORDINAL2, RELAT_2, PRELAMB, FINSEQ_5, LANG1, CIRCTRM1, REWRITE2,
ORDINAL1, FINSET_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, FINSET_1, RELAT_1,
DOMAIN_1, XCMPLX_0, NAT_1, FINSEQ_5, FUNCT_1, RELSET_1, XXREAL_0,
AFINSQ_1, RELAT_2, FINSEQ_1, REWRITE1, FLANG_1, LANG1, PARTIT_2;
constructors NAT_1, FINSEQ_5, REWRITE1, FLANG_1, LANG1, XREAL_0, RELSET_1,
PARTIT_2;
registrations NAT_1, AFINSQ_1, REWRITE1, FINSEQ_1, XXREAL_0, XBOOLE_0,
RELAT_1, FUNCT_1, XREAL_0, ORDINAL1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin :: Preliminaries: finite sequences.
reserve x for set;
reserve k, l for Nat;
reserve p, q for FinSequence;
theorem :: REWRITE2:1
not k in dom p & k + 1 in dom p implies k = 0;
theorem :: REWRITE2:2
k > len p & k <= len (p^q) implies ex l st k = len p + l & l >= 1
& l <= len q;
:: Preliminaries: reduction sequences.
reserve R for Relation;
reserve p, q for RedSequence of R;
theorem :: REWRITE2:3
k >= 1 implies p | k is RedSequence of R;
theorem :: REWRITE2:4
k in dom p implies ex q st len q = k & q.1 = p.1 & q.len q = p.k;
begin
:: XFinSequence yielding functions and finite sequences.
:: These definitions will be later used for introduction of
:: reduction sequences between words from E^omega (XFinSequences).
definition
let f be Function;
attr f is XFinSequence-yielding means
:: REWRITE2:def 1
x in dom f implies f.x is XFinSequence;
end;
registration
cluster empty -> XFinSequence-yielding for Function;
end;
registration
let f be XFinSequence;
cluster <*f*> -> XFinSequence-yielding;
end;
registration
let p be XFinSequence-yielding Function;
let x be object;
cluster p.x -> finite Function-like Relation-like;
end;
registration
let p be XFinSequence-yielding Function;
let x be object;
cluster p.x -> Sequence-like;
end;
registration
cluster XFinSequence-yielding for FinSequence;
end;
registration
let E be set;
cluster -> XFinSequence-yielding for FinSequence of E^omega;
end;
registration
let p, q be XFinSequence-yielding FinSequence;
cluster p^q -> XFinSequence-yielding;
end;
begin
:: Concatenation (left-sided and right-sided ) of an XFinSequence
:: with all elements of a XFinSequence-yielding Function.
definition
let s be XFinSequence;
let p be XFinSequence-yielding Function;
func s ^+ p -> XFinSequence-yielding Function means
:: REWRITE2:def 2
dom it = dom p & for x st x in dom p holds it.x = s^(p.x);
func p +^ s -> XFinSequence-yielding Function means
:: REWRITE2:def 3
dom it = dom p & for x st x in dom p holds it.x = (p.x)^s;
end;
registration
let s be XFinSequence;
let p be XFinSequence-yielding FinSequence;
cluster s ^+ p -> FinSequence-like;
cluster p +^ s -> FinSequence-like;
end;
:: Properties of the left-sided and right-sided concatenation.
reserve E for set;
reserve s, t for XFinSequence;
reserve p, q for XFinSequence-yielding FinSequence;
theorem :: REWRITE2:5
len (s ^+ p) = len p & len(p +^ s) = len p;
theorem :: REWRITE2:6
<%>E ^+ p = p & p +^ <%>E = p;
theorem :: REWRITE2:7
s ^+ (t ^+ p) = (s^t) ^+ p & (p +^ t) +^ s = p +^ (t^s);
theorem :: REWRITE2:8
s ^+ (p +^ t) = (s ^+ p) +^ t;
theorem :: REWRITE2:9
s ^+ (p^q) = (s ^+ p)^(s ^+ q) & (p^q) +^ s = (p +^ s)^(q +^ s);
begin
:: Redefinitions for E^omega:
definition
let E be set;
let p be FinSequence of E^omega;
let k be Nat;
redefine func p.k -> Element of E^omega;
end;
definition
let E be set;
let s be Element of E^omega;
let p be FinSequence of E^omega;
redefine func s ^+ p -> FinSequence of E^omega;
redefine func p +^ s -> FinSequence of E^omega;
end;
:: Definitions of semi-Thue systems and Thue systems.
definition
let E be set;
mode semi-Thue-system of E is Relation of E^omega;
end;
reserve E for set;
reserve S, T, U for semi-Thue-system of E;
registration
let S be Relation;
cluster S \/ S~-> symmetric;
end;
registration
let E;
cluster symmetric for semi-Thue-system of E;
end;
definition
let E be set;
mode Thue-system of E is symmetric semi-Thue-system of E;
end;
begin
:: Direct derivations.
reserve s, t, s1, t1, u, v, u1, v1, w for Element of E^omega;
reserve p for FinSequence of E^omega;
definition
let E, S, s, t;
pred s -->. t, S means
:: REWRITE2:def 4
[s, t] in S;
end;
definition
let E, S, s, t;
pred s ==>. t, S means
:: REWRITE2:def 5
ex v, w, s1, t1 st s = v^s1^w & t = v^t1^w & s1 -->. t1, S;
end;
theorem :: REWRITE2:10
s -->. t, S implies s ==>. t, S;
theorem :: REWRITE2:11
s ==>. s, S implies ex v, w, s1 st s = v^s1^w & s1 -->. s1, S;
theorem :: REWRITE2:12
s ==>. t, S implies u^s ==>. u^t, S & s^u ==>. t^u, S;
theorem :: REWRITE2:13
s ==>. t, S implies u^s^v ==>. u^t^v, S;
theorem :: REWRITE2:14
s -->. t, S implies u^s ==>. u^t, S & s^u ==>. t^u, S;
theorem :: REWRITE2:15
s -->. t, S implies u^s^v ==>. u^t^v, S;
theorem :: REWRITE2:16
S is Thue-system of E & s -->. t, S implies t -->. s, S;
theorem :: REWRITE2:17
S is Thue-system of E & s ==>. t, S implies t ==>. s, S;
theorem :: REWRITE2:18
S c= T & s -->. t, S implies s -->.t, T;
theorem :: REWRITE2:19
S c= T & s ==>. t, S implies s ==>.t, T;
theorem :: REWRITE2:20
not s ==>. t, {}(E^omega, E^omega);
theorem :: REWRITE2:21
s ==>. t, S \/ T implies s ==>. t, S or s ==>. t, T;
begin
:: ==>.-relation is introduced to define derivations
:: using concepts from REWRITE1.
definition
let E;
redefine func id E -> Relation of E;
end;
definition
let E, S;
func ==>.-relation(S) -> Relation of E^omega means
:: REWRITE2:def 6
[s, t] in it iff s ==>. t, S;
end;
theorem :: REWRITE2:22
S c= ==>.-relation(S);
theorem :: REWRITE2:23
p is RedSequence of ==>.-relation(S) implies p +^ u is
RedSequence of ==>.-relation(S) & u ^+ p is RedSequence of ==>.-relation(S);
theorem :: REWRITE2:24
p is RedSequence of ==>.-relation(S) implies t ^+ p +^ u is
RedSequence of ==>.-relation(S);
theorem :: REWRITE2:25
S is Thue-system of E implies ==>.-relation(S) = (==>.-relation( S))~;
theorem :: REWRITE2:26
S c= T implies ==>.-relation(S) c= ==>.-relation(T);
theorem :: REWRITE2:27
==>.-relation(id (E^omega)) = id (E^omega);
theorem :: REWRITE2:28
==>.-relation(S \/ id (E^omega)) = ==>.-relation(S) \/ id (E ^omega);
theorem :: REWRITE2:29
==>.-relation({}(E^omega, E^omega)) = {}(E^omega, E^omega);
theorem :: REWRITE2:30
s ==>. t, ==>.-relation(S) implies s ==>. t, S;
theorem :: REWRITE2:31
==>.-relation(==>.-relation(S)) = ==>.-relation(S);
begin :: Derivations.
definition
let E, S, s, t;
pred s ==>* t, S means
:: REWRITE2:def 7
==>.-relation(S) reduces s, t;
end;
theorem :: REWRITE2:32
s ==>* s, S;
theorem :: REWRITE2:33
s ==>. t, S implies s ==>* t, S;
theorem :: REWRITE2:34
s -->. t, S implies s ==>* t, S;
theorem :: REWRITE2:35
s ==>* t, S & t ==>* u, S implies s ==>* u, S;
theorem :: REWRITE2:36
s ==>* t, S implies s^u ==>* t^u, S & u^s ==>* u^t, S;
theorem :: REWRITE2:37
s ==>* t, S implies u^s^v ==>* u^t^v, S;
theorem :: REWRITE2:38
s ==>* t, S & u ==>* v, S implies s^u ==>* t^v, S & u^s ==>* v^t, S;
theorem :: REWRITE2:39
S is Thue-system of E & s ==>* t, S implies t ==>* s, S;
theorem :: REWRITE2:40
S c= T & s ==>* t, S implies s ==>* t, T;
theorem :: REWRITE2:41
s ==>* t, S iff s ==>* t, S \/ id (E^omega);
theorem :: REWRITE2:42
s ==>* t, {}(E^omega, E^omega) implies s = t;
theorem :: REWRITE2:43
s ==>* t, ==>.-relation(S) implies s ==>* t, S;
theorem :: REWRITE2:44
s ==>* t, S & u ==>. v, {[s, t]} implies u ==>* v, S;
theorem :: REWRITE2:45
s ==>* t, S & u ==>* v, S \/ {[s, t]} implies u ==>* v, S;
begin :: Languages generated by semi-Thue systems.
definition
let E, S, w;
func Lang(w, S) -> Subset of E^omega equals
:: REWRITE2:def 8
{ s : w ==>* s, S };
end;
theorem :: REWRITE2:46
s in Lang(w, S) iff w ==>* s, S;
theorem :: REWRITE2:47
w in Lang(w, S);
registration
let E be non empty set;
let S be semi-Thue-system of E;
let w be Element of E^omega;
cluster Lang(w, S) -> non empty;
end;
theorem :: REWRITE2:48
S c= T implies Lang(w, S) c= Lang(w, T);
theorem :: REWRITE2:49
Lang(w, S) = Lang(w, S \/ id (E^omega));
theorem :: REWRITE2:50
Lang(w, {}(E^omega, E^omega)) = {w};
theorem :: REWRITE2:51
Lang(w, id (E^omega)) = {w};
begin :: Equivalence of semi-Thue systems.
definition
let E, S, T, w;
pred S, T are_equivalent_wrt w means
:: REWRITE2:def 9
Lang(w, S) = Lang(w, T);
end;
theorem :: REWRITE2:52
S, S are_equivalent_wrt w;
theorem :: REWRITE2:53
S, T are_equivalent_wrt w implies T, S are_equivalent_wrt w;
theorem :: REWRITE2:54
S, T are_equivalent_wrt w & T, U are_equivalent_wrt w implies S, U
are_equivalent_wrt w;
theorem :: REWRITE2:55
S, S \/ id (E^omega) are_equivalent_wrt w;
theorem :: REWRITE2:56
S, T are_equivalent_wrt w & S c= U & U c= T implies S, U
are_equivalent_wrt w & U, T are_equivalent_wrt w;
theorem :: REWRITE2:57
S, ==>.-relation(S) are_equivalent_wrt w;
theorem :: REWRITE2:58
S, T are_equivalent_wrt w & ==>.-relation(S \/ T) reduces w, s
implies ==>.-relation(S) reduces w, s;
theorem :: REWRITE2:59
S, T are_equivalent_wrt w & w ==>* s, S \/ T implies w ==>* s, S;
theorem :: REWRITE2:60
S, T are_equivalent_wrt w implies S, S \/ T are_equivalent_wrt w;
theorem :: REWRITE2:61
s ==>. t, S implies S, (S \/ {[s, t]}) are_equivalent_wrt w;
theorem :: REWRITE2:62
s ==>* t, S implies S, (S \/ {[s, t]}) are_equivalent_wrt w;