Mercurial > hg > Members > kono > Proof > automaton1

changeset 2:b4548639121e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ntrace
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 14 Nov 2020 09:27:57 +0900
parents 7399aae907fc
children bf6d7843ba11
files automaton.agda nfa.agda
diffstat 2 files changed, 64 insertions(+), 42 deletions(-) [+]
line wrap: on
line diff
--- a/automaton.agda	Fri Nov 13 13:03:56 2020 +0900
+++ b/automaton.agda	Sat Nov 14 09:27:57 2020 +0900
@@ -15,8 +15,8 @@
 open Automaton
 
 accept : {n  : Level} {Q : Set n} {Σ : Set } → Automaton Q Σ → Q → List Σ → Set 
-accept {Q} {Σ} atm q [] = F atm q
-accept {Q} {Σ} atm q (x ∷ input) = 
+accept {n} {Q} {Σ} atm q [] = F atm q
+accept {n} {Q} {Σ} atm q (x ∷ input) = 
     accept atm (δ atm q x ) input
 
 trace : {n  : Level} {Q : Set n} {Σ : Set } → (A : Automaton Q Σ) → (start : Q) → (input : List Σ ) → accept A start input → List Q
--- a/nfa.agda	Fri Nov 13 13:03:56 2020 +0900
+++ b/nfa.agda	Sat Nov 14 09:27:57 2020 +0900
@@ -12,21 +12,30 @@
     field
           Nδ : Q → Σ → Q → Set
           NF : Q → Set
-          Nexists : (Q → Set)  → Set
 
 open NAutomaton
 
+naccept : {n  : Level} {Q : Set n} {Σ : Set } → (Nexists : (Q → Set)  → Set) → NAutomaton Q Σ → (Q → Set) → List Σ → Set 
+naccept {n} {Q} {Σ} Nexists nfa qs [] = Nexists (λ q → qs q ∧ NF nfa q )
+naccept {n} {Q} {Σ} Nexists nfa qs (x ∷ input) = 
+    naccept Nexists nfa (λ q' → Nexists (λ q → qs q ∧ Nδ nfa q x q' ))  input
 
-naccept : {n : Level} {Q : Set n} {Σ : Set} → NAutomaton Q Σ → (Q → Set) → List Σ → Set
-naccept {n} {Q} {Σ} nfa qs [] = Nexists nfa (λ q → qs q ∧ NF nfa q )
-naccept {n} {Q} {Σ} nfa qs (x ∷ input) = 
-    Nexists nfa (λ q → qs q ∧ (naccept nfa (Nδ nfa q x) input ))
+qlist : {n : Level} {Q : Set n} → (P : Q → Set ) → ((q : Q) → Dec ( P q))  → List Q → List Q
+qlist P dec [] = []
+qlist P dec (q ∷ qs) with dec q
+... | yes _ = q ∷ qlist P dec qs
+... | no _ = qlist P dec qs
 
-record DecStates {n : Level} ( Q : Set n ) : Set (Suc n) where
-    field
-          QList   : List Q 
-          QDec  : (P : Q → Set) → (q : Q) → Dec (P q)
-
+ntrace : {n  : Level} {Q : Set n} {Σ : Set } → (Nexists : (Q → Set)  → Set) → (nfa : NAutomaton Q Σ) → (qs : Q → Set ) → (input : List Σ )
+     → naccept Nexists nfa qs input
+     → ((qs : Q → Set) (q : Q) → Dec (qs q ∧ NF nfa q))
+     → ((qs : Q → Set) (x : Σ) (t : List Σ) (q : Q) → Dec (naccept Nexists nfa (λ q' → qs q ∧ Nδ nfa q x q') t))
+     → List Q
+     → List (List Q)
+ntrace {n} {Q} {Σ} Nexists nfa qs [] a decNF decNδ L = qlist (λ q → qs q ∧ NF nfa q) (decNF qs) L ∷ []
+ntrace {n} {Q} {Σ} Nexists nfa qs (x ∷ t) a decNF decNδ L = 
+      qlist (λ q → (naccept Nexists nfa (λ q' → qs q ∧ Nδ nfa q x q' ) t )) (decNδ qs x t) L
+      ∷ ( ntrace Nexists nfa (λ q' → Nexists (λ q → qs q ∧ Nδ nfa q x q' )) t a decNF decNδ L )
 
 data transition136 : Q3  → Σ2  → Q3 → Set  where
     d0 : transition136 q₁ s1 q₂ 
