Mercurial > hg > Members > kono > Proof > automaton

changeset 70:702ce92c45ab

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add concat
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 06 Nov 2019 23:19:53 +0900
parents f124fceba460
children 5cf460a98937
files agda/finiteSet.agda agda/nat.agda agda/regular-language.agda agda/sbconst2.agda
diffstat 4 files changed, 147 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/agda/finiteSet.agda	Wed Nov 06 17:18:58 2019 +0900
+++ b/agda/finiteSet.agda	Wed Nov 06 23:19:53 2019 +0900
@@ -15,6 +15,8 @@
         F←Q : Q → Fin n
         finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
         finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f
+     finℕ : ℕ
+     finℕ = n
      lt0 : (n : ℕ) →  n Data.Nat.≤ n
      lt0 zero = z≤n
      lt0 (suc n) = s≤s (lt0 n)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/nat.agda	Wed Nov 06 23:19:53 2019 +0900
@@ -0,0 +1,53 @@
+module nat where
+
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
+open import Data.Empty
+open import Relation.Nullary
+open import  Relation.Binary.PropositionalEquality
+open import  logic
+
+
+nat-<> : { x y : Nat } → x < y → y < x → ⊥
+nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
+
+nat-<≡ : { x : Nat } → x < x → ⊥
+nat-<≡  (s≤s lt) = nat-<≡ lt
+
+nat-≡< : { x y : Nat } → x ≡ y → x < y → ⊥
+nat-≡< refl lt = nat-<≡ lt
+
+¬a≤a : {la : Nat} → Suc la ≤ la → ⊥
+¬a≤a  (s≤s lt) = ¬a≤a  lt
+
+a<sa : {la : Nat} → la < Suc la 
+a<sa {Zero} = s≤s z≤n
+a<sa {Suc la} = s≤s a<sa 
+
+=→¬< : {x : Nat  } → ¬ ( x < x )
+=→¬< {Zero} ()
+=→¬< {Suc x} (s≤s lt) = =→¬< lt
+
+>→¬< : {x y : Nat  } → (x < y ) → ¬ ( y < x )
+>→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x
+
+<-∨ : { x y : Nat } → x < Suc y → ( (x ≡ y ) ∨ (x < y) )
+<-∨ {Zero} {Zero} (s≤s z≤n) = case1 refl
+<-∨ {Zero} {Suc y} (s≤s lt) = case2 (s≤s z≤n)
+<-∨ {Suc x} {Zero} (s≤s ())
+<-∨ {Suc x} {Suc y} (s≤s lt) with <-∨ {x} {y} lt
+<-∨ {Suc x} {Suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → Suc k ) eq)
+<-∨ {Suc x} {Suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)
+
+max : (x y : Nat) → Nat
+max Zero Zero = Zero
+max Zero (Suc x) = (Suc x)
+max (Suc x) Zero = (Suc x)
+max (Suc x) (Suc y) = Suc ( max x y )
+
+-- _*_ : Nat → Nat → Nat
+-- _*_ zero _ = zero
+-- _*_ (suc n) m = m + ( n * m )
+
+exp : Nat → Nat → Nat
+exp _ Zero = 1
+exp n (Suc m) = n * ( exp n m )
--- a/agda/regular-language.agda	Wed Nov 06 17:18:58 2019 +0900
+++ b/agda/regular-language.agda	Wed Nov 06 23:19:53 2019 +0900
@@ -3,12 +3,13 @@
 open import Level renaming ( suc to Suc ; zero to Zero )
 open import Data.List 
 open import Data.Nat hiding ( _≟_ )
-open import Data.Fin
+open import Data.Fin hiding ( _+_ )
 open import Data.Product
 -- open import Data.Maybe
 open import  Relation.Nullary
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 open import logic
+open import nat
 open import automaton
 open import finiteSet
 
@@ -24,6 +25,8 @@
    field
       states : Set 
       astart : states 
+      aℕ : ℕ
+      afin : FiniteSet states {aℕ}
       automaton : Automaton states Σ
    contain : List Σ → Bool
    contain x = accept automaton astart x
@@ -60,17 +63,14 @@
 M-Union {Σ} A B = record {
        states =  states A × states B
      ; astart = ( astart A , astart B )
+     ; aℕ = {!!}
+     ; afin = {!!}
      ; automaton = record {
              δ = λ q x → ( δ (automaton A) (proj₁ q) x , δ (automaton B) (proj₂ q) x )
            ; aend = λ q → ( aend (automaton A) (proj₁ q) \/ aend (automaton B) (proj₂ q) )
         }
    } 
 
--- 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) ≡
@@ -95,3 +95,86 @@
 -- 
 -- closed-in-concat :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )
 -- closed-in-concat = {!!}
