|
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 open Automaton
|
|
|
24
|
|
|
25 record RegularLanguage ( Σ : Set ) : Set (Suc Zero) where
|
|
|
26 field
|
|
|
27 states : Set
|
|
|
28 astart : states
|
|
|
29 automaton : Automaton states Σ
|
|
|
30 contain : List Σ → Bool
|
|
|
31 contain x = accept automaton astart x
|
|
|
32
|
|
|
33 Union : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
|
|
|
34 Union {Σ} A B x = (A x ) \/ (B x)
|
|
|
35
|
|
|
36 split : {Σ : Set} → (List Σ → Bool)
|
|
|
37 → ( List Σ → Bool) → List Σ → Bool
|
|
|
38 split x y [] = x [] /\ y []
|
|
|
39 split x y (h ∷ t) = (x [] /\ y (h ∷ t)) \/
|
|
|
40 split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t
|
|
|
41
|
|
|
42 Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
|
|
|
43 Concat {Σ} A B = split A B
|
|
|
44
|
|
|
45 {-# TERMINATING #-}
|
|
|
46 Star : {Σ : Set} → ( A : language {Σ} ) → language {Σ}
|
|
|
47 Star {Σ} A = split A ( Star {Σ} A )
|
|
|
48
|
|
141
|
49 open import automaton-ex
|
|
|
50
|
|
87
|
51 test-AB→split : {Σ : Set} → {A B : List In2 → Bool} → split A B ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ (
|
|
69
|
52 ( A [] /\ B ( i0 ∷ i1 ∷ i0 ∷ [] ) ) \/
|
|
|
53 ( A ( i0 ∷ [] ) /\ B ( i1 ∷ i0 ∷ [] ) ) \/
|
|
|
54 ( A ( i0 ∷ i1 ∷ [] ) /\ B ( i0 ∷ [] ) ) \/
|
|
|
55 ( A ( i0 ∷ i1 ∷ i0 ∷ [] ) /\ B [] )
|
|
|
56 )
|
|
87
|
57 test-AB→split {_} {A} {B} = refl
|
|
69
|
58
|
|
65
|
59 open RegularLanguage
|
|
|
60 isRegular : {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage Σ ) → Set
|
|
|
61 isRegular A x r = A x ≡ contain r x
|
|
|
62
|
|
126
|
63 -- postulate
|
|
|
64 -- fin-× : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A × B) {a * b}
|
|
73
|
65
|
|
65
|
66 M-Union : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ
|
|
|
67 M-Union {Σ} A B = record {
|
|
|
68 states = states A × states B
|
|
|
69 ; astart = ( astart A , astart B )
|
|
|
70 ; automaton = record {
|
|
|
71 δ = λ q x → ( δ (automaton A) (proj₁ q) x , δ (automaton B) (proj₂ q) x )
|
|
|
72 ; aend = λ q → ( aend (automaton A) (proj₁ q) \/ aend (automaton B) (proj₂ q) )
|
|
|
73 }
|
|
141
|
74 }
|
|
65
|
75
|
|
|
76 closed-in-union : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Union (contain A) (contain B)) x ( M-Union A B )
|
|
|
77 closed-in-union A B [] = lemma where
|
|
|
78 lemma : aend (automaton A) (astart A) \/ aend (automaton B) (astart B) ≡
|
|
|
79 aend (automaton A) (astart A) \/ aend (automaton B) (astart B)
|
|
|
80 lemma = refl
|
|
|
81 closed-in-union {Σ} A B ( h ∷ t ) = lemma1 t ((δ (automaton A) (astart A) h)) ((δ (automaton B) (astart B) h)) where
|
|
|
82 lemma1 : (t : List Σ) → (qa : states A ) → (qb : states B ) →
|
|
|
83 accept (automaton A) qa t \/ accept (automaton B) qb t
|
|
|
84 ≡ accept (automaton (M-Union A B)) (qa , qb) t
|
|
|
85 lemma1 [] qa qb = refl
|
|
|
86 lemma1 (h ∷ t ) qa qb = lemma1 t ((δ (automaton A) qa h)) ((δ (automaton B) qb h))
|
|
|
87
|
