|
65
|
1 module regular-language where
|
|
|
2
|
|
|
3 open import Level renaming ( suc to Suc ; zero to Zero )
|
|
|
4 open import Data.List
|
|
|
5 open import Data.Nat hiding ( _≟_ )
|
|
70
|
6 open import Data.Fin hiding ( _+_ )
|
|
72
|
7 open import Data.Empty
|
|
101
|
8 open import Data.Unit
|
|
65
|
9 open import Data.Product
|
|
|
10 -- open import Data.Maybe
|
|
|
11 open import Relation.Nullary
|
|
|
12 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
13 open import logic
|
|
70
|
14 open import nat
|
|
65
|
15 open import automaton
|
|
|
16
|
|
|
17 language : { Σ : Set } → Set
|
|
|
18 language {Σ} = List Σ → Bool
|
|
|
19
|
|
|
20 language-L : { Σ : Set } → Set
|
|
|
21 language-L {Σ} = List (List Σ)
|
|
|
22
|
|
|
23 Union : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
|
|
|
24 Union {Σ} A B x = (A x ) \/ (B x)
|
|
|
25
|
|
|
26 split : {Σ : Set} → (List Σ → Bool)
|
|
|
27 → ( List Σ → Bool) → List Σ → Bool
|
|
|
28 split x y [] = x [] /\ y []
|
|
|
29 split x y (h ∷ t) = (x [] /\ y (h ∷ t)) \/
|
|
|
30 split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t
|
|
|
31
|
|
|
32 Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
|
|
|
33 Concat {Σ} A B = split A B
|
|
|
34
|
|
|
35 {-# TERMINATING #-}
|
|
|
36 Star : {Σ : Set} → ( A : language {Σ} ) → language {Σ}
|
|
266
|
37 Star {Σ} A [] = true
|
|
|
38 Star {Σ} A (h ∷ t) = split A ( Star {Σ} A ) (h ∷ t)
|
|
65
|
39
|
|
141
|
40 open import automaton-ex
|
|
|
41
|
|
87
|
42 test-AB→split : {Σ : Set} → {A B : List In2 → Bool} → split A B ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ (
|
|
69
|
43 ( A [] /\ B ( i0 ∷ i1 ∷ i0 ∷ [] ) ) \/
|
|
|
44 ( A ( i0 ∷ [] ) /\ B ( i1 ∷ i0 ∷ [] ) ) \/
|
|
|
45 ( A ( i0 ∷ i1 ∷ [] ) /\ B ( i0 ∷ [] ) ) \/
|
|
|
46 ( A ( i0 ∷ i1 ∷ i0 ∷ [] ) /\ B [] )
|
|
|
47 )
|
|
87
|
48 test-AB→split {_} {A} {B} = refl
|
|
69
|
49
|
|
266
|
50 star-nil : {Σ : Set} → ( A : language {Σ} ) → Star A [] ≡ true
|
|
|
51 star-nil A = refl
|
|
|
52
|
|
267
|
53 open Automaton
|
|
268
|
54 open import finiteSet
|
|
|
55 open import finiteSetUtil
|
|
267
|
56
|
|
|
57 record RegularLanguage ( Σ : Set ) : Set (Suc Zero) where
|
|
|
58 field
|
|
268
|
59 states : Set
|
|
|
60 astart : states
|
|
|
61 afin : FiniteSet states
|
|
267
|
62 automaton : Automaton states Σ
|
|
|
63 contain : List Σ → Bool
|
|
|
64 contain x = accept automaton astart x
|
|
|
65
|
|
268
|
66 open RegularLanguage
|
|
|
67
|
|
|
68 isRegular : {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage Σ ) → Set
|
|
|
69 isRegular A x r = A x ≡ contain r x
|
|
|
70
|
|
267
|
71 RegularLanguage-is-language : { Σ : Set } → RegularLanguage Σ → language {Σ}
|
|
|
72 RegularLanguage-is-language {Σ} R = RegularLanguage.contain R
|
|
|
73
|
|
|
74 RegularLanguage-is-language' : { Σ : Set } → RegularLanguage Σ → List Σ → Bool
|
|
|
75 RegularLanguage-is-language' {Σ} R x = accept (automaton R) (astart R) x where
|
|
|
76 open RegularLanguage
|
|
|
77
|
|
|
78 -- a language is implemented by an automaton
|
|
65
|
79
|
|
126
|
80 -- postulate
|
|
|
81 -- fin-× : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A × B) {a * b}
|
|
73
|
82
|
|
65
|
83 M-Union : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ
|
|
|
84 M-Union {Σ} A B = record {
|
|
|
85 states = states A × states B
|
|
|
86 ; astart = ( astart A , astart B )
|
|
268
|
87 ; afin = fin-× (afin A) (afin B)
|
|
65
|
88 ; automaton = record {
|
|
|
89 δ = λ q x → ( δ (automaton A) (proj₁ q) x , δ (automaton B) (proj₂ q) x )
|
|
|
90 ; aend = λ q → ( aend (automaton A) (proj₁ q) \/ aend (automaton B) (proj₂ q) )
|
|
|
91 }
|
|
141
|
92 }
|
|
65
|
93
|
|
|
94 closed-in-union : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Union (contain A) (contain B)) x ( M-Union A B )
|
|
|
95 closed-in-union A B [] = lemma where
|
|
|
96 lemma : aend (automaton A) (astart A) \/ aend (automaton B) (astart B) ≡
|
|
|
97 aend (automaton A) (astart A) \/ aend (automaton B) (astart B)
|
|
|
98 lemma = refl
|
|
|
99 closed-in-union {Σ} A B ( h ∷ t ) = lemma1 t ((δ (automaton A) (astart A) h)) ((δ (automaton B) (astart B) h)) where
|
|
|
100 lemma1 : (t : List Σ) → (qa : states A ) → (qb : states B ) →
|
|
|
101 accept (automaton A) qa t \/ accept (automaton B) qb t
|
|
|
102 ≡ accept (automaton (M-Union A B)) (qa , qb) t
|
|
|
103 lemma1 [] qa qb = refl
|
|
|
104 lemma1 (h ∷ t ) qa qb = lemma1 t ((δ (automaton A) qa h)) ((δ (automaton B) qb h))
|
|
|
105
|
