Mercurial > hg > Members > kono > Proof > automaton

changeset 383:708570e55a91

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add regex2 (we need source reorganization)
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 25 Jul 2023 11:26:17 +0900
parents 9fba498b0a7a
children a5c874396cc4
files automaton-in-agda/src/derive.agda automaton-in-agda/src/finiteSetUtil.agda automaton-in-agda/src/regex1.agda automaton-in-agda/src/regex2.agda automaton-in-agda/src/regular-language.agda automaton-in-agda/src/regular-star.agda
diffstat 6 files changed, 130 insertions(+), 18 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/derive.agda	Mon Jul 24 19:01:09 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Tue Jul 25 11:26:17 2023 +0900
@@ -270,10 +270,14 @@
 ... | true = ε
 ... | false = φ
 ISB→Regex φ f = φ
-ISB→Regex (r *) f = {!!}
-ISB→Regex (r & r₁) f = {!!}
-ISB→Regex (r || r₁) f = {!!}
-ISB→Regex < x > f = {!!}
+ISB→Regex (r *) f =  ( ISB→Regex  r (λ i → f record { s = ISB.s i ; is-sub = sub* (ISB.is-sub i) } ) ) *
+ISB→Regex (x & y) f =   ISB→Regex  x (λ i → f record { s = ISB.s i ; is-sub = sub&1 x y _ (ISB.is-sub i) } )   
+                     || ISB→Regex  y (λ i → f record { s = ISB.s i ; is-sub = sub&2 x y _ (ISB.is-sub i) } )   
+ISB→Regex (x || y) f =  ISB→Regex  x (λ i → f record { s = ISB.s i ; is-sub = sub|1 (ISB.is-sub i) } )   
+                     || ISB→Regex  y (λ i → f record { s = ISB.s i ; is-sub = sub|2 (ISB.is-sub i) } )   
+ISB→Regex < x > f with f record { s = < x > ; is-sub = sunit  }
+... | true = < x >
+... | false = φ
 
 lem00 : (r : Regex Σ) → (z : Σ) (x : List Σ )→ regex-language r eq? (z ∷ x ) ≡  
                                                regex-language (ISB→Regex r (λ isb → (sbderive r (toSB r ) z isb)))  eq? x  
--- a/automaton-in-agda/src/finiteSetUtil.agda	Mon Jul 24 19:01:09 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Tue Jul 25 11:26:17 2023 +0900
@@ -133,6 +133,11 @@
 data One : Set where
    one : One
 
