Mercurial > hg > Members > kono > Proof > automaton

comparison agda/regular-language.agda @ 65:293a2075514b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 31 Oct 2019 10:08:55 +0900
parents
children f124fceba460
comparison
equal deleted inserted replaced
64:475923938f50 65:293a2075514b
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 = {!!}