From 1f740f74d94187a2376228a86faf79ea949c0dff Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 17 Jan 2013 12:59:25 +0000 Subject: [PATCH] normal and tuples --- .../lib/turing/multi_universal/alphabet.ma | 34 +-- .../lib/turing/multi_universal/normalTM.ma | 231 ++++++++++++++++++ .../lib/turing/multi_universal/tuples.ma | 115 +++++++++ 3 files changed, 365 insertions(+), 15 deletions(-) create mode 100644 matita/matita/lib/turing/multi_universal/normalTM.ma create mode 100644 matita/matita/lib/turing/multi_universal/tuples.ma diff --git a/matita/matita/lib/turing/multi_universal/alphabet.ma b/matita/matita/lib/turing/multi_universal/alphabet.ma index 8a6859669..fdd433f07 100644 --- a/matita/matita/lib/turing/multi_universal/alphabet.ma +++ b/matita/matita/lib/turing/multi_universal/alphabet.ma @@ -1,18 +1,16 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| + \ / This file is distributed under the terms of the + \ / GNU General Public License Version 2 + V_____________________________________________________________*) include "basics/finset.ma". +include "basics/lists/list.ma". inductive unialpha : Type[0] ≝ | bit : bool → unialpha @@ -46,5 +44,11 @@ definition FSUnialpha ≝ (*************************** testing characters *******************************) definition is_bit ≝ λc.match c with [ bit _ ⇒ true | _ ⇒ false ]. -definition is_bar ≝ λc.match c with [ bar ⇒ true | _ ⇒ false ]. -definition is_null ≝ λc.match c with [ null ⇒ true | _ ⇒ false ]. \ No newline at end of file +definition is_bar ≝ λc:DeqUnialpha. c == bar. +definition is_null ≝ λc:DeqUnialpha. c == null. + +definition only_bits ≝ λl. + ∀c.mem ? c l → is_bit c = true. + +definition no_bars ≝ λl. + ∀c.mem ? c l → is_bar c = false. diff --git a/matita/matita/lib/turing/multi_universal/normalTM.ma b/matita/matita/lib/turing/multi_universal/normalTM.ma new file mode 100644 index 000000000..13ef8a66c --- /dev/null +++ b/matita/matita/lib/turing/multi_universal/normalTM.ma @@ -0,0 +1,231 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| + \ / This file is distributed under the terms of the + \ / GNU General Public License Version 2 + V_____________________________________________________________*) + +include "turing/multi_universal/alphabet.ma". +include "turing/mono.ma". + +(************************* turning DeqMove into a DeqSet **********************) +definition move_eq ≝ λm1,m2:move. + match m1 with + [R ⇒ match m2 with [R ⇒ true | _ ⇒ false] + |L ⇒ match m2 with [L ⇒ true | _ ⇒ false] + |N ⇒ match m2 with [N ⇒ true | _ ⇒ false]]. + +lemma move_eq_true:∀m1,m2. + move_eq m1 m2 = true ↔ m1 = m2. +* + [* normalize [% #_ % |2,3: % #H destruct ] + |* normalize [1,3: % #H destruct |% #_ % ] + |* normalize [1,2: % #H destruct |% #_ % ] +qed. + +definition DeqMove ≝ mk_DeqSet move move_eq move_eq_true. + +unification hint 0 ≔ ; + X ≟ DeqMove +(* ---------------------------------------- *) ⊢ + move ≡ carr X. + +unification hint 0 ≔ m1,m2; + X ≟ DeqMove +(* ---------------------------------------- *) ⊢ + move_eq m1 m2 ≡ eqb X m1 m2. + + +(************************ turning DeqMove into a FinSet ***********************) +definition move_enum ≝ [L;R;N]. + +lemma move_enum_unique: uniqueb ? [L;R;N] = true. +// qed. + +lemma move_enum_complete: ∀x:move. memb ? x [L;R;N] = true. +* // qed. + +definition FinMove ≝ + mk_FinSet DeqMove [L;R;N] move_enum_unique move_enum_complete. + +unification hint 0 ≔ ; + X ≟ FinMove +(* ---------------------------------------- *) ⊢ + move ≡ FinSetcarr X. + +(*************************** normal Turing Machines ***************************) + +(* A normal turing machine is just an ordinary machine where: + 1. the tape alphabet is bool + 2. the finite state are supposed to be an initial segment of the natural + numbers. + Formally, it is specified by a record with the number n of states, a proof + that n is positive, the transition function and the halting function. +*) + +definition trans_source ≝ λn. + FinProd (initN n) (FinOption FinBool). + +definition trans_target ≝ λn. + FinProd (FinProd (initN n) (FinOption FinBool)) FinMove. + +record normalTM : Type[0] ≝ +{ no_states : nat; + pos_no_states : (0 < no_states); + ntrans : trans_source no_states → trans_target no_states; + nhalt : initN no_states → bool +}. + +(* A normal machine is just a special case of Turing Machine. *) + +definition normalTM_to_TM ≝ λM:normalTM. + mk_TM FinBool (initN (no_states M)) + (ntrans M) (mk_Sig ?? 0 (pos_no_states M)) (nhalt M). + +coercion normalTM_to_TM. + +definition nconfig ≝ λn. config FinBool (initN n). + +(******************************** tuples **************************************) + +(* By general results on FinSets we know that every function f between two +finite sets A and B can be described by means of a finite graph of pairs +〈a,f a〉. Hence, the transition function of a normal turing machine can be +described by a finite set of tuples 〈i,c〉,〈j,action〉〉 of the following type: + (Nat_to n × (option FinBool)) × (Nat_to n × (option FinBool) × move). +Unfortunately this description is not suitable for a Universal Machine, since +such a machine must work with a fixed alphabet, while the size on n is unknown. +Hence, we must pass from natural numbers to a representation for them on a +finitary, e.g. binary, alphabet. In general, we shall associate +to a pair 〈〈i,x〉,〈j,y,m〉〉 a tuple with the following syntactical structure + | w_i x w_j y m +where +1. "|" is a special character used to separate tuples +2. w_i and w_j are list of booleans representing the states $i$ and $j$; +3. x and y are encoding +4. finally, m ... +*) + +definition mk_tuple ≝ λqin,cin,qout,cout,mv. + bar::qin@cin::qout@[cout;mv]. + +definition tuple_TM : nat → list unialpha → Prop ≝ + λn,t.∃qin,cin,qout,cout,mv. + only_bits qin ∧ only_bits qout ∧ cin ≠ bar ∧ cout ≠ bar ∧ mv ≠ bar ∧ + |qin| = n ∧ |qout| = n ∧ + t = mk_tuple qin cin qout cout mv. + +(***************************** state encoding *********************************) +(* p < n is represented with a list of bits of lenght n with the p-th bit from +left set to 1. An additional intial bit is set to 1 if the state is final and +to 0 otherwise. *) + +let rec to_bitlist n p: list bool ≝ + match n with [ O ⇒ [ ] | S q ⇒ (eqb p q)::to_bitlist q p]. + +let rec from_bitlist l ≝ + match l with + [ nil ⇒ 0 (* assert false *) + | cons b tl ⇒ if b then |tl| else from_bitlist tl]. + +lemma bitlist_length: ∀n,p.|to_bitlist n p| = n. +#n elim n normalize // +qed. + +lemma bitlist_inv1: ∀n,p.p(not_eq_to_eqb_false … Hpn) normalize @Hind @ltpn + |#Heq >(eq_to_eqb_true … Heq) normalize eqtl @le_n + ] +qed. + +definition nat_of: ∀n. Nat_to n → nat. +#n normalize * #p #_ @p +qed. + +definition bits_of_state ≝ λn.λh:Nat_to n → bool.λs:Nat_to n. + map ? unialpha (λx.bit x) (h s::(to_bitlist n (nat_of n s))). + +lemma only_bits_bits_of_state : ∀n,h,p. only_bits (bits_of_state n h p). +#n #h #p #x whd in match (bits_of_state n h p); +#H cases H -H + [#H >H % + |elim (to_bitlist n (nat_of n p)) + [@False_ind |#b #l #Hind #H cases H -H #H [>H % |@Hind @H ]] + ] +qed. + +(******************************** action encoding *****************************) + +definition low_char ≝ λc. + match c with + [ None ⇒ null + | Some b ⇒ bit b + ]. + +definition low_mv ≝ λm. + match m with + [ R ⇒ bit true + | L ⇒ bit false + | N ⇒ null + ]. + +(******************************** tuple encoding ******************************) +definition tuple_type ≝ λn. + (Nat_to n × (option FinBool)) × (Nat_to n × (option FinBool) × move). + +definition tuple_encoding ≝ λn.λh:Nat_to n→bool. + λp:tuple_type n. + let 〈inp,outp〉 ≝ p in + let 〈q,a〉 ≝ inp in + let 〈qn,an,m〉 ≝ outp in + let qin ≝ bits_of_state n h q in + let qout ≝ bits_of_state n h qn in + let cin ≝ low_char a in + let cout ≝ low_char an in + let mv ≝ low_mv m in + mk_tuple qin cin qout cout mv. + +lemma is_tuple: ∀n,h,p. tuple_TM (S n) (tuple_encoding n h p). +#n #h * * #q #a * * #qn #an #m +%{(bits_of_state n h q)} %{(low_char a)} +%{(bits_of_state n h qn)} %{(low_char an)} %{(low_mv m)} +% // % + [%[%[%[%[% /2/ |% cases a normalize [|#b] #H destruct] + |% cases an normalize [|#b] #H destruct] + |% cases m normalize #H destruct] + |>length_map normalize @eq_f //] + |>length_map normalize @eq_f //] +qed. + +definition tuple_length ≝ λn.2*n+4. + +lemma length_of_tuple: ∀n,t. tuple_TM n t → + |t| = tuple_length n. +#n #t * #qin * #cin * #qout * #cout * #mv *** #_ #Hqin #Hqout #eqt +>eqt normalize >length_append >Hqin -Hqin normalize >length_append +normalize >Hqout // +qed. + +definition tuples_list ≝ λn.λh.map … (λp.tuple_encoding n h p). + + + + diff --git a/matita/matita/lib/turing/multi_universal/tuples.ma b/matita/matita/lib/turing/multi_universal/tuples.ma new file mode 100644 index 000000000..76e56068d --- /dev/null +++ b/matita/matita/lib/turing/multi_universal/tuples.ma @@ -0,0 +1,115 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| + \ / This file is distributed under the terms of the + \ / GNU General Public License Version 2 + V_____________________________________________________________*) + + +(****************************** table of tuples *******************************) +include "turing/multi_universal/normalTM.ma". + +(* a well formed table is a list of tuples *) + +definition table_TM ≝ λn,l,h.flatten ? (tuples_list n h l). + +lemma table_TM_cons: ∀n,h,t,o. + table_TM n (t::o) h = (tuple_encoding n h t)@(table_TM n o h). +// qed. + +(************************** matching in a table *******************************) +lemma list_to_table: ∀n,l,h,tup. mem ? tup (tuples_list n h l) → + ∃ll,lr.table_TM n l h = ll@tup@lr. +#n #l #h #tup elim l + [@False_ind + |#hd #tl #Hind * + [#Htup %{[]} %{(table_TM n tl h)} >Htup % + |#H cases (Hind H) #ll * #lr #H1 + %{((tuple_encoding n h hd)@ll)} %{lr} + >associative_append

Heq1 >(cons_injective_l ????? Heq) // + |%2 % // >Heq1 >(cons_injective_l ????? Heq) // + ] + |@(cons_injective_r ????? Heq) + ] + ] + ] +qed. + +lemma table_to_list: ∀n,l,h,c. is_config n c → + (∃ll,lr.table_TM n l h = ll@c@lr) → + ∃out,t. tuple_encoding n h t = (c@out) ∧ mem ? t l. +#n #l #h #c * #qin * #cin * * * #H1 #H2 #H3 #H4 + * #ll * #lr lapply ll -ll elim l + [>H4 #ll cases ll normalize [|#hd #tl ] #Habs destruct + |#t1 #othert #Hind #ll >table_TM_cons #Htuple + cut (S n < |ll@c@lr|) + [length_append >(length_of_tuple … (is_tuple … )) + /2 by transitive_lt, le_n/] #Hsplit lapply Htuple -Htuple + cases (is_tuple … n h t1) #q1 * #c1 * #q2 * #c2 * #m + * * * * * * * #Hq1 #Hq2 #Hc1 #Hc2 #Hm #Hlen1 #Hlen2 + whd in ⊢ (???%→?); #Ht1 + (* if ll is empty we match the first tuple t1, otherwise + we match inside othert *) + cases ll + [>H4 >Ht1 normalize in ⊢ (???%→?); + >associative_append whd in ⊢ (??%?→?); #Heq destruct (Heq) -Heq + >associative_append in e0; #e0 + lapply (append_l1_injective … e0) [>H3 @Hlen1] #Heq1 + lapply (append_l2_injective … e0) [>H3 @Hlen1] + normalize in ⊢ (???%→?); whd in ⊢ (??%?→?); #Htemp + lapply (cons_injective_l ????? Htemp) #Hc1 + lapply (cons_injective_r ????? Htemp) -Htemp #Heq2 + %{(q2@[c2;m])} %{t1} % + [>Ht1 >Heq1 >Hc1 @eq_f >associative_append % + |%1 % + ] + |(* ll not nil *) + #b #tl >Ht1 normalize in ⊢ (???%→?); + whd in ⊢ (??%?→?); #Heq destruct (Heq) + cases (compare_append … e0) #l * + [* cases l + [#_ #Htab cases (Hind [ ] (sym_eq … Htab)) #out * #t * #Ht #Hmemt + %{out} %{t} % // %2 // + |(* this case is absurd *) + #al #tll #Heq1 >H4 #Heq2 @False_ind + lapply (cons_injective_l ? bar … Heq2) #Hbar Heq1 @mem_append_l2 %1 // + |% #Hmembar cases (mem_append ???? Hmembar) -Hmembar + [#Hmembar lapply(Hq1 bar Hmembar) normalize #Habs destruct (Habs) + |* [#Habs @absurd //] + #Hmembar cases (mem_append ???? Hmembar) -Hmembar + [#Hmembar lapply(Hq2 bar Hmembar) normalize #Habs destruct (Habs) + |* [#Habs @absurd //] #Hmembar @(absurd ?? Hm) @sym_eq @mem_single // + ] + ] + ] + ] + |* #Htl #Htab cases (Hind … Htab) #out * #t * #Ht #Hmemt + %{out} %{t} % // %2 // + ] + ] + ] +qed. + -- 2.39.2