Mercurial > hg > Members > kono > Proof > automaton

changeset 34:a904b6bc76af

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add regular language
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 06 Nov 2018 12:50:11 +0900
parents f163122da10c
children 95f2e129cf9e
files agda/epautomaton.agda agda/nfa.agda agda/regex1.agda agda/sbconst1.agda
diffstat 4 files changed, 94 insertions(+), 36 deletions(-) [+]
line wrap: on
line diff
--- a/agda/epautomaton.agda	Mon Nov 05 21:56:44 2018 +0900
+++ b/agda/epautomaton.agda	Tue Nov 06 12:50:11 2018 +0900
@@ -9,7 +9,7 @@
 open import Relation.Nullary using (¬_; Dec; yes; no)
 
 open import automaton
-
+open import nfa-list
 
 nth : {S : Set } →  ℕ → List S → Maybe S
 nth _ [] = nothing
--- a/agda/nfa.agda	Mon Nov 05 21:56:44 2018 +0900
+++ b/agda/nfa.agda	Tue Nov 06 12:50:11 2018 +0900
@@ -30,41 +30,6 @@
 
 open NAutomaton
 
-Nmoves1 : { Q : Set } { Σ : Set  }
-    → NAutomaton Q  Σ
-    →  ∀ {q : Q} → ( (q : Q ) → Bool )  → Σ → Q → Bool
-Nmoves1 {Q} { Σ} M {q'} Qs  s q  = (Qs q') ∧ ( Nδ M q' s q ) 
-
-Naccept2 : { Q : Set } { Σ : Set  } 
-    → NAutomaton Q  Σ
-    → List  Σ  → {q : Q} → Bool
-Naccept2 {Q} {Σ} M input {q} = Naccept3 M ( Nstart M ) input {q}
-   where
-      Naccept3 : NAutomaton Q  Σ → ( Q → Bool ) →  List  Σ  → {q : Q} →  Bool
-      Naccept3 M sb []  {q} =  sb q ∧ Nend M q
-      Naccept3 M sb (i ∷ t ) {q} = Naccept3 M ( Nmoves1 M {q} sb i ) t {q}
-
-record FiniteSet' ( Q : Set ) { n : ℕ }
-        : Set  where
-     field
-        Q←F : (m : ℕ) → m < n  → Q
-        F←Q : Q → ℕ 
-        F←Q<n :  ∀{q : Q } → F←Q q < n
-        finiso→ : (q : Q) → Q←F ( F←Q q ) F←Q<n  ≡ q
-        finiso← : (f : ℕ ) → (f<n : f < n ) → F←Q ( Q←F f f<n) ≡ f
-     lt0 : (n : ℕ) →  n Data.Nat.≤ n
-     lt0 zero = z≤n
-     lt0 (suc n) = s≤s (lt0 n)
-     lt2 : {m n : ℕ} → m  < n →  m Data.Nat.≤ n
-     lt2 {zero} lt = z≤n
-     lt2 {suc m} {zero} ()
-     lt2 {suc m} {suc n} (s≤s lt) = s≤s (lt2 lt)
-     exists : ( Q → Bool ) → Bool
-     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 m m<n ) ∨ exists1 m (lt2 m<n) p
-
 record FiniteSet ( Q : Set ) { n : ℕ }
         : Set  where
      field
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/regex1.agda	Tue Nov 06 12:50:11 2018 +0900
@@ -0,0 +1,92 @@
+module regex1 where
+
+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.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
+open import  Relation.Binary.PropositionalEquality as RBF hiding ( [_] ) 
+open import Relation.Nullary using (¬_; Dec; yes; no)
+
+
+data Regex   ( Σ : Set  ) : Set  where
+   _*    : Regex  Σ → Regex  Σ
+   _&_   : Regex  Σ → Regex  Σ → Regex Σ
+   _||_  : Regex  Σ → Regex  Σ → Regex Σ
+   <_>   : Σ → Regex  Σ
+
+open import nfa
+
+_‖_ : {Σ : Set} ( x y : List Σ → Bool) → List Σ → Bool
+x ‖ y = λ s → x s ∨ y s
+
+
+split : {Σ : Set} → (List Σ → Bool)
+      → ( List Σ → Bool) → List Σ → Bool
+split x y  [] = x [] ∧ y []
+split x y (h  ∷ t) = (x [] ∧ y (h  ∷ t)) ∨
+  split (λ t1 → x ( ( h ∷ [] ) ++ t1 ))  (λ t2 → y t2 ) t
+
+_・_ : {Σ : Set} → ( x y : List Σ → Bool) → List Σ → Bool
+x ・ y = λ z → split x y z
+
+{-# TERMINATING #-}
+repeat : {Σ : Set} → (List Σ → Bool) → List Σ → Bool
+repeat x [] = true
+repeat {Σ} x ( h  ∷ t ) = split x (repeat {Σ} x) ( h  ∷ t )
+
+open FiniteSet
+
+cmpi :  {Σ : Set} → {n : ℕ } (fin : FiniteSet Σ {n}) → (x y : Σ ) → Dec (F←Q fin x ≡  F←Q fin y) 
+cmpi fin x y = F←Q fin x ≟  F←Q fin y 
+
+regular-language : {Σ : Set} → Regex Σ → {n : ℕ } (fin : FiniteSet Σ {n}) →  List Σ → Bool
+regular-language (x *) f = repeat ( regular-language x f )
+regular-language (x & y) f = ( regular-language x f ) ・ ( regular-language y f )
+regular-language (x || y) f = ( regular-language x f ) ‖ ( regular-language y f )
+regular-language < h > f [] = false
+regular-language < h > f (h1  ∷ [] ) with cmpi f h h1
+... | yes _ = true
+... | no _  = false
+regular-language < h > f _ = false
+
+finIn2 : FiniteSet In2
+finIn2 = record {
+        Q←F = Q←F'
+      ; F←Q  = F←Q'
+      ; finiso→ = finiso→'
+      ; finiso← = finiso←'
+   } where
+       Q←F' : Fin 2 → In2
+       Q←F' zero = i0
+       Q←F' (suc zero) = i1
+       Q←F' (suc (suc ())) 
+       F←Q' : In2 → Fin 2
+       F←Q' i0 = zero
+       F←Q' i1 = suc (zero)
+       finiso→' : (q : In2) → Q←F' (F←Q' q) ≡ q
+       finiso→' i0 = refl
+       finiso→' i1 = refl
+       finiso←' : (f : Fin 2) → F←Q' (Q←F' f) ≡ f
+       finiso←' zero = refl
+       finiso←' (suc zero) = refl
+       finiso←' (suc (suc ()))
+
+
+test-r1 = < i0 > & < i1 >
+test-r2 = regular-language (< i0 > & < i1 >) finIn2 ( i0  ∷ i1  ∷ [] )
+test-r3 = regular-language (< i0 > & < i1 >) finIn2 ( i0  ∷ i0  ∷ [] )
+
+regex2nfa : {Σ : Set} → Regex Σ → {n : ℕ } {fin : FiniteSet Σ {n}} → NAutomaton (Regex Σ) Σ
+regex2nfa {Σ} r {n} {fin} = record {
+          Nδ     = Nδ
+      ;   Nstart = Nstart
+      ;   Nend   = Nend
+  } where
+          Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
+          Nδ = {!!}
+          Nstart : (Regex Σ) → Bool
+          Nstart = {!!}
+          Nend  :  (Regex Σ) → Bool
+          Nend  = {!!}
+
--- a/agda/sbconst1.agda	Mon Nov 05 21:56:44 2018 +0900
+++ b/agda/sbconst1.agda	Tue Nov 06 12:50:11 2018 +0900
@@ -13,6 +13,7 @@
 
 
 open import automaton
+open import nfa-list
 open Automaton
 open NAutomaton