Mercurial > hg > Members > kono > Proof > automaton

comparison a08/lecture.ind @ 127:0e8a0e50ed26

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add some files
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 23 Nov 2019 12:59:45 +0900
parents
children a3fb231feeb9
comparison
equal deleted inserted replaced
126:a79e2c2e1642 127:0e8a0e50ed26
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