@@ -40,53 +49,64 @@
 start136 q = q ≡ q₁
 
 nfa136 :  NAutomaton Q3 Σ2 
-nfa136 =  record { Nδ = transition136 ; NF = λ q → q ≡ q₁ ; Nexists = exists-in-Q3 }
+nfa136 =  record { Nδ = transition136 ; NF = λ q → q ≡ q₁ }
 
-example136-1 = naccept nfa136 start136 ( s0  ∷ s1  ∷ s0 ∷ s0 ∷ [] )
+example136-1 = naccept exists-in-Q3 nfa136 start136 ( s0  ∷ s1  ∷ s0 ∷ s0 ∷ [] )
 
-example136-0 = naccept nfa136 start136 ( s0 ∷ [] )
+example136-0 = naccept exists-in-Q3 nfa136 start136 ( s0 ∷ [] )
 
-example136-2 = naccept nfa136 start136 ( s1  ∷ s0  ∷ s1 ∷ s0 ∷ s1 ∷ [] )
+example136-2 = naccept exists-in-Q3 nfa136 start136 ( s1  ∷ s0  ∷ s1 ∷ s0 ∷ s1 ∷ [] )
 
-nfa136-P : (q : Q3 → Set) → (input : List Σ2 ) → Dec (naccept nfa136 q input )
-nfa136-P q [] = {!!}
-nfa136-P q (x ∷ t) = {!!}
+nfa136-FN : (q : Q3 ) → Dec ( NF nfa136 q )
+nfa136-FN q₁ = yes refl
+nfa136-FN q₂ = no (λ ())
+nfa136-FN q₃ = no (λ ())
 
 Q3List : List Q3
 Q3List = q₁ ∷ q₂ ∷ q₃ ∷ []
 
-nfa136trace : (q : Q3 → Set) → (input : List Σ2 ) → naccept nfa136 q input → List (List Q3)
-nfa136trace q [] (qe1 [ proj1 , refl ]) = {!!}
-nfa136trace q (x ∷ t) (qe1 [ proj1 , a ]) = {!!}
-nfa136trace q (x ∷ t) (qe2 [ proj1 , a ]) = {!!}
-nfa136trace q (x ∷ t) (qe3 [ proj1 , a ]) = {!!}
+decFN136 : (qs qs' : Q3 → Set)  → (x : List Σ2) → naccept exists-in-Q3 nfa136 qs x → (q : Q3) → Dec (qs' q ∧ NF nfa136 q)
+decFN136 qs qs' (_ ∷ _)  _ _ = {!!}
+decFN136 qs qs' [] (qe1 x) q₁ = {!!}
+decFN136 qs qs' []  _ q₂ = no (λ ())
+decFN136 qs qs' []  _ q₃ = no (λ ())
 
