Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/regular-language.agda @ 405:af8f630b7e60
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 24 Sep 2023 18:02:04 +0900 |
| parents | 62a4d1a2c48d |
| children | a60132983557 |
| rev | line source |
|---|---|
| 405 | 1 {-# OPTIONS --cubical-compatible --safe #-} |
| 2 | |
| 65 | 3 module regular-language where |
| 4 | |
| 5 open import Level renaming ( suc to Suc ; zero to Zero ) | |
| 6 open import Data.List | |
| 7 open import Data.Nat hiding ( _≟_ ) | |
| 70 | 8 open import Data.Fin hiding ( _+_ ) |
| 72 | 9 open import Data.Empty |
| 101 | 10 open import Data.Unit |
| 65 | 11 open import Data.Product |
| 12 -- open import Data.Maybe | |
| 13 open import Relation.Nullary | |
| 14 open import Relation.Binary.PropositionalEquality hiding ( [_] ) | |
| 15 open import logic | |
| 70 | 16 open import nat |
| 65 | 17 open import automaton |
| 18 | |
| 19 language : { Σ : Set } → Set | |
| 20 language {Σ} = List Σ → Bool | |
| 21 | |
| 22 language-L : { Σ : Set } → Set | |
| 23 language-L {Σ} = List (List Σ) | |
| 24 | |
| 25 Union : {Σ : Set} → ( A B : language {Σ} ) → language {Σ} | |
| 330 | 26 Union {Σ} A B x = A x \/ B x |
| 65 | 27 |
| 330 | 28 split : {Σ : Set} → (x y : language {Σ} ) → language {Σ} |
| 65 | 29 split x y [] = x [] /\ y [] |
| 30 split x y (h ∷ t) = (x [] /\ y (h ∷ t)) \/ | |
| 31 split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t | |
| 32 | |
| 33 Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ} | |
| 34 Concat {Σ} A B = split A B | |
| 35 | |
| 405 | 36 -- {-# TERMINATING #-} |
| 37 -- Star1 : {Σ : Set} → ( A : language {Σ} ) → language {Σ} | |
| 38 -- Star1 {Σ} A [] = true | |
| 39 -- Star0 {Σ} A (h ∷ t) = split A ( Star1 {Σ} A ) (h ∷ t) | |
|
383
708570e55a91
add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
330
diff
changeset
|
40 |
| 401 | 41 -- Terminating version of Star1 |
| 42 -- | |
| 384 | 43 repeat : {Σ : Set} → (x : List Σ → Bool) → (y : List Σ ) → Bool |
| 401 | 44 repeat2 : {Σ : Set} → (x : List Σ → Bool) → (pre y : List Σ ) → Bool |
| 45 repeat2 x pre [] = false | |
| 46 repeat2 x pre (h ∷ y) = | |
| 47 (x (pre ++ (h ∷ [])) /\ repeat x y ) | |
| 48 \/ repeat2 x (pre ++ (h ∷ [])) y | |
| 49 | |
| 384 | 50 repeat {Σ} x [] = true |
| 401 | 51 repeat {Σ} x (h ∷ y) = repeat2 x [] (h ∷ y) |
|
383
708570e55a91
add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
330
diff
changeset
|
52 |
| 384 | 53 Star : {Σ : Set} → (x : List Σ → Bool) → (y : List Σ ) → Bool |
| 54 Star {Σ} x y = repeat x y | |
| 65 | 55 |
| 141 | 56 open import automaton-ex |
| 57 | |
| 87 | 58 test-AB→split : {Σ : Set} → {A B : List In2 → Bool} → split A B ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ ( |
| 69 | 59 ( A [] /\ B ( i0 ∷ i1 ∷ i0 ∷ [] ) ) \/ |
| 60 ( A ( i0 ∷ [] ) /\ B ( i1 ∷ i0 ∷ [] ) ) \/ | |
| 61 ( A ( i0 ∷ i1 ∷ [] ) /\ B ( i0 ∷ [] ) ) \/ | |
| 62 ( A ( i0 ∷ i1 ∷ i0 ∷ [] ) /\ B [] ) | |
| 63 ) | |
| 87 | 64 test-AB→split {_} {A} {B} = refl |
| 69 | 65 |
| 266 | 66 star-nil : {Σ : Set} → ( A : language {Σ} ) → Star A [] ≡ true |
| 67 star-nil A = refl | |
| 68 | |
| 267 | 69 open Automaton |
| 268 | 70 open import finiteSet |
| 71 open import finiteSetUtil | |
| 267 | 72 |
| 73 record RegularLanguage ( Σ : Set ) : Set (Suc Zero) where | |
| 74 field | |
| 268 | 75 states : Set |
| 76 astart : states | |
| 77 afin : FiniteSet states | |
| 267 | 78 automaton : Automaton states Σ |
| 79 contain : List Σ → Bool | |
| 80 contain x = accept automaton astart x | |
| 81 | |
| 268 | 82 open RegularLanguage |
| 83 | |
| 84 isRegular : {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage Σ ) → Set | |
| 85 isRegular A x r = A x ≡ contain r x | |
| 86 | |
| 267 | 87 RegularLanguage-is-language : { Σ : Set } → RegularLanguage Σ → language {Σ} |
| 88 RegularLanguage-is-language {Σ} R = RegularLanguage.contain R | |
| 89 | |
| 90 RegularLanguage-is-language' : { Σ : Set } → RegularLanguage Σ → List Σ → Bool | |
| 91 RegularLanguage-is-language' {Σ} R x = accept (automaton R) (astart R) x where | |
| 92 open RegularLanguage | |
| 93 | |
| 94 -- a language is implemented by an automaton | |
| 65 | 95 |
| 126 | 96 -- postulate |
| 97 -- fin-× : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A × B) {a * b} | |
| 73 | 98 |
| 65 | 99 M-Union : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ |
| 100 M-Union {Σ} A B = record { | |
| 101 states = states A × states B | |
| 102 ; astart = ( astart A , astart B ) | |
| 268 | 103 ; afin = fin-× (afin A) (afin B) |
| 65 | 104 ; automaton = record { |
| 105 δ = λ q x → ( δ (automaton A) (proj₁ q) x , δ (automaton B) (proj₂ q) x ) | |
| 106 ; aend = λ q → ( aend (automaton A) (proj₁ q) \/ aend (automaton B) (proj₂ q) ) | |
| 107 } | |
| 141 | 108 } |
| 65 | 109 |
| 110 closed-in-union : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Union (contain A) (contain B)) x ( M-Union A B ) | |
| 111 closed-in-union A B [] = lemma where | |
| 112 lemma : aend (automaton A) (astart A) \/ aend (automaton B) (astart B) ≡ | |
| 113 aend (automaton A) (astart A) \/ aend (automaton B) (astart B) | |
| 114 lemma = refl | |
| 115 closed-in-union {Σ} A B ( h ∷ t ) = lemma1 t ((δ (automaton A) (astart A) h)) ((δ (automaton B) (astart B) h)) where | |
| 116 lemma1 : (t : List Σ) → (qa : states A ) → (qb : states B ) → | |
| 117 accept (automaton A) qa t \/ accept (automaton B) qb t | |
| 118 ≡ accept (automaton (M-Union A B)) (qa , qb) t | |
| 119 lemma1 [] qa qb = refl | |
| 120 lemma1 (h ∷ t ) qa qb = lemma1 t ((δ (automaton A) qa h)) ((δ (automaton B) qb h)) | |
| 121 |