Mercurial > hg > Members > kono > Proof > automaton

changeset 335:ce4e44cee2d3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 09 Jul 2023 15:37:18 +0900
parents 1466e18c8180
children 1bf4163de311
files automaton-in-agda/src/automaton-ex.agda automaton-in-agda/src/automaton.agda automaton-in-agda/src/bijection.agda automaton-in-agda/src/cfg.agda automaton-in-agda/src/cfg1.agda automaton-in-agda/src/chap0.agda automaton-in-agda/src/derive.agda automaton-in-agda/src/deriveUtil.agda automaton-in-agda/src/even.agda automaton-in-agda/src/extended-automaton.agda automaton-in-agda/src/fin.agda automaton-in-agda/src/finiteSet.agda automaton-in-agda/src/finiteSetUtil.agda automaton-in-agda/src/flcagl.agda automaton-in-agda/src/gcd.agda automaton-in-agda/src/halt.agda automaton-in-agda/src/index.ind automaton-in-agda/src/induction-ex.agda automaton-in-agda/src/lang-text.agda automaton-in-agda/src/libbijection.agda automaton-in-agda/src/logic.agda automaton-in-agda/src/nat.agda automaton-in-agda/src/nfa.agda automaton-in-agda/src/nfa136.agda automaton-in-agda/src/non-regular.agda automaton-in-agda/src/omega-automaton.agda automaton-in-agda/src/prime.agda automaton-in-agda/src/pushdown.agda automaton-in-agda/src/puzzle.agda automaton-in-agda/src/regex.agda automaton-in-agda/src/regex1.agda automaton-in-agda/src/regular-concat.agda automaton-in-agda/src/regular-language.agda automaton-in-agda/src/regular-star.agda automaton-in-agda/src/root2.agda automaton-in-agda/src/sbconst2.agda automaton-in-agda/src/temporal-logic.agda automaton-in-agda/src/turing.agda automaton-in-agda/src/utm.agda
diffstat 3 files changed, 44 insertions(+), 103 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/derive.agda	Tue Mar 21 08:23:44 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Sun Jul 09 15:37:18 2023 +0900
@@ -7,15 +7,9 @@
 
 module derive ( Σ : Set) ( fin : FiniteSet Σ ) ( eq? : (x y : Σ) → Dec (x ≡ y)) where
 
--- open import nfa
-open import Data.Nat
--- open import Data.Nat hiding ( _<_ ; _>_ )
--- open import Data.Fin hiding ( _<_ )
-open import finiteSetUtil
 open import automaton
 open import logic
 open import regex
-open FiniteSet
 
 -- whether a regex accepts empty input
 --
@@ -37,7 +31,7 @@
 derivative (x & y) s with empty? x
 ... | true with derivative x s | derivative y s
 ... | ε | φ = φ
-... | ε | t = y || t
+... | ε | t = t || y
 ... | φ | t = t
 ... | x1 | φ = x1 & y
 ... | x1 | y1 = (x1 & y) || y1
@@ -64,6 +58,22 @@
 
 open Derivative
 
+derive-step : (r : Regex   Σ) (d0 : Derivative r) → (s : Σ) → regex-states r (derivative (state d0) s)
+derive-step r d0 s = derive (is-derived d0) s
+
+regex→automaton : (r : Regex   Σ) → Automaton (Derivative r) Σ
+regex→automaton r = record { δ = λ d s → record { state = derivative (state d) s ; is-derived = derive-step r d s} 
+   ; aend = λ d → empty? (state d) }  
+
+regex-match : (r : Regex   Σ) →  (List Σ) → Bool
+regex-match ex is = accept ( regex→automaton ex ) record { state =  ex ; is-derived = unit } is 
+
+-- open import nfa
+open import Data.Nat
+-- open import Data.Nat hiding ( _<_ ; _>_ )
+-- open import Data.Fin hiding ( _<_ )
+open import finiteSetUtil
+open FiniteSet
 open import Data.Fin hiding (_<_)
 
 -- derivative generates   (x & y) || ... form. y and x part is a substerm of original regex
@@ -76,102 +86,31 @@
 -- in case of automaton, number of derivative is limited by iteration of input length, so it is finite.
 -- so we cannot say derived automaton is finite i.e. regex-match is regular language now
 
