|
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 ( _≟_ )
|
|
|
6 open import Data.Fin
|
|
|
7 open import Data.Product
|
|
|
8 -- open import Data.Maybe
|
|
|
9 open import Relation.Nullary
|
|
|
10 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
11 open import logic
|
|
|
12 open import automaton
|
|
|
13 open import finiteSet
|
|
|
14
|
|
|
15 language : { Σ : Set } → Set
|
|
|
16 language {Σ} = List Σ → Bool
|
|
|
17
|
|
|
18 language-L : { Σ : Set } → Set
|
|
|
19 language-L {Σ} = List (List Σ)
|
|
|
20
|
|
|
21 open Automaton
|
|
|
22
|
|
|
23 record RegularLanguage ( Σ : Set ) : Set (Suc Zero) where
|
|
|
24 field
|
|
|
25 states : Set
|
|
|
26 astart : states
|
|
|
27 automaton : Automaton states Σ
|
|
|
28 contain : List Σ → Bool
|
|
|
29 contain x = accept automaton astart x
|
|
|
30
|
|
|
31 Union : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
|
|
|
32 Union {Σ} A B x = (A x ) \/ (B x)
|
|
|
33
|
|
|
34 split : {Σ : Set} → (List Σ → Bool)
|
|
|
35 → ( List Σ → Bool) → List Σ → Bool
|
|
|
36 split x y [] = x [] /\ y []
|
|
|
37 split x y (h ∷ t) = (x [] /\ y (h ∷ t)) \/
|
|
|
38 split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t
|
|
|
39
|
|
|
40 Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
|
|
|
41 Concat {Σ} A B = split A B
|
|
|
42
|
|
|
43 {-# TERMINATING #-}
|
|
|
44 Star : {Σ : Set} → ( A : language {Σ} ) → language {Σ}
|
|
|
45 Star {Σ} A = split A ( Star {Σ} A )
|
|
|
46
|
|
|
47 open RegularLanguage
|
|
|
48 isRegular : {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage Σ ) → Set
|
|
|
49 isRegular A x r = A x ≡ contain r x
|
|
|
50
|
|
|
51 M-Union : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ
|
|
|
52 M-Union {Σ} A B = record {
|
|
|
53 states = states A × states B
|
|
|
54 ; astart = ( astart A , astart B )
|
|
|
55 ; automaton = record {
|
|
|
56 δ = λ q x → ( δ (automaton A) (proj₁ q) x , δ (automaton B) (proj₂ q) x )
|
|
|
57 ; aend = λ q → ( aend (automaton A) (proj₁ q) \/ aend (automaton B) (proj₂ q) )
|
|
|
58 }
|
|
|
59 }
|
|
|
60
|
|
|
61 closed-in-union : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Union (contain A) (contain B)) x ( M-Union A B )
|
|
|
62 closed-in-union A B [] = lemma where
|
|
|
63 lemma : aend (automaton A) (astart A) \/ aend (automaton B) (astart B) ≡
|
|
|
64 aend (automaton A) (astart A) \/ aend (automaton B) (astart B)
|
|
|
65 lemma = refl
|
|
|
66 closed-in-union {Σ} A B ( h ∷ t ) = lemma1 t ((δ (automaton A) (astart A) h)) ((δ (automaton B) (astart B) h)) where
|
|
|
67 lemma1 : (t : List Σ) → (qa : states A ) → (qb : states B ) →
|
|
|
68 accept (automaton A) qa t \/ accept (automaton B) qb t
|
|
|
69 ≡ accept (automaton (M-Union A B)) (qa , qb) t
|
|
|
70 lemma1 [] qa qb = refl
|
|
|
71 lemma1 (h ∷ t ) qa qb = lemma1 t ((δ (automaton A) qa h)) ((δ (automaton B) qb h))
|
|
|
72
|
|
|
73 -- M-Concat : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ
|
|
|
74 -- M-Concat {Σ} A B = record {
|
|
|
75 -- states = states A ∨ states B
|
|
|
76 -- ; astart = case1 (astart A )
|
|
|
77 -- ; automaton = record {
|
|
|
78 -- δ = {!!}
|
|
|
79 -- ; aend = {!!}
|
|
|
80 -- }
|
|
|
81 -- }
|
|
|
82 --
|
|
|
83 -- closed-in-concat : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )
|
|
|
84 -- closed-in-concat = {!!}
|
