Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/derive.agda @ 274:1c8ed1220489
fixes
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 18 Dec 2021 16:27:46 +0900 |
| parents | f60c1041ae8e |
| children | 407684f806e4 |
| 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 |
| 10 -- open import nfa | |
| 11 open import Data.Nat | |
| 12 -- open import Data.Nat hiding ( _<_ ; _>_ ) | |
| 13 -- open import Data.Fin hiding ( _<_ ) | |
|
270
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
183
diff
changeset
|
14 open import finiteSetUtil |
| 138 | 15 open import automaton |
| 141 | 16 open import logic |
| 17 open import regex | |
| 271 | 18 open FiniteSet |
| 141 | 19 |
| 274 | 20 -- whether a regex accepts empty input |
| 21 -- | |
| 141 | 22 empty? : Regex Σ → Bool |
| 23 empty? ε = true | |
| 24 empty? φ = false | |
| 25 empty? (x *) = true | |
| 26 empty? (x & y) = empty? x /\ empty? y | |
| 27 empty? (x || y) = empty? x \/ empty? y | |
| 28 empty? < x > = false | |
| 29 | |
| 30 derivative : Regex Σ → Σ → Regex Σ | |
| 31 derivative ε s = φ | |
| 32 derivative φ s = φ | |
| 33 derivative (x *) s with derivative x s | |
| 34 ... | ε = x * | |
| 35 ... | φ = φ | |
| 36 ... | t = t & (x *) | |
| 37 derivative (x & y) s with empty? x | |
| 38 ... | true with derivative x s | derivative y s | |
| 39 ... | ε | φ = φ | |
| 40 ... | ε | t = y || t | |
| 41 ... | φ | t = t | |
| 42 ... | x1 | φ = x1 & y | |
| 43 ... | x1 | y1 = (x1 & y) || y1 | |
| 44 derivative (x & y) s | false with derivative x s | |
| 45 ... | ε = y | |
| 46 ... | φ = φ | |
| 47 ... | t = t & y | |
| 48 derivative (x || y) s with derivative x s | derivative y s | |
| 49 ... | φ | y1 = y1 | |
| 50 ... | x1 | φ = x1 | |
| 51 ... | x1 | y1 = x1 || y1 | |
| 52 derivative < x > s with eq? x s | |
| 53 ... | yes _ = ε | |
| 54 ... | no _ = φ | |
| 138 | 55 |
| 141 | 56 data regex-states (x : Regex Σ ) : Regex Σ → Set where |
| 57 unit : regex-states x x | |
| 58 derive : { y : Regex Σ } → regex-states x y → (s : Σ) → regex-states x ( derivative y s ) | |
| 44 | 59 |
| 141 | 60 record Derivative (x : Regex Σ ) : Set where |
| 61 field | |
| 62 state : Regex Σ | |
| 63 is-derived : regex-states x state | |
| 64 | |
| 65 open Derivative | |
| 66 | |
|
270
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
183
diff
changeset
|
67 open import Data.Fin hiding (_<_) |
| 141 | 68 |
| 69 -- derivative generates (x & y) || ... form. y and x part is a substerm of original regex | |
|
270
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
183
diff
changeset
|
70 -- since subterm is finite, only finite number of state is generated for each operator |
| 141 | 71 -- this does not work, becuase it depends on input sequences |
| 72 -- finite-derivative : (r : Regex Σ) → FiniteSet Σ → FiniteSet (Derivative r) | |
|
270
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
183
diff
changeset
|
73 -- order : Regex Σ → ℕ |
|
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
183
diff
changeset
|
74 -- decline-derive : (x : Regex Σ ) (i : Σ ) → 0 < order x → order (derivative x i) < order x |
|
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
183
diff
changeset
|
75 -- is not so easy |
| 141 | 76 -- in case of automaton, number of derivative is limited by iteration of input length, so it is finite. |
|
270
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
183
diff
changeset
|
77 -- so we cannot say derived automaton is finite i.e. regex-match is regular language now |
| 141 | 78 |
| 79 regex→automaton : (r : Regex Σ) → Automaton (Derivative r) Σ | |
| 80 regex→automaton r = record { δ = λ d s → record { state = derivative (state d) s ; is-derived = derive-step d s} ; aend = λ d → empty? (state d) } where | |
| 81 derive-step : (d0 : Derivative r) → (s : Σ) → regex-states r (derivative (state d0) s) | |
| 82 derive-step d0 s = derive (is-derived d0) s | |
| 83 | |
|
270
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
183
diff
changeset
|
84 regex-match : (r : Regex Σ) → (List Σ) → Bool |
|
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
183
diff
changeset
|
85 regex-match ex is = accept ( regex→automaton ex ) record { state = ex ; is-derived = unit } is |
| 271 | 86 |
| 87 open import Relation.Binary.Definitions | |
| 88 | |
| 272 | 89 cmp-regex : (x y : Regex Σ) → Dec ( x ≡ y ) |
| 90 cmp-regex ε ε = yes refl | |
| 91 cmp-regex ε φ = no (λ ()) | |
| 92 cmp-regex ε (y *) = no (λ ()) | |
| 93 cmp-regex ε (y & y₁) = no (λ ()) | |
| 94 cmp-regex ε (y || y₁) = no (λ ()) | |
| 95 cmp-regex ε < x > = no (λ ()) | |
| 96 cmp-regex φ ε = no (λ ()) | |
| 97 cmp-regex φ φ = yes refl | |
| 98 cmp-regex φ (y *) = no (λ ()) | |
| 99 cmp-regex φ (y & y₁) = no (λ ()) | |
| 100 cmp-regex φ (y || y₁) = no (λ ()) | |
| 101 cmp-regex φ < x > = no (λ ()) | |
| 102 cmp-regex (x *) ε = no (λ ()) | |
| 103 cmp-regex (x *) φ = no (λ ()) | |
| 104 cmp-regex (x *) (y *) with cmp-regex x y | |
| 105 ... | yes refl = yes refl | |
| 106 ... | no ne = no (λ x → ne (cmp1 x)) where | |
| 107 cmp1 : (x *) ≡ (y *) → x ≡ y | |
| 108 cmp1 refl = refl | |
| 109 cmp-regex (x *) (y & y₁) = no (λ ()) | |
| 110 cmp-regex (x *) (y || y₁) = no (λ ()) | |
| 111 cmp-regex (x *) < x₁ > = no (λ ()) | |
| 112 cmp-regex (x & x₁) ε = no (λ ()) | |
| 113 cmp-regex (x & x₁) φ = no (λ ()) | |
| 114 cmp-regex (x & x₁) (y *) = no (λ ()) | |
| 115 cmp-regex (x & x₁) (y & y₁) with cmp-regex x y | cmp-regex x₁ y₁ | |
| 116 ... | yes refl | yes refl = yes refl | |
| 117 ... | no ne | _ = no (λ x → ne (cmp1 x)) where | |
| 118 cmp1 : x & x₁ ≡ y & y₁ → x ≡ y | |
| 119 cmp1 refl = refl | |
| 120 ... | _ | no ne = no (λ x → ne (cmp1 x)) where | |
| 121 cmp1 : x & x₁ ≡ y & y₁ → x₁ ≡ y₁ | |
| 122 cmp1 refl = refl | |
| 123 cmp-regex (x & x₁) (y || y₁) = no (λ ()) | |
| 124 cmp-regex (x & x₁) < x₂ > = no (λ ()) | |
| 125 cmp-regex (x || x₁) ε = no (λ ()) | |
| 126 cmp-regex (x || x₁) φ = no (λ ()) | |
| 127 cmp-regex (x || x₁) (y *) = no (λ ()) | |
| 128 cmp-regex (x || x₁) (y & y₁) = no (λ ()) | |
| 129 cmp-regex (x || x₁) (y || y₁) with cmp-regex x y | cmp-regex x₁ y₁ | |
| 130 ... | yes refl | yes refl = yes refl | |
| 131 ... | no ne | _ = no (λ x → ne (cmp1 x)) where | |
| 132 cmp1 : x || x₁ ≡ y || y₁ → x ≡ y | |
| 133 cmp1 refl = refl | |
| 134 ... | _ | no ne = no (λ x → ne (cmp1 x)) where | |
| 135 cmp1 : x || x₁ ≡ y || y₁ → x₁ ≡ y₁ | |
| 136 cmp1 refl = refl | |
| 137 cmp-regex (x || x₁) < x₂ > = no (λ ()) | |
| 138 cmp-regex < x > ε = no (λ ()) | |
| 139 cmp-regex < x > φ = no (λ ()) | |
| 140 cmp-regex < x > (y *) = no (λ ()) | |
| 141 cmp-regex < x > (y & y₁) = no (λ ()) | |
| 142 cmp-regex < x > (y || y₁) = no (λ ()) | |
| 143 cmp-regex < x > < x₁ > with equal? fin x x₁ | inspect ( equal? fin x ) x₁ | |
| 144 ... | false | record { eq = eq } = no (λ x → ¬-bool eq (cmp1 x)) where | |
| 145 cmp1 : < x > ≡ < x₁ > → equal? fin x x₁ ≡ true | |
| 146 cmp1 refl = equal?-refl fin | |
| 147 ... | true | record { eq = eq } with equal→refl fin eq | |
| 148 ... | refl = yes refl | |
| 271 | 149 |
| 272 | 150 insert : List (Regex Σ) → (Regex Σ) → List (Regex Σ) |
| 151 insert [] k = k ∷ [] | |
| 152 insert (x ∷ t) k with cmp-regex k x | |
| 153 ... | no n = x ∷ (insert t k) | |
| 154 ... | yes y = x ∷ t | |
| 271 | 155 |
| 272 | 156 regex-derive : List (Regex Σ) → List (Regex Σ) |
| 271 | 157 regex-derive t = regex-derive0 t t where |
| 272 | 158 regex-derive1 : Regex Σ → List Σ → List (Regex Σ) → List (Regex Σ) |
| 271 | 159 regex-derive1 x [] t = t |
| 160 regex-derive1 x (i ∷ t) r = regex-derive1 x t (insert r (derivative x i)) | |
| 272 | 161 regex-derive0 : List (Regex Σ) → List (Regex Σ) → List (Regex Σ) |
| 162 regex-derive0 [] t = t | |
| 163 regex-derive0 (x ∷ r) t = regex-derive0 r (regex-derive1 x (to-list fin (λ _ → true)) t) | |
| 271 | 164 |
| 274 | 165 -- |
| 166 -- if (Derivative r is finite, regex→automaton is finite | |
| 167 -- | |
| 168 drive-is-finite : (r : Regex Σ) → FiniteSet (Derivative r) | |
| 169 drive-is-finite ε = {!!} | |
| 170 drive-is-finite φ = {!!} | |
| 171 drive-is-finite (r *) = {!!} where | |
| 172 d1 : FiniteSet (Derivative r ) | |
| 173 d1 = drive-is-finite r | |
| 174 drive-is-finite (r & r₁) = {!!} | |
| 175 drive-is-finite (r || r₁) = {!!} | |
| 176 drive-is-finite < x > = {!!} | |
| 177 |