Mercurial > hg > Members > kono > Proof > automaton1

comparison nfa.agda @ 0:9615a94b18ca

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
new automaton in agda
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 12 Nov 2020 11:45:34 +0900
parents
children 7399aae907fc
comparison
equal deleted inserted replaced
-1:000000000000 0:9615a94b18ca
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