Mercurial > hg > Members > kono > Proof > automaton

changeset 36:9558d870e8ae

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add cfg and derive
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 28 Nov 2018 21:15:49 +0900
parents 95f2e129cf9e
children a7f09c9a2c7a
files agda/cfg.agda agda/derive.agda agda/nfa.agda agda/regex1.agda
diffstat 4 files changed, 84 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/cfg.agda	Wed Nov 28 21:15:49 2018 +0900
@@ -0,0 +1,14 @@
+module cfg where
+
+open import Level renaming ( suc to succ ; zero to Zero )
+-- open import Data.Fin
+open import Data.Nat
+open import Data.Product
+-- open import Data.List
+open import Data.Maybe
+open import Data.Bool using ( Bool ; true ; false )
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Data.String
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/derive.agda	Wed Nov 28 21:15:49 2018 +0900
@@ -0,0 +1,31 @@
+module derive where
+
+open import nfa
+open import regex1
+open import Data.Nat
+open import Data.List
+
+open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+
+
+derivatives : {Σ : Set} → Σ → Regex  Σ → Regex  Σ
+derivatives x (r *) = {!!}
+derivatives x (r & r₁) = {!!}
+derivatives x (r || r₁) = {!!}
+derivatives x < x₁ > = {!!}
+
+daccept : {Σ : Set} → ( r : Regex  Σ ) →  {n : ℕ } (fin : FiniteSet Σ {n}) → ( s :  List Σ ) → Bool
+daccept r fin [] = {!!}
+daccept r fin (h ∷ t) =  regular-language ( derivatives h r ) fin t
+
+lemma1 : {Σ : Set} → ( r : Regex  Σ ) →  {n : ℕ } (fin : FiniteSet Σ {n}) → ( s :  List Σ )
+     → regular-language r fin s ≡ true → daccept r fin s  ≡ true
+lemma1 = {!!}
+
+lemma2 : {Σ : Set} → ( r : Regex  Σ ) →  {n : ℕ } (fin : FiniteSet Σ {n}) → ( s :  List Σ )
+     → daccept r fin s  ≡ true → regular-language r fin s ≡ true 
+lemma2 = {!!}
+
+
+
--- a/agda/nfa.agda	Wed Nov 07 14:46:54 2018 +0900
+++ b/agda/nfa.agda	Wed Nov 28 21:15:49 2018 +0900
@@ -11,6 +11,7 @@
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Relation.Nullary using (¬_; Dec; yes; no)
 
+
 data  States1   : Set  where
    sr : States1
    ss : States1
@@ -140,7 +141,7 @@
 
 test2 = Nmoves am2 finState1 start1 
 
-test4 : Fin 2 → Bool
-test4 zero = {!!}
-test4 (suc zero) = {!!}
-test4 (suc (suc ()))
+-- test4 : Fin 2 → Bool
+-- test4 zero = {!!}
+-- test4 (suc zero) = {!!}
+-- test4 (suc (suc ()))
--- a/agda/regex1.agda	Wed Nov 07 14:46:54 2018 +0900
+++ b/agda/regex1.agda	Wed Nov 28 21:15:49 2018 +0900
@@ -3,7 +3,7 @@
 open import Level renaming ( suc to succ ; zero to Zero )
 open import Data.Fin
 open import Data.Nat hiding ( _≟_ )
-open import Data.List
+open import Data.List hiding ( any )
 open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
 open import  Relation.Binary.PropositionalEquality as RBF hiding ( [_] ) 
 open import Relation.Nullary using (¬_; Dec; yes; no)
@@ -15,6 +15,24 @@
    _||_  : Regex  Σ → Regex  Σ → Regex Σ
    <_>   : Σ → Regex  Σ
 
+-- postulate a b c d : Set
+
+data hoge : Set where
+   a : hoge
+   b : hoge
+   c : hoge
+   d : hoge
+
+infixr 40 _&_ _||_
+
+r1' =    (< a > & < b >) & < c >
+r1 =    < a > & < b > & < c >
+any = < a > || < b >  || < c >
+r2 =    ( any * ) & ( < a > & < b > & < c > )
+r3 =    ( any * ) & ( < a > & < b > & < c > & < a > & < b > & < c > )
+r4 =    ( < a > & < b > & < c > ) || ( < b > & < c > & < d > )
+r5 =    ( any * ) & ( < a > & < b > & < c > || < b > & < c > & < d > )
+
 open import nfa
 
 _‖_ : {Σ : Set} ( x y : List Σ → Bool) → List Σ → Bool
@@ -77,6 +95,20 @@
 test-r2 = regular-language (< i0 > & < i1 >) finIn2 ( i0  ∷ i1  ∷ [] )
 test-r3 = regular-language (< i0 > & < i1 >) finIn2 ( i0  ∷ i0  ∷ [] )
 
+issub : {Σ : Set} {n : ℕ } → Regex Σ → Regex Σ → FiniteSet Σ {n} → Bool
+issub (r *) s f = issub r s f
+issub (r & r₁) s f = issub r s f ∨ issub r₁ s f
+issub (r || r₁) s f =  issub r s f ∨ issub r₁ s f
+issub < x > < s > f with cmpi f x s 
+issub < x > < s > f | yes p = true
+issub < x > < s > f | no ¬p = false
+issub < x > s f  = false
+
+record RegexSub {Σ : Set} (R :  Regex Σ) {n : ℕ }  (fin :  FiniteSet Σ {n} ): Set where
+    field
+       Subterm : Regex Σ
+       sub     : issub R Subterm fin ≡ true
+
 regex2nfa : {Σ : Set} → Regex Σ → {n : ℕ } (fin : FiniteSet Σ {n}) → NAutomaton (Regex Σ) Σ
 regex2nfa {Σ} (r *) fin = record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } where
           nr0 = regex2nfa r fin
@@ -119,7 +151,7 @@
 
 test-r4 = regex2nfa  (< i0 > & < i1 >) finIn2 
 
-testr5 = Naccept test-r4 {!!} ( i0  ∷ i1  ∷ [] )
+-- testr5 = Naccept test-r4 {!!} ( i0  ∷ i1  ∷ [] )