Mercurial > hg > Members > kono > Proof > automaton

changeset 398:d7ea37e49f35

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, 06 Aug 2023 00:03:48 +0900
parents 2e22a1f3a55a
children 1cff8b68578a
files automaton-in-agda/src/derive.agda automaton-in-agda/src/sbconst2.agda
diffstat 2 files changed, 80 insertions(+), 23 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/derive.agda	Thu Aug 03 18:13:59 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Sun Aug 06 00:03:48 2023 +0900
@@ -158,6 +158,9 @@
 rank (r || r₁) = max (rank r) (rank r₁)
 rank < x > = 0
 
+--
+-- s is subterm of r
+--
 data SB : (r s : Regex Σ) → Set where
     sε  : SB ε ε
     sφ  : SB φ φ
@@ -167,9 +170,12 @@
     sub*   : {x y : Regex Σ} → SB x y  → SB (x *) y
     sub&1  : (x y z : Regex Σ) → SB x z → SB (x & y) z
     sub&2  : (x y z : Regex Σ) → SB y z → SB (x & y) z
-    sub*&  : (x y : Regex Σ) → rank x < rank y  → SB y x → SB (y *) (x & (y *)) 
-    sub&&  : (x y z : Regex Σ) → rank z < rank (x & z)  → SB (x & y) z → SB (x & y) (z & y) 
+    sub*&  : (x y : Regex Σ)   → rank x < rank y  → SB y x       → SB (y *)   (x & (y *)) 
+    sub&&  : (x y z : Regex Σ) → rank z < rank x  → SB (x & y) z → SB (x & y) (z & y) 
 
+--
+-- set of subterm of s
+--
 record ISB (r : Regex Σ) : Set where
     field
         s : Regex Σ
@@ -236,33 +242,76 @@
 ... | yes _ = true
 ... | no _ = false
 
+-- whether one of subset of subterm accepts empty input
+-- in case of empty set, return true
+--
 sbempty? : (r : Regex Σ) → (ISB r → Bool) → Bool
 sbempty? ε f with f record { s = ε ; is-sub = sε  }
 ... | true = true
-... | false = false
-sbempty? φ f = false
-sbempty? (r *) f with f record { s = r * ; is-sub = sub* ?  }
-... | true = true 
-... | false = false 
-sbempty? (r & r₁) f with f record { s = r & r₁ ; is-sub = sub&& ? ? ? ? ? }
-... | false = false
-... | true = empty? r /\ empty? r₁
-sbempty? (r || r₁) f with f record { s = r || r₁ ; is-sub = ? }
-... | false = false
-... | true = empty? r \/ empty? r₁ 
-sbempty? < x > f = false
+... | false = true
+sbempty? φ f with f record { s = φ ; is-sub = sφ  }
+... | true = false
+... | false = true
+sbempty? (r *) f = true
+sbempty? (r & r₁) f = ? where
+   sb01 : (isb : ISB (r & r₁)) → ( ISB.is-sub isb ≡ sub&1 _ _ _ ? ) 
+        ∨ ( ISB.is-sub isb ≡ sub&2 _ _ _ ? )
+        ∨ ( ISB.is-sub isb ≡ subst (λ k → SB ? ?) ? (sub&& _ _ _ ? ? ))
+   sb01 isb with ISB.is-sub isb | inspect ISB.is-sub isb 
+   ... | sub&1 .r .r₁ .(ISB.s isb) t | record { eq = refl } = case1 refl
+   ... | sub&2 .r .r₁ .(ISB.s isb) t | record { eq = refl } = case2 (case1 refl)
+   ... | sub&& .r .r₁ z x t | record { eq = refl } = case2 (case2 refl)
+   sb00 : ISB r → Bool
+   sb00 record { s = s ; is-sub = is-sub } = f record { s = s ; is-sub = sub&1 _ _ _ is-sub }
+sbempty? (r || r₁) f with f record { s = r ; is-sub = sub|1 ? } | f record { s = r₁ ; is-sub = sub|2 ? }
+... | false | t = true
+... | true | t = empty? r \/ empty? r₁ 
+sbempty? < x > f with f record { s = < x > ; is-sub = s<> }
+... | false = true
+... | true = false
 
 sbderive : (r : Regex Σ) →  (ISB r → Bool) → Σ → ISB r → Bool
 sbderive ε f s record { s = .ε ; is-sub = sε } = false
 sbderive φ f s record { s = t ; is-sub = sφ } = false
