Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/derive.agda @ 365:c46f04f7c99a
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 21 Jul 2023 12:01:16 +0900 |
| parents | 00f5076ef2de |
| children | 19410aadd636 |
| 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 | |
| 341 | 97 sbε : SB ε 0 |
| 98 sbφ : SB φ 0 | |
| 339 | 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 | |
| 341 | 101 sb* : (x : Regex Σ) → (xn : ℕ) → SB x xn → SB (x *) (suc xn) |
| 102 sb& : (x y : Regex Σ) → (xn yn : ℕ) → xn < yn → ( sx : SB x xn ) (sy : SB y yn ) → SB (x & y) (suc yn) | |
| 103 | |
| 104 sb-id : (r : Regex Σ) → SB r (rank r) → Bool | |
| 105 sb-id r sb with rank r | inspect rank r | |
| 106 sb-id ε sbε | zero | _ = true | |
| 107 sb-id φ sbφ | zero | _ = true | |
| 108 sb-id < t > (sb<> s) | zero | _ with eq? t s | |
| 109 ... | yes _ = true | |
| 110 ... | no _ = false | |
| 111 sb-id (x0 || y0) (sb| x y xn yn .zero sb sb₁ x₁) | zero | record { eq = eq1 } = sb-id x0 ? /\ sb-id y0 ? | |
| 112 sb-id _ (sb| x y xn yn .(suc k) sb sb₁ x₁) | suc k | record { eq = eq1 } = sb-id x ? /\ sb-id y ? | |
| 113 sb-id (y *) (sb* x t u) | suc k | record{ eq = eq1 } = sb-id y ? | |
| 114 sb-id (x0 & y0) (sb& .x0 .y0 xn .k x z z₁) | suc k | record { eq = eq1 } = sb-id x0 ? /\ sb-id y0 ? | |
| 271 | 115 |
| 338 | 116 open import bijection using ( InjectiveF ; Is ) |
| 336 | 117 |
| 338 | 118 finSBTA : (r : Regex Σ) → FiniteSet (SB r (rank r) → Bool) |
| 119 finSBTA r = fin→ ( fb00 (rank r) r refl ) where | |
| 120 fb00 : (n : ℕ ) → (r : Regex Σ) → rank r ≡ n → FiniteSet (SB r (rank r)) | |
| 364 | 121 fb00 zero ε eq = record { finite = 1 ; Q←F = λ _ → sbε ; F←Q = λ _ → # 0 ; finiso→ = ? ; finiso← = ? } |
| 122 fb00 zero φ eq = record { finite = 1 ; Q←F = λ _ → sbφ ; F←Q = λ _ → # 0 ; finiso→ = ? ; finiso← = ? } | |
| 123 fb00 zero (r || r₁) eq = iso-fin (fin-∨ (fb00 zero r ?) (fb00 zero r₁ ?)) ? | |
| 124 fb00 zero < x > eq = iso-fin fin ? | |
| 125 fb00 (suc n) (r *) eq = iso-fin (fb00 n r ?) ? | |
| 126 fb00 (suc n) (r & r₁) eq = iso-fin (fin-∧ (fb00 n r ?) (fb00 n r₁ ?)) ? | |
| 127 fb00 (suc n) (r || r₁) eq = iso-fin (fin-∧ (fb00 (suc n) r ?) (fb00 (suc n) r₁ ?)) ? | |
| 338 | 128 |
| 364 | 129 record SBf (r : Regex Σ) (n : ℕ) : Set where |
| 130 field | |
| 131 rank=n : rank r ≡ n | |
| 132 f : Derivative r → SB r n → Bool | |
| 133 sb-inject : {x y : Derivative r} → f x ≡ f y → x ≡ y | |
| 134 dec : (a : SB r n → Bool ) → Dec (Is (Derivative r) (SB r n → Bool) f a ) | |
| 135 | |
| 136 SBN : (r : Regex Σ) → SBf r (rank r) | |
| 365 | 137 SBN ε = record { rank=n = refl ; f = fb02 ; sb-inject = fl05 ; dec = fl03 } where |
| 138 fb02 : Derivative ε → SB ε 0 → Bool | |
| 139 fb02 d sbε = true | |
| 140 fl03 : (a : SB ε 0 → Bool) → Dec (Is (Derivative ε) (SB ε 0 → Bool) fb02 a) | |
| 141 fl03 a with a sbε | inspect a sbε | |
| 142 ... | true | record { eq = eq1 } = yes record { a = record { state = ε ; is-derived = unit } | |
| 143 ; fa=c = f-extensionality fl04 } where | |
| 144 fl04 : (x : SB ε 0) → fb02 (record { state = ε ; is-derived = unit }) x ≡ a x | |
| 145 fl04 sbε = sym eq1 | |
| 146 ... | false | record { eq = eq1} = no (λ n → ¬-bool {a sbε} eq1 (fl04 n)) where | |
| 147 fl04 : Is (Derivative ε) (SB ε 0 → Bool) fb02 a → a sbε ≡ true | |
| 148 fl04 n = sym (cong (λ k → k sbε) (Is.fa=c n)) | |
| 149 fl05 : {x y : Derivative ε} → fb02 x ≡ fb02 y → x ≡ y | |
| 150 fl05 {x} {y} eq = ? | |
| 364 | 151 SBN φ = ? |
| 152 SBN (r *) = ? | |
| 153 SBN (r & r₁) = record { rank=n = ? ; f = ? ; sb-inject = ? ; dec = ? } | |
| 154 SBN (r || r₁) = ? | |
| 365 | 155 SBN < x > = record { rank=n = refl ; f = ? ; sb-inject = ? ; dec = ? } |
| 364 | 156 |
| 338 | 157 finite-derivative : (r : Regex Σ) → FiniteSet (Derivative r) |
| 364 | 158 finite-derivative r = inject-fin (finSBTA r) record { f = SBf.f (SBN r) ; inject = SBf.sb-inject (SBN r) } (SBf.dec (SBN r)) |
| 335 | 159 |
| 160 | |
| 161 | |
| 338 | 162 |