+finOne : FiniteSet One
+finOne =  record { finite = 1 ;  Q←F = λ _ → one ; F←Q = λ _ → # 0 ; finiso→ = fin00 ; finiso← = fin1≡0  }  where
+    fin00 : (q : One) → one ≡ q
+    fin00 one = refl
+
 fin-∨1 : {B : Set} → (fb : FiniteSet B ) → FiniteSet (One ∨ B) 
 fin-∨1 {B} fb =  record {
        Q←F = Q←F
--- a/automaton-in-agda/src/regex1.agda	Mon Jul 24 19:01:09 2023 +0900
+++ b/automaton-in-agda/src/regex1.agda	Tue Jul 25 11:26:17 2023 +0900
@@ -11,6 +11,7 @@
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import regex
 open import logic
+open import regular-language
 
 -- postulate a b c d : Set
 
@@ -35,10 +36,10 @@
 open import nfa
 
 --    former ++ later  ≡ x
-split : {Σ : Set} → (x : List Σ → Bool) → (y :  List Σ → Bool) → (z : 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
+-- split : {Σ : Set} → (x : List Σ → Bool) → (y :  List Σ → Bool) → (z : 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
 
 ---   ( a ∷ b ∷ c ∷ [] )
 --
@@ -116,13 +117,13 @@
 test-regex1 = refl
 
                                                                                                                     
-test-AB→split : {Σ : Set} → {A B : List In → Bool} → split A B ( a ∷ b ∷ a ∷ [] ) ≡ (
-       ( A [] /\ B ( a ∷ b ∷ a ∷ [] ) ) \/
-       ( A ( a ∷ [] ) /\ B ( b ∷ a ∷ [] ) ) \/
-       ( A ( a ∷ b ∷ [] ) /\ B ( a ∷ [] ) ) \/
-       ( A ( a ∷ b ∷ a ∷ [] ) /\ B  []  )
-   )
-test-AB→split {_} {A} {B} = refl
+--test-AB→split : {Σ : Set} → {A B : List In → Bool} → split A B ( a ∷ b ∷ a ∷ [] ) ≡ (
+--        ( A [] /\ B ( a ∷ b ∷ a ∷ [] ) ) \/
+--        ( A ( a ∷ [] ) /\ B ( b ∷ a ∷ [] ) ) \/
+--        ( A ( a ∷ b ∷ [] ) /\ B ( a ∷ [] ) ) \/
+--        ( A ( a ∷ b ∷ a ∷ [] ) /\ B  []  )
+--    )
+-- test-AB→split {_} {A} {B} = refl
 
 list-eq : {Σ : Set} → (cmpi : (s t : Σ)  → Dec (s ≡ t ))  → (s t : List Σ ) → Bool
 list-eq cmpi [] [] = true
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/automaton-in-agda/src/regex2.agda	Tue Jul 25 11:26:17 2023 +0900
@@ -0,0 +1,86 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+
+open import Relation.Binary.PropositionalEquality hiding ( [_] )
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Data.List hiding ( [_] )        
+open import Data.Empty                 
+open import finiteSet
+open import finiteSetUtil
+open import fin
+
+module regex2 ( Σ : Set) ( fin : FiniteSet Σ ) ( eq? : (x y : Σ) → Dec (x ≡ y)) where
+
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Data.Fin hiding ( pred )
+open import Data.Nat hiding ( _≟_ )
+open import Data.List hiding ( any ;  [_] )
+-- import Data.Bool using ( Bool ; true ; false ; _∧_ )
+-- open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
+open import  Relation.Binary.PropositionalEquality as RBF hiding ( [_] ) 
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import regex
+open import regular-language
+open import automaton
+open import regex1
+open import logic
+
+open import regular-star 
+open import regular-concat 
+
+open Automaton
+open FiniteSet
+
+open RegularLanguage
+
+regex→RegularLanguage : Regex Σ → RegularLanguage Σ
+regex→RegularLanguage ε = record { states = One ∨ One ; astart = case1 one ; afin = fin-∨1 finOne
+    ; automaton = record { δ = λ _ _ → case2 one ; aend = rg00 } } where
+      rg00 : One ∨ One → Bool
+      rg00 (case1 one) = true
+      rg00 (case2 one) = false
+regex→RegularLanguage φ = record { states = One ; astart = one ; afin = finOne ; automaton = record { δ = λ _ _ → one ; aend = λ _ → false } }
+regex→RegularLanguage (r *) = M-Star ( regex→RegularLanguage r )
+regex→RegularLanguage (r & r₁) = M-Concat ( regex→RegularLanguage r ) (regex→RegularLanguage r₁ )
+regex→RegularLanguage (r || r₁) = M-Union ( regex→RegularLanguage r ) (regex→RegularLanguage r₁ )
+regex→RegularLanguage < x > = record { states = One ∨ One ∨ One ; astart = case1 one ; afin = fin-∨1 (fin-∨1 finOne)
+     ; automaton = record { δ = rg01 ; aend = rg00 } } where
+      rg00 : One ∨ One ∨ One → Bool
+      rg00 (case1 one) = false             -- empty case failure
+      rg00 (case2 (case1 one)) = true      -- may true on this phase
+      rg00 (case2 (case2 one)) = false     -- no success never after
+      rg01 : One ∨ One ∨ One → Σ → One ∨ One ∨ One
+      rg01 (case1 one) s with eq? s x
+      ... | yes _  = case2 (case1 one)
+      ... | no _   = case2 (case2 one)
+      rg01 (case2 (case1 one)) s = case2 (case2 one)
+      rg01 (case2 (case2 one)) s = case2 (case2 one)
+
+
+open Split
+
+open _∧_
+
+open import Data.List.Properties
+
+regex-concat : {a b : Regex Σ} → (x : List Σ) → regex-language (a & b) eq? x ≡ Concat (regex-language a eq?) (regex-language b eq?) x
+regex-concat  {_} {_} x = refl
+
+open import sbconst2
+
+regex-is-regular :  (r : Regex Σ ) → ( x : List Σ ) → isRegular (regex-language r eq?)  x ( regex→RegularLanguage r  )
+regex-is-regular r x = rg00 r x where
+      rg00 : (r : Regex Σ) → (x : List Σ) →   regex-language r eq? x ≡ accept (automaton (regex→RegularLanguage r)) (astart (regex→RegularLanguage r)) x 
+      rg00 ε x = ?
+      rg00 φ x = ?
+      rg00 (r *) x = ?
+      rg00 (r & r₁) x = begin
+              split (regex-language r eq?) (regex-language r₁ eq?) x ≡⟨ cong₂ (λ j k → Concat j k x) 
+                   (f-extensionality (rg00 r)) (f-extensionality (rg00 r₁))   ⟩
+              Concat (contain (regex→RegularLanguage r)) (contain (regex→RegularLanguage r₁)) x 
+                  ≡⟨  closed-in-concat (regex→RegularLanguage r) (regex→RegularLanguage r₁) x ⟩
+              contain (M-Concat (regex→RegularLanguage r) (regex→RegularLanguage r₁)) x  ∎
+                 where open ≡-Reasoning
+      rg00 (r || r₁) x = ?
+      rg00 < s > x = ?
+
+-- end
--- a/automaton-in-agda/src/regular-language.agda	Mon Jul 24 19:01:09 2023 +0900
+++ b/automaton-in-agda/src/regular-language.agda	Tue Jul 25 11:26:17 2023 +0900
@@ -32,9 +32,19 @@
 Concat {Σ} A B = split A B
 
 {-# TERMINATING #-}
-Star : {Σ : Set} → ( A : language {Σ} ) → language {Σ}
-Star {Σ} A [] = true
-Star {Σ} A (h ∷ t) = split A ( Star {Σ} A ) (h ∷ t)
+Star1 : {Σ : Set} → ( A : language {Σ} ) → language {Σ}
+Star1 {Σ} A [] = true
+Star1 {Σ} A (h ∷ t) = split A ( Star1 {Σ} A ) (h ∷ t)
+
+Star : {Σ : Set} → (x : List Σ → Bool) → (y : List Σ ) → Bool 
+Star {Σ} x [] = true
+Star {Σ} x (h ∷ y) = repeat2 [] (h ∷ y) where
+    repeat2 : (pre y : List Σ ) → Bool
+    repeat2 pre [] = false
+    repeat2 pre (h ∷ y) = 
+       (x (pre ++ (h ∷ [])) /\ Star x y )
+       \/ repeat2 (pre ++ (h ∷ [])) y 
+
 
 open import automaton-ex
 
--- a/automaton-in-agda/src/regular-star.agda	Mon Jul 24 19:01:09 2023 +0900
+++ b/automaton-in-agda/src/regular-star.agda	Tue Jul 25 11:26:17 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+
 module regular-star where
 
 open import Level renaming ( suc to Suc ; zero to Zero )
@@ -27,6 +29,10 @@
 
 open RegularLanguage
 
+--
+--   Star (contain A) = Concat (contain A) ( Star (contain A ) ) \/ Empty
+--
+
 Star-NFA :  {Σ : Set} → (A : RegularLanguage Σ ) → NAutomaton (states A ) Σ 
 Star-NFA {Σ} A  = record { Nδ = δnfa ; Nend = nend } 
    module Star-NFA where