Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/derive.agda @ 340:b818fbd86d0b
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 10 Jul 2023 14:28:39 +0900 |
| parents | 40f7b6c3d276 |
| children | 9120a5872a5b |
| rev | line source |
|---|---|
| 141 | 1 {-# OPTIONS --allow-unsolved-metas #-} |
| 36 | 2 |
| 44 | 3 open import Relation.Binary.PropositionalEquality hiding ( [_] ) |
| 4 open import Relation.Nullary using (¬_; Dec; yes; no) | |
| 141 | 5 open import Data.List hiding ( [_] ) |
| 271 | 6 open import finiteSet |
| 141 | 7 |
| 271 | 8 module derive ( Σ : Set) ( fin : FiniteSet Σ ) ( eq? : (x y : Σ) → Dec (x ≡ y)) where |
| 141 | 9 |
| 138 | 10 open import automaton |
| 141 | 11 open import logic |
| 12 open import regex | |
| 13 | |
| 274 | 14 -- whether a regex accepts empty input |
| 15 -- | |
| 141 | 16 empty? : Regex Σ → Bool |
| 17 empty? ε = true | |
| 18 empty? φ = false | |
| 19 empty? (x *) = true | |
| 20 empty? (x & y) = empty? x /\ empty? y | |
| 21 empty? (x || y) = empty? x \/ empty? y | |
| 22 empty? < x > = false | |
| 23 | |
| 24 derivative : Regex Σ → Σ → Regex Σ | |
| 25 derivative ε s = φ | |
| 26 derivative φ s = φ | |
| 27 derivative (x *) s with derivative x s | |
| 28 ... | ε = x * | |
| 29 ... | φ = φ | |
| 30 ... | t = t & (x *) | |
| 31 derivative (x & y) s with empty? x | |
| 32 ... | true with derivative x s | derivative y s | |
| 33 ... | ε | φ = φ | |
| 335 | 34 ... | ε | t = t || y |
| 141 | 35 ... | φ | t = t |
| 36 ... | x1 | φ = x1 & y | |
| 37 ... | x1 | y1 = (x1 & y) || y1 | |
| 38 derivative (x & y) s | false with derivative x s | |
| 39 ... | ε = y | |
| 40 ... | φ = φ | |
| 41 ... | t = t & y | |
| 42 derivative (x || y) s with derivative x s | derivative y s | |
| 43 ... | φ | y1 = y1 | |
| 44 ... | x1 | φ = x1 | |
| 45 ... | x1 | y1 = x1 || y1 | |
| 46 derivative < x > s with eq? x s | |
| 47 ... | yes _ = ε | |
| 48 ... | no _ = φ | |
| 138 | 49 |
| 141 | 50 data regex-states (x : Regex Σ ) : Regex Σ → Set where |
| 51 unit : regex-states x x | |
| 52 derive : { y : Regex Σ } → regex-states x y → (s : Σ) → regex-states x ( derivative y s ) | |
| 44 | 53 |
| 141 | 54 record Derivative (x : Regex Σ ) : Set where |
| 55 field | |
| 56 state : Regex Σ | |
| 57 is-derived : regex-states x state | |
| 58 | |
| 59 open Derivative | |
| 60 | |
| 335 | 61 derive-step : (r : Regex Σ) (d0 : Derivative r) → (s : Σ) → regex-states r (derivative (state d0) s) |
| 62 derive-step r d0 s = derive (is-derived d0) s | |
| 63 | |
| 64 regex→automaton : (r : Regex Σ) → Automaton (Derivative r) Σ | |
| 65 regex→automaton r = record { δ = λ d s → record { state = derivative (state d) s ; is-derived = derive-step r d s} | |
| 66 ; aend = λ d → empty? (state d) } | |
| 67 | |
| 68 regex-match : (r : Regex Σ) → (List Σ) → Bool | |
| 69 regex-match ex is = accept ( regex→automaton ex ) record { state = ex ; is-derived = unit } is | |
| 70 | |
| 71 -- open import nfa | |
| 72 open import Data.Nat | |
| 73 -- open import Data.Nat hiding ( _<_ ; _>_ ) | |
| 74 -- open import Data.Fin hiding ( _<_ ) | |
| 336 | 75 open import nat |
| 335 | 76 open import finiteSetUtil |
| 77 open FiniteSet | |
|
270
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
183
diff
changeset
|
78 open import Data.Fin hiding (_<_) |
| 141 | 79 |
| 336 | 80 -- finiteness of derivative |
| 81 -- term generate x & y for each * and & only once | |
| 82 -- rank : Regex → ℕ | |
| 83 -- r₀ & r₁ ... r | |
| 337 | 84 -- generated state is a subset of the term set |
| 141 | 85 |
| 271 | 86 open import Relation.Binary.Definitions |
| 87 | |
| 336 | 88 rank : (r : Regex Σ) → ℕ |
| 89 rank ε = 0 | |
| 90 rank φ = 0 | |
| 91 rank (r *) = suc (rank r) | |
| 92 rank (r & r₁) = suc (max (rank r) (rank r₁)) | |
| 93 rank (r || r₁) = max (rank r) (rank r₁) | |
| 94 rank < x > = 0 | |
| 95 | |
| 96 data SB : (r : Regex Σ) → (rn : ℕ) → Set where | |
| 339 | 97 sbε : (r : Regex Σ) → SB ε 0 |
| 98 sbφ : (r : Regex Σ) → SB φ 0 | |
| 99 sb<> : (s : Σ) → SB < s > 0 | |
| 100 sb| : (x y : Regex Σ) → (xn yn xy : ℕ) → SB x xn → SB y yn → xy ≡ max xn yn → SB (x || y) xy | |
| 336 | 101 sb* : (x : Regex Σ) → (xn : ℕ) → SB (x & (x *)) (suc xn) |
| 102 sb& : (x y : Regex Σ) → (xn yn : ℕ) → xn < yn → SB (x & y) (suc yn) | |
| 271 | 103 |
| 338 | 104 SBTA : (r : Regex Σ) → Automaton (SB r (rank r) → Bool) Σ |
| 335 | 105 SBTA = ? |
| 271 | 106 |
| 338 | 107 open import bijection using ( InjectiveF ; Is ) |
| 336 | 108 |
| 338 | 109 finSBTA : (r : Regex Σ) → FiniteSet (SB r (rank r) → Bool) |
| 110 finSBTA r = fin→ ( fb00 (rank r) r refl ) where | |
| 111 fb00 : (n : ℕ ) → (r : Regex Σ) → rank r ≡ n → FiniteSet (SB r (rank r)) | |
| 112 fb00 zero ε eq = ? | |
| 113 fb00 zero φ eq = ? | |
| 114 fb00 zero (r || r₁) eq = ? | |
| 115 fb00 zero < x > eq = ? | |
| 116 fb00 (suc n) (r *) eq = ? | |
| 117 fb00 (suc n) (r & r₁) eq = ? | |
| 118 fb00 (suc n) (r || r₁) eq = ? | |
| 119 | |
| 120 injSB : (r : Regex Σ) → InjectiveF (Derivative r) (SB r (rank r) → Bool) | |
| 121 injSB r = record { f = fb01 (rank r) r refl ; inject = ? } where | |
| 122 fb01 : (n : ℕ ) → (r : Regex Σ) → rank r ≡ n → Derivative r → SB r (rank r) → Bool | |
| 340 | 123 fb01 n r eq d sb with is-derived d |
| 124 fb01 n r eq d sb | unit = true | |
| 125 fb01 zero .ε eq d (sbε r) | derive {y} ss i = true | |
| 126 fb01 zero .φ eq d (sbφ r) | derive {y} ss i = false | |
| 127 fb01 zero .(< s >) eq d (sb<> s) | derive {y} ss i = ? | |
| 128 fb01 zero .(x || y) eq d (sb| x y xn yn .(rank (x || y)) sb sb₁ x₁) | derive {y₂} ss i = ? | |
| 129 fb01 (suc n) .(x || y) eq d (sb| x y xn yn .(rank (x || y)) sb sb₁ x₁) | derive {y₂} ss i = ? | |
| 130 fb01 (suc n) .(x & (x *)) eq d (sb* x .(max (rank x) (rank (x *)))) | derive {y₂} ss i = ? | |
| 131 fb01 (suc n) .(x & y) eq d (sb& x y xn .(max (rank x) (rank y)) x₁) | derive {y₂} ss i = ? | |
| 338 | 132 |
| 133 finite-derivative : (r : Regex Σ) → FiniteSet (Derivative r) | |
| 134 finite-derivative r = inject-fin (finSBTA r) (injSB r) ? | |
| 335 | 135 |
| 136 | |
| 137 | |
| 338 | 138 |