|
127
|
1 -title: push donwオートマトンと文法クラス
|
|
|
2
|
|
|
3 任意のnについて 0{n}1{n} に対応する有限オートマトンはない。
|
|
|
4
|
|
|
5 inputnn : { n : ℕ } → { Σ : Set } → ( x y : Σ ) → List Σ → List Σ
|
|
|
6 inputnn {zero} {_} _ _ s = s
|
|
|
7 inputnn {suc n} x y s = x ∷ ( inputnn {n} x y ( y ∷ s ) )
|
|
|
8
|
|
|
9 inputnn だけ受け付けて、それ以外を受け付けないということができない。
|
|
|
10
|
|
|
11
|
|
|
12
|
|
|
13 かっこの対応が取れないことに相当する。
|
|
|
14
|
|
|
15
|
|
|
16 --push down automaton
|
|
|
17
|
|
|
18
|
|
|
19 data PushDown ( Γ : Set ) : Set where
|
|
|
20 pop : PushDown Γ
|
|
|
21 push : Γ → PushDown Γ
|
|
|
22
|
|
|
23 record PushDownAutomaton ( Q : Set ) ( Σ : Set ) ( Γ : Set )
|
|
|
24 : Set where
|
|
|
25 field
|
|
|
26 pδ : Q → Σ → Γ → Q × ( PushDown Γ )
|
|
|
27 pstart : Q
|
|
|
28 pz0 : Γ
|
|
|
29 pmoves : Q → List Σ → ( Q × List Γ )
|
|
|
30 pmoves q L = move q L [ pz0 ]
|
|
|
31 where
|
|
|
32 move : Q → ( List Σ ) → ( List Γ ) → ( Q × List Γ )
|
|
|
33 move q _ [] = ( q , [] )
|
|
|
34 move q [] S = ( q , S )
|
|
|
35 move q ( H ∷ T ) ( SH ∷ ST ) with pδ q H SH
|
|
|
36 ... | (nq , pop ) = move nq T ST
|
|
|
37 ... | (nq , push ns ) = move nq T ( ns ∷ SH ∷ ST )
|
|
|
38 paccept : List Σ → Bool
|
|
|
39 paccept L = move pstart L [ pz0 ]
|
|
|
40 where
|
|
|
41 move : (q : Q ) ( L : List Σ ) ( L : List Γ ) → Bool
|
|
|
42 move q [] [] = true
|
|
|
43 move q _ [] = false
|
|
|
44 move q [] (_ ∷ _ ) = false
|
|
|
45 move q ( H ∷ T ) ( SH ∷ ST ) with pδ q H SH
|
|
|
46 ... | (nq , pop ) = move nq T ST
|
|
|
47 ... | (nq , push ns ) = move nq T ( ns ∷ SH ∷ ST )
|
|
|
48
|
|
|
49
|
|
|
50 --文脈自由文法
|
|
|
51
|
|
|
52
|
|
|
53
|
|
|
54 ---問題8.1 push down automaton
|
|
|
55
|
|
|
56
|
|
|
57 <a href="../exercise/004.html"> 例題 </a> <!--- Exercise 8.1 --->
|
|
|
58
|
|
|
59
|
|
|
60
|
