--- /dev/null
+(*
+ ||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/lists/listb.ma".
+
+(****** DeqSet: a set with a decidbale equality ******)
+
+record FinSet : Type[1] ≝
+{ carr:> DeqSet;
+ enum: list carr;
+ enum_complete: ∀x.memb carr x enum = true;
+ enum_unique: uniqueb carr enum = true
+}.
+
+(*
+definition DeqBool ≝ mk_DeqSet bool beqb beqb_true.
+
+unification hint 0 ≔ ;
+ X ≟ mk_DeqSet bool beqb beqb_true
+(* ---------------------------------------- *) ⊢
+ bool ≡ carr X.
+
+unification hint 0 ≔ b1,b2:bool;
+ X ≟ mk_DeqSet bool beqb beqb_true
+(* ---------------------------------------- *) ⊢
+ beqb b1 b2 ≡ eqb X b1 b2.
+
+example exhint: ∀b:bool. (b == false) = true → b = false.
+#b #H @(\P H).
+qed.
+
+(* pairs *)
+definition eq_pairs ≝
+ λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).
+
+lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
+ eq_pairs A B p1 p2 = true ↔ p1 = p2.
+#A #B * #a1 #b1 * #a2 #b2 %
+ [#H cases (andb_true …H) #eqa #eqb >(\P eqa) >(\P eqb) //
+ |#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
+ ]
+qed.
+
+definition DeqProd ≝ λA,B:DeqSet.
+ mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
+
+unification hint 0 ≔ C1,C2;
+ T1 ≟ carr C1,
+ T2 ≟ carr C2,
+ X ≟ DeqProd C1 C2
+(* ---------------------------------------- *) ⊢
+ T1×T2 ≡ carr X.
+
+unification hint 0 ≔ T1,T2,p1,p2;
+ X ≟ DeqProd T1 T2
+(* ---------------------------------------- *) ⊢
+ eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
+
+example hint2: ∀b1,b2.
+ 〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
+#b1 #b2 #H @(\P H).
+*)
\ No newline at end of file
interpretation "nil" 'nil = (nil ?).
interpretation "cons" 'cons hd tl = (cons ? hd tl).
-definition not_nil: ∀A:Type[0].list A → Prop ≝
+definition is_nil: ∀A:Type[0].list A → Prop ≝
λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ].
theorem nil_cons:
∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
- #A #l #a @nmk #Heq (change with (not_nil ? (a::l))) >Heq //
+ #A #l #a @nmk #Heq (change with (is_nil ? (a::l))) >Heq //
qed.
(*
notation "|M|" non associative with precedence 60 for @{'norm $M}.
interpretation "norm" 'norm l = (length ? l).
+lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l).
+#A #l elim l //
+qed.
+
lemma length_append: ∀A.∀l1,l2:list A.
|l1@l2| = |l1|+|l2|.
#A #l1 elim l1 // normalize /2/
qed.
+lemma length_map: ∀A,B,l.∀f:A→B. length ? (map ?? f l) = length ? l.
+#A #B #l #f elim l // #a #tl #Hind normalize //
+qed.
+
(****************************** nth ********************************)
let rec nth n (A:Type[0]) (l:list A) (d:A) ≝
match n with
include "basics/sets.ma".
include "basics/deqsets.ma".
+(********* isnilb *********)
+let rec isnilb A (l: list A) on l ≝
+match l with
+[ nil ⇒ true
+| cons hd tl ⇒ false
+].
+
(********* search *********)
let rec memb (S:DeqSet) (x:S) (l: list S) on l ≝
--- /dev/null
+(*
+ ||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".
+
+record Vector (A:Type[0]) (n:nat): Type[0] ≝
+{ vec :> list A;
+ len: length ? vec = n
+}.
+
+definition vec_tail ≝ λA.λn.λv:Vector A n.
+mk_Vector A (pred n) (tail A v) ?.
+>length_tail >(len A n v) //
+qed.
+
+definition vec_cons ≝ λA.λa.λn.λv:Vector A n.
+mk_Vector A (S n) (cons A a v) ?.
+normalize >(len A n v) //
+qed.
+
+definition vec_append ≝ λA.λn1,n2.λv1:Vector A n1.λv2: Vector A n2.
+mk_Vector A (n1+n2) (v1@v2).
+
+definition vec_map ≝ λA,B.λf:A→B.λn.λv:Vector A n.
+mk_Vector B n (map ?? f v)
+ (trans_eq … (length_map …) (len A n v)).
+
+let rec pmap A B C (f:A→B→C) l1 l2 on l1 ≝
+ match l1 with
+ [ nil ⇒ nil C
+ | cons a tlA ⇒
+ match l2 with
+ [nil ⇒ nil C
+ |cons b tlB ⇒ (f a b)::pmap A B C f tlA tlB
+ ]
+ ].
+
+lemma length_pmap: ∀A,B,C.∀f:A→B→C.∀l1,l2.
+length C (pmap A B C f l1 l2) =
+ min (length A l1) (length B l2).
+#A #B #C #f #l1 elim l1 // #a #tlA #Hind #l2 cases l2 //
+#b #tlB lapply (Hind tlB) normalize
+cases (true_or_false (leb (length A tlA) (length B tlB))) #H >H
+normalize //
+qed.
+
+definition pmap_vec ≝ λA,B,C.λf:A→B→C.λn.λvA:Vector A n.λvB:Vector B n.
+mk_Vector C n (pmap A B C f vA vB) ?.
+>length_pmap >(len A n vA) >(len B n vB) normalize
+>(le_to_leb_true … (le_n n)) //
+qed.
+
include "re/re.ma".
include "basics/lists/listb.ma".
+(*
+Moves
+
+We now define the move operation, that corresponds to the advancement of the
+state in response to the processing of an input character a. The intuition is
+clear: we have to look at points inside $e$ preceding the given character a,
+let the point traverse the character, and broadcast it. All other points must
+be removed.
+
+We can give a particularly elegant definition in terms of the
+lifted operators of the previous section:
+*)
+
let rec move (S: DeqSet) (x:S) (E: pitem S) on E : pre S ≝
match E with
[ pz ⇒ 〈 `∅, false 〉
[>(\P H) % [* // #bot @False_ind //| #H1 destruct /2/]
|% [@False_ind |#H1 cases (\Pf H) #H2 @H2 destruct //]
]
- |#i1 #i2 #HI1 #HI2 #w >move_cat
- @iff_trans[|@sem_odot] >same_kernel >sem_cat_w
- @iff_trans[||@(iff_or_l … (HI2 w))] @iff_or_r
+ |#i1 #i2 #HI1 #HI2 #w
+ (* lhs = w∈\sem{move S a (i1·i2)} *)
+ >move_cat
+ (* lhs = w∈\sem{move S a i1}⊙\sem{move S a i2} *)
+ @iff_trans[|@sem_odot] >same_kernel
+ (* lhs = w∈\sem{move S a i1}·\sem{|i2|} ∨ a∈\sem{move S a i2} *)
+ (* now we work on the rhs, that is
+ rhs = a::w1∈\sem{i1·i2} *)
+ >sem_cat_w
+ (* rhs = a::w1∈\sem{i1}\sem{|i2|} ∨ a::w∈\sem{i2} *)
+ @iff_trans[||@(iff_or_l … (HI2 w))]
+ (* rhs = a::w1∈\sem{i1}\sem{|i2|} ∨ w∈\sem{move S a i2} *)
+ @iff_or_r
+ check deriv_middot
+ (* we are left to prove that
+ w∈\sem{move S a i1}·\sem{|i2|} ↔ a::w∈\sem{i1}\sem{|i2|}
+ we use deriv_middot on the rhs *)
@iff_trans[||@iff_sym @deriv_middot //]
+ (* w∈\sem{move S a i1}·\sem{|i2|} ↔ w∈(deriv S \sem{i1} a) · \sem{|i2|} *)
@cat_ext_l @HI1
|#i1 #i2 #HI1 #HI2 #w >(sem_plus S i1 i2) >move_plus >sem_plus_w
@iff_trans[|@sem_oplus]
#S #w elim w
[* #i #b >moves_empty cases b % /2/
|#a #w1 #Hind #e >moves_cons
+ check not_epsilon_sem
@iff_trans [||@iff_sym @not_epsilon_sem]
@iff_trans [||@move_ok] @Hind
]
qed.
-(* lemma not_true_to_false: ∀b.b≠true → b =false.
-#b * cases b // #H @False_ind /2/
-qed. *)
-
(************************ pit state ***************************)
definition pit_pre ≝ λS.λi.〈blank S (|i|), false〉.
(* bisimulation *)
definition cofinal ≝ λS.λp:(pre S)×(pre S).
\snd (\fst p) = \snd (\snd p).
-
+
+(* As a corollary of decidable_sem, we have that two expressions
+e1 and e2 are equivalent iff for any word w the states reachable
+through w are cofinal. *)
+
theorem equiv_sem: ∀S:DeqSet.∀e1,e2:pre S.
\sem{e1} =1 \sem{e2} ↔ ∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
#S #e1 #e2 %
|#H #w1 @iff_trans [||@decidable_sem] <H @iff_sym @decidable_sem]
qed.
+(* This does not directly imply decidability: we have no bound over the
+length of w; moreover, so far, we made no assumption over the cardinality
+of S. Instead of requiring S to be finite, we may restrict the analysis
+to characters occurring in the given pres. *)
+
definition occ ≝ λS.λe1,e2:pre S.
unique_append ? (occur S (|\fst e1|)) (occur S (|\fst e2|)).
//
qed.
+(* The following is a stronger version of equiv_sem, relative to characters
+occurring the given regular expressions. *)
+
lemma equiv_sem_occ: ∀S.∀e1,e2:pre S.
(∀w.(sublist S w (occ S e1 e2))→ cofinal ? 〈moves ? w e1,moves ? w e2〉)
→ \sem{e1}=1\sem{e2}.
#S #e1 #e2 #H @(proj2 … (equiv_sem …)) @occ_enough #w @H
qed.
+(*
+We say that a list of pairs of pres is a bisimulation if it is closed
+w.r.t. moves, and all its members are cofinal.
+*)
+
+(* the sons of p w.r.t a list of symbols l are all states reachable from p
+with a move in l *)
+
definition sons ≝ λS:DeqSet.λl:list S.λp:(pre S)×(pre S).
map ?? (λa.〈move S a (\fst (\fst p)),move S a (\fst (\snd p))〉) l.
definition is_bisim ≝ λS:DeqSet.λl:list ?.λalpha:list S.
∀p:(pre S)×(pre S). memb ? p l = true → cofinal ? p ∧ (sublist ? (sons ? alpha p) l).
+(* Using lemma equiv_sem_occ it is easy to prove the following result: *)
+
lemma bisim_to_sem: ∀S:DeqSet.∀l:list ?.∀e1,e2: pre S.
is_bisim S l (occ S e1 e2) → memb ? 〈e1,e2〉 l = true → \sem{e1}=1\sem{e2}.
#S #l #e1 #e2 #Hbisim #Hmemb @equiv_sem_occ
]
qed.
-(* the algorithm *)
+(* This is already an interesting result: checking if l is a bisimulation
+is decidable, hence we could generate l with some untrusted piece of code
+and then run a (boolean version of) is_bisim to check that it is actually
+a bisimulation.
+However, in order to prove that equivalence of regular expressions
+is decidable we must prove that we can always effectively build such a list
+(or find a counterexample).
+The idea is that the list we are interested in is just the set of
+all pair of pres reachable from the initial pair via some
+sequence of moves.
+
+The algorithm for computing reachable nodes in graph is a very
+traditional one. We split nodes in two disjoint lists: a list of
+visited nodes and a frontier, composed by all nodes connected
+to a node in visited but not visited already. At each step we select a node
+a from the frontier, compute its sons, add a to the set of
+visited nodes and the (not already visited) sons to the frontier.
+
+Instead of fist computing reachable nodes and then performing the
+bisimilarity test we can directly integrate it in the algorithm:
+the set of visited nodes is closed by construction w.r.t. reachability,
+so we have just to check cofinality for any node we add to visited.
+
+Here is the extremely simple algorithm: *)
+
let rec bisim S l n (frontier,visited: list ?) on n ≝
match n with
[ O ⇒ 〈false,visited〉 (* assert false *)
]
].
#S #l #n cases n // qed.
-
+
+(* The integer n is an upper bound to the number of recursive call,
+equal to the dimension of the graph. It returns a pair composed
+by a boolean and a the set of visited nodes; the boolean is true
+if and only if all visited nodes are cofinal.
+
+The following results explicitly state the behaviour of bisim is the general
+case and in some relevant instances *)
+
lemma bisim_never: ∀S,l.∀frontier,visited: list ?.
bisim S l O frontier visited = 〈false,visited〉.
#frontier #visited >unfold_bisim //
#b cases b normalize //
qed.
+(* In order to prove termination of bisim we must be able to effectively
+enumerate all possible pres: *)
+
let rec pitem_enum S (i:re S) on i ≝
match i with
[ z ⇒ [pz S]
#S #e1 #e2 @(memb_compose … (λi,b.〈i,b〉))
// qed.
+(* We are ready to prove that bisim is correct; we use the invariant
+that at each call of bisim the two lists visited and frontier only contain
+nodes reachable from \langle e_1,e_2\rangle, hence it is absurd to suppose
+to meet a pair which is not cofinal. *)
+
definition all_reachable ≝ λS.λe1,e2:pre S.λl: list ?.
uniqueb ? l = true ∧
∀p. memb ? p l = true →
definition sub_sons ≝ λS,l,l1,l2.∀x:(pre S) × (pre S).
memb ? x l1 = true → sublist ? (sons ? l x) l2.
+(* For completeness, we use the invariant that all the nodes in visited are cofinal,
+and the sons of visited are either in visited or in the frontier; since
+at the end frontier is empty, visited is hence a bisimulation. *)
+
lemma bisim_complete:
∀S,l,n.∀frontier,visited,visited_res:list ?.
all_true S visited →
definition exp2 ≝ a·(b·a)^*.
definition exp4 ≝ (b·a)^*.
+definition exp5 ≝ (a·(a·(a·b)^*·b)^*·b)^*.
+
+example
+ moves1: \snd (moves DeqNat [0;1;0] (•(blank ? exp2))) = true.
+normalize //
+qed.
+
+example
+ moves2: \snd (moves DeqNat [0;1;0;0;0] (•(blank ? exp2))) = false.
+normalize // qed.
+
+example
+ moves3: \snd (moves DeqNat [0;0;0;1;0;1;1;0;1;1] (•(blank ? exp5))) = true.
+normalize // qed.
+
+example
+ moves4: \snd (moves DeqNat [0;0;0;1;0;1;1;0;1;1;1;0] (•(blank ? exp5))) = false.
+normalize // qed.
+
definition exp6 ≝ a·(a ·a ·b^* + b^* ).
definition exp7 ≝ a · a^* · b^*.
+\v
\ No newline at end of file
include "re/lang.ma".
+(* The type re of regular expressions over an alphabet $S$ is the smallest
+collection of objects generated by the following constructors: *)
+
inductive re (S: DeqSet) : Type[0] ≝
z: re S
| e: re S
notation "`∅" non associative with precedence 90 for @{ 'empty }.
interpretation "empty" 'empty = (z ?).
+(* The language sem{e} associated with the regular expression e is inductively
+defined by the following function: *)
+
let rec in_l (S : DeqSet) (r : re S) on r : word S → Prop ≝
match r with
[ z ⇒ ∅
lemma rsem_star : ∀S.∀r: re S. \sem{r^*} = \sem{r}^*.
// qed.
+(*
+Pointed Regular expressions
+
+We now introduce pointed regular expressions, that are the main tool we shall
+use for the construction of the automaton.
+A pointed regular expression is just a regular expression internally labelled
+with some additional points. Intuitively, points mark the positions inside the
+regular expression which have been reached after reading some prefix of
+the input string, or better the positions where the processing of the remaining
+string has to be started. Each pointed expression for $e$ represents a state of
+the {\em deterministic} automaton associated with $e$; since we obviously have
+only a finite number of possible labellings, the number of states of the automaton
+is finite.
+
+Pointed regular expressions provide the tool for an algebraic revisitation of
+McNaughton and Yamada's algorithm for position automata, making the proof of its
+correctness, that is far from trivial, particularly clear and simple. In particular,
+pointed expressions offer an appealing alternative to Brzozowski's derivatives,
+avoiding their weakest point, namely the fact of being forced to quotient derivatives
+w.r.t. a suitable notion of equivalence in order to get a finite number of states
+(that is not essential for recognizing strings, but is crucial for comparing regular
+expressions).
+
+Our main data structure is the notion of pointed item, that is meant whose purpose
+is to encode a set of positions inside a regular expression.
+The idea of formalizing pointers inside a data type by means of a labelled version
+of the data type itself is probably one of the first, major lessons learned in the
+formalization of the metatheory of programming languages. For our purposes, it is
+enough to mark positions preceding individual characters, so we shall have two kinds
+of characters •a (pp a) and a (ps a) according to the case a is pointed or not. *)
-(* pointed items *)
inductive pitem (S: DeqSet) : Type[0] ≝
pz: pitem S
| pe: pitem S
| po: pitem S → pitem S → pitem S
| pk: pitem S → pitem S.
+(* A pointed regular expression (pre) is just a pointed item with an additional
+boolean, that must be understood as the possibility to have a trailing point at
+the end of the expression. As we shall see, pointed regular expressions can be
+understood as states of a DFA, and the boolean indicates if
+the state is final or not. *)
+
definition pre ≝ λS.pitem S × bool.
interpretation "pitem star" 'star a = (pk ? a).
interpretation "pitem epsilon" 'epsilon = (pe ?).
interpretation "pitem empty" 'empty = (pz ?).
+(* The carrier $|i|$ of an item i is the regular expression obtained from i by
+removing all the points. Similarly, the carrier of a pointed regular expression
+is the carrier of its item. *)
+
let rec forget (S: DeqSet) (l : pitem S) on l: re S ≝
match l with
[ pz ⇒ `∅
lemma erase_star : ∀S.∀i:pitem S.|i^*| = |i|^*.
// qed.
-(* boolean equality *)
+(*
+Comparing items and pres
+
+Items and pres are very concrete datatypes: they can be effectively compared,
+and enumerated. In particular, we can define a boolean equality beqitem and a proof
+beqitem_true that it refects propositional equality, enriching the set (pitem S)
+to a DeqSet. *)
+
let rec beqitem S (i1,i2: pitem S) on i1 ≝
match i1 with
[ pz ⇒ match i2 with [ pz ⇒ true | _ ⇒ false]
definition DeqItem ≝ λS.
mk_DeqSet (pitem S) (beqitem S) (beqitem_true S).
-
+
+(* We also add a couple of unification hints to allow the type inference system
+to look at (pitem S) as the carrier of a DeqSet, and at beqitem as if it was the
+equality function of a DeqSet. *)
+
unification hint 0 ≔ S;
X ≟ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S)
(* ---------------------------------------- *) ⊢
(* ---------------------------------------- *) ⊢
beqitem S i1 i2 ≡ eqb X i1 i2.
-(* semantics *)
+(*
+Semantics of pointed regular expressions
+
+The intuitive semantic of a point is to mark the position where
+we should start reading the regular expression. The language associated
+to a pre is the union of the languages associated with its points. *)
let rec in_pl (S : DeqSet) (r : pitem S) on r : word S → Prop ≝
match r with
interpretation "in_prl mem" 'mem w l = (in_prl ? l w).
interpretation "in_prl" 'in_l E = (in_prl ? E).
+(* The following, trivial lemmas are only meant for rewriting purposes. *)
+
lemma sem_pre_true : ∀S.∀i:pitem S.
\sem{〈i,true〉} = \sem{i} ∪ {ϵ}.
// qed.
\sem{i^*} w = (∃w1,w2.w1 @ w2 = w ∧ \sem{i} w1 ∧ \sem{|i|}^* w2).
// qed.
+(* Below are a few, simple, semantic properties of items. In particular:
+- not_epsilon_item : ∀S:DeqSet.∀i:pitem S. ¬ (\sem{i} ϵ).
+- epsilon_pre : ∀S.∀e:pre S. (\sem{i} ϵ) ↔ (\snd e = true).
+- minus_eps_item: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}.
+- minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
+The first property is proved by a simple induction on $i$; the other
+results are easy corollaries. We need an auxiliary lemma first. *)
+
lemma append_eq_nil : ∀S.∀w1,w2:word S. w1 @ w2 = ϵ → w1 = ϵ.
#S #w1 #w2 cases w1 // #a #tl normalize #H destruct qed.
]
qed.
-(* lemma 12 *)
lemma epsilon_to_true : ∀S.∀e:pre S. ϵ ∈ e → \snd e = true.
#S * #i #b cases b // normalize #H @False_ind /2/
qed.
]
qed.
+(*
+Broadcasting points
+
+Intuitively, a regular expression e must be understood as a pointed expression with a single
+point in front of it. Since however we only allow points before symbols, we must broadcast
+this initial point inside e traversing all nullable subexpressions, that essentially corresponds
+to the ϵ-closure operation on automata. We use the notation •(_) to denote such an operation;
+its definition is the expected one: let us start discussing an example.
+
+Example
+Let us broadcast a point inside (a + ϵ)(b*a + b)b. We start working in parallel on the
+first occurrence of a (where the point stops), and on ϵ that gets traversed. We have hence
+reached the end of a + ϵ and we must pursue broadcasting inside (b*a + b)b. Again, we work in
+parallel on the two additive subterms b^*a and b; the first point is allowed to both enter the
+star, and to traverse it, stopping in front of a; the second point just stops in front of b.
+No point reached that end of b^*a + b hence no further propagation is possible. In conclusion:
+ •((a + ϵ)(b^*a + b)b) = 〈(•a + ϵ)((•b)^*•a + •b)b, false〉
+*)
+
+(* Broadcasting a point inside an item generates a pre, since the point could possibly reach
+the end of the expression.
+Broadcasting inside a i1+i2 amounts to broadcast in parallel inside i1 and i2.
+If we define
+ 〈i1,b1〉 ⊕ 〈i2,b2〉 = 〈i1 + i2, b1 ∨ b2〉
+then, we just have •(i1+i2) = •(i1)⊕ •(i2).
+*)
+
definition lo ≝ λS:DeqSet.λa,b:pre S.〈\fst a + \fst b,\snd a ∨ \snd b〉.
notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
interpretation "oplus" 'oplus a b = (lo ? a b).
lemma lo_def: ∀S.∀i1,i2:pitem S.∀b1,b2. 〈i1,b1〉⊕〈i2,b2〉=〈i1+i2,b1∨b2〉.
// qed.
+(*
+Concatenation is a bit more complex. In order to broadcast a point inside i1 · i2
+we should start broadcasting it inside i1 and then proceed into i2 if and only if a
+point reached the end of i1. This suggests to define •(i1 · i2) as •(i1) ▹ i2, where
+e ▹ i is a general operation of concatenation between a pre and an item, defined by
+cases on the boolean in e:
+
+ 〈i1,true〉 ▹ i2 = i1 ◃ •(i_2)
+ 〈i1,false〉 ▹ i2 = i1 · i2
+
+In turn, ◃ says how to concatenate an item with a pre, that is however extremely simple:
+
+ i1 ◃ 〈i1,b〉 = 〈i_1 · i2, b〉
+
+Let us come to the formalized definitions:
+*)
+
definition pre_concat_r ≝ λS:DeqSet.λi:pitem S.λe:pre S.
match e with [ mk_Prod i1 b ⇒ 〈i · i1, b〉].
notation "i ◃ e" left associative with precedence 60 for @{'lhd $i $e}.
interpretation "pre_concat_r" 'lhd i e = (pre_concat_r ? i e).
+(* The behaviour of ◃ is summarized by the following, easy lemma: *)
+
lemma eq_to_ex_eq: ∀S.∀A,B:word S → Prop.
A = B → A =1 B.
#S #A #B #H >H /2/ qed.
#S #i * #i1 #b1 cases b1 [2: @eq_to_ex_eq //]
>sem_pre_true >sem_cat >sem_pre_true /2/
qed.
-
+
+(* The definition of $•(-)$ (eclose) and ▹ (pre_concat_l) are mutually recursive.
+In this situation, a viable alternative that is usually simpler to reason about,
+is to abstract one of the two functions with respect to the other. In particular
+we abstract pre_concat_l with respect to an input bcast function from items to
+pres. *)
+
definition pre_concat_l ≝ λS:DeqSet.λbcast:∀S:DeqSet.pitem S → pre S.λe1:pre S.λi2:pitem S.
match e1 with
[ mk_Prod i1 b1 ⇒ match b1 with
notation "•" non associative with precedence 60 for @{eclose ?}.
+(* We are ready to give the formal definition of the broadcasting operation. *)
+
let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝
match i with
[ pz ⇒ 〈 `∅, false 〉
notation "• x" non associative with precedence 60 for @{'eclose $x}.
interpretation "eclose" 'eclose x = (eclose ? x).
+(* Here are a few simple properties of ▹ and •(-) *)
+
lemma eclose_plus: ∀S:DeqSet.∀i1,i2:pitem S.
•(i1 + i2) = •i1 ⊕ •i2.
// qed.
•i^* = 〈(\fst(•i))^*,true〉.
// qed.
-definition lift ≝ λS.λf:pitem S →pre S.λe:pre S.
- match e with
- [ mk_Prod i b ⇒ 〈\fst (f i), \snd (f i) ∨ b〉].
-
-definition preclose ≝ λS. lift S (eclose S).
-interpretation "preclose" 'eclose x = (preclose ? x).
-
-(* theorem 16: 2 *)
-lemma sem_oplus: ∀S:DeqSet.∀e1,e2:pre S.
- \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}.
-#S * #i1 #b1 * #i2 #b2 #w %
- [cases b1 cases b2 normalize /2/ * /3/ * /3/
- |cases b1 cases b2 normalize /2/ * /3/ * /3/
- ]
-qed.
-
lemma odot_true :
∀S.∀i1,i2:pitem S.
〈i1,true〉 ▹ i2 = i1 ◃ (•i2).
〈i1,false〉 ▹ i2 = 〈i1 · i2, false〉.
// qed.
-lemma LcatE : ∀S.∀e1,e2:pitem S.
- \sem{e1 · e2} = \sem{e1} · \sem{|e2|} ∪ \sem{e2}.
-// qed.
+(* The definition of •(-) (eclose) can then be lifted from items to pres
+in the obvious way. *)
+
+definition lift ≝ λS.λf:pitem S →pre S.λe:pre S.
+ match e with
+ [ mk_Prod i b ⇒ 〈\fst (f i), \snd (f i) ∨ b〉].
+
+definition preclose ≝ λS. lift S (eclose S).
+interpretation "preclose" 'eclose x = (preclose ? x).
+
+(* Obviously, broadcasting does not change the carrier of the item,
+as it is easily proved by structural induction. *)
lemma erase_bull : ∀S.∀i:pitem S. |\fst (•i)| = |i|.
#S #i elim i //
]
qed.
-(*
-lemma sem_eclose_star: ∀S:DeqSet.∀i:pitem S.
- \sem{〈i^*,true〉} =1 \sem{〈i,false〉}·\sem{|i|}^* ∪ {ϵ}.
-/2/ qed.
-*)
+(* We are now ready to state the main semantic properties of ⊕, ◃ and •(-):
+
+sem_oplus: \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}
+sem_pcl: \sem{e1 ▹ i2} =1 \sem{e1} · \sem{|i2|} ∪ \sem{i2}
+sem_bullet \sem{•i} =1 \sem{i} ∪ \sem{|i|}
+
+The proof of sem_oplus is straightforward. *)
+
+lemma sem_oplus: ∀S:DeqSet.∀e1,e2:pre S.
+ \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}.
+#S * #i1 #b1 * #i2 #b2 #w %
+ [cases b1 cases b2 normalize /2/ * /3/ * /3/
+ |cases b1 cases b2 normalize /2/ * /3/ * /3/
+ ]
+qed.
+
+(* For the others, we proceed as follow: we first prove the following
+auxiliary lemma, that assumes sem_bullet:
+
+sem_pcl_aux:
+ \sem{•i2} =1 \sem{i2} ∪ \sem{|i2|} →
+ \sem{e1 ▹ i2} =1 \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
+
+Then, using the previous result, we prove sem_bullet by induction
+on i. Finally, sem_pcl_aux and sem_bullet give sem_pcl. *)
+
+lemma LcatE : ∀S.∀e1,e2:pitem S.
+ \sem{e1 · e2} = \sem{e1} · \sem{|e2|} ∪ \sem{e2}.
+// qed.
-(* theorem 16: 1 → 3 *)
lemma odot_dot_aux : ∀S.∀e1:pre S.∀i2:pitem S.
\sem{•i2} =1 \sem{i2} ∪ \sem{|i2|} →
\sem{e1 ▹ i2} =1 \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
@eqP_substract_r //
qed.
-(* theorem 16: 1 *)
theorem sem_bull: ∀S:DeqSet. ∀i:pitem S. \sem{•i} =1 \sem{i} ∪ \sem{|i|}.
#S #e elim e
[#w normalize % [/2/ | * //]
|/2/
|#x normalize #w % [ /2/ | * [@False_ind | //]]
|#x normalize #w % [ /2/ | * // ]
- |#i1 #i2 #IH1 #IH2 >eclose_dot
- @eqP_trans [|@odot_dot_aux //] >sem_cat
+ |#i1 #i2 #IH1 #IH2
+ (* lhs = \sem{•(i1 ·i2)} *)
+ >eclose_dot
+ (* lhs =\sem{•(i1) ▹ i2)} *)
+ @eqP_trans [|@odot_dot_aux //]
+ (* lhs = \sem{•(i1)·\sem{|i2|}∪\sem{i2} *)
@eqP_trans
[|@eqP_union_r
[|@eqP_trans [|@(cat_ext_l … IH1)] @distr_cat_r]]
+ (* lhs = \sem{i1}·\sem{|i2|}∪\sem{|i1|}·\sem{|i2|}∪\sem{i2} *)
@eqP_trans [|@union_assoc]
+ (* lhs = \sem{i1}·\sem{|i2|}∪(\sem{|i1|}·\sem{|i2|}∪\sem{i2}) *)
+ (* Now we work on the rhs that is
+ rhs = \sem{i1·i2} ∪ \sem{|i1·i2|} *)
+ >sem_cat
+ (* rhs = \sem{i1}·\sem{|i2|} ∪ \sem{i2} ∪ \sem{|i1·i2|} *)
@eqP_trans [||@eqP_sym @union_assoc]
- @eqP_union_l //
+ (* rhs = \sem{i1}·\sem{|i2|}∪ (\sem{i2} ∪ \sem{|i1·i2|}) *)
+ @eqP_union_l @union_comm
|#i1 #i2 #IH1 #IH2 >eclose_plus
@eqP_trans [|@sem_oplus] >sem_plus >erase_plus
@eqP_trans [|@(eqP_union_l … IH2)]
]
qed.
-(* blank item *)
+(*
+Blank item
+
+As a corollary of theorem sem_bullet, given a regular expression e, we can easily
+find an item with the same semantics of $e$: it is enough to get an item (blank e)
+having e as carrier and no point, and then broadcast a point in it. The semantics of
+(blank e) is obviously the empty language: from the point of view of the automaton,
+it corresponds with the pit state. *)
+
let rec blank (S: DeqSet) (i: re S) on i :pitem S ≝
match i with
[ z ⇒ `∅
@eqP_trans [|@union_comm] @union_empty_r.
qed.
-(* lefted operations *)
+(*
+Lifted Operators
+
+Plus and bullet have been already lifted from items to pres. We can now
+do a similar job for concatenation ⊙ and Kleene's star ⊛. *)
+
definition lifted_cat ≝ λS:DeqSet.λe:pre S.
lift S (pre_concat_l S eclose e).
#S * #i1 * * #i2 #b2 // >odot_true_b //
qed.
+(* Let us come to the star operation: *)
+
definition lk ≝ λS:DeqSet.λe:pre S.
match e with
[ mk_Prod i1 b1 ⇒
cases (e1 ▹ i) #i1 #b1 cases b1 #H @H
qed.
+(* We conclude this section with the proof of the main semantic properties
+of ⊙ and ⊛. *)
+
lemma sem_odot:
∀S.∀e1,e2: pre S. \sem{e1 ⊙ e2} =1 \sem{e1}· \sem{|\fst e2|} ∪ \sem{e2}.
#S #e1 * #i2 *
|>sem_pre_false >eq_odot_false @odot_dot_aux //
]
qed.
-
-(* theorem 16: 4 *)
+
theorem sem_ostar: ∀S.∀e:pre S.
\sem{e^⊛} =1 \sem{e} · \sem{|\fst e|}^*.
#S * #i #b cases b
- [>sem_pre_true >sem_pre_true >sem_star >erase_bull
+ [(* lhs = \sem{〈i,true〉^⊛} *)
+ >sem_pre_true (* >sem_pre_true *)
+ (* lhs = \sem{(\fst (•i))^*}∪{ϵ} *)
+ >sem_star >erase_bull
+ (* lhs = \sem{\fst (•i)}·(\sem{|i|)^*∪{ϵ} *)
@eqP_trans [|@eqP_union_r[|@cat_ext_l [|@minus_eps_pre_aux //]]]
+ (* lhs = (\sem{i}∪(\sem{|i|}-{ϵ})·(\sem{|i|)^*∪{ϵ} *)
@eqP_trans [|@eqP_union_r [|@distr_cat_r]]
+ (* lhs = (\sem{i}·(\sem{|i|)^*∪(\sem{|i|}-{ϵ})·(\sem{|i|)^*∪{ϵ} *)
+ @eqP_trans [|@union_assoc]
+ (* lhs = (\sem{i}·(\sem{|i|)^*∪((\sem{|i|}-{ϵ})·(\sem{|i|)^*∪{ϵ}) *)
+ @eqP_trans [|@eqP_union_l[|@eqP_sym @star_fix_eps]]
+ (* lhs = (\sem{i}·(\sem{|i|)^*∪(\sem{|i|)^* *)
+ (* now we work on the right hand side, that is
+ rhs = \sem{〈i,true〉}·(\sem{|i|}^* *)
@eqP_trans [||@eqP_sym @distr_cat_r]
- @eqP_trans [|@union_assoc] @eqP_union_l
- @eqP_trans [||@eqP_sym @epsilon_cat_l] @eqP_sym @star_fix_eps
+ (* rhs = (\sem{i}·(\sem{|i|)^*∪{ϵ}·(\sem{|i|)^* *)
+ @eqP_union_l @eqP_sym @epsilon_cat_l
|>sem_pre_false >sem_pre_false >sem_star /2/
]
qed.
--- /dev/null
+(*
+ ||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/star.ma".
+include "turing/turing.ma".
+
+(*
+record Vector (A:Type[0]) (n:nat): Type[0] ≝
+{ vec :> list A;
+ len: length ? vec = n
+}.
+
+record tape (sig:FinSet): Type[0] ≝
+{ left : list sig;
+ right: list sig
+}.
+
+inductive move : Type[0] ≝
+| L : move
+| R : move
+| N : move
+.
+*)
+
+record NTM (sig:FinSet): Type[1] ≝
+{ states : FinSet;
+ tapes_no: nat; (* additional working tapes *)
+ trans : list ((states × (Vector (option sig) (S tapes_no))) ×
+ (states × (Vector (sig × move) (S tapes_no))));
+ output: list sig;
+ start: states;
+ halt : states → bool;
+ accept : states → bool
+}.
+
+record config (sig:FinSet) (M:NTM sig): Type[0] ≝
+{ state : states sig M;
+ tapes : Vector (tape sig) (S (tapes_no sig M))
+}.
+
+(*
+definition option_hd ≝ λA.λl:list A.
+ match l with
+ [nil ⇒ None ?
+ |cons a _ ⇒ Some ? a
+ ].
+
+lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l).
+#A #l elim l //
+qed.
+
+definition vec_tail ≝ λA.λn.λv:Vector A n.
+mk_Vector A (pred n) (tail A v) ?.
+>length_tail >(len A n v) //
+qed.
+
+definition vec_cons ≝ λA.λa.λn.λv:Vector A n.
+mk_Vector A (S n) (cons A a v) ?.
+normalize >(len A n v) //
+qed.
+
+lemma length_map: ∀A,B,l.∀f:A→B. length ? (map ?? f l) = length ? l.
+#A #B #l #f elim l // #a #tl #Hind normalize //
+qed.
+
+definition vec_map ≝ λA,B.λf:A→B.λn.λv:Vector A n.
+mk_Vector B n (map ?? f v)
+ (trans_eq … (length_map …) (len A n v)).
+
+definition tape_move ≝ λsig.λt: tape sig.λm:sig × move.
+ match \snd m with
+ [ R ⇒ mk_tape sig ((\fst m)::(left ? t)) (tail ? (right ? t))
+ | L ⇒ mk_tape sig (tail ? (left ? t)) ((\fst m)::(right ? t))
+ ].
+*)
+
+(*
+definition hds ≝ λsig.λM.λc:config sig M. vec_map ?? (option_hd ?) (tapes_no sig M) (\snd c).
+
+definition tls ≝ λsig.λM.λc:config sig M.vec_map ?? (tail ?) (tapes_no sig M) (\snd c).
+*)
+(*
+let rec compose A B C (f:A→B→C) l1 l2 on l1 ≝
+ match l1 with
+ [ nil ⇒ nil C
+ | cons a tlA ⇒
+ match l2 with
+ [nil ⇒ nil C
+ |cons b tlB ⇒ (f a b)::compose A B C f tlA tlB
+ ]
+ ].
+
+lemma length_compose: ∀A,B,C.∀f:A→B→C.∀l1,l2.
+length C (compose A B C f l1 l2) =
+ min (length A l1) (length B l2).
+#A #B #C #f #l1 elim l1 // #a #tlA #Hind #l2 cases l2 //
+#b #tlB lapply (Hind tlB) normalize
+cases (true_or_false (leb (length A tlA) (length B tlB))) #H >H
+normalize //
+qed.
+
+definition compose_vec ≝ λA,B,C.λf:A→B→C.λn.λvA:Vector A n.λvB:Vector B n.
+mk_Vector C n (compose A B C f vA vB) ?.
+>length_compose >(len A n vA) >(len B n vB) normalize
+>(le_to_leb_true … (le_n n)) //
+qed.
+*)
+
+definition current_chars ≝ λsig.λM:NTM sig.λc:config sig M.
+ vec_map ?? (λt.option_hd ? (right ? t)) (S (tapes_no sig M)) (tapes ?? c).
+
+let rec mem A (a:A) (l:list A) on l ≝
+ match l with
+ [ nil ⇒ False
+ | cons hd tl ⇒ a=hd ∨ mem A a tl
+ ].
+
+definition reach ≝ λsig.λM:NTM sig.λc,c1:config sig M.
+ ∃q,l,q1,mvs.
+ state ?? c = q ∧
+ halt ?? q = false ∧
+ current_chars ?? c = l ∧
+ mem ? 〈〈q,l〉,〈q1,mvs〉〉 (trans ? M) ∧
+ state ?? c1 = q1 ∧
+ tapes ?? c1 = (compose_vec ??? (tape_move sig) ? (tapes ?? c) mvs).
+
+(*
+definition empty_tapes ≝ λsig.λn.
+mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?.
+elim n // normalize //
+qed.
+*)
+
+definition init ≝ λsig.λM:NTM sig.λi:(list sig).
+ mk_config ??
+ (start sig M)
+ (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M))).
+
+definition accepted ≝ λsig.λM:NTM sig.λw:(list sig).
+∃c. star ? (reach sig M) (init sig M w) c ∧
+ accept ?? (state ?? c) = true.
+
--- /dev/null
+(*
+ ||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/turing.ma".
+
+(* Oracle machines *)
+
+record TM (sig:FinSet): Type[1] ≝
+{ states : FinSet;
+ tapes_no: nat; (* additional working tapes *)
+ trans : states × (Vector (option sig) (S tapes_no)) →
+ states × (Vector (sig × move) (S tapes_no)) × (option sig) ;
+ output: list sig;
+ start: states;
+ halt : states → bool
+}.
+
+inductive oracle_states :Type[0] ≝
+ | query : oracle_states
+ | yes : oracle_states
+ | no : oracle_states.
+
+record config (sig:FinSet) (M:TM sig): Type[0] ≝
+{ state : states sig M;
+ query : list sig;
+ tapes : Vector (tape sig) (S (tapes_no sig M));
+ out : list sig
+}.
+
+definition option_hd ≝ λA.λl:list A.
+ match l with
+ [nil ⇒ None ?
+ |cons a _ ⇒ Some ? a
+ ].
+
+definition tape_move ≝ λsig.λt: tape sig.λm:sig × move.
+ match \snd m with
+ [ R ⇒ mk_tape sig ((\fst m)::(left ? t)) (tail ? (right ? t))
+ | L ⇒ mk_tape sig (tail ? (left ? t)) ((\fst m)::(right ? t))
+ | N ⇒ mk_tape sig (left ? t) ((\fst m)::(tail ? (right ? t)))
+ ].
+
+definition current_chars ≝ λsig.λM:TM sig.λc:config sig M.
+ vec_map ?? (λt.option_hd ? (right ? t)) (S (tapes_no sig M)) (tapes ?? c).
+
+definition opt_cons ≝ λA.λa:option A.λl:list A.
+ match a with
+ [ None ⇒ l
+ | Some a ⇒ a::l
+ ].
+
+definition step ≝ λsig.λM:TM sig.λc:config sig M.
+ let 〈news,mvs,outchar〉 ≝ trans sig M 〈state ?? c,current_chars ?? c〉 in
+ mk_config ??
+ news
+ (pmap_vec ??? (tape_move sig) ? (tapes ?? c) mvs)
+ (opt_cons ? outchar (out ?? c)).
+
+definition empty_tapes ≝ λsig.λn.
+mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?.
+elim n // normalize //
+qed.
+
+definition init ≝ λsig.λM:TM sig.λi:(list sig).
+ mk_config ??
+ (start sig M)
+ (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M)))
+ [ ].
+
+definition stop ≝ λsig.λM:TM sig.λc:config sig M.
+ halt sig M (state sig M c).
+
+let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
+ match n with
+ [ O ⇒ None ?
+ | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
+ ].
+
+(* Compute ? M f states that f is computed by M *)
+definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
+∀l.∃i.∃c.
+ loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
+ out ?? c = f l.
+
+(* for decision problems, we accept a string if on termination
+output is not empty *)
+
+definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool.
+∀l.∃i.∃c.
+ loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
+ (isnilb ? (out ?? c) = false).
--- /dev/null
+(*
+ ||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/vectors.ma".
+
+record tape (sig:FinSet): Type[0] ≝
+{ left : list sig;
+ right: list sig
+}.
+
+inductive move : Type[0] ≝
+| L : move
+| R : move
+| N : move.
+
+(* We do not distinuish an input tape *)
+
+record TM (sig:FinSet): Type[1] ≝
+{ states : FinSet;
+ tapes_no: nat; (* additional working tapes *)
+ trans : states × (Vector (option sig) (S tapes_no)) →
+ states × (Vector (sig × move) (S tapes_no)) × (option sig) ;
+ output: list sig;
+ start: states;
+ halt : states → bool
+}.
+
+record config (sig:FinSet) (M:TM sig): Type[0] ≝
+{ state : states sig M;
+ tapes : Vector (tape sig) (S (tapes_no sig M));
+ out : list sig
+}.
+
+definition option_hd ≝ λA.λl:list A.
+ match l with
+ [nil ⇒ None ?
+ |cons a _ ⇒ Some ? a
+ ].
+
+definition tape_move ≝ λsig.λt: tape sig.λm:sig × move.
+ match \snd m with
+ [ R ⇒ mk_tape sig ((\fst m)::(left ? t)) (tail ? (right ? t))
+ | L ⇒ mk_tape sig (tail ? (left ? t)) ((\fst m)::(right ? t))
+ | N ⇒ mk_tape sig (left ? t) ((\fst m)::(tail ? (right ? t)))
+ ].
+
+definition current_chars ≝ λsig.λM:TM sig.λc:config sig M.
+ vec_map ?? (λt.option_hd ? (right ? t)) (S (tapes_no sig M)) (tapes ?? c).
+
+definition opt_cons ≝ λA.λa:option A.λl:list A.
+ match a with
+ [ None ⇒ l
+ | Some a ⇒ a::l
+ ].
+
+definition step ≝ λsig.λM:TM sig.λc:config sig M.
+ let 〈news,mvs,outchar〉 ≝ trans sig M 〈state ?? c,current_chars ?? c〉 in
+ mk_config ??
+ news
+ (pmap_vec ??? (tape_move sig) ? (tapes ?? c) mvs)
+ (opt_cons ? outchar (out ?? c)).
+
+definition empty_tapes ≝ λsig.λn.
+mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?.
+elim n // normalize //
+qed.
+
+definition init ≝ λsig.λM:TM sig.λi:(list sig).
+ mk_config ??
+ (start sig M)
+ (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M)))
+ [ ].
+
+definition stop ≝ λsig.λM:TM sig.λc:config sig M.
+ halt sig M (state sig M c).
+
+let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
+ match n with
+ [ O ⇒ None ?
+ | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
+ ].
+
+(* Compute ? M f states that f is computed by M *)
+definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
+∀l.∃i.∃c.
+ loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
+ out ?? c = f l.
+
+(* for decision problems, we accept a string if on termination
+output is not empty *)
+
+definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool.
+∀l.∃i.∃c.
+ loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
+ (isnilb ? (out ?? c) = false).
--- /dev/null
+(*
+ ||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".
+
+record Vector (A:Type[0]) (n:nat): Type[0] ≝
+{ vec :> list A;
+ len: length ? vec = n
+}.
+
+record TM (sig:FinSet): Type[1] ≝
+{ states : FinSet;
+ tapes_no: nat;
+ trans : states × (option sig) × (Vector (option sig) tapes_no) →
+ states × bool × (Vector (list sig) tapes_no);
+ start: states;
+ halt : states
+}.
+
+definition config ≝ λsig.λM:TM sig.
+ states sig M × (list sig) × (Vector (list sig) (tapes_no sig M)).
+
+definition option_hd ≝ λA.λl:list A.
+ match l with
+ [nil ⇒ None ?
+ |cons a _ ⇒ Some ? a
+ ].
+
+lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l).
+#A #l elim l //
+qed.
+
+definition vec_tail ≝ λA.λn.λv:Vector A n.
+mk_Vector A (pred n) (tail A v) ?.
+>length_tail >(len A n v) //
+qed.
+
+definition vec_cons ≝ λA.λa.λn.λv:Vector A n.
+mk_Vector A (S n) (cons A a v) ?.
+normalize >(len A n v) //
+qed.
+
+lemma length_map: ∀A,B,l.∀f:A→B. length ? (map ?? f l) = length ? l.
+#A #B #l #f elim l // #a #tl #Hind normalize //
+qed.
+
+definition vec_map ≝ λA,B.λf:A→B.λn.λv:Vector A n.
+mk_Vector B n (map ?? f v)
+ (trans_eq … (length_map …) (len A n v)).
+
+definition hds ≝ λsig.λM.λc:config sig M. vec_map ?? (option_hd ?) (tapes_no sig M) (\snd c).
+
+definition tls ≝ λsig.λM.λc:config sig M.vec_map ?? (tail ?) (tapes_no sig M) (\snd c).
+
+let rec compose A B C (f:A→B→C) l1 l2 on l1 ≝
+ match l1 with
+ [ nil ⇒ nil C
+ | cons a tlA ⇒
+ match l2 with
+ [nil ⇒ nil C
+ |cons b tlB ⇒ (f a b)::compose A B C f tlA tlB
+ ]
+ ].
+
+lemma length_compose: ∀A,B,C.∀f:A→B→C.∀l1,l2.
+length C (compose A B C f l1 l2) =
+ min (length A l1) (length B l2).
+#A #B #C #f #l1 elim l1 // #a #tlA #Hind #l2 cases l2 //
+#b #tlB lapply (Hind tlB) normalize
+cases (true_or_false (leb (length A tlA) (length B tlB))) #H >H
+normalize //
+qed.
+
+definition compose_vec ≝ λA,B,C.λf:A→B→C.λn.λvA:Vector A n.λvB:Vector B n.
+mk_Vector C n (compose A B C f vA vB) ?.
+>length_compose >(len A n vA) >(len B n vB) normalize
+>(le_to_leb_true … (le_n n)) //
+qed.
+
+definition step ≝ λsig.λM:TM sig.λc:config sig M.
+ match (trans sig M 〈〈\fst (\fst c),option_hd ? (\snd (\fst c))〉,hds sig M c〉) with
+ [mk_Prod p l ⇒
+ let work_tapes ≝ compose_vec ??? (append ?) (tapes_no sig M) l (tls sig M c) in
+ match p with
+ [mk_Prod s b ⇒
+ let old_input ≝ \snd (\fst c) in
+ let input ≝ if b then tail ? old_input else old_input in
+ 〈〈s,input〉,work_tapes〉]].
+
+definition empty_tapes ≝ λsig.λM:TM sig.
+mk_Vector ? (tapes_no sig M) (make_list (list sig) [ ] (tapes_no sig M)) ?.
+elim (tapes_no sig M) // normalize //
+qed.
+
+definition init ≝ λsig.λM:TM sig.λi:(list sig).
+ 〈〈start sig M,i〉,empty_tapes sig M〉.
+
+definition stop ≝ λsig.λM:TM sig.λc:config sig M.
+ eqb (states sig M) (\fst(\fst c)) (halt sig M).
+
+let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
+ match n with
+ [ O ⇒ None ?
+ | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
+ ].
+
+definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
+∀l.∃i.∃c.((loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c) ∧
+ (hd ? (\snd c) [ ] = f l)).
+
+(* An extended machine *)
\ No newline at end of file
projects / helm.git / commitdiff