+
+open import nfa
+open import sbconst2
+open FiniteSet
+open import Data.Nat.Properties
+open import Relation.Binary as B hiding (Decidable)
+
+fin-∨ : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A ∨ B) {a + b}
+fin-∨ {A} {B} {c} {b} fa fb = record {
+              Q←F = f0
+            ; F←Q = f1
+            ; finiso→ = f2
+            ; finiso← = f3
+   } where
+        f0 : Fin (c + b) → A ∨ B
+        f0 x with <-cmp (toℕ x) c
+        f0 x | tri< a ¬b ¬c = case1 ( Q←F fa (fromℕ≤ a ) )
+        f0 x | tri≈ ¬a b ¬c = case2 ( Q←F fb (fromℕ≤ {!!} ))
+        f0 x | tri> ¬a ¬b c = case2 ( Q←F fb (fromℕ≤ {!!} ))
+        f1 : A ∨ B → Fin (c + b)
+        f1 (case1 x) = inject+ b (F←Q fa x )
+        f1 (case2 x) = raise c (F←Q fb x )
+        f2 : (q : A ∨ B) → f0 (f1 q) ≡ q
+        f2 = {!!}
+        f3 : (f : Fin (c + b)) → f1 (f0 f) ≡ f
+        f3 = {!!}
+
+fin→ : {A : Set} → { a : ℕ } → FiniteSet A {a} → FiniteSet (A → Bool ) {exp 2 a}
+fin→ {A} {a} fa = record {
+              Q←F = f0
+            ; F←Q = {!!}
+            ; finiso→ = {!!}
+            ; finiso← = {!!}
+      } where
+          f0 : Fin (exp 2 a) → A → Bool
+          f0 = {!!}
+          f1 : (A → Bool) → Fin (exp 2 a)
+          f1 = {!!}
+
+Concat-NFA :  {Σ : Set} → (A B : RegularLanguage Σ ) → NAutomaton (states A ∨ states B) Σ 
+Concat-NFA {Σ} A B = record { Nδ = δnfa ; Nend = nend } where
+       δnfa : states A ∨ states B → Σ → states A ∨ states B → Bool
+       δnfa (case1 q) i (case1 q₁) = equal? (afin A) (δ (automaton A) q i) q₁
+       δnfa (case1 qa) i (case2 qb) = (aend (automaton A) qa ) /\ (equal? (afin B) qb (astart B) )
+       δnfa (case2 q) i (case2 q₁) = equal? (afin B) (δ (automaton B) q i) q₁
+       δnfa _ i _ = false
+       nend : states A ∨ states B → Bool
+       nend (case2 q) = aend (automaton B) q
+       nend _ = false
+
+Concat-NFA-start :  {Σ : Set} → (A B : RegularLanguage Σ ) → states A ∨ states B → Bool
+Concat-NFA-start A B (case1 q) = equal? (afin A) q (astart A)
+Concat-NFA-start _ _ _ = false
+
+M-Concat : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ
+M-Concat {Σ} A B = record {
+       states = states A ∨ states B → Bool
+     ; astart = Concat-NFA-start A B
+     ; aℕ = finℕ finf
+     ; afin = finf
+     ; automaton = subset-construction fin (Concat-NFA A B) (case1 (astart A))
+   } where
+       fin : FiniteSet (states A ∨ states B ) {aℕ A + aℕ B}
+       fin = fin-∨ (afin A) (afin B)
+       finf : FiniteSet (states A ∨ states B → Bool ) 
+       finf = fin→ fin 
+       
+lemma1 : {Σ : Set} →  ( x y : List Σ )
+    → (A B : RegularLanguage Σ ) 
+    → accept (automaton A) (astart A) x ≡ true
+    → accept (automaton B) (astart B) y ≡ true
+    → Naccept (Concat-NFA A B) (fin-∨ (afin A) (afin B)) (Concat-NFA-start A B) ( x ++ y ) ≡ true
+lemma1 {Σ} x y A B aA aB = lemma2 x (astart A) (Concat-NFA-start A B) aA where
+    lemma2 : (x : List Σ) → (q : states A) → (qab : states A ∨ states B → Bool)
+       → accept (automaton A) q x ≡ true → Naccept (Concat-NFA A B) (fin-∨ (afin A) (afin B)) qab ( x ++ y ) ≡ true
+    lemma2 [] q qab aA = {!!}
+    lemma2 (h ∷ t ) q qab aA  = lemma2 t {!!} {!!} {!!}
+
+-- closed-in-concat :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )
+-- closed-in-concat A B x with  split {!!} {!!} x
+-- closed-in-concat A B x | true = {!!}
+-- closed-in-concat A B x | false = {!!}
+
--- a/agda/sbconst2.agda	Wed Nov 06 17:18:58 2019 +0900
+++ b/agda/sbconst2.agda	Wed Nov 06 23:19:53 2019 +0900
@@ -17,7 +17,7 @@
 
 open Bool
 
-δconv : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q {n} →  ( nδ : Q → Σ → Q → Bool ) → (Q → Bool) → Σ → (Q → Bool)
+δconv : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q {n} →  ( nδ : Q → Σ → Q → Bool ) → (f : Q → Bool) → (i : Σ) → (Q → Bool)
 δconv {Q} { Σ} { n} N nδ f i q =  exists N ( λ r → f r /\ nδ r i q )
 
 open FiniteSet
@@ -26,12 +26,8 @@
     (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 q = exists fin ( λ q1 → equal? fin  q q1)
-     aend1 : (Q → Bool) → Bool
-     aend1 f = exists fin ( λ q → f q /\ Nend NFA q )
+     ;  aend = λ f → exists fin ( λ q → f q /\ Nend NFA q )
+   } 
 
 am2start = λ q1 → equal? finState1 ss q1