annotate a04/lecture.ind @ 406:a60132983557

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 08 Nov 2023 21:35:54 +0900
parents 6f3636fbc481
children 3d0aa205edf9
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
37
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 -title: 非決定性オートマトン
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 決定性オートマトンは入力に対して次の状態が一意に決まる。一つの入力に対して可能な状態が複数ある場合を考える。
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
4 例えば、ドアの鍵がテンキーだったら、次に何を入れるかには自由度がある。
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
5 この拡張は容易で、状態遷移関数が状態の代わりに状態のリストを返せば良い。しかし、リストを使うとかなり煩雑になる。
37
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
7 このようなものが必要な理由は、 Regular Language の Concatを考えるためである。
104
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
8
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
9 Regular Language は Concatについて閉じている。これは オートマトン A と B があった時に、z を前半 x ++ y
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
10 にわけて x を A が受理し、y を B で受理するものを、単一ののオートマトンで実現できると言う意味である。
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
11 しかい、 これを決定性オートマトンで示すのは難しい。A ++ B の 境目がどこかを前もって予測することができないからである。
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
12
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
13 二つのオートマトンが、a0..ae b0..be につながる様子を図にしてみる。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
14
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
15 <center><img src="fig/concat.svg"></center>
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
16
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
17 このためには後半のB automatonを、前半のA automatonが終わる可能性がある時だけ、
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
18 一文字毎に増やしてやればよい。増やしたものの一つでも成功すればよい。Bが増えるので、その増えた状態を覚えておく必要がある。
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
19
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
20 an (Aのn番目の状態)と、b0...bn の部分集合
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
21
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
22 状態はAの状態とBの状態の部分集合の組になる。
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
23
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
24 --(a.*f)(b.*f) を考えよう
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
25
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
26 abcfbffbcdf は、この正規表現にマッチする。a.*fb.*f と書いても良い。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
27
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
28 a.*f は以下の状態遷移で書ける。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
29
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
30 State は a0,a1,ae,af で、ae ならば受理。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
31
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
32 δa a0 a = a1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
33 δa a1 f = ae
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
34 δa a1 _ = a1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
35 δa a0 _ = af
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
36
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
37 b.*f もどうように書ける。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
38
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
39 δb b0 b = b1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
40 δb b1 f = be
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
41 δb b1 _ = b1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
42 δb b0 _ = bf
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
43
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
44 これを使って、a.*fb.*f を受理してみる。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
45
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
46 <center><img src="fig/af-concat.svg"></center>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
47
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
48 受理パターンは二通りある。これを非決定性があるという。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
49
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
50 この状況は、f がきた時に a.*f を終了しても良く、終了しなくてよいことから来てる。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
51
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
52 なので、それを許すオートマトンを考える。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
53
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
54 --非決定性オートマトン
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
55
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
56 オートマトンの状態遷移は関数だった。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
57
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
58 δ : Q → Σ → Q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
59
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
60 その代わりに、複数の状態を許したい。Aの場合なら、f でaeにもa1にもいって良い。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
61 それには、a1の状態で f がきた時に ae と a1 で true を返すようにすると良い。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
62 行き先の状態を Q → Bool で、部分集合として指定する。
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
63
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
64 record NAutomaton ( Q : Set ) ( Σ : Set )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
65 : Set where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
66 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
67 Nδ : Q → Σ → Q → Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
68 Nend : Q → Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
69
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
70 これを非決定性オートマトンという。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
71
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
72 入力にそって、可能な状態の集合を作ってやれば良い。そうすると
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
73 決定性オートマトンにできる。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
74
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
75 <center><img src="fig/afbf.svg"></center>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
76
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
77
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
78 --もう一つの例
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
79
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
80
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
81 この場合では 1 が来た時に q1 に行っても、q2,q3 に行っても良い。q1から始める。
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
82
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
83 q1 0 → q1
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
84 q1 1 → q1
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
85 q1 1 → q2
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
86 q1 1 → q3
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
87 q2 0 → q3
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
88 q3 1 → q4
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
89 q4 0 → q4
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
90 q4 1 → q4
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
91
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
92 最後に q4で accept。
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
93
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
94 <center><img src="fig/nfa.svg"></center>
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
95
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
96 この時に、入力に従って状態の部分集合を計算していく方法でNFAのacceptを決定できる。
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
97
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
98 このNFA(nondeterministic automaton)は .*(101|11).* に対応している。
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
99
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
100
104
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
101 --Agda での非決定性オートマトン
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
102
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
103 ここでは、部分集合を写像を使って表す。集合 Q から Bool (true または false) への写像を使う。true になる要素が
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
104 部分集合になる。すると、遷移関数は入力Σと状態から Bool への写像となる。終了条件は変わらない。
37
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 record NAutomaton ( Q : Set ) ( Σ : Set )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107 : Set where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108 field
69
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
109 Nδ : Q → Σ → Q → Bool
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
110 Nend : Q → Bool
37
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111
104
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
112 これを非決定性オートマトンという。Agda では同じ名前を使いまわしすることはできない(monomorpphism)ので、Nを付けた。
37
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
114 たとえば、以下のように非決定的な状態遷移を定義する
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
115
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
116 transition3 : States1 → In2 → States1 → Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
117 transition3 sr i0 sr = true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
118 transition3 sr i1 ss = true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
119 transition3 sr i1 sr = true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
120 transition3 ss i0 sr = true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
121 transition3 ss i1 st = true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
122 transition3 st i0 sr = true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
123 transition3 st i1 st = true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
124 transition3 _ _ _ = false
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
125
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
126
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
127 <a href="../agda/src/nfa.agda"> nfa.agda </a>
37
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
128
104
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
129 --NAutomatonの受理と遷移
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
130
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
131 非決定性オートマトンでは、一つの入力に対して、複数の状態が行き先になる。複数の状態を経由した経路のどれかが
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
132 入力を読み終わった後に、終了状態になれば受理されることになる。
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
133
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
134 このためには、状態の集合Qから条件 P : Q → Bool で true になるものを見つけ出す必要がある。
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
135
326
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
136 --状態と入力の List を使って深さ優先探索する
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
137
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
138 {-# TERMINATING #-}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
139 NtraceDepth : { Q : Set } { Σ : Set }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
140 → NAutomaton Q Σ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
141 → (Nstart : Q → Bool) → List Q → List Σ → List (List ( Σ ∧ Q ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
142 NtraceDepth {Q} {Σ} M sb all is = ndepth all sb is [] [] where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
143 ndepth : List Q → (q : Q → Bool ) → List Σ → List ( Σ ∧ Q ) → List (List ( Σ ∧ Q ) ) → List (List ( Σ ∧ Q ) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
144 ndepth1 : Q → Σ → List Q → List Σ → List ( Σ ∧ Q ) → List ( List ( Σ ∧ Q )) → List ( List ( Σ ∧ Q ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
145 ndepth1 q i [] is t t1 = t1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
146 ndepth1 q i (x ∷ qns) is t t1 = ndepth all (Nδ M x i) is (⟪ i , q ⟫ ∷ t) (ndepth1 q i qns is t t1 )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
147 ndepth [] sb is t t1 = t1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
148 ndepth (q ∷ qs) sb [] t t1 with sb q /\ Nend M q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
149 ... | true = ndepth qs sb [] t ( t ∷ t1 )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
150 ... | false = ndepth qs sb [] t t1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
151 ndepth (q ∷ qs) sb (i ∷ is) t t1 with sb q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
152 ... | true = ndepth qs sb (i ∷ is) t (ndepth1 q i all is t t1 )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
153 ... | false = ndepth qs sb (i ∷ is) t t1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
154
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
155 確かに動く。しかし、複雑すぎる。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
156
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
157 --状態の部分集合を使う
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
158
104
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
159 true になるものは複数あるので、やはり部分集合で表される。つまり、
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
160
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
161 exists : ( P : Q → Bool ) → Q → Bool
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
162
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
163 このような関数を実現する必要がある。
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
164
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
165 もし、Q が有限集合なら、P を順々に調べていけばよい。やはり List で良いのだが、ここでは Agda の Data.Fin を使ってみよう。
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
166
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
167
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
168 --NAutomatonの受理と遷移
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
169
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
170 状態の受理と遷移は exists を使って以下のようになる。
37
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
171
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
172 Nmoves : { Q : Set } { Σ : Set }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
173 → NAutomaton Q Σ
332
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
174 → (exists : ( Q → Bool ) → Bool)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
175 → ( Qs : Q → Bool ) → (s : Σ ) → ( Q → Bool )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
176 Nmoves {Q} { Σ} M exists Qs s = λ q → exists ( λ qn → (Qs qn /\ ( Nδ M qn s q ) ))
37
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
177
104
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
178 Qs は Q → Bool の型を持っているので、Qs qn は true または false である。今の状態集合 Qs に含まれていて、
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
179 Nδ M qn s q つまり、非決定オートマトン M の遷移関数 Nδ : Q → Σ → Q → Bool で true を返すものが存在すれば
326
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
180 遷移可能になる。(だいぶ簡単になった)
104
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
181
332
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
182
104
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
183 Naccept : { Q : Set } { Σ : Set }
37
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
184 → NAutomaton Q Σ
332
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
185 → (exists : ( Q → Bool ) → Bool)
69
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
186 → (Nstart : Q → Bool) → List Σ → Bool
332
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
187 Naccept M exists sb [] = exists ( λ q → sb q /\ Nend M q )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
188 Naccept M exists sb (i ∷ t ) = Naccept M exists (λ q → exists ( λ qn → (sb qn /\ ( Nδ M qn i q ) ))) t
69
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
189
104
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
190 Naccept では終了条件を調べる。状態の集合 sb で Nend を満たすものがあることを exists を使って調べればよい。
69
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
191
37
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
192 --例題
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
193
104
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
194 例題1.36 を考えよう。状態遷移関数は以下のようになる。
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
195
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
196 transition136 : StatesQ → A2 → StatesQ → Bool
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
197 transition136 q1 b0 q2 = true
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
198 transition136 q1 a0 q1 = true -- q1 → ep → q3
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
199 transition136 q2 a0 q2 = true
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
200 transition136 q2 a0 q3 = true
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
201 transition136 q2 b0 q3 = true
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
202 transition136 q3 a0 q1 = true
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
203 transition136 _ _ _ = false
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
204
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
205 教科書にはε遷移(入力がなくても遷移できる)があるが、ここでは、ε遷移先の矢印を全部手元に持ってきてしまうという
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
206 ことしてしまう。
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
207
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
208 end136 : StatesQ → Bool
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
209 end136 q1 = true
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
210 end136 _ = false
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
211
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
212 start136 : StatesQ → Bool
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
213 start136 q1 = true
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
214 start136 _ = false
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
215
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
216 nfa136 : NAutomaton StatesQ A2
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
217 nfa136 = record { Nδ = transition136; Nend = end136 }
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
218
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
219 <a href=" ../agda/nfa136.agda"> 1.36 の例題 </a>
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
220
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
221 example136-1 = Naccept nfa136 finStateQ start136( a0 ∷ b0 ∷ a0 ∷ [] )
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
222
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
223 最初の状態 q1 から a0 ∷ b0 ∷ a0 ∷ [] の入力を受けとる場合を考える。
37
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
224
104
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
225 a0 を受けとると、q1 にしか行けない。q1 で b0 を受けとると、q2 に移動する。q2 で a0 を受けとると、q3 か、または、
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
226 q2 に行ける。どちらも終了状態ではないので、不受理となる。ここで、もう一つ a0 が来れば q3 から q1 に行ける。q2
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
227 から行けないが、どれかの経路が成功すれば良いので受理となる。
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
228
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
229 example136-2 = Naccept nfa136 finStateQ start136( a0 ∷ b0 ∷ a0 ∷ a0 ∷ [] )
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
230
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
231
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
232
326
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
233
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
234
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
235
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
237
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
238
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
239
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
240
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
241
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
242