Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/regular-star.agda @ 270:dd98e7e5d4a5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
derive worked but finiteness is difficult add regular star
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 26 Nov 2021 20:02:06 +0900
parents automaton-in-agda/src/regular-concat.agda@52ed73a116d0
children 1c8ed1220489
comparison
equal deleted inserted replaced
269:52ed73a116d0 270:dd98e7e5d4a5
1 module regular-star 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 hiding ( _+_ )
7 open import Data.Empty
8 open import Data.Unit
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
14 open import nat
15 open import automaton
16 open import regular-language
17
18 open import nfa
19 open import sbconst2
20 open import finiteSet
21 open import finiteSetUtil
22 open import Relation.Binary.PropositionalEquality hiding ( [_] )
23 open import regular-concat
24
25 open Automaton
26 open FiniteSet
27
28 open RegularLanguage
29
30 Star-NFA : {Σ : Set} → (A : RegularLanguage Σ ) → NAutomaton (states A ) Σ
31 Star-NFA {Σ} A = record { Nδ = δnfa ; Nend = nend }
32 module Star-NFA where
33 δnfa : states A → Σ → states A → Bool
34 δnfa q i q₁ with aend (automaton A) q
35 ... | true = equal? (afin A) ( astart A) q₁
36 ... | false = equal? (afin A) (δ (automaton A) q i) q₁
37 δnfa _ i _ = false
38 nend : states A → Bool
39 nend q = aend (automaton A) q
40
41 Star-NFA-start : {Σ : Set} → (A : RegularLanguage Σ ) → states A → Bool
42 Star-NFA-start A q = equal? (afin A) (astart A) q \/ aend (automaton A) q
43
44 SNFA-exist : {Σ : Set} → (A : RegularLanguage Σ ) → (states A → Bool) → Bool
45 SNFA-exist A qs = exists (afin A) qs
46
47 M-Star : {Σ : Set} → (A : RegularLanguage Σ ) → RegularLanguage Σ
48 M-Star {Σ} A = record {
49 states = states A → Bool
50 ; astart = Star-NFA-start A
51 ; afin = fin→ (afin A)
52 ; automaton = subset-construction (SNFA-exist A ) (Star-NFA A )
53 }
54
55 open Split
56
57 open _∧_
58
59 open NAutomaton
60 open import Data.List.Properties
61
62 closed-in-star : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Star (contain A) ) x ( M-Star A )
63 closed-in-star {Σ} A B x = ≡-Bool-func closed-in-star→ closed-in-star← where
64 NFA = (Star-NFA A )
65
66 closed-in-star→ : Star (contain A) x ≡ true → contain (M-Star A ) x ≡ true
67 closed-in-star→ star = {!!}
68
69 open Found
70
71 closed-in-star← : contain (M-Star A ) x ≡ true → Star (contain A) x ≡ true
72 closed-in-star← C with subset-construction-lemma← (SNFA-exist A ) NFA {!!} x C
73 ... | CC = {!!}
74
75
76
77