Mercurial > hg > Members > kono > Proof > automaton

comparison agda/turing.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 6ec8e933ab43
comparison
equal deleted inserted replaced
16:911899e36b96 17:08b589172493
1 module turing 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 Turing ( Q : Set ) ( Σ : Set )
20 : Set where
21 field
22 tδ : Q → Σ → Q × ( PushDown Σ ) × ( PushDown Σ )
23 tstart : Q
24 tend : Q → Bool
25 tz0 : Σ
26 tmoves : Q → List Σ → ( Q × List Σ × List Σ )
27 tmoves q L = move q L [ pz0 ]
28 where
29 move : Q → ( List Σ ) → ( List Σ ) → ( Q × List Σ × List Σ )
30 move q _ [] = ( q , [] )
31 move q [] S = ( q , S )
32 move q ( H ∷ T ) ( SH ∷ ST ) with pδ q H SH
33 ... | (nq , pop ) = move nq T ST
34 ... | (nq , push ns ) = move nq T ( ns ∷ SH ∷ ST )
35 taccept : List Σ → Bool
36 taccept L = move pstart L [ pz0 ]
37 where
38 move : (q : Q ) ( L : List Σ ) ( L : List Σ ) → Bool
39 move q [] [] = true
40 move q _ [] = false
41 move q [] (_ ∷ _ ) = false
42 move q ( H ∷ T ) ( SH ∷ ST ) with pδ q H SH
43 ... | (nq , pop ) = move nq T ST
44 ... | (nq , push ns ) = move nq T ( ns ∷ SH ∷ ST )
45
46
47
48