Mercurial > hg > Members > kono > Proof > automaton
changeset 270:dd98e7e5d4a5
derive worked but finiteness is difficult
add regular star
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 26 Nov 2021 20:02:06 +0900 |
| parents | 52ed73a116d0 |
| children | 5e066b730d73 |
| files | automaton-in-agda/src/derive.agda automaton-in-agda/src/nfa.agda automaton-in-agda/src/regular-concat.agda automaton-in-agda/src/regular-star.agda |
| diffstat | 4 files changed, 100 insertions(+), 53 deletions(-) [+] |
line wrap: on
line diff
--- a/automaton-in-agda/src/derive.agda Fri Nov 26 09:58:19 2021 +0900 +++ b/automaton-in-agda/src/derive.agda Fri Nov 26 20:02:06 2021 +0900 @@ -12,7 +12,7 @@ -- open import Data.Fin hiding ( _<_ ) open import finiteSet -open import FSetUtil +open import finiteSetUtil open import automaton open import logic open import regex @@ -25,18 +25,6 @@ empty? (x || y) = empty? x \/ empty? y empty? < x > = false -derivative0 : Regex Σ → Σ → Regex Σ -derivative0 ε s = φ -derivative0 φ s = φ -derivative0 (x *) s = derivative0 x s & (x *) -derivative0 (x & y) s with empty? x -... | true = (derivative0 x s & y) || derivative0 y s -... | false = derivative0 x s & y -derivative0 (x || y) s = derivative0 x s || derivative0 y s -derivative0 < x > s with eq? x s -... | yes _ = ε -... | no _ = φ - derivative : Regex Σ → Σ → Regex Σ derivative ε s = φ derivative φ s = φ @@ -74,53 +62,22 @@ open Derivative -open import Data.Fin +open import Data.Fin hiding (_<_) -- derivative generates (x & y) || ... form. y and x part is a substerm of original regex --- since subterm is finite, only finite number of state is negerated, if we normalize ||-list. - -data subterm (r : Regex Σ) : Regex Σ → Set where - sε : subterm r ε - sφ : subterm r φ - orig : subterm r r - x& : {x y : Regex Σ } → subterm r (x & y) → subterm r x - &y : {x y : Regex Σ } → subterm r (x & y) → subterm r y - x| : {x y : Regex Σ } → subterm r (x || y) → subterm r x - |y : {x y : Regex Σ } → subterm r (x || y) → subterm r y - s* : {x : Regex Σ } → subterm r (x *) → subterm r x - s<_> : (s : Σ) → subterm r < s > → subterm r < s > - -record Subterm (r : Regex Σ) : Set where - field - subt : Regex Σ - is-subt : subterm r subt - -finsub : (r : Regex Σ ) → FiniteSet (Subterm r) -finsub ε = {!!} -finsub φ = {!!} -finsub (r *) = {!!} -finsub (r & r₁) = {!!} -finsub (r || r₁) = {!!} -finsub < x > = {!!} - -finsubList : (r : Regex Σ ) → FiniteSet (Subterm r ∧ Subterm r → Bool ) -finsubList r = fin→ ( fin-∧ (finsub r) (finsub r) ) - --- derivative is subset of Subterm r → Subterm r → Bool - -der2ssb : {r : Regex Σ } → Derivative r → Subterm r ∧ Subterm r → Bool -der2ssb = {!!} - --- we cannot say this, because Derivative is redundant --- der2inject : {r : Regex Σ } → (x y : Derivative r ) → ( ( s t : Subterm r ∧ Subterm r ) → der2ssb x s ≡ der2ssb y t ) → x ≡ y - +-- since subterm is finite, only finite number of state is generated for each operator -- this does not work, becuase it depends on input sequences -- finite-derivative : (r : Regex Σ) → FiniteSet Σ → FiniteSet (Derivative r) - +-- order : Regex Σ → ℕ +-- decline-derive : (x : Regex Σ ) (i : Σ ) → 0 < order x → order (derivative x i) < order x +-- is not so easy -- 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
--- a/automaton-in-agda/src/nfa.agda Fri Nov 26 09:58:19 2021 +0900 +++ b/automaton-in-agda/src/nfa.agda Fri Nov 26 20:02:06 2021 +0900 @@ -71,6 +71,18 @@ to-list (λ q → sb q ) ∷ Ntrace M exists to-list (λ q → exists ( λ qn → (sb qn /\ ( Nδ M qn i q ) ))) t +data-fin-00 : ( Fin 3 ) → Bool +data-fin-00 zero = {!!} +data-fin-00 (suc zero) = {!!} +data-fin-00 (suc (suc zero)) = {!!} +data-fin-00 (suc (suc (suc ()))) + +data-fin-01 : (x : ℕ ) → x < 3 → Bool +data-fin-01 zero lt = {!!} +data-fin-01 (suc zero) lt = {!!} +data-fin-01 (suc (suc zero)) lt = {!!} +data-fin-01 (suc (suc (suc x))) (s≤s (s≤s (s≤s ()))) + {-# TERMINATING #-} NtraceDepth : { Q : Set } { Σ : Set } → NAutomaton Q Σ @@ -122,6 +134,7 @@ t-2 = Ntrace am2 existsS1 to-listS1 start1 ( i0 ∷ i1 ∷ i0 ∷ [] ) t-3 = NtraceDepth am2 start1 LStates1 ( i1 ∷ i1 ∷ i1 ∷ [] ) t-4 = NtraceDepth am2 start1 LStates1 ( i0 ∷ i1 ∷ i0 ∷ [] ) +t-5 = NtraceDepth am2 start1 LStates1 ( i0 ∷ [] ) transition4 : States1 → In2 → States1 → Bool transition4 sr i0 sr = true
--- a/automaton-in-agda/src/regular-concat.agda Fri Nov 26 09:58:19 2021 +0900 +++ b/automaton-in-agda/src/regular-concat.agda Fri Nov 26 20:02:06 2021 +0900 @@ -203,7 +203,7 @@ contain-A (h ∷ t) nq fn qa cond with bool-≡-? ((aend (automaton A) qa) /\ accept (automaton B) (δ (automaton B) (astart B) h) t ) true ... | yes eq = bool-or-41 eq -- found A ++ B all end ... | no ne = bool-or-31 (contain-A t (Nmoves NFA (CNFA-exist A B) nq h) fn (δ (automaton A) qa h) lemma11 ) where -- B failed continue with ab-base condtion - --- prove ab-ase condition (we haven't checked but case2 b may happen) + --- prove ab-case condition (we haven't checked but case2 b may happen) lemma11 : (q : states A ∨ states B) → exists finab (λ qn → nq qn /\ Nδ NFA qn h q) ≡ true → ab-case q (δ (automaton A) qa h) t lemma11 (case1 qa') ex with found← finab ex ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S))
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/automaton-in-agda/src/regular-star.agda Fri Nov 26 20:02:06 2021 +0900 @@ -0,0 +1,77 @@ +module regular-star where + +open import Level renaming ( suc to Suc ; zero to Zero ) +open import Data.List +open import Data.Nat hiding ( _≟_ ) +open import Data.Fin hiding ( _+_ ) +open import Data.Empty +open import Data.Unit +open import Data.Product +-- open import Data.Maybe +open import Relation.Nullary +open import Relation.Binary.PropositionalEquality hiding ( [_] ) +open import logic +open import nat +open import automaton +open import regular-language + +open import nfa +open import sbconst2 +open import finiteSet +open import finiteSetUtil +open import Relation.Binary.PropositionalEquality hiding ( [_] ) +open import regular-concat + +open Automaton +open FiniteSet + +open RegularLanguage + +Star-NFA : {Σ : Set} → (A : RegularLanguage Σ ) → NAutomaton (states A ) Σ +Star-NFA {Σ} A = record { Nδ = δnfa ; Nend = nend } + module Star-NFA where + δnfa : states A → Σ → states A → Bool + δnfa q i q₁ with aend (automaton A) q + ... | true = equal? (afin A) ( astart A) q₁ + ... | false = equal? (afin A) (δ (automaton A) q i) q₁ + δnfa _ i _ = false + nend : states A → Bool + nend q = aend (automaton A) q + +Star-NFA-start : {Σ : Set} → (A : RegularLanguage Σ ) → states A → Bool +Star-NFA-start A q = equal? (afin A) (astart A) q \/ aend (automaton A) q + +SNFA-exist : {Σ : Set} → (A : RegularLanguage Σ ) → (states A → Bool) → Bool +SNFA-exist A qs = exists (afin A) qs + +M-Star : {Σ : Set} → (A : RegularLanguage Σ ) → RegularLanguage Σ +M-Star {Σ} A = record { + states = states A → Bool + ; astart = Star-NFA-start A + ; afin = fin→ (afin A) + ; automaton = subset-construction (SNFA-exist A ) (Star-NFA A ) + } + +open Split + +open _∧_ + +open NAutomaton +open import Data.List.Properties + +closed-in-star : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Star (contain A) ) x ( M-Star A ) +closed-in-star {Σ} A B x = ≡-Bool-func closed-in-star→ closed-in-star← where + NFA = (Star-NFA A ) + + closed-in-star→ : Star (contain A) x ≡ true → contain (M-Star A ) x ≡ true + closed-in-star→ star = {!!} + + open Found + + closed-in-star← : contain (M-Star A ) x ≡ true → Star (contain A) x ≡ true + closed-in-star← C with subset-construction-lemma← (SNFA-exist A ) NFA {!!} x C + ... | CC = {!!} + + + +