-regex→automaton : (r : Regex   Σ) → Automaton (Derivative r) Σ
-regex→automaton r = record { δ = λ d s → record { state = derivative (state d) s ; is-derived = derive-step d s} ; aend = λ d → empty? (state d) }  where
-    derive-step : (d0 : Derivative r) → (s : Σ) → regex-states r (derivative (state d0) s)
-    derive-step d0 s = derive (is-derived d0) s
-
-regex-match : (r : Regex   Σ) →  (List Σ) → Bool
-regex-match ex is = accept ( regex→automaton ex ) record { state =  ex ; is-derived = unit } is 
-
 open import Relation.Binary.Definitions
 
-cmp-regex : (x y : Regex Σ) → Dec ( x ≡ y )
-cmp-regex ε ε = yes refl
-cmp-regex ε φ = no (λ ())
-cmp-regex ε (y *) = no (λ ())
-cmp-regex ε (y & y₁) = no (λ ())
-cmp-regex ε (y || y₁) = no (λ ())
-cmp-regex ε < x > = no (λ ())
-cmp-regex φ ε = no (λ ())
-cmp-regex φ φ = yes refl
-cmp-regex φ (y *) =  no (λ ())
-cmp-regex φ (y & y₁) =  no (λ ())
-cmp-regex φ (y || y₁) =  no (λ ())
-cmp-regex φ < x > =  no (λ ())
-cmp-regex (x *) ε =  no (λ ())
-cmp-regex (x *) φ =  no (λ ())
-cmp-regex (x *) (y *) with cmp-regex x y
-... | yes refl = yes refl
-... | no ne = no (λ x → ne (cmp1 x)) where
-   cmp1 : (x *) ≡ (y *) → x ≡ y
-   cmp1 refl = refl
-cmp-regex (x *) (y & y₁) = no (λ ())
-cmp-regex (x *) (y || y₁) = no (λ ())
-cmp-regex (x *) < x₁ > = no (λ ())
-cmp-regex (x & x₁) ε = no (λ ())
-cmp-regex (x & x₁) φ = no (λ ())
-cmp-regex (x & x₁) (y *) = no (λ ())
-cmp-regex (x & x₁) (y & y₁) with cmp-regex x y | cmp-regex x₁ y₁ 
-... | yes refl | yes refl = yes refl
-... | no ne | _ = no (λ x → ne (cmp1 x)) where
-   cmp1 :  x & x₁ ≡ y & y₁ → x ≡ y
-   cmp1 refl = refl
-... | _ | no ne  = no (λ x → ne (cmp1 x)) where
-   cmp1 :  x & x₁ ≡ y & y₁ → x₁ ≡ y₁
-   cmp1 refl = refl
-cmp-regex (x & x₁) (y || y₁) = no (λ ())
-cmp-regex (x & x₁) < x₂ > = no (λ ())
-cmp-regex (x || x₁) ε = no (λ ())
-cmp-regex (x || x₁) φ = no (λ ())
-cmp-regex (x || x₁) (y *) = no (λ ())
-cmp-regex (x || x₁) (y & y₁) = no (λ ())
-cmp-regex (x || x₁) (y || y₁) with cmp-regex x y | cmp-regex x₁ y₁ 
-... | yes refl | yes refl = yes refl
-... | no ne | _ = no (λ x → ne (cmp1 x)) where
-   cmp1 :  x || x₁ ≡ y || y₁ → x ≡ y
-   cmp1 refl = refl
-... | _ | no ne  = no (λ x → ne (cmp1 x)) where
-   cmp1 :  x || x₁ ≡ y || y₁ → x₁ ≡ y₁
-   cmp1 refl = refl
-cmp-regex (x || x₁) < x₂ > = no (λ ())
-cmp-regex < x > ε = no (λ ())
-cmp-regex < x > φ = no (λ ())
-cmp-regex < x > (y *) = no (λ ())
-cmp-regex < x > (y & y₁) = no (λ ())
-cmp-regex < x > (y || y₁) = no (λ ())
-cmp-regex < x > < x₁ > with equal? fin x x₁ | inspect ( equal? fin x ) x₁
-... | false | record { eq = eq } = no (λ x → ¬-bool eq (cmp1 x)) where
-   cmp1 :  < x > ≡ < x₁ > →  equal? fin x x₁ ≡ true 
-   cmp1 refl = equal?-refl fin
-... | true | record { eq = eq } with equal→refl fin eq
-... | refl = yes refl
+data SB : (r s : Regex Σ) → Set where
+    sbε : SB ε ε
+    sbφ : SB φ φ
+    sb*x : (x : Regex Σ) → SB (x *) x
+    sb*  : (x : Regex Σ) → SB (x *) (x *)
+    sb&x : (x y : Regex Σ) → SB (x & y) x
+    sb&y : (x y : Regex Σ) → SB (x & y) y
+    sb& : (x y : Regex Σ) → SB (x & y) (x & y)
+    sb|x : (x y : Regex Σ) → SB (x || y) x
+    sb|y : (x y : Regex Σ) → SB (x || y) y
+    sb| : (x y : Regex Σ) → SB (x || y) (x || y)
+    sb<> : (x : Σ) → SB < x > < x >
 
