|
127
|
1 -title: push donwオートマトンと文法クラス
|
|
|
2
|
|
|
3 任意のnについて 0{n}1{n} に対応する有限オートマトンはない。
|
|
|
4
|
|
326
|
5 inputnn0 : ( n : ℕ ) → { Σ : Set } → ( x y : Σ ) → List Σ → List Σ
|
|
|
6 inputnn0 zero {_} _ _ s = s
|
|
|
7 inputnn0 (suc n) x y s = x ∷ ( inputnn0 n x y ( y ∷ s ) )
|
|
127
|
8
|
|
|
9 inputnn だけ受け付けて、それ以外を受け付けないということができない。
|
|
|
10
|
|
326
|
11 かっこの対応が取れないことに相当する。
|
|
|
12
|
|
|
13 inputnn : List In2 → Maybe (List In2)
|
|
|
14 inputnn [] = just []
|
|
|
15 inputnn (i1 ∷ t) = just (i1 ∷ t)
|
|
|
16 inputnn (i0 ∷ t) with inputnn t
|
|
|
17 ... | nothing = nothing
|
|
|
18 ... | just [] = nothing
|
|
|
19 ... | just (i0 ∷ t1) = nothing -- can't happen
|
|
|
20 ... | just (i1 ∷ t1) = just t1 -- remove i1 from later part
|
|
|
21
|
|
|
22 inputnn1 : List In2 → Bool
|
|
|
23 inputnn1 s with inputnn s
|
|
|
24 ... | nothing = false
|
|
|
25 ... | just [] = true
|
|
|
26 ... | just _ = false
|
|
|
27
|
|
|
28 こちらは 0{n}1{n} を受け付けるかどうか調べるプログラムである。
|
|
|
29
|
|
|
30 inputnn1 が inpuynn0 を受けつけるかどうかを証明する必要がある。
|
|
|
31
|
|
|
32 nn01 : (i : ℕ) → inputnn1 ( inputnn0 i i0 i1 [] ) ≡ true
|
|
|
33 nn01 = ?
|
|
|
34
|
|
|
35 これはやさしくない。一般的にプログラムが正しく動くことを証明することに相当する。
|
|
|
36
|
|
|
37 --pumping lemma
|
|
|
38
|
|
|
39 まず Trace を定義する。
|
|
|
40
|
|
|
41 data Trace { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) : (is : List Σ) → Q → Set where
|
|
|
42 tend : {q : Q} → aend fa q ≡ true → Trace fa [] q
|
|
|
43 tnext : (q : Q) → {i : Σ} { is : List Σ}
|
|
|
44 → Trace fa is (δ fa q i) → Trace fa (i ∷ is) q
|
|
|
45
|
|
|
46 これは Automaton が受け付ける文字列を生成する data である。実際、
|
|
|
47
|
|
|
48 tr-accept→ : { Q : Set } { Σ : Set }
|
|
|
49 → (fa : Automaton Q Σ )
|
|
|
50 → (is : List Σ) → (q : Q) → Trace fa is q → accept fa q is ≡ true
|
|
|
51 tr-accept→ {Q} {Σ} fa [] q (tend x) = x
|
|
|
52 tr-accept→ {Q} {Σ} fa (i ∷ is) q (tnext _ tr) = tr-accept→ {Q} {Σ} fa is (δ fa q i) tr
|
|
|
53
|
|
|
54 tr-accept← : { Q : Set } { Σ : Set }
|
|
|
55 → (fa : Automaton Q Σ )
|
|
|
56 → (is : List Σ) → (q : Q) → accept fa q is ≡ true → Trace fa is q
|
|
|
57 tr-accept← {Q} {Σ} fa [] q ac = tend ac
|
|
|
58 tr-accept← {Q} {Σ} fa (x ∷ []) q ac = tnext _ (tend ac )
|
|
|
59 tr-accept← {Q} {Σ} fa (x ∷ x1 ∷ is) q ac = tnext _ (tr-accept← fa (x1 ∷ is) (δ fa q x) ac)
|
|
|
60
|
|
|
61 もし、ある文字列を受け付ける Automaton の状態に重複があれば
|
|
127
|
62
|
|
|
63
|
|
326
|
64 record TA { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) ( q : Q ) (is : List Σ) : Set where
|
|
|
65 field
|
|
|
66 x y z : List Σ
|
|
|
67 xyz=is : x ++ y ++ z ≡ is
|
|
|
68 trace-xyz : Trace fa (x ++ y ++ z) q
|
|
|
69 trace-xyyz : Trace fa (x ++ y ++ y ++ z) q
|
|
|
70 non-nil-y : ¬ (y ≡ [])
|
|
127
|
71
|
|
326
|
72 pumping-lemma : { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) (finq : FiniteSet Q) (q qd : Q) (is : List Σ)
|
|
|
73 → (tr : Trace fa is q )
|
|
|
74 → dup-in-list finq qd (tr→qs fa is q tr) ≡ true
|
|
|
75 → TA fa q is
|
|
|
76
|
|
|
77 を示すことができる。(Agda ではあんまりやさしくないが、割と自明)
|
|
|
78
|
|
|
79 状態数よりも長い文字列を使えば、必ずこの方法で延長できる。 inputnn0 は、この性質を持たないので(なぜか?)
|
|
|
80 inputnn0 が正規言語でないことがわかる。
|
|
127
|
81
|
|
|
82 --push down automaton
|
|
|
83
|
|
326
|
84 Automatonを拡張して、これを受け付けるようにすることができる。
|
|
127
|
85
|
|
|
86 data PushDown ( Γ : Set ) : Set where
|
|
|
87 pop : PushDown Γ
|
|
|
88 push : Γ → PushDown Γ
|
|
326
|
89 none : PushDown Γ
|
|
127
|
90
|
|
326
|
91 record PDA ( Q : Set ) ( Σ : Set ) ( Γ : Set )
|
|
127
|
92 : Set where
|
|
|
93 field
|
|
326
|
94 automaton : Automaton Q Σ
|
|
|
95 pδ : Q → PushDown Γ
|
|
|
96 open Automaton
|
|
|
97 paccept : (q : Q ) ( In : List Σ ) ( sp : List Γ ) → Bool
|
|
|
98 paccept q [] [] = aend automaton q
|
|
|
99 paccept q (H ∷ T) [] with pδ (δ automaton q H)
|
|
|
100 paccept q (H ∷ T) [] | pop = paccept (δ automaton q H) T []
|
|
|
101 paccept q (H ∷ T) [] | none = paccept (δ automaton q H) T []
|
|
|
102 paccept q (H ∷ T) [] | push x = paccept (δ automaton q H) T (x ∷ [] )
|
|
|
103 paccept q [] (_ ∷ _ ) = false
|
|
|
104 paccept q ( H ∷ T ) ( SH ∷ ST ) with pδ (δ automaton q H)
|
|
|
105 ... | pop = paccept (δ automaton q H) T ST
|
|
|
106 ... | none = paccept (δ automaton q H) T (SH ∷ ST)
|
|
|
107 ... | push ns = paccept (δ automaton q H) T ( ns ∷ SH ∷ ST )
|
|
|
108
|
|
|
109 例えば
|
|
127
|
110
|
|
326
|
111 pnnp : PDA States2 In2 States2
|
|
|
112 pnnp = record {
|
|
|
113 automaton = record { aend = aend ; δ = δ }
|
|
|
114 ; pδ = pδ
|
|
|
115 } where
|
|
|
116 δ : States2 → In2 → States2
|
|
|
117 δ ph1 i0 = ph1
|
|
|
118 δ ph1 i1 = ph2
|
|
|
119 δ ph2 i1 = ph2
|
|
|
120 δ _ _ = phf
|
|
|
121 aend : States2 → Bool
|
|
|
122 aend ph2 = true
|
|
|
123 aend _ = false
|
|
|
124 pδ : States2 → PushDown States2
|
|
|
125 pδ ph1 = push ph1
|
|
|
126 pδ ph2 = pop
|
|
|
127 pδ phf = none
|
|
|
128
|
|
|
129 これと inputnn1 が同じ動作をすることを示せれば良い。
|
|
127
|
130
|
|
|
131 --文脈自由文法
|
|
|
132
|
|
326
|
133 PDA で受け付ける言語を文脈自由文法(context free grammer)という。
|
|
127
|
134
|
|
326
|
135 実際のプログラミング言語は、型宣言とかの文脈に依存するので、CFGではない。
|
|
|
136
|
|
|
137 しかし、文法自体は CFG で定義されることが多い。
|
|
|
138
|
|
332
|
139 文法定義には BNF (Buckas Noar Form)を使う。
|
|
326
|
140
|
|
332
|
141 expr : EA | EB | EC ;
|
|
|
142 statement :
|
|
|
143 SA | SB | SC
|
|
|
144 | IF expr THEN statement
|
|
|
145 | IF expr THEN statement ELSE statement
|
|
|
146 ;
|
|
326
|
147
|
|
|
148 これらを実際に parse するのには再帰下降法が便利なことが知られている。
|
|
|
149
|
|
|
150 現在のコンパイラは。だいたいそれで実装されている。
|
|
|
151
|
|
|
152 文法規則がプログラムで直接記述されるという利点もある。
|
|
|
153
|
|
|
154 --文脈依存文法
|
|
|
155
|
|
332
|
156 expr : EA | EB | EC ;
|
|
326
|
157
|
|
|
158 の部分を
|
|
|
159
|
|
332
|
160 delcare exprt : EA | EB | EC ;
|
|
326
|
161
|
|
332
|
162 のように : の左側に複数の要素を許す
|
|
|
163 と、文脈依存文法になる。これを判定して停止するプログラムは、stack を二つ持つ Automaton になるが、
|
|
326
|
164 Turing Machine と呼ばれる。 その停止性を判定することはできない。それを次の講義で示す。
|
|
|
165
|
|
|
166 実用的には文法規則の適当な subset を停止することが分かっているアルゴリズムで決めれば良い。
|
|
127
|
167
|
|
|
168 ---問題8.1 push down automaton
|
|
|
169
|
|
|
170
|
|
|
171 <a href="../exercise/004.html"> 例題 </a> <!--- Exercise 8.1 --->
|
|
|
172
|
|
|
173
|
|
|
174
|
