|
17
|
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
|
