Mercurial > hg > Members > kono > Proof > automaton

comparison agda/pushdown.agda @ 17:08b589172493

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add pushdown and turing
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 26 Aug 2018 17:48:26 +0900
parents
children ab265470c2d0
comparison
equal deleted inserted replaced
16:911899e36b96 17:08b589172493
1 module pushdown where
2
3 open import Level renaming ( suc to succ ; zero to Zero )
4 open import Data.Nat
5 open import Data.List
6 open import Data.Maybe
7 open import Data.Bool using ( Bool ; true ; false )
8 open import Relation.Binary.PropositionalEquality hiding ( [_] )
9 open import Relation.Nullary using (¬_; Dec; yes; no)
10 open import Level renaming ( suc to succ ; zero to Zero )
11 open import Data.Product
12
13
14 data PushDown ( Γ : Set ) : Set where
15 pop : PushDown Γ
16 push : Γ → PushDown Γ
17
18
19 record PushDownAutomaton ( Q : Set ) ( Σ : Set ) ( Γ : Set )
20 : Set where
21 field
22 pδ : Q → Σ → Γ → Q × ( PushDown Γ )
23 pstart : Q
24 pz0 : Γ
25 pmoves : Q → List Σ → ( Q × List Γ )
26 pmoves q L = move q L [ pz0 ]
27 where
28 move : Q → ( List Σ ) → ( List Γ ) → ( Q × List Γ )
29 move q _ [] = ( q , [] )
30 move q [] S = ( q , S )
31 move q ( H ∷ T ) ( SH ∷ ST ) with pδ q H SH
32 ... | (nq , pop ) = move nq T ST
33 ... | (nq , push ns ) = move nq T ( ns ∷ SH ∷ ST )
34 paccept : List Σ → Bool
35 paccept L = move pstart L [ pz0 ]
36 where
37 move : (q : Q ) ( L : List Σ ) ( L : List Γ ) → Bool
38 move q [] [] = true
39 move q _ [] = false
40 move q [] (_ ∷ _ ) = false
41 move q ( H ∷ T ) ( SH ∷ ST ) with pδ q H SH
42 ... | (nq , pop ) = move nq T ST
43 ... | (nq , push ns ) = move nq T ( ns ∷ SH ∷ ST )
44
45
46
47