-sbderive (r *) f s record { s = t ; is-sub = (sub* is-sub) } = ?
-sbderive (r *) f s record { s = .(x & (r *)) ; is-sub = (sub*& x .r x₁ is-sub) } = ?
-sbderive (r & r₁) f s record { s = t ; is-sub = (sub&1 .r .r₁ .t is-sub) } = ?
-sbderive (r & r₁) f s record { s = t ; is-sub = (sub&2 .r .r₁ .t is-sub) } = ?
+sbderive (r *) f s record { s = t ; is-sub = sub* is-sub } with f record { s = t ; is-sub = sub* is-sub } 
+... | false = true
+... | true with derivative r s
+... | ε = true
+... | φ = false
+... | t₁ * = false
+... | t₁ & t₂ = false
+... | t₁ || t₂ = false
+... | < x > = false
+sbderive (r *) f s record { s = .(x & (r *)) ; is-sub = sub*& x .r x₁ is-sub } with f record { s = (x & (r *)) ; is-sub = sub*& x r x₁ is-sub } 
+... | false = true
+... | true with derivative r s
+... | ε = false
+... | φ = false
+... | t₁ * = true
+... | t₁ & t₂ = true
+... | t₁ || t₂ = true
+... | < s > = true
+sbderive (r & r₁) f s record { s = t ; is-sub = sub&1 .r .r₁ .t is-sub } with f record { s = t ; is-sub = sub&1 r r₁ t is-sub } 
+... | false = true
+... | true = false
+sbderive (r & r₁) f s record { s = t ; is-sub = sub&2 .r .r₁ .t is-sub } with f record { s = t ; is-sub = sub&2 r r₁ t is-sub } f 
+... | false = true
+... | true with derivative r s | derivative r₁ s
+... | ε | φ = false
+... | ε | t = true
+... | φ | t = false
+... | x1 | φ = false
+... | x1 | y1 = false
 sbderive (r & r₁) f s record { s = .(z & r₁) ; is-sub = (sub&& .r .r₁ z x is-sub) } = ?
-sbderive (r || r₁) f s₁ record { s = s ; is-sub = (sub|1 is-sub) } = ?
-sbderive (r || r₁) f s₁ record { s = s ; is-sub = (sub|2 is-sub) } = ?
-sbderive < x > f s record { s = t ; is-sub = is-sub } = ?
+sbderive (r || r₁) f s₁ record { s = s ; is-sub = (sub|1 is-sub) } = sbderive r sb00 s₁  record { s = s ; is-sub = is-sub } where
+    sb00 : ISB r → Bool 
+    sb00 record { s = s ; is-sub = is-sub } = f record { s = s ; is-sub = sub|1 is-sub } 
+sbderive (r || r₁) f s₁ record { s = s ; is-sub = (sub|2 is-sub) } = sbderive r₁ sb00 s₁  record { s = s ; is-sub = is-sub } where
+    sb00 : ISB r₁ → Bool 
+    sb00 record { s = s ; is-sub = is-sub } = f record { s = s ; is-sub = sub|2 is-sub } 
+sbderive < x > f s record { s = .(< x >) ; is-sub = s<> } with eq? x s
+... | yes _  = false
+... | no _  = false
 
 -- finDerive : (r : Regex Σ) → FiniteSet (Derived r)
 --    this is not correct because it contains s || s || s || .....
@@ -310,10 +359,10 @@
 derive=ISB (r *) x = ?
 derive=ISB (r & r₁) x = ?
 derive=ISB (r || r₁) x = ?
-derive=ISB < x₁ > [] = refl
+derive=ISB < x₁ > [] = ?
 derive=ISB < x₁ > (x ∷ []) with eq? x₁ x
 ... | yes _ = ?
-... | no _ = refl
+... | no _ = ?
 derive=ISB < x₁ > (x ∷ x₂ ∷ x₃) = ?
 
 ISB-is-regex-language : (r : Regex Σ) → (x : List Σ )→ regex-language r eq? x ≡  regex-match1 r x
--- a/automaton-in-agda/src/sbconst2.agda	Thu Aug 03 18:13:59 2023 +0900
+++ b/automaton-in-agda/src/sbconst2.agda	Sun Aug 06 00:03:48 2023 +0900
@@ -29,6 +29,14 @@
      ;  aend = λ f → exists ( λ q → f q /\ Nend NFA q )
    } 
 
+subset-construction' : { Q : Set } { Σ : Set  } → 
+    ( ( Q → Bool ) → Bool ) →
+    (NAutomaton Q  Σ ) → (Automaton (Q → Bool)  Σ )  
+subset-construction' {Q} { Σ}  exists NFA = record {
+        δ = λ f i q → exists ( λ r → f r /\ Nδ   NFA r i q )
+     ;  aend = λ f  → exists ( λ q → f q /\ Nend NFA q )
+   } 
+
 test4 = subset-construction existsS1 am2 
 
 test51 = accept test4 start1 ( i0  ∷ i1  ∷ i0  ∷ [] )