---
--- ((Q → Set)  → Set) → ((Q → Set) → Set) → Set
---
+decF̨δ136 :  (qs qs' : Q3 → Set) (x : Σ2) (t : List Σ2) → naccept exists-in-Q3 nfa136 qs' t → (q : Q3) →
+    Dec (naccept exists-in-Q3 nfa136 (λ q' → qs' q ∧ Nδ nfa136 q x q') t)
+decF̨δ136 qs qs' x t a q₁ = {!!}
+decF̨δ136 qs qs' x t a q₂ = {!!}
+decF̨δ136 qs qs' x t a q₃ = {!!}
 
-data Nexists→exits  {n : Level} { Q : Set n }  {Σ : Set} ( NFA : NAutomaton Q  Σ ) : ((Q → Set) → Set) → Set where
-   one-of : Nexists→exits NFA  (Nexists NFA)
+nfa136trace : (qs : Q3 → Set) → (input : List Σ2 ) → naccept exists-in-Q3 nfa136 qs input → List (List Q3)
+nfa136trace qs x a = ntrace exists-in-Q3 nfa136 qs x a (λ qs' q → decFN136 qs qs' x a q ) (λ qs' x t q →  decF̨δ136 qs qs' x {!!} a q) Q3List
 
-subset-construction : {n : Level} { Q : Set n } { Σ : Set  }   → 
+subset-construction : {n : Level} { Q : Set n } { Σ : Set  }   → (Nexists : (Q → Set)  → Set) → 
     (NAutomaton Q  Σ ) → Automaton {Suc Zero ⊔ n} (Q → Set) Σ 
-subset-construction {n} {Q} { Σ}  NFA = record {
-        δ = λ qs x qs → Nexists NFA (λ q → Nδ NFA q x qs )
-     ;  F = λ qs → Nexists NFA ( λ q → NF NFA q )
+subset-construction {n} {Q} { Σ} Nexists  nfa = record {
+        δ = λ qs x q' → Nexists (λ q → qs q ∧ Nδ nfa q x q' )
+     ;  F = λ qs → Nexists ( λ q → NF nfa q )
    } 
 
+dfa136 : Automaton (Q3 → Set) Σ2
+dfa136 = subset-construction  exists-in-Q3 nfa136
+
+t136 : accept dfa136 start136 (s0 ∷ s1 ∷ s0 ∷ s0 ∷ []) → List ( Q3 → Set )
+t136 = trace dfa136 start136 ( s0  ∷ s1  ∷ s0 ∷ s0 ∷ [] ) 
+
 subset-construction-lemma→ : { Q : Set } { Σ : Set  }   →   
+    (Nexists : (Q → Set)  → Set) →
     (NFA : NAutomaton Q  Σ ) → (astart : Q → Set )
     → (x : List Σ)
-    → naccept NFA ( λ q1 → astart q1) x 
-    → accept (  subset-construction NFA ) ( λ q1 → astart q1) x 
+    → naccept Nexists NFA ( λ q1 → astart q1) x 
+    → accept (  subset-construction Nexists NFA ) ( λ q1 → astart q1) x 
 subset-construction-lemma→ = {!!}
 
 subset-construction-lemma← : { Q : Set } { Σ : Set  }   → 
+    (Nexists : (Q → Set)  → Set) →
     (NFA : NAutomaton Q  Σ ) → (astart : Q → Set )
     → (x : List Σ)
-    → accept (  subset-construction NFA ) ( λ q1 → astart q1) x 
-    → naccept NFA ( λ q1 →  astart q1) x 
+    → accept (  subset-construction Nexists NFA ) ( λ q1 → astart q1) x 
+    → naccept Nexists NFA ( λ q1 →  astart q1) x 
 subset-construction-lemma← = {!!}
 
 open import regular-language 
@@ -95,11 +115,11 @@
 open Automaton
 open import Data.Empty 
 
--- Concat-exists : {n : Level}  {Σ : Set} → (A B : RegularLanguage {n} Σ ) →  (states A ∨ states B → Set) → Set
--- Concat-exists {n} {Σ} A B P = exists (automaton A) (λ q → P (case1 q)) ∨ exists (automaton B) (λ q → P (case2 q))
+Union-Nexists : {n m : Level}  → {A : Set n} → {B : Set m}  → ( (A → Set) → Set )→ ( (B → Set) → Set ) → ( (A ∨ B → Set) → Set )
+Union-Nexists {n} {m} {A} {B} PA PB P = PA (λ q → P (case1 q)) ∨ PB (λ q → P (case2 q))
 
-Concat-NFA : {n : Level}  {Σ : Set} → (A B : RegularLanguage {n} Σ ) → NAutomaton (states A ∨ states B) Σ 
-Concat-NFA {n} {Σ} A B = record { Nδ = δnfa ; NF = nend  ; Nexists = {!!} }
+Concat-NFA : {n : Level}  {Σ : Set} → (A B : RegularLanguage {n} Σ )  → NAutomaton (states A ∨ states B) Σ 
+Concat-NFA {n} {Σ} A B = record { Nδ = δnfa ; NF = nend  }
    module Concat-NFA where
        data δnfa : states A ∨ states B → Σ → states A ∨ states B → Set where
          a-case   : {q : states A}  {i : Σ } → δnfa ( case1 q) i (case1 (δ (automaton A) q i))
@@ -113,8 +133,10 @@
    this : (a : states A)  → state-is A a
 
 closed-in-concat :  {n : Level} {Σ : Set } → (A B : RegularLanguage {n}  Σ ) → ( x : List Σ ) 
+   (PA : (states A  → Set)  → Set) 
+   (PB : (states B  → Set)  → Set) 
    → isRegular (Concat {n} (contain A) (contain B)) x record {states = states A ∨ states B → Set ; astart = λ q → state-is A (astart A)
-         ; automaton = subset-construction ( Concat-NFA A B )}
+         ; automaton = subset-construction (Union-Nexists PA PB) ( Concat-NFA A B )}
 closed-in-concat {Σ} A B x = {!!}