-insert : List (Regex Σ) → (Regex Σ) → List (Regex Σ) 
-insert [] k = k ∷ []
-insert (x ∷ t) k with cmp-regex k x
-... | no n = x ∷ (insert t k) 
-... | yes y = x ∷ t
+record SBS (r : Regex Σ) : Set where
+   field
+      s : Regex Σ
+      sb : SB r s
 
-regex-derive : List (Regex Σ) → List (Regex Σ)
-regex-derive t = regex-derive0 t t where
-   regex-derive1 : Regex Σ → List Σ → List (Regex Σ) → List (Regex Σ)
-   regex-derive1 x [] t = t
-   regex-derive1 x (i ∷ t) r =  regex-derive1 x t (insert r (derivative x i))
-   regex-derive0 :  List (Regex Σ)  → List (Regex Σ) → List (Regex Σ)
-   regex-derive0 [] t = t
-   regex-derive0 (x ∷ r) t = regex-derive0 r (regex-derive1 x (to-list fin (λ _ → true)) t) 
+SBTA : (r : Regex Σ) → Automaton (SBS r) Σ
+SBTA = ?
 
---
--- if (Derivative r is finite,  regex→automaton is finite
---
--- drive-is-finite : (r : Regex   Σ) → FiniteSet (Derivative r) 
--- drive-is-finite ε = {!!}
--- drive-is-finite φ = {!!}
--- drive-is-finite (r *) = {!!} where
---    d1 :  FiniteSet (Derivative r )
---    d1 = drive-is-finite r
--- drive-is-finite (r & r₁) = {!!}
--- drive-is-finite (r || r₁) = {!!}
--- drive-is-finite < x > = {!!}
--- 
+finie-deverive : (r : Regex Σ) → (c : Σ) → (x : List Σ) → regex-match r x ≡ true → accept (SBTA r) ? x ≡ true
+finie-deverive = ?
+
+
+
--- a/automaton-in-agda/src/fin.agda	Tue Mar 21 08:23:44 2023 +0900
+++ b/automaton-in-agda/src/fin.agda	Sun Jul 09 15:37:18 2023 +0900
@@ -295,3 +295,5 @@
            -- if the list without the max element is only one length shorter, we can recurse
            fdup : FDup-in-list n (list-less qs)
            fdup = fin-dup-in-list>n (list-less qs) (fless qs lt ne)
+
+--
--- a/automaton-in-agda/src/omega-automaton.agda	Tue Mar 21 08:23:44 2023 +0900
+++ b/automaton-in-agda/src/omega-automaton.agda	Sun Jul 09 15:37:18 2023 +0900
@@ -47,7 +47,7 @@
 open  Muller 
 --  always sometimes p
 --
---                       not p
+--                       not p 
 --                   ------------>
 --        [] <> p *                 [] <> p 
 --                   <-----------
@@ -183,7 +183,7 @@
           ( not ( flip-seq n ) )
        ∎
 
-flip-dec2 : (n : ℕ ) → not flip-seq (suc n)  ≡  flip-seq n 
+flip-dec2 : (n : ℕ ) → ? -- not flip-seq (suc n)  ≡  flip-seq n 
 flip-dec2 n = {!!}