Mercurial > hg > Members > kono > Proof > automaton

changeset 69:f124fceba460

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
subset construction
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 06 Nov 2019 17:18:58 +0900
parents 13822f5f9c85
children 702ce92c45ab
files a04/lecture.ind agda/finiteSet.agda agda/nfa.agda agda/regular-language.agda agda/sbconst2.agda
diffstat 5 files changed, 131 insertions(+), 96 deletions(-) [+]
line wrap: on
line diff
--- a/a04/lecture.ind	Thu Oct 31 21:41:54 2019 +0900
+++ b/a04/lecture.ind	Wed Nov 06 17:18:58 2019 +0900
@@ -9,65 +9,14 @@
     record NAutomaton ( Q : Set ) ( Σ : Set  )
            : Set  where
         field
-              nδ : Q → Σ → List Q
-              sid : Q  →  ℕ
-              nstart : Q
-              nend  : Q → Bool
+              Nδ : Q → Σ → Q → Bool
+              Nend  :  Q → Bool
 
 これを非決定性オートマトンという。Agda では同じ名前を使いまわしすることはできない(monomorpphism)ので、nを付けた。
 
-次の状態は状態の集合(List)になる。次の次の状態は、可能な状態の次の状態の集合を合わせた(union)ものになる。
-
-少し複雑がだが、insert と merge を定義して、
-
-<a href="../agda/nfa-list.agda"> nfa-list.agda </a>
-
-    insert : { Q : Set } {  Σ : Set } → ( NAutomaton Q  Σ  ) →  List Q  → Q  → List Q
-    insert  M  [] q =  q ∷ []
-    insert  M  ( q  ∷ T ) q' with  (sid M q ) ≟ (sid M q')
-    ... | yes _ = insert  M  T q'
-    ... | no _ = q  ∷ (insert  M  T q' )
-
-    merge : { Q : Set } {  Σ : Set } → ( NAutomaton Q  Σ  ) → List Q  → List Q  → List Q
-    merge  M L1 [] = L1
-    merge  M L1 ( H  ∷ L  ) =  insert M (merge M L1 L ) H
-
-    Nmoves : { Q : Set } { Σ : Set  }
-        → NAutomaton Q  Σ
-        → List Q → List  Σ → List Q
-    Nmoves {Q} { Σ} M q L = Nmoves1 q L []
-       where
-          Nmoves1 : (q : List Q ) ( L : List  Σ ) → List Q → List Q
-          Nmoves1 q  [] _ = q
-          Nmoves1 []  (_  ∷ L) LQ = Nmoves1 LQ L []
-          Nmoves1 (q  ∷ T ) (H  ∷ L) LQ = Nmoves1 T  (H  ∷ L) ( merge M  ( nδ M q H ) LQ )
+<a href="../agda/nfa.agda"> nfa.agda </a>
 
-    Naccept : { Q : Set } { Σ : Set  }
-        → NAutomaton Q  Σ
-        →  List  Σ → Bool
-    Naccept {Q} { Σ} M L =
-           checkAccept ( Nmoves M ((nstart M)  ∷ [] )  L )
-       where
-          checkAccept : (q : List Q ) → Bool
-          checkAccept [] = false
-          checkAccept ( H ∷ L ) with (nend M) H
-          ... | true = true
-          ... | false = checkAccept L
-
-とする。 
-
---部分集合を使うと簡単になる
-
-<a href="../agda/nfa-list.agda"> nfa-list.agda </a>
-
-
-    record NAutomaton ( Q : Set ) ( Σ : Set  )
-           : Set  where
-        field
-              Nδ : Q → Σ → Q → Bool
-              Nstart : Q → Bool
-              Nend  :  Q → Bool
-
+状態の受理と遷移は以下のようになる。
 
     Nmoves : { Q : Set } { Σ : Set  }
         → NAutomaton Q  Σ
@@ -76,16 +25,18 @@
     Nmoves {Q} { Σ} M fin  Qs  s q  =
           exists fin ( λ qn → (Qs qn ∧ ( Nδ M qn s q )  ))
 
-
-    Naccept : { Q : Set } { Σ : Set  } 
+    Naccept : { Q : Set } { Σ : Set  }
         → NAutomaton Q  Σ
         → {n : ℕ } → FiniteSet Q {n}
-        → List  Σ  → Bool
-    Naccept {Q} {Σ} M fin input = Naccept1 M ( Nstart M ) input
-       where
-          Naccept1 : NAutomaton Q  Σ → ( Q → Bool ) →  List  Σ  →  Bool
-          Naccept1 M sb []  = exists fin ( λ q → sb q ∧ Nend M q )
-          Naccept1 M sb (i ∷ t ) = Naccept1 M ( Nmoves M  fin sb i ) t
+        → (Nstart : Q → Bool) → List  Σ → Bool
+    Naccept M fin sb []  = exists fin ( λ q → sb q ∧ Nend M q )
+    Naccept M fin sb (i ∷ t ) = Naccept M fin ( Nmoves M  fin sb i ) t
+
+次の状態は状態の集合(List)になる。次の次の状態は、可能な状態の次の状態の集合を合わせた(union)ものになる。
+しかし、List で定義すると少し複雑になる。
+
+部分集合を使うと簡単になる。Q の部分集合は Q → Bool で true になるものであるとする。
+
 
 --例題
 
@@ -109,9 +60,21 @@
     start1 _ = false
 
     am2  :  NAutomaton  States1 In2
-    am2  =  record { Nδ = transition3 ; Nstart = start1 ; Nend = fin1}
+    am2  =  record { Nδ = transition3 ; Nend = fin1}
+
+    example2-1 = Naccept am2 finState1 start1 ( i0  ∷ i1  ∷ i0  ∷ [] )
+    example2-2 = Naccept am2 finState1 start1 ( i1  ∷ i1  ∷ i1  ∷ [] )
 
-    example2-1 = Naccept am2 finState1 ( i0  ∷ i1  ∷ i0  ∷ [] ) 
-    example2-2 = Naccept am2 finState1 ( i1  ∷ i1  ∷ i1  ∷ [] ) 
+    fin0 :  States1  → Bool
+    fin0 st = false
+    fin0 ss = false
+    fin0 sr = false
 
+    test0 : Bool
+    test0 = exists finState1 fin0
 
+    test1 : Bool
+    test1 = exists finState1 fin1
+
+    test2 = Nmoves am2 finState1 start1
+
--- a/agda/finiteSet.agda	Thu Oct 31 21:41:54 2019 +0900
+++ b/agda/finiteSet.agda	Wed Nov 06 17:18:58 2019 +0900
@@ -1,10 +1,12 @@
 module finiteSet  where
 
-open import Data.Nat
-open import Data.Bool
+open import Data.Nat hiding ( _≟_ )
 open import Data.Fin renaming ( _<_ to _<<_ )
+open import Data.Fin.Properties
+open import Relation.Nullary
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality
+open import logic
 
 record FiniteSet ( Q : Set ) { n : ℕ }
         : Set  where
@@ -24,8 +26,13 @@
      exists p = exists1 n (lt0 n) p where
          exists1 : (m : ℕ ) → m Data.Nat.≤ n  → ( Q → Bool ) → Bool
          exists1  zero  _ _ = false
-         exists1 ( suc m ) m<n p = p (Q←F (fromℕ≤ {m} {n} m<n)) ∨ exists1 m (lt2 m<n) p
+         exists1 ( suc m ) m<n p = p (Q←F (fromℕ≤ {m} {n} m<n)) \/ exists1 m (lt2 m<n) p
+     equal? : Q → Q → Bool
+     equal? q0 q1 with F←Q q0 ≟ F←Q q1
+     ... | yes p = true
+     ... | no ¬p = false
 
 fless : {n : ℕ} → (f : Fin n ) → toℕ f < n
 fless zero = s≤s z≤n
 fless (suc f) = s≤s ( fless f )
+
--- a/agda/nfa.agda	Thu Oct 31 21:41:54 2019 +0900
+++ b/agda/nfa.agda	Wed Nov 06 17:18:58 2019 +0900
@@ -7,10 +7,11 @@
 open import Data.Maybe
 open import Relation.Nullary
 open import Data.Empty
-open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
+-- open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import finiteSet
+open import logic
 
 data  States1   : Set  where
    sr : States1
@@ -26,7 +27,6 @@
        : Set  where
     field
           Nδ : Q → Σ → Q → Bool
-          Nstart : Q → Bool
           Nend  :  Q → Bool
 
 open NAutomaton
@@ -42,11 +42,10 @@
        Q←F zero = sr
        Q←F (suc zero) = ss
        Q←F (suc (suc zero)) = st
-       Q←F (suc (suc (suc ()))) 
        F←Q : States1 → Fin 3
        F←Q sr = zero
-       F←Q ss = suc (zero)
-       F←Q st = suc ( suc zero )
+       F←Q ss = suc zero
+       F←Q st = suc (suc zero)
        finiso→ : (q : States1) → Q←F (F←Q q) ≡ q
        finiso→ sr = refl
        finiso→ ss = refl
@@ -63,20 +62,17 @@
 Nmoves : { Q : Set } { Σ : Set  }
     → NAutomaton Q  Σ
     → {n : ℕ } → FiniteSet Q  {n}
-    →  ( Q → Bool )  → Σ → Q → Bool
+    →  ( Qs : Q → Bool )  → (s : Σ ) → Q → Bool
 Nmoves {Q} { Σ} M fin  Qs  s q  =
-      exists fin ( λ qn → (Qs qn ∧ ( Nδ M qn s q )  ))
+      exists fin ( λ qn → (Qs qn /\ ( Nδ M qn s q )  ))
 
 
 Naccept : { Q : Set } { Σ : Set  } 
     → NAutomaton Q  Σ
     → {n : ℕ } → FiniteSet Q {n}
-    → List  Σ  → Bool
-Naccept {Q} {Σ} M fin input = Naccept1 M ( Nstart M ) input
-   where
-      Naccept1 : NAutomaton Q  Σ → ( Q → Bool ) →  List  Σ  →  Bool
-      Naccept1 M sb []  = exists fin ( λ q → sb q ∧ Nend M q )
-      Naccept1 M sb (i ∷ t ) = Naccept1 M ( Nmoves M  fin sb i ) t
+    → (Nstart : Q → Bool) → List  Σ → Bool
+Naccept M fin sb []  = exists fin ( λ q → sb q /\ Nend M q )
+Naccept M fin sb (i ∷ t ) = Naccept M fin ( Nmoves M  fin sb i ) t
 
 
 transition3 : States1  → In2  → States1 → Bool
@@ -99,10 +95,34 @@
 start1 _ = false
 
 am2  :  NAutomaton  States1 In2
-am2  =  record { Nδ = transition3 ; Nstart = start1 ; Nend = fin1}
+am2  =  record { Nδ = transition3 ; Nend = fin1}
+
+example2-1 = Naccept am2 finState1 start1 ( i0  ∷ i1  ∷ i0  ∷ [] ) 
+example2-2 = Naccept am2 finState1 start1 ( i1  ∷ i1  ∷ i1  ∷ [] ) 
 
-example2-1 = Naccept am2 finState1 ( i0  ∷ i1  ∷ i0  ∷ [] ) 
-example2-2 = Naccept am2 finState1 ( i1  ∷ i1  ∷ i1  ∷ [] ) 
+transition4 : States1  → In2  → States1 → Bool
+transition4 sr i0 sr = true
+transition4 sr i1 ss = true
+transition4 sr i1 sr = true
+transition4 ss i0 ss = true
+transition4 ss i1 st = true
+transition4 st i0 st = true
+transition4 st i1 st = true
+transition4 _ _ _ = false
+
+fin4 :  States1  → Bool
+fin4 st = true
+fin4 _ = false
+
+start4 : States1 → Bool
+start4 ss = true
+start4 _ = false
+
+am4  :  NAutomaton  States1 In2
+am4  =  record { Nδ = transition4 ; Nend = fin4}
+
+example4-1 = Naccept am4 finState1 start4 ( i0  ∷ i1  ∷ i1  ∷ i0 ∷ [] ) 
+example4-2 = Naccept am4 finState1 start4 ( i0  ∷ i1  ∷ i1  ∷ i1 ∷ [] ) 
 
 fin0 :  States1  → Bool
 fin0 st = false
--- a/agda/regular-language.agda	Thu Oct 31 21:41:54 2019 +0900
+++ b/agda/regular-language.agda	Wed Nov 06 17:18:58 2019 +0900
@@ -44,6 +44,14 @@
 Star : {Σ : Set} → ( A : language {Σ} ) → language {Σ}
 Star {Σ} A = split A ( Star {Σ} A )
 
+test-split : {Σ : Set} → {A B : List In2 → Bool} → split A B ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ (
+       ( A [] /\ B ( i0 ∷ i1 ∷ i0 ∷ [] ) ) \/ 
+       ( A ( i0 ∷ [] ) /\ B ( i1 ∷ i0 ∷ [] ) ) \/ 
+       ( A ( i0 ∷ i1 ∷ [] ) /\ B ( i0 ∷ [] ) ) \/
+       ( A ( i0 ∷ i1 ∷ i0 ∷ [] ) /\ B  []  ) 
+   )
+test-split {_} {A} {B} = refl
+
 open RegularLanguage 
 isRegular : {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage Σ ) → Set
 isRegular A x r = A x ≡ contain r x 
@@ -58,6 +66,11 @@
         }
    } 
 
