Members/kono/Proof/automaton: a04/lecture.ind annotate

annotate a04/lecture.ind @ 294:248711134141

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Wed, 29 Dec 2021 19:08:28 +0900
parents	b3f05cd08d24
children	a3fb231feeb9

rev	line source
37 a7f09c9a2c7a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	1 -title: 非決定性オートマトン
a7f09c9a2c7a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	2
a7f09c9a2c7a fix 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 a7f09c9a2c7a fix 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
141 b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	13 <center><img src="fig/concat.svg"></center>
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	14
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	15 このためには後半のB automatonを、前半のA automatonが終わる可能性がある時だけ、
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	16 一文字毎に増やしてやればよい。増やしたものの一つでも成功すればよい。Bが増えるので、その増えた状態を覚えておく必要がある。
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	17
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	18 an (Aのn番目の状態)と、b0...bn の部分集合
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 状態はAの状態とBの状態の部分集合の組になる。
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 --非決定性オートマトン
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	23
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	24 そこで、状態の部分集合からなるオートマトンを考える。
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	25
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	26 これは状態遷移が非決定的な場合に相当する。この場合では 1 が来た時に q1 に
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	27 行っても、q2,q3 に行っても良い。q1から始める。
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	28
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	29 q1 0 → q1
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	30 q1 1 → q1
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	31 q1 1 → q2
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	32 q1 1 → q3
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	33 q2 0 → q3
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	34 q3 1 → q4
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	35 q4 0 → q4
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	36 q4 1 → q4
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	37
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	38 最後に q4で accept。
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	39
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	40 <center><img src="fig/nfa.svg"></center>
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	41
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	42 この時に、入力に従って状態の部分集合を計算していく方法でNFAのacceptを決定できる。
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	43
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	44 このNFA(nondeterministic automaton)は .(101\|11). に対応している。
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	45
b3f05cd08d24 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 104 diff changeset	46
104 fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	47 --Agda での非決定性オートマトン
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	48
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	49 ここでは、部分集合を写像を使って表す。集合 Q から Bool (true または false) への写像を使う。true になる要素が
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	50 部分集合になる。すると、遷移関数は入力Σと状態から Bool への写像となる。終了条件は変わらない。
37 a7f09c9a2c7a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	51
a7f09c9a2c7a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	52 record NAutomaton ( Q : Set ) ( Σ : Set )
a7f09c9a2c7a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	53 : Set where
a7f09c9a2c7a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	54 field
69 f124fceba460 subset construction Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 37 diff changeset	55 Nδ : Q → Σ → Q → Bool
f124fceba460 subset construction Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 37 diff changeset	56 Nend : Q → Bool
37 a7f09c9a2c7a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	57
104 fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	58 これを非決定性オートマトンという。Agda では同じ名前を使いまわしすることはできない(monomorpphism)ので、Nを付けた。
37 a7f09c9a2c7a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	59
69 f124fceba460 subset construction Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 37 diff changeset	60 <a href="../agda/nfa.agda"> nfa.agda </a>
37 a7f09c9a2c7a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	61
104 fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	62 --NAutomatonの受理と遷移
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	63
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	64 非決定性オートマトンでは、一つの入力に対して、複数の状態が行き先になる。複数の状態を経由した経路のどれかが
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	65 入力を読み終わった後に、終了状態になれば受理されることになる。
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	66
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	67 このためには、状態の集合Qから条件 P : Q → Bool で true になるものを見つけ出す必要がある。
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	68
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	69 true になるものは複数あるので、やはり部分集合で表される。つまり、
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	70
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	71 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	72
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	73 このような関数を実現する必要がある。
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	74
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	75 もし、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	76
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	77 --finiteSet
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	78
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	79 Data.Fin だけを使って記述することもできるが、数字だけというのも味気ない。
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	80
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	81 record FiniteSet ( Q : Set ) { n : ℕ } : Set where
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	82 field
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	83 Q←F : Fin n → Q
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	84 F←Q : Q → Fin n
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	85 finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	86 finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	87
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	88 という感じで、Data.Fin と状態を対応させる。そうすると、
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	89
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	90 lt0 : (n : ℕ) → n Data.Nat.≤ n
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	91 lt0 zero = z≤n
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	92 lt0 (suc n) = s≤s (lt0 n)
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	93
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	94 exists1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → Bool
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	95 exists1 zero _ _ = false
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	96 exists1 ( suc m ) m<n p = p (Q←F (fromℕ≤ {m} {n} m<n)) \/ exists1 m (lt2 m<n) p
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	97
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	98 exists : ( Q → Bool ) → Bool
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	99 exists p = exists1 n (lt0 n) p
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	100
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	101 という形で、 exists を記述することができる。
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 <a href="../agda/finiteSet.agda"> finiteSet.agda </a>
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	104
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	105
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	106 --NAutomatonの受理と遷移
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	107
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	108 状態の受理と遷移は exists を使って以下のようになる。
37 a7f09c9a2c7a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	109
a7f09c9a2c7a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	110 Nmoves : { Q : Set } { Σ : Set }
a7f09c9a2c7a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	111 → NAutomaton Q Σ
a7f09c9a2c7a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	112 → {n : ℕ } → FiniteSet Q {n}
104 fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	113 → ( Qs : Q → Bool ) → (s : Σ ) → Q → Bool
37 a7f09c9a2c7a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	114 Nmoves {Q} { Σ} M fin Qs s q =
104 fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	115 exists fin ( λ qn → (Qs qn /\ ( Nδ M qn s q ) ))
37 a7f09c9a2c7a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	116
104 fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	117 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	118 Nδ M qn s q つまり、非決定オートマトン M の遷移関数 Nδ : Q → Σ → Q → Bool で true を返すものが存在すれば
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	119 遷移可能になる。
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	120
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	121 Naccept : { Q : Set } { Σ : Set }
37 a7f09c9a2c7a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	122 → NAutomaton Q Σ
a7f09c9a2c7a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	123 → {n : ℕ } → FiniteSet Q {n}
69 f124fceba460 subset construction Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 37 diff changeset	124 → (Nstart : Q → Bool) → List Σ → Bool
104 fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	125 Naccept M fin sb [] = exists fin ( λ q → sb q /\ Nend M q )
69 f124fceba460 subset construction Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 37 diff changeset	126 Naccept M fin sb (i ∷ t ) = Naccept M fin ( Nmoves M fin sb i ) t
f124fceba460 subset construction Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 37 diff changeset	127
104 fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	128 Naccept では終了条件を調べる。状態の集合 sb で Nend を満たすものがあることを exists を使って調べればよい。
69 f124fceba460 subset construction Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 37 diff changeset	129
37 a7f09c9a2c7a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	130
a7f09c9a2c7a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	131 --例題
a7f09c9a2c7a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	132
104 fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	133 例題1.36 を考えよう。状態遷移関数は以下のようになる。
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	134
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	135 transition136 : StatesQ → A2 → StatesQ → Bool
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	136 transition136 q1 b0 q2 = true
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	137 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	138 transition136 q2 a0 q2 = true
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	139 transition136 q2 a0 q3 = true
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	140 transition136 q2 b0 q3 = true
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	141 transition136 q3 a0 q1 = true
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	142 transition136 _ _ _ = false
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	143
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	144 教科書にはε遷移(入力がなくても遷移できる)があるが、ここでは、ε遷移先の矢印を全部手元に持ってきてしまうという
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	145 ことしてしまう。
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	146
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	147 end136 : StatesQ → Bool
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	148 end136 q1 = true
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	149 end136 _ = false
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	150
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	151 start136 : StatesQ → Bool
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	152 start136 q1 = true
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	153 start136 _ = false
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	154
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	155 nfa136 : NAutomaton StatesQ A2
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	156 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	157
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	158 <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	159
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	160 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	161
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	162 最初の状態 q1 から a0 ∷ b0 ∷ a0 ∷ [] の入力を受けとる場合を考える。
37 a7f09c9a2c7a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	163
104 fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	164 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	165 q2 に行ける。どちらも終了状態ではないので、不受理となる。ここで、もう一つ a0 が来れば q3 から q1 に行ける。q2
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 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	169
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	170
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	171 --問題
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	172
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	173 ... 作成中...
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	174
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	175
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	176 --非決定性オートマトンと決定性オートマトン
37 a7f09c9a2c7a fix 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 record Automaton ( Q : Set ) ( Σ : Set )
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	179 : Set where
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	180 field
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	181 δ : Q → Σ → Q
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	182 aend : Q → Bool
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	183
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	184 の Q に Q → Bool を入れてみる。
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	185
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	186 δ : (Q → Bool ) → Σ → Q → Bool
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	187 aend : (Q → Bool ) → Bool
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	188
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	189 これを、
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	190
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	191 record NAutomaton ( Q : Set ) ( Σ : Set )
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	192 : Set where
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	193 field
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	194 Nδ : Q → Σ → Q → Bool
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	195 Nend : Q → Bool
37 a7f09c9a2c7a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	196
104 fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	197 これの Nδ と Nend から作れれば、NFA から DFA を作れることになる。
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	198
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	199 NFAの受理を考えると、状態の集合を持ち歩いて受理を判断している。つまり、状態の集合を状態とする Automaton を考えることになる。
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	200
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	201 遷移条件は、状態の集合を受けとって、条件を満たす状態の集合を返せば良い。条件は
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	202
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	203 Nδ : Q → Σ → Q → Bool
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 だった。つまり、入力の状態集合を選別する関数 f と、 Nδ との /\ を取ってやればよい。q は何かの状態、iは入力、nq は次の状態である。
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 f q /\ Nδ NFA q i nq
69 f124fceba460 subset construction Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 37 diff changeset	208
104 fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	209 これが true になるものを exists を使って探し出す。
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	210
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	211 δconv : { Q : Set } { Σ : Set } { n : ℕ } → FiniteSet Q {n} → ( nδ : Q → Σ → Q → Bool ) → (f : Q → Bool) → (i : Σ) → (Q → Bool)
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	212 δconv {Q} { Σ} { n} N nδ f i q = exists N ( λ r → f r /\ nδ r i q )
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	213
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	214 ここで、( nδ : Q → Σ → Q → Bool ) は NFAの状態遷移関数を受けとる部分である。
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 終了条件は
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	217
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	218 f q /\ Nend NFA q )
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	219 '
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	220 で良い。これが true になるものを exists を使って探し出す。
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	221
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	222 Q が FiniteSet Q {n} であれば
37 a7f09c9a2c7a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	223
104 fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	224 subset-construction : { Q : Set } { Σ : Set } { n : ℕ } → FiniteSet Q {n} →
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	225 (NAutomaton Q Σ ) → (astart : Q ) → (Automaton (Q → Bool) Σ )
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	226 subset-construction {Q} { Σ} {n} fin NFA astart = record {
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	227 δ = λ f i → δconv fin ( Nδ NFA ) f i
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	228 ; aend = λ f → exists fin ( λ q → f q /\ Nend NFA q )
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	229 }
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 という形で書くことができる。状態の部分集合を作っていくので、subset construction と呼ばれる。
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	232
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	233 λ f i → δconv fin ( Nδ NFA ) f i
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	234 は
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	235 λ f i q → δconv fin ( Nδ NFA ) f i q
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	236
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	237 であることに注意しよう。これは、Curry 化の省略になっている。省略があるので、δ : (Q → Bool ) → Σ → Q → Bool という形に見える。
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	238
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	239 <a href=" ../agda/sbconst2.agda"> subset construction </a>
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	240
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	241 --subset constructionの状態数
37 a7f09c9a2c7a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	242
104 fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	243 実際にこれを計算すると、状態数 n のNFAから、最大、2^n の状態を持つDFAが生成される。しかし、この論理式からそれを
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	244 自明に理解することは難しい。しかし、f は Q → Bool なので、例えば、3状態でも、
37 a7f09c9a2c7a fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	245
104 fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	246 q1 q2 q3
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	247 false false false
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	248 false false true
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	249 false true false
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	250 false true true
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	251 true false false
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	252 true false true
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	253 true true false
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	254 true true true
69 f124fceba460 subset construction Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 37 diff changeset	255
104 fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	256 という8個の状態を持つ。exists は、このすべての場合を尽くすように働いている。
69 f124fceba460 subset construction Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 37 diff changeset	257
104 fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	258 アルゴリズムとしてこのまま実装すると、 exists が必要な分だけ計算するようになっている。これは結構遅い。
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	259 前もって、可能な状態を Automaton として探し出そうとすると、指数関数的な爆発になってしまう。
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	260
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	261 実際に、指数関数的な状態を作る NFA が存在するので、これを避けることはできない。
fba1cd54581d use exists in cond, nfa example Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	262

Mercurial > hg > Members > kono > Proof > automaton

annotate a04/lecture.ind @ 294:248711134141