Mercurial > hg > Members > kono > Proof > automaton
annotate agda/turing.agda @ 19:e5d67f06aca8
turing machine done
15 step / 5 min
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 27 Aug 2018 17:17:00 +0900 |
| parents | 6ec8e933ab43 |
| children | 6032a2317ffa |
| rev | line source |
|---|---|
| 17 | 1 module turing where |
| 2 | |
| 3 open import Level renaming ( suc to succ ; zero to Zero ) | |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
4 open import Data.Nat hiding ( erase ) |
| 17 | 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 | |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
14 data Write ( Σ : Set ) : Set where |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
15 write : Σ → Write Σ |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
16 wnone : Write Σ |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
17 -- erase write tnone |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
18 |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
19 data Move ( Σ : Set ) : Set where |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
20 left : Move Σ |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
21 right : Move Σ |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
22 mnone : Move Σ |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
23 |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
24 -- at tδ both stack is poped |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
25 |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
26 -- write S push S , push SR |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
27 -- erase push SL , push tone |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
28 -- none push SL , push SR |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
29 -- left push SR , pop |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
30 -- right pop , push SL |
| 17 | 31 |
| 32 | |
| 33 record Turing ( Q : Set ) ( Σ : Set ) | |
| 34 : Set where | |
| 35 field | |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
36 tδ : Q → Σ → Q × ( Write Σ ) × ( Move Σ ) |
| 17 | 37 tstart : Q |
| 38 tend : Q → Bool | |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
39 tnone : Σ |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
40 {-# TERMINATING #-} |
| 19 | 41 move : (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) |
| 42 move q L [] = move q L ( tnone ∷ [] ) | |
| 43 move q [] R = move q ( tnone ∷ [] ) R | |
| 44 move q ( LH ∷ LT ) ( RH ∷ RT ) with tδ q LH | |
| 45 ... | nq , write x , left = ( nq , ( RH ∷ x ∷ LT ) , RT ) | |
| 46 ... | nq , write x , right = ( nq , LT , ( x ∷ RH ∷ RT ) ) | |
| 47 ... | nq , write x , mnone = ( nq , ( x ∷ LT ) , ( RH ∷ RT ) ) | |
| 48 ... | nq , wnone , left = ( nq , ( RH ∷ LH ∷ LT ) , RT ) | |
| 49 ... | nq , wnone , right = ( nq , LT , ( LH ∷ RH ∷ RT ) ) | |
| 50 ... | nq , wnone , mnone = ( nq , ( LH ∷ LT ) , ( RH ∷ RT ) ) | |
| 51 {-# TERMINATING #-} | |
| 52 move-loop : (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) | |
| 53 move-loop q L R with tend q | |
| 54 ... | true = ( q , L , R ) | |
| 55 ... | flase = move-loop ( proj₁ next ) ( proj₁ ( proj₂ next ) ) ( proj₂ ( proj₂ next ) ) | |
| 56 where | |
| 57 next = move q L R | |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
58 taccept : List Σ → ( Q × List Σ × List Σ ) |
| 19 | 59 taccept L = move-loop tstart L [] |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
60 |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
61 data CopyStates : Set where |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
62 s1 : CopyStates |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
63 s2 : CopyStates |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
64 s3 : CopyStates |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
65 s4 : CopyStates |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
66 s5 : CopyStates |
| 19 | 67 H : CopyStates |
| 17 | 68 |
| 69 | |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
70 Copyδ : CopyStates → Bool → CopyStates × ( Write Bool ) × ( Move Bool ) |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
71 Copyδ s1 false = (H , wnone , mnone ) |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
72 Copyδ s1 true = (s2 , write false , right ) |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
73 Copyδ s2 false = (s3 , write false , right ) |
| 19 | 74 Copyδ s2 true = (s2 , write true , right ) |
| 75 Copyδ s3 false = (s4 , write true , left ) | |
| 76 Copyδ s3 true = (s3 , write true , right ) | |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
77 Copyδ s4 false = (s5 , write false , left ) |
| 19 | 78 Copyδ s4 true = (s4 , write true , left ) |
| 79 Copyδ s5 false = (s1 , write true , right ) | |
| 80 Copyδ s5 true = (s5 , write true , left ) | |
| 81 Copyδ H _ = (H , wnone , mnone ) | |
| 17 | 82 |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
83 copyMachine : Turing CopyStates Bool |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
84 copyMachine = record { |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
85 tδ = Copyδ |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
86 ; tstart = s1 |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
87 ; tend = tend |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
88 ; tnone = false |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
89 } where |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
90 tend : CopyStates → Bool |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
91 tend H = true |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
92 tend _ = false |
| 17 | 93 |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
94 test1 : CopyStates × ( List Bool ) × ( List Bool ) |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
95 test1 = Turing.taccept copyMachine ( true ∷ true ∷ false ∷ false ∷ false ∷ [] ) |
| 19 | 96 |
| 97 test2 : ℕ → CopyStates × ( List Bool ) × ( List Bool ) | |
| 98 test2 n = loop n (Turing.tstart copyMachine) ( true ∷ true ∷ false ∷ false ∷ false ∷ [] ) [] | |
| 99 where | |
| 100 loop : ℕ → CopyStates → ( List Bool ) → ( List Bool ) → CopyStates × ( List Bool ) × ( List Bool ) | |
| 101 loop zero q L R = ( q , L , R ) | |
| 102 loop (suc n) q L R = loop n ( proj₁ t1 ) ( proj₁ ( proj₂ t1 ) ) ( proj₂ ( proj₂ t1 ) ) | |
| 103 where | |
| 104 t1 = Turing.move copyMachine q L R |