:: Equivalence of Epsilon, Nondeterministic [Finite] Automata and Deterministic
:: [Finite] Automata
:: by Micha{\l} Trybulec
::
:: Received May 25, 2009
:: Copyright (c) 2009-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, XBOOLE_0, SUBSET_1, AFINSQ_1, NAT_1, REWRITE3, XXREAL_0,
ARYTM_3, CARD_1, FINSEQ_1, ORDINAL4, RELAT_1, FUNCT_1, FLANG_1, FSM_1,
STRUCT_0, ZFMISC_1, TARSKI, FINSET_1, REWRITE2, PRELAMB, FSM_2, LANG1,
REWRITE1, MCART_1, FSM_3;
notations CARD_1, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XCMPLX_0, ORDINAL1,
DOMAIN_1, FUNCT_1, RELSET_1, XXREAL_0, FINSET_1, AFINSQ_1, SUBSET_1,
REWRITE1, FLANG_1, STRUCT_0, NUMBERS, MCART_1, FINSEQ_1, REWRITE3;
constructors NAT_1, MEMBERED, REWRITE1, FLANG_1, XREAL_0, REWRITE3, RELSET_1,
XTUPLE_0;
registrations CARD_1, NAT_1, XREAL_0, XBOOLE_0, XXREAL_0, STRUCT_0, SUBSET_1,
REWRITE1, AFINSQ_1, RELAT_1, FINSET_1, FINSEQ_1, REWRITE3, FUNCT_1,
RELSET_1, ORDINAL1, XTUPLE_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin
reserve x, y, X for set;
reserve E for non empty set;
reserve e for Element of E;
reserve u, u1, v, v1, v2, w, w9, w1, w2 for Element of E^omega;
reserve F for Subset of E^omega;
reserve i, k, l for Nat;
reserve TS for non empty transition-system over F;
reserve S, T for Subset of TS;
:: Preliminaries - Natural Numbers
theorem :: FSM_3:1
i >= k + l implies i >= k;
:: Preliminaries - Sequences
theorem :: FSM_3:2
for a, b being FinSequence holds a ^ b = a or b ^ a = a implies b = {};
theorem :: FSM_3:3
for p, q being FinSequence st k in dom p & len p + 1 = len q
holds k + 1 in dom q;
:: Preliminaries - XFinSequences and Words in E^omega
theorem :: FSM_3:4
len u = 1 implies ex e st <%e%> = u & e = u.0;
theorem :: FSM_3:5
k <> 0 & len u <= k + 1 implies ex v1, v2 st len v1 <= k & len v2
<= k & u = v1^v2;
theorem :: FSM_3:6
for p, q being XFinSequence st <%x%>^p = <%y%>^q holds x = y & p = q;
theorem :: FSM_3:7
len u > 0 implies ex e, u1 st u = <%e%>^u1;
:: Preliminaries - Lex
registration
let E;
cluster Lex(E) -> non empty;
end;
theorem :: FSM_3:8
not <%>E in Lex(E);
theorem :: FSM_3:9
u in Lex(E) iff len u = 1;
theorem :: FSM_3:10
u <> v & u in Lex(E) & v in Lex(E) implies not ex w st u^w = v or w^u = v;
:: Transition Systems over Lex(E)
theorem :: FSM_3:11
for TS being transition-system over Lex E
holds the Tran of TS is Function implies TS is deterministic;
:: Powerset Construction for Transition Systems
:: This is a construction that limits new transitions to single character ones.
definition
let E, F, TS;
func _bool TS -> strict transition-system over Lex(E) means
:: FSM_3:def 1
the
carrier of it = bool (the carrier of TS) & for S, w, T holds [[S, w], T] in the
Tran of it iff len w = 1 & T = w-succ_of (S, TS);
end;
registration
let E, F, TS;
cluster _bool TS -> non empty deterministic;
end;
registration
let E, F;
let TS be finite non empty transition-system over F;
cluster _bool TS -> finite;
end;
theorem :: FSM_3:12
x, <%e%> ==>* y, <%>E, _bool TS implies x, <%e%> ==>. y, <%>E, _bool TS;
theorem :: FSM_3:13
len w = 1 implies (X = w-succ_of (S, TS) iff S, w ==>* X, _bool TS);
:: Semiautomata
definition
let E, F;
struct (transition-system over F) semiautomaton over F (# carrier -> set,
Tran -> Relation of [: the carrier, F :], the carrier, InitS -> Subset of the
carrier #);
end;
definition
let E, F;
let SA be semiautomaton over F;
attr SA is deterministic means
:: FSM_3:def 2
(the transition-system of SA) is deterministic & card (the InitS of SA) = 1;
end;
registration
let E, F;
cluster strict non empty finite deterministic for semiautomaton over F;
end;
reserve SA for non empty semiautomaton over F;
registration
let E, F, SA;
cluster the transition-system of SA -> non empty;
end;
definition
let E, F, SA;
func _bool SA -> strict semiautomaton over Lex(E) means
:: FSM_3:def 3
the
transition-system of it = _bool the transition-system of SA & the InitS of it =
{ <%>E-succ_of (the InitS of SA, SA) };
end;
registration
let E, F, SA;
cluster _bool SA -> non empty deterministic;
end;
theorem :: FSM_3:14
the carrier of _bool SA = bool the carrier of SA;
registration
let E, F;
let SA be finite non empty semiautomaton over F;
cluster _bool SA -> finite;
end;
:: Left-languages
definition
let E, F, SA;
let Q be Subset of SA;
func left-Lang(Q) -> Subset of E^omega equals
:: FSM_3:def 4
{ w : Q meets w-succ_of (the
InitS of SA, SA) };
end;
theorem :: FSM_3:15
for Q being Subset of SA holds w in left-Lang(Q) iff Q meets w
-succ_of (the InitS of SA, SA);
:: Automata
definition
let E, F;
struct (semiautomaton over F) automaton over F (# carrier -> set, Tran ->
Relation of [: the carrier, F :], the carrier, InitS -> Subset of the carrier,
FinalS -> Subset of the carrier #);
end;
definition
let E, F;
let A be automaton over F;
attr A is deterministic means
:: FSM_3:def 5
(the semiautomaton of A) is deterministic;
end;
registration
let E, F;
cluster strict non empty finite deterministic for automaton over F;
end;
reserve A for non empty automaton over F;
reserve p, q for Element of A;
registration
let E, F, A;
cluster the transition-system of A -> non empty;
cluster the semiautomaton of A -> non empty;
end;
definition
let E, F, A;
func _bool A -> strict automaton over Lex(E) means
:: FSM_3:def 6
the semiautomaton
of it = _bool the semiautomaton of A & the FinalS of it = { Q where Q is
Element of it : Q meets (the FinalS of A) };
end;
registration
let E, F, A;
cluster _bool A -> non empty deterministic;
end;
theorem :: FSM_3:16
the carrier of _bool A = bool the carrier of A;
registration
let E, F;
let A be finite non empty automaton over F;
cluster _bool A -> finite;
end;
:: Languages Accepted by Automata
definition
let E, F, A;
let Q be Subset of A;
func right-Lang(Q) -> Subset of E^omega equals
:: FSM_3:def 7
{ w : w-succ_of (Q, A) meets
(the FinalS of A) };
end;
theorem :: FSM_3:17
for Q being Subset of A holds w in right-Lang(Q) iff w-succ_of (
Q, A) meets (the FinalS of A);
definition
let E, F, A;
func Lang(A) -> Subset of E^omega equals
:: FSM_3:def 8
{ u : ex p, q st p in the InitS of
A & q in the FinalS of A & p, u ==>* q, A };
end;
theorem :: FSM_3:18
w in Lang(A) iff ex p, q st p in the InitS of A & q in the
FinalS of A & p, w ==>* q, A;
theorem :: FSM_3:19
w in Lang(A) iff w-succ_of (the InitS of A, A) meets (the FinalS of A);
theorem :: FSM_3:20
Lang(A) = left-Lang(the FinalS of A);
theorem :: FSM_3:21
Lang(A) = right-Lang(the InitS of A);
:: Equivalence (with respect to the accepted languages)
:: of nondeterministic [finite] automata and deterministic [finite] automata.
reserve TS for non empty transition-system over Lex(E) \/ {<%>E};
theorem :: FSM_3:22
for R being RedSequence of ==>.-relation(TS) st (R.1)`2 = <%e%>^
u & (R.len R)`2 = <%>E holds (R.2)`2 = <%e%>^u or (R.2)`2 = u;
theorem :: FSM_3:23
for R being RedSequence of ==>.-relation(TS) st (R.1)`2 = u & (R
.len R)`2 = <%>E holds len R > len u;
theorem :: FSM_3:24
for R being RedSequence of ==>.-relation(TS) st (R.1)`2 = u^v &
(R.len R)`2 = <%>E ex l st l in dom R & (R.l)`2 = v;
definition
let E, u, v;
func chop(u, v) -> Element of E^omega means
:: FSM_3:def 9
for w st w^v = u holds it = w if ex w st w^v = u otherwise it = u;
end;
theorem :: FSM_3:25
for p being RedSequence of ==>.-relation(TS) st p.1 = [x, u^w] &
p.len p = [y, v^w] ex q being RedSequence of ==>.-relation(TS) st q.1 = [x, u]
& q.len q = [y, v];
theorem :: FSM_3:26
==>.-relation(TS) reduces [x, u^w], [y, v^w] implies
==>.-relation(TS) reduces [x, u], [y, v];
theorem :: FSM_3:27
x, u^w ==>* y, v^w, TS implies x, u ==>* y, v, TS;
theorem :: FSM_3:28
for p, q being Element of TS st p, u^v ==>* q, TS holds ex r
being Element of TS st p, u ==>* r, TS & r, v ==>* q, TS;
theorem :: FSM_3:29
w^v-succ_of (X, TS) = v-succ_of (w-succ_of (X, TS), TS);
theorem :: FSM_3:30
_bool TS is non empty transition-system over Lex(E) \/ {<%>E};
theorem :: FSM_3:31
w-succ_of ({ v-succ_of (X, TS) }, _bool TS) = { v^w-succ_of (X, TS) };
reserve SA for non empty semiautomaton over Lex(E) \/ {<%>E};
theorem :: FSM_3:32
w-succ_of ({ <%>E-succ_of (X, SA) }, _bool SA) = { w-succ_of (X, SA) };
reserve A for non empty automaton over Lex(E) \/ {<%>E};
reserve P for Subset of A;
theorem :: FSM_3:33
x in the FinalS of A & x in P implies P in the FinalS of _bool A;
theorem :: FSM_3:34
X in the FinalS of _bool A implies X meets the FinalS of A;
theorem :: FSM_3:35
the InitS of _bool A = { <%>E-succ_of (the InitS of A, A) };
theorem :: FSM_3:36
w-succ_of ({ <%>E-succ_of (X, A) }, _bool A) = { w-succ_of (X, A ) };
theorem :: FSM_3:37
w-succ_of (the InitS of _bool A, _bool A) = { w-succ_of (the InitS of A, A) }
;
theorem :: FSM_3:38
Lang(A) = Lang(_bool A);
theorem :: FSM_3:39
for A being non empty automaton over Lex(E) \/ {<%>E} ex DA being non
empty deterministic automaton over Lex(E) st Lang(A) = Lang(DA);
theorem :: FSM_3:40
for FA being non empty finite automaton over Lex(E) \/ {<%>E} ex DFA
being non empty deterministic finite automaton over Lex(E) st Lang(FA) = Lang(
DFA);