+-- closed-in-union' :  {Σ : Set} → (A B : RegularLanguage Σ )
+--    → ( M : Automaton {!!} Σ ) → ( astart : {!!}  )
+--    → ( x : List Σ ) → (Union (contain A) (contain B) x) ≡ true → accept M astart x ≡ true
+-- closed-in-union' = {!!}
+
 closed-in-union :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Union (contain A) (contain B)) x ( M-Union A B )
 closed-in-union A B [] = lemma where
    lemma : aend (automaton A) (astart A) \/ aend (automaton B) (astart B) ≡
--- a/agda/sbconst2.agda	Thu Oct 31 21:41:54 2019 +0900
+++ b/agda/sbconst2.agda	Wed Nov 06 17:18:58 2019 +0900
@@ -2,32 +2,64 @@
 
 open import Level renaming ( suc to succ ; zero to Zero )
 open import Data.Nat
+open import Data.Fin
 open import Data.List
-open import Data.Bool using ( Bool ; true ; false ; _∧_ )
 
 open import automaton
 open import nfa
+open import logic
 open NAutomaton
 open Automaton
 open import finiteSet
 open FiniteSet
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+
+
+open Bool
 
 δconv : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q {n} →  ( nδ : Q → Σ → Q → Bool ) → (Q → Bool) → Σ → (Q → Bool)
