Mercurial > hg > Members > kono > Proof > automaton

comparison a04/lecture.ind @ 331:9324852d3a17

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 07 Dec 2022 14:51:25 +0900
parents a3fb231feeb9
children 6f3636fbc481
comparison
equal deleted inserted replaced
330:407684f806e4 331:9324852d3a17
8 8
9 Regular Language は Concatについて閉じている。これは オートマトン A と B があった時に、z を前半 x ++ y 9 Regular Language は Concatについて閉じている。これは オートマトン A と B があった時に、z を前半 x ++ y
10 にわけて x を A が受理し、y を B で受理するものを、単一ののオートマトンで実現できると言う意味である。 10 にわけて x を A が受理し、y を B で受理するものを、単一ののオートマトンで実現できると言う意味である。
11 しかい、 これを決定性オートマトンで示すのは難しい。A ++ B の 境目がどこかを前もって予測することができないからである。 11 しかい、 これを決定性オートマトンで示すのは難しい。A ++ B の 境目がどこかを前もって予測することができないからである。
12 12
13 二つのオートマトンが、a0..ae b0..be につながる様子を図にしてみる。
14
13 <center><img src="fig/concat.svg"></center> 15 <center><img src="fig/concat.svg"></center>
14 16
15 このためには後半のB automatonを、前半のA automatonが終わる可能性がある時だけ、 17 このためには後半のB automatonを、前半のA automatonが終わる可能性がある時だけ、
16 一文字毎に増やしてやればよい。増やしたものの一つでも成功すればよい。Bが増えるので、その増えた状態を覚えておく必要がある。 18 一文字毎に増やしてやればよい。増やしたものの一つでも成功すればよい。Bが増えるので、その増えた状態を覚えておく必要がある。
17 19
18 an (Aのn番目の状態)と、b0...bn の部分集合 20 an (Aのn番目の状態)と、b0...bn の部分集合
19 21
20 状態はAの状態とBの状態の部分集合の組になる。 22 状態はAの状態とBの状態の部分集合の組になる。
21 23
24 --(a.*f)(b.*f) を考えよう
25
26 abcfbffbcdf は、この正規表現にマッチする。a.*fb.*f と書いても良い。
27
28 a.*f は以下の状態遷移で書ける。
29
30 State は a0,a1,ae,af で、ae ならば受理。
31
32 δa a0 a = a1
33 δa a1 f = ae
34 δa a1 _ = a1
35 δa a0 _ = af
36
37 b.*f もどうように書ける。
38
39 δb b0 b = b1
40 δb b1 f = be
41 δb b1 _ = b1
42 δb b0 _ = bf
43
44 これを使って、a.*fb.*f を受理してみる。
45
46 <center><img src="fig/af-concat.svg"></center>
47
48 受理パターンは二通りある。これを非決定性があるという。
49
50 この状況は、f がきた時に a.*f を終了しても良く、終了しなくてよいことから来てる。
51
52 なので、それを許すオートマトンを考える。
53
22 --非決定性オートマトン 54 --非決定性オートマトン
23 55
24 そこで、状態の部分集合からなるオートマトンを考える。 56 オートマトンの状態遷移は関数だった。
25 57
26 これは状態遷移が非決定的な場合に相当する。この場合では 1 が来た時に q1 に 58 δ : Q → Σ → Q
27 行っても、q2,q3 に行っても良い。q1から始める。 59
60 その代わりに、複数の状態を許したい。Aの場合なら、f でaeにもa1にもいって良い。
61 それには、a1の状態で f がきた時に ae と a1 で true を返すようにすると良い。
62 行き先の状態を Q → Bool で、部分集合として指定する。
63
64 record NAutomaton ( Q : Set ) ( Σ : Set )
65 : Set where
66 field
67 Nδ : Q → Σ → Q → Bool
68 Nend : Q → Bool
69
70 これを非決定性オートマトンという。
71
72 入力にそって、可能な状態の集合を作ってやれば良い。そうすると
73 決定性オートマトンにできる。
74
75 <center><img src="fig/afbf.svg"></center>
76
77
78 --もう一つの例
79
80
81 この場合では 1 が来た時に q1 に行っても、q2,q3 に行っても良い。q1から始める。
28 82
29 q1 0 → q1 83 q1 0 → q1
30 q1 1 → q1 84 q1 1 → q1
31 q1 1 → q2 85 q1 1 → q2
32 q1 1 → q3 86 q1 1 → q3
55 Nδ : Q → Σ → Q → Bool 109 Nδ : Q → Σ → Q → Bool
56 Nend : Q → Bool 110 Nend : Q → Bool
57 111
58 これを非決定性オートマトンという。Agda では同じ名前を使いまわしすることはできない(monomorpphism)ので、Nを付けた。 112 これを非決定性オートマトンという。Agda では同じ名前を使いまわしすることはできない(monomorpphism)ので、Nを付けた。
59 113
60 <a href="../agda/nfa.agda"> nfa.agda </a> 114 たとえば、以下のように非決定的な状態遷移を定義する
115
116 transition3 : States1 → In2 → States1 → Bool
117 transition3 sr i0 sr = true
118 transition3 sr i1 ss = true
119 transition3 sr i1 sr = true
120 transition3 ss i0 sr = true
121 transition3 ss i1 st = true
122 transition3 st i0 sr = true
123 transition3 st i1 st = true
124 transition3 _ _ _ = false
125
126
127 <a href="../agda/src/nfa.agda"> nfa.agda </a>
61 128
62 --NAutomatonの受理と遷移 129 --NAutomatonの受理と遷移
63 130
64 非決定性オートマトンでは、一つの入力に対して、複数の状態が行き先になる。複数の状態を経由した経路のどれかが 131 非決定性オートマトンでは、一つの入力に対して、複数の状態が行き先になる。複数の状態を経由した経路のどれかが
65 入力を読み終わった後に、終了状態になれば受理されることになる。 132 入力を読み終わった後に、終了状態になれば受理されることになる。