|
0
|
1 module nfa where
|
|
|
2 open import Level renaming ( suc to Suc ; zero to Zero )
|
|
|
3
|
|
|
4 open import Relation.Binary.PropositionalEquality
|
|
|
5 open import Data.List
|
|
|
6 open import automaton
|
|
|
7 open import logic
|
|
|
8
|
|
|
9 record NAutomaton {n : Level} ( Q : Set n ) ( Σ : Set )
|
|
|
10 : Set (Suc n) where
|
|
|
11 field
|
|
|
12 Nδ : Q → Σ → Q → Set
|
|
|
13 NF : Q → Set
|
|
|
14 Nexists : (Q → Set) → Set
|
|
|
15
|
|
|
16 open NAutomaton
|
|
|
17
|
|
|
18 naccept : {n : Level} {Q : Set n} {Σ : Set} → NAutomaton Q Σ → (Q → Set) → List Σ → Set
|
|
|
19 naccept {n} {Q} {Σ} nfa qs [] = Nexists nfa (λ q → qs q ∧ NF nfa q )
|
|
|
20 naccept {n} {Q} {Σ} nfa qs (x ∷ input) =
|
|
|
21 Nexists nfa (λ q → qs q ∧ (naccept nfa (Nδ nfa q x) input ))
|
|
|
22
|
|
|
23 ntrace : {n : Level} {Q : Set n} {Σ : Set } → (NFA : NAutomaton Q Σ) → (start : Q → Set ) → (input : List Σ ) → naccept NFA start input
|
|
|
24 → ((Q → Set) → List Q)
|
|
|
25 → List (List Q)
|
|
|
26 ntrace {n} {Q} {Σ} A q [] a list = list q ∷ []
|
|
|
27 ntrace {n} {Q} {Σ} A q (x ∷ t) a list = list q ∷ ( ntrace A {!!} t {!!} list )
|
|
|
28
|
|
|
29 data transition136 : Q3 → Σ2 → Q3 → Set where
|
|
|
30 d0 : transition136 q₁ s1 q₂
|
|
|
31 d1 : transition136 q₁ s0 q₁
|
|
|
32 d2 : transition136 q₂ s0 q₂
|
|
|
33 d3 : transition136 q₂ s0 q₃
|
|
|
34 d4 : transition136 q₂ s1 q₃
|
|
|
35 d5 : transition136 q₃ s0 q₁
|
|
|
36
|
|
|
37 start136 : Q3 → Set
|
|
|
38 start136 q = q ≡ q₁
|
|
|
39
|
|
|
40 nfa136 : NAutomaton Q3 Σ2
|
|
|
41 nfa136 = record { Nδ = transition136 ; NF = λ q → q ≡ q₁ ; Nexists = exists-in-Q3 }
|
|
|
42
|
|
|
43 example136-1 = naccept nfa136 start136 ( s0 ∷ s1 ∷ s0 ∷ s0 ∷ [] )
|
|
|
44
|
|
|
45 example136-0 = naccept nfa136 start136 ( s0 ∷ [] )
|
|
|
46
|
|
|
47 example136-2 = naccept nfa136 start136 ( s1 ∷ s0 ∷ s1 ∷ s0 ∷ s1 ∷ [] )
|
|
|
48
|
|
|
49 --
|
|
|
50 -- ((Q → Set) → Set) → ((Q → Set) → Set) → Set
|
|
|
51 --
|
|
|
52
|
|
|
53 data Nexists→exits {n : Level} { Q : Set n } {Σ : Set} ( NFA : NAutomaton Q Σ ) : ((Q → Set) → Set) → Set where
|
|
|
54 one-of : Nexists→exits NFA (Nexists NFA)
|
|
|
55
|
|
|
56 subset-construction : {n : Level} { Q : Set n } { Σ : Set } →
|
|
|
57 (NAutomaton Q Σ ) → Automaton {Suc Zero ⊔ n} (Q → Set) Σ
|
|
|
58 subset-construction {n} {Q} { Σ} NFA = record {
|
|
|
59 δ = λ qs x qs → Nexists NFA (λ q → Nδ NFA q x qs )
|
|
|
60 ; F = λ qs → Nexists NFA ( λ q → NF NFA q )
|
|
|
61 ; exists = Nexists→exits NFA -- what this means?
|
|
|
62 }
|
|
|
63
|
|
|
64 subset-construction-lemma→ : { Q : Set } { Σ : Set } →
|
|
|
65 (NFA : NAutomaton Q Σ ) → (astart : Q → Set )
|
|
|
66 → (x : List Σ)
|
|
|
67 → naccept NFA ( λ q1 → astart q1) x
|
|
|
68 → accept ( subset-construction NFA ) ( λ q1 → astart q1) x
|
|
|
69 subset-construction-lemma→ = {!!}
|
|
|
70
|
|
|
71 subset-construction-lemma← : { Q : Set } { Σ : Set } →
|
|
|
72 (NFA : NAutomaton Q Σ ) → (astart : Q → Set )
|
|
|
73 → (x : List Σ)
|
|
|
74 → accept ( subset-construction NFA ) ( λ q1 → astart q1) x
|
|
|
75 → naccept NFA ( λ q1 → astart q1) x
|
|
|
76 subset-construction-lemma← = {!!}
|
|
|
77
|
|
|
78 open import regular-language
|
|
|
79
|
|
|
80 open RegularLanguage
|
|
|
81 open Automaton
|
|
|
82 open import Data.Empty
|
|
|
83
|
|
|
84 Concat-exists : {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → (states A ∨ states B → Set) → Set
|
|
|
85 Concat-exists {n} {Σ} A B P = exists (automaton A) (λ q → P (case1 q)) ∨ exists (automaton B) (λ q → P (case2 q))
|
|
|
86
|
|
|
87 Concat-NFA : {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → NAutomaton (states A ∨ states B) Σ
|
|
|
88 Concat-NFA {n} {Σ} A B = record { Nδ = δnfa ; NF = nend ; Nexists = Concat-exists A B }
|
|
|
89 module Concat-NFA where
|
|
|
90 data δnfa : states A ∨ states B → Σ → states A ∨ states B → Set where
|
|
|
91 a-case : {q : states A} {i : Σ } → δnfa ( case1 q) i (case1 (δ (automaton A) q i))
|
|
|
92 ab-trans : {q : states A} {i : Σ } → F (automaton A) q → δnfa ( case1 q) i (case2 (δ (automaton B) (astart B) i))
|
|
|
93 b-case : {q : states B} {i : Σ } → δnfa ( case2 q) i (case2 (δ (automaton B) q i))
|
|
|
94 nend : states A ∨ states B → Set
|
|
|
95 nend (case2 q) = F (automaton B) q
|
|
|
96 nend (case1 q) = F (automaton A) q ∧ F (automaton B) (astart B) -- empty B case
|
|
|
97
|
|
|
98 data state-is {n : Level} {Σ : Set } (A : RegularLanguage {n} Σ ) : (a : states A ) → Set where
|
|
|
99 this : (a : states A) → state-is A a
|
|
|
100
|
|
|
101 closed-in-concat : {n : Level} {Σ : Set } → (A B : RegularLanguage {n} Σ ) → ( x : List Σ )
|
|
|
102 → isRegular (Concat {n} (contain A) (contain B)) x record {states = states A ∨ states B → Set ; astart = λ q → state-is A (astart A)
|
|
|
103 ; automaton = subset-construction ( Concat-NFA A B )}
|
|
|
104 closed-in-concat {Σ} A B x = {!!}
|
|
|
105
|
|
|
106
|
|
|
107
|
|
|
108
|
|
|
109
|
