chapter 9

diff --git a/weblib/tutorial/acUbc.gif b/weblib/tutorial/acUbc.gif
index 5812fc8f462a99d6f138ae01d7758fca10b2bd8f..9222a3418585ed44c08c9d813cd7f6b8603d1d41 100644 (file)
Binary files a/weblib/tutorial/acUbc.gif and b/weblib/tutorial/acUbc.gif differ

diff --git a/weblib/tutorial/chapter9.ma b/weblib/tutorial/chapter9.ma
index c68c8f1a0e978c2188fd53ef313c7a3c0e355501..fb11216e53fb538d84099769257b5e77045687f2 100644 (file)
--- a/weblib/tutorial/chapter9.ma
+++ b/weblib/tutorial/chapter9.ma
@@ -158,7 +158,7 @@ Let us discuss a couple of examples.
 \ 5b\ 6Example\ 5/b\ 6. 
 Below is the DFA associated with the regular expression (ac+bc)*.
 
 \ 5b\ 6Example\ 5/b\ 6. 
 Below is the DFA associated with the regular expression (ac+bc)*.
 

-\ 5img src="acUbc.gif" alt="some_text"/\ 6  
+\ 5img src="http://www.cs.unibo.it/~asperti/FIGURES/acUbc.gif" alt="DFA for (ac+bc)"/\ 6  

 
 The graphical description of the automaton is the traditional one, with nodes for 
 states and labelled arcs for transitions. Unreachable states are not shown.
 
 The graphical description of the automaton is the traditional one, with nodes for 
 states and labelled arcs for transitions. Unreachable states are not shown.


@@ -176,16 +176,24 @@ Let us consider a more complex case.
 \ 5b\ 6Example\ 5/b\ 6. 
 Starting form the regular expression (a+ϵ)(b*a + b)b, we obtain the following automaton.
 
 \ 5b\ 6Example\ 5/b\ 6. 
 Starting form the regular expression (a+ϵ)(b*a + b)b, we obtain the following automaton.
 

-\ 5img src="automaton.pdf" alt="some_text"/\ 6 
+\ 5img src="http://www.cs.unibo.it/~asperti/FIGURES/automaton.gif" alt="DFA for (a+ϵ)(b*a + b)b"/\ 6 

 
 Remarkably, this DFA is minimal, testifying the small number of states produced by our 
 
 Remarkably, this DFA is minimal, testifying the small number of states produced by our 

-technique (the pair ofstates $6-8$ and $7-9$ differ for the fact that $6$ and $7$ 
-are final, while $8$ and $9$ are not). 
+technique (the pair ofstates 6-8 and 7-9 differ for the fact that 6 and 7 
+are final, while 8 and 9 are not). 

 *) 
 
 *) 
 

-(************************ pit state ***************************)
+(*
+\ 5h2\ 6Move to pit\ 5/h2\ 6. 
+
+We conclude this chapter with a few properties of the move opertions in relation
+with the pit state. *).
+

 definition pit_pre ≝ λS.λi.〈blank S (|i|), false〉. 
 
 definition pit_pre ≝ λS.λi.〈blank S (|i|), false〉. 
 

+(* The following function compute if a symbol in S occurs in a given
+item i *).
+

 let rec occur (S: DeqSet) (i: re S) on i ≝  
   match i with
   [ z ⇒ [ ]
 let rec occur (S: DeqSet) (i: re S) on i ≝  
   match i with
   [ z ⇒ [ ]


@@ -195,6 +203,9 @@ let rec occur (S: DeqSet) (i: re S) on i ≝
   | c e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2) 
   | k e ⇒ occur S e].
 
   | c e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2) 
   | k e ⇒ occur S e].
 

+(* If a symbol a does not occur in i, then move(i,a) gets to the
+pit state. *).
+

 lemma not_occur_to_pit: ∀S,a.∀i:pitem S. memb S a (occur S (|i|)) ≠ true →
   move S a i  = pit_pre S i.
 #S #a #i elim i //
 lemma not_occur_to_pit: ∀S,a.∀i:pitem S. memb S a (occur S (|i|)) ≠ true →
   move S a i  = pit_pre S i.
 #S #a #i elim i //


@@ -209,6 +220,8 @@ lemma not_occur_to_pit: ∀S,a.∀i:pitem S. memb S a (occur S (|i|)) ≠ true 
   ]
 qed.
 
   ]
 qed.
 

+(* We cannot escape form the pit state. *).
+

 lemma move_pit: ∀S,a,i. move S a (\fst (pit_pre S i)) = pit_pre S i.
 #S #a #i elim i //
   [#i1 #i2 #Hind1 #Hind2 >move_cat >Hind1 >Hind2 // 
 lemma move_pit: ∀S,a,i. move S a (\fst (pit_pre S i)) = pit_pre S i.
 #S #a #i elim i //
   [#i1 #i2 #Hind1 #Hind2 >move_cat >Hind1 >Hind2 // 


@@ -221,6 +234,9 @@ lemma moves_pit: ∀S,w,i. moves S w (pit_pre S i) = pit_pre S i.
 #S #w #i elim w // 
 qed. 
  
 #S #w #i elim w // 
 qed. 
  

+(* If any character in w does not occur in i, then moves(i,w) gets
+to the pit state. *).
+

 lemma to_pit: ∀S,w,e. ¬ sublist S w (occur S (|\fst e|)) →
  moves S w e = pit_pre S (\fst e).
 #S #w elim w
 lemma to_pit: ∀S,w,e. ¬ sublist S w (occur S (|\fst e|)) →
  moves S w e = pit_pre S (\fst e).
 #S #w elim w