|
37
|
1 -title: 決定性オートマトン
|
|
|
2
|
|
|
3 -- Automaton オートマトンの定義 ( Q, Σ, σ, q0, F )
|
|
|
4
|
|
|
5 1. Q is a finte set calles states
|
|
|
6 2. Σ is a finte set calles alphabet
|
|
|
7 3. δ : Q x Σ is the transition function
|
|
|
8 4. q0 ∈ Q is the start state
|
|
|
9 5. F ⊆ Q is the set of accept states
|
|
|
10
|
|
|
11 これを Agda で表すには record を使う。
|
|
|
12
|
|
|
13 record Automaton ( Q : Set ) ( Σ : Set )
|
|
|
14 : Set where
|
|
|
15 field
|
|
|
16 δ : Q → Σ → Q
|
|
|
17 aend : Q → Bool
|
|
|
18
|
|
|
19 <a href="../agda/automaton.agda"> automaton.agda </a>
|
|
65
|
20 <br>
|
|
|
21 <a href="../agda/logic.agda"> logic.agda </a>
|
|
|
22 <br>
|
|
|
23 <a href="../agda/finiteSet.agda"> finiteSet.agda </a>
|
|
|
24 <br>
|
|
37
|
25
|
|
|
26 record は名前のついた数学的構造で、二つの集合 Q と Σの関係定義する関数からなる。
|
|
|
27
|
|
|
28 record は直積で複数の集合の組だが、ここでは関係を表す論理式/関数の型の組になっている。
|
|
|
29
|
|
|
30 δ : Q → Σ → Q
|
|
|
31
|
|
|
32 は関数で、引数を二つ持っている。ここでは論理式ではない。入力となるaplhabet(文字) とstate (状態)から次の状態を指定する関数である。
|
|
|
33 transition function (状態遷移関数)と呼ばれる。
|
|
|
34
|
|
|
35 aend : Q → Bool
|
|
|
36
|
|
|
37 これはQの部分集合を指定している。Bool は
|
|
|
38
|
|
|
39 data Bool : Set where
|
|
|
40 true : Bool
|
|
|
41 false : Bool
|
|
|
42
|
|
|
43 で、true false の二つの要素を持つ集合である。(これでどうして部分集合になるのか? F ⊆ Q を Agda ではどう定義するべきか?)
|
|
|
44
|
|
63
|
45 start state はrecordで定義しない方が便利だと言うことがこの後わかる。
|
|
|
46
|
|
37
|
47 --オートマトンの入力
|
|
|
48
|
|
|
49 オートマトンの入力は文字列である。文字列を表すには List を用いる。
|
|
|
50
|
|
|
51 data List (A : Set ) : Set where
|
|
|
52 [] : List A
|
|
|
53 _∷_ : A → List A → List A
|
|
|
54
|
|
|
55 l2 = a ∷ b ∷ a ∷ c ∷ []
|
|
|
56
|
|
|
57 だったことを思い出そう。(Agda のbuiltinのListは ∷ を使う)
|
|
|
58
|
|
|
59
|
|
|
60 --状態遷移
|
|
|
61
|
|
|
62 状態遷移関数をListに適用する。
|
|
|
63
|
|
|
64 moves : { Q : Set } { Σ : Set }
|
|
|
65 → Automaton Q Σ
|
|
|
66 → Q → List Σ → Q
|
|
|
67 moves {Q} { Σ} M q L = move q L
|
|
|
68 where
|
|
|
69 move : (q : Q ) ( L : List Σ ) → Q
|
|
|
70 move q [] = q
|
|
|
71 move q ( H ∷ T ) = move ( (δ M) q H ) T
|
|
|
72
|
|
|
73 List に沿って、状態が変わる。
|
|
|
74
|
|
|
75 accept : { Q : Set } { Σ : Set }
|
|
|
76 → Automaton Q Σ
|
|
63
|
77 → (astart : Q)
|
|
37
|
78 → List Σ → Bool
|
|
63
|
79 accept {Q} { Σ} M astart L = move astart L
|
|
37
|
80 where
|
|
|
81 move : (q : Q ) ( L : List Σ ) → Bool
|
|
|
82 move q [] = aend M q
|
|
|
83 move q ( H ∷ T ) = move ( (δ M) q H ) T
|
|
|
84
|
|
63
|
85
|
|
37
|
86 最後の状態が aend ならば accept される。これらを、record Automaton 内で定義しても良い。
|
|
|
87
|
|
|
88 ---具体的なオートマトン
|
|
|
89
|
|
|
90 reccord Automaton は抽象的なオートマトンで実装がない。(Java/C++ の abstract classと同じ)
|
|
|
91 実装を与えるには、record のfield の型を持つ関数を与えれば良い。
|
|
|
92
|
|
|
93 まず、状態と文字を定義する。
|
|
|
94
|
|
|
95 data States1 : Set where
|
|
|
96 sr : States1
|
|
|
97 ss : States1
|
|
|
98 st : States1
|
|
|
99
|
|
|
100 data In2 : Set where
|
|
|
101 i0 : In2
|
|
|
102 i1 : In2
|
|
|
103
|
|
|
104 状態遷移関数と accept state を作ろう。
|
|
|
105
|
|
|
106 transition1 : States1 → In2 → States1
|
|
|
107 transition1 sr i0 = sr
|
|
|
108 transition1 sr i1 = ss
|
|
|
109 transition1 ss i0 = sr
|
|
|
110 transition1 ss i1 = st
|
|
|
111 transition1 st i0 = sr
|
|
|
112 transition1 st i1 = st
|
|
|
113
|
|
|
114 fin1 : States1 → Bool
|
|
|
115 fin1 st = true
|
|
|
116 fin1 _ = false
|
|
|
117
|
|
|
118 st になればok。record は以下のように作る。
|
|
|
119
|
|
|
120 am1 : Automaton States1 In2
|
|
63
|
121 am1 = record { δ = transition1 ; aend = fin1 }
|
|
37
|
122
|
|
|
123 これを動かすには、
|
|
|
124
|
|
|
125 example1-1 = accept am1 ( i0 ∷ i1 ∷ i0 ∷ [] )
|
|
|
126 example1-2 = accept am1 ( i1 ∷ i1 ∷ i1 ∷ [] )
|
|
|
127
|
|
|
128 とする。( example1-1 の型は何か?)
|
|
|
129
|
|
|
130 --問題 3.1
|
|
|
131
|
|
|
132 教科書のAutomatonの例のいくつかを Agda で定義してみよ。
|
|
|
133
|
|
|
134 accept される入力と accept されない入力を示し、Agda で true false を確認せよ。
|
|
|
135
|
|
|
136 <a href=""> </a> <!--- Exercise 3.1 --->
|
|
|
137
|
|
|
138
|
|
59
|
139 --Regular Language
|
|
37
|
140
|
|
59
|
141 Language とは?
|
|
|
142
|
|
|
143 Regular Language とは?
|
|
|
144
|
|
|
145 --Regular Languageの演算
|
|
|
146
|
|
|
147 Concatenation
|
|
|
148
|
|
|
149 Union
|
|
|
150
|
|
|
151 Star
|
|
|
152
|
|
65
|
153 <a href="../agda/regular-language.agda"> Agda での Regular Language </a>
|
|
59
|
154
|
|
|
155
|
|
|
156
|
