|
37
|
1 -title: 非決定性オートマトン
|
|
|
2
|
|
|
3 決定性オートマトンは入力に対して次の状態が一意に決まる。一つの入力に対して可能な状態が複数ある場合を考える。
|
|
|
4
|
|
|
5 例えば、ドアの鍵がテンキーだったら、次に何を入れるかには自由度がある。
|
|
|
6
|
|
|
7 この拡張は容易で、状態遷移関数が状態の代わりに状態のリストを返せば良い。部分集合を使っても良いが、ここではリストを使おう。
|
|
|
8
|
|
|
9 record NAutomaton ( Q : Set ) ( Σ : Set )
|
|
|
10 : Set where
|
|
|
11 field
|
|
69
|
12 Nδ : Q → Σ → Q → Bool
|
|
|
13 Nend : Q → Bool
|
|
37
|
14
|
|
|
15 これを非決定性オートマトンという。Agda では同じ名前を使いまわしすることはできない(monomorpphism)ので、nを付けた。
|
|
|
16
|
|
69
|
17 <a href="../agda/nfa.agda"> nfa.agda </a>
|
|
37
|
18
|
|
69
|
19 状態の受理と遷移は以下のようになる。
|
|
37
|
20
|
|
|
21 Nmoves : { Q : Set } { Σ : Set }
|
|
|
22 → NAutomaton Q Σ
|
|
|
23 → {n : ℕ } → FiniteSet Q {n}
|
|
|
24 → ( Q → Bool ) → Σ → Q → Bool
|
|
|
25 Nmoves {Q} { Σ} M fin Qs s q =
|
|
|
26 exists fin ( λ qn → (Qs qn ∧ ( Nδ M qn s q ) ))
|
|
|
27
|
|
69
|
28 Naccept : { Q : Set } { Σ : Set }
|
|
37
|
29 → NAutomaton Q Σ
|
|
|
30 → {n : ℕ } → FiniteSet Q {n}
|
|
69
|
31 → (Nstart : Q → Bool) → List Σ → Bool
|
|
|
32 Naccept M fin sb [] = exists fin ( λ q → sb q ∧ Nend M q )
|
|
|
33 Naccept M fin sb (i ∷ t ) = Naccept M fin ( Nmoves M fin sb i ) t
|
|
|
34
|
|
|
35 次の状態は状態の集合(List)になる。次の次の状態は、可能な状態の次の状態の集合を合わせた(union)ものになる。
|
|
|
36 しかし、List で定義すると少し複雑になる。
|
|
|
37
|
|
|
38 部分集合を使うと簡単になる。Q の部分集合は Q → Bool で true になるものであるとする。
|
|
|
39
|
|
37
|
40
|
|
|
41 --例題
|
|
|
42
|
|
|
43 transition3 : States1 → In2 → States1 → Bool
|
|
|
44 transition3 sr i0 sr = true
|
|
|
45 transition3 sr i1 ss = true
|
|
|
46 transition3 sr i1 sr = true
|
|
|
47 transition3 ss i0 sr = true
|
|
|
48 transition3 ss i1 st = true
|
|
|
49 transition3 st i0 sr = true
|
|
|
50 transition3 st i1 st = true
|
|
|
51 transition3 _ _ _ = false
|
|
|
52
|
|
|
53 fin1 : States1 → Bool
|
|
|
54 fin1 st = true
|
|
|
55 fin1 ss = false
|
|
|
56 fin1 sr = false
|
|
|
57
|
|
|
58 start1 : States1 → Bool
|
|
|
59 start1 sr = true
|
|
|
60 start1 _ = false
|
|
|
61
|
|
|
62 am2 : NAutomaton States1 In2
|
|
69
|
63 am2 = record { Nδ = transition3 ; Nend = fin1}
|
|
|
64
|
|
|
65 example2-1 = Naccept am2 finState1 start1 ( i0 ∷ i1 ∷ i0 ∷ [] )
|
|
|
66 example2-2 = Naccept am2 finState1 start1 ( i1 ∷ i1 ∷ i1 ∷ [] )
|
|
37
|
67
|
|
69
|
68 fin0 : States1 → Bool
|
|
|
69 fin0 st = false
|
|
|
70 fin0 ss = false
|
|
|
71 fin0 sr = false
|
|
37
|
72
|
|
69
|
73 test0 : Bool
|
|
|
74 test0 = exists finState1 fin0
|
|
37
|
75
|
|
69
|
76 test1 : Bool
|
|
|
77 test1 = exists finState1 fin1
|
|
|
78
|
|
|
79 test2 = Nmoves am2 finState1 start1
|
|
|
80
|