-δconv {Q} { Σ} { n} N nδ f i q =  exists N ( λ r → f r ∧ nδ r i q )
+δconv {Q} { Σ} { n} N nδ f i q =  exists N ( λ r → f r /\ nδ r i q )
+
+open FiniteSet
 
 subset-construction : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q {n} →  
-    (NAutomaton Q  Σ ) → (Automaton (Q → Bool)  Σ )  
-subset-construction {Q} { Σ} {n} N NFA = record {
-        δ = λ q x → δconv N ( Nδ NFA ) q x
-     ;  astart = astart1
+    (NAutomaton Q  Σ ) → (astart : Q ) → (Automaton (Q → Bool)  Σ )  
+subset-construction {Q} { Σ} {n} fin NFA astart = record {
+        δ = λ q x → δconv fin ( Nδ NFA ) q x
      ;  aend = aend1
    } where
      astart1 : Q → Bool
-     astart1 = Nstart NFA 
+     astart1 q = exists fin ( λ q1 → equal? fin  q q1)
      aend1 : (Q → Bool) → Bool
-     aend1 f = exists N ( λ q → f q ∧ Nend NFA q )
+     aend1 f = exists fin ( λ q → f q /\ Nend NFA q )
+
+am2start = λ q1 → equal? finState1 ss q1
+
+test4 = subset-construction finState1 am2 ss
+
+test5 = accept test4 ( λ q1 → equal? finState1 ss q1) ( i0  ∷ i1  ∷ i0  ∷ [] )
+test6 = accept test4 ( λ q1 → equal? finState1 ss q1) ( i1  ∷ i1  ∷ i1  ∷ [] )
 
-test4 = subset-construction finState1 am2
+subset-construction-lemma→ : { Q : Set } { Σ : Set  } { n  : ℕ }  → (fin : FiniteSet Q {n} ) →  
+    (NFA : NAutomaton Q  Σ ) → (astart : Q )
+    → (x : List Σ)
+    → Naccept NFA fin ( λ q1 → equal? fin  astart q1) x ≡ true
+    → accept (  subset-construction fin NFA astart ) ( λ q1 → equal? fin  astart q1) x ≡ true
+subset-construction-lemma→ {Q} {Σ} {n} fin NFA astart x naccept = lemma1 x ( λ q1 → equal? fin  astart q1) naccept where
+    lemma1 :  (x : List Σ) → ( states : Q → Bool )
+       → Naccept NFA fin states x ≡ true
+       → accept (  subset-construction fin NFA astart ) states x ≡ true
+    lemma1 [] states naccept = naccept
+    lemma1 (h ∷ t ) states naccept = lemma1 t (δconv fin (Nδ NFA) states h) naccept
 
-test5 = accept test4  ( i0  ∷ i1  ∷ i0  ∷ [] )
-test6 = accept test4  ( i1  ∷ i1  ∷ i1  ∷ [] )
+subset-construction-lemma← : { Q : Set } { Σ : Set  } { n  : ℕ }  → (fin : FiniteSet Q {n} ) →  
+    (NFA : NAutomaton Q  Σ ) → (astart : Q )
+    → (x : List Σ)
+    → accept (  subset-construction fin NFA astart ) ( λ q1 → equal? fin  astart q1) x ≡ true
+    → Naccept NFA fin ( λ q1 → equal? fin  astart q1) x ≡ true
+subset-construction-lemma← {Q} {Σ} {n} fin NFA astart x saccept = lemma2 x ( λ q1 → equal? fin  astart q1) saccept where
+    lemma2 :  (x : List Σ) → ( states : Q → Bool )
+       → accept (  subset-construction fin NFA astart ) states x ≡ true
+       → Naccept NFA fin states x ≡ true
+    lemma2 [] states saccept = saccept
+    lemma2 (h ∷ t ) states saccept = lemma2 t (δconv fin (Nδ NFA) states h) saccept