Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/turing.agda @ 309:acb0214ea4d8
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 02 Jan 2022 15:27:17 +0900 |
| parents | 3fa72793620b |
| children | 91781b7c65a8 |
| rev | line source |
|---|---|
| 139 | 1 {-# OPTIONS --allow-unsolved-metas #-} |
| 17 | 2 module turing where |
| 3 | |
| 4 open import Level renaming ( suc to succ ; zero to Zero ) | |
| 139 | 5 open import Data.Nat -- hiding ( erase ) |
| 17 | 6 open import Data.List |
| 164 | 7 open import Data.Maybe hiding ( map ) |
| 20 | 8 open import Data.Bool using ( Bool ; true ; false ) renaming ( not to negate ) |
| 17 | 9 open import Relation.Binary.PropositionalEquality hiding ( [_] ) |
| 10 open import Relation.Nullary using (¬_; Dec; yes; no) | |
| 11 open import Level renaming ( suc to succ ; zero to Zero ) | |
| 164 | 12 open import Data.Product hiding ( map ) |
| 17 | 13 |
| 14 | |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
15 data Write ( Σ : Set ) : Set where |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
16 write : Σ → Write Σ |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
17 wnone : Write Σ |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
18 -- erase write tnone |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
19 |
| 20 | 20 data Move : Set where |
| 21 left : Move | |
| 22 right : Move | |
| 23 mnone : Move | |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
24 |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
25 -- 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
|
26 |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
27 -- 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
|
28 -- erase push SL , push tone |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
29 -- none push SL , push SR |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
30 -- left push SR , pop |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
31 -- right pop , push SL |
| 17 | 32 |
| 39 | 33 {-# TERMINATING #-} |
| 139 | 34 move : {Q Σ : Set } → { tnone : Σ} → {tδ : Q → Σ → Q × ( Write Σ ) × Move } → (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) |
| 39 | 35 move {Q} {Σ} {tnone} {tδ} q L [] = move {Q} {Σ} {tnone} {tδ} q L ( tnone ∷ [] ) |
| 36 move {Q} {Σ} {tnone} {tδ} q [] R = move {Q} {Σ} {tnone} {tδ} q ( tnone ∷ [] ) R | |
| 37 move {Q} {Σ} {tnone} {tδ} q ( LH ∷ LT ) ( RH ∷ RT ) with tδ q LH | |
| 38 ... | nq , write x , left = ( nq , ( RH ∷ x ∷ LT ) , RT ) | |
| 39 ... | nq , write x , right = ( nq , LT , ( x ∷ RH ∷ RT ) ) | |
| 40 ... | nq , write x , mnone = ( nq , ( x ∷ LT ) , ( RH ∷ RT ) ) | |
| 41 ... | nq , wnone , left = ( nq , ( RH ∷ LH ∷ LT ) , RT ) | |
| 42 ... | nq , wnone , right = ( nq , LT , ( LH ∷ RH ∷ RT ) ) | |
| 43 ... | nq , wnone , mnone = ( nq , ( LH ∷ LT ) , ( RH ∷ RT ) ) | |
| 44 {-# TERMINATING #-} | |
| 139 | 45 move-loop : {Q Σ : Set } → {tend : Q → Bool} → { tnone : Σ} → {tδ : Q → Σ → Q × ( Write Σ ) × Move } |
| 46 → (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) | |
| 47 move-loop {Q} {Σ} {tend} {tnone} {tδ} q L R with tend q | |
| 39 | 48 ... | true = ( q , L , R ) |
| 139 | 49 ... | flase = move-loop {Q} {Σ} {tend} {tnone} {tδ} ( proj₁ next ) ( proj₁ ( proj₂ next ) ) ( proj₂ ( proj₂ next ) ) |
| 39 | 50 where |
| 139 | 51 next = move {Q} {Σ} {tnone} {tδ} q L R |
| 52 | |
| 53 {-# TERMINATING #-} | |
| 54 move0 : {Q Σ : Set } ( tend : Q → Bool ) (tnone : Σ ) (tδ : Q → Σ → Q × ( Write Σ ) × Move) | |
| 55 (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) | |
| 56 move0 tend tnone tδ q L R with tend q | |
| 57 ... | true = ( q , L , R ) | |
| 58 move0 tend tnone tδ q L [] | false = move0 tend tnone tδ q L ( tnone ∷ [] ) | |
| 59 move0 tend tnone tδ q [] R | false = move0 tend tnone tδ q ( tnone ∷ [] ) R | |
| 60 move0 tend tnone tδ q ( LH ∷ LT ) ( RH ∷ RT ) | false with tδ q LH | |
| 61 ... | nq , write x , left = move0 tend tnone tδ nq ( RH ∷ x ∷ LT ) RT | |
| 62 ... | nq , write x , right = move0 tend tnone tδ nq LT ( x ∷ RH ∷ RT ) | |
| 63 ... | nq , write x , mnone = move0 tend tnone tδ nq ( x ∷ LT ) ( RH ∷ RT ) | |
| 64 ... | nq , wnone , left = move0 tend tnone tδ nq ( RH ∷ LH ∷ LT ) RT | |
| 65 ... | nq , wnone , right = move0 tend tnone tδ nq LT ( LH ∷ RH ∷ RT ) | |
| 66 ... | nq , wnone , mnone = move0 tend tnone tδ nq ( LH ∷ LT ) ( RH ∷ RT ) | |
| 17 | 67 |
| 68 record Turing ( Q : Set ) ( Σ : Set ) | |
| 69 : Set where | |
| 70 field | |
| 20 | 71 tδ : Q → Σ → Q × ( Write Σ ) × Move |
| 17 | 72 tstart : Q |
| 73 tend : Q → Bool | |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
74 tnone : Σ |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
75 taccept : List Σ → ( Q × List Σ × List Σ ) |
| 139 | 76 taccept L = move0 tend tnone tδ tstart L [] |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
77 |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
78 data CopyStates : Set where |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
79 s1 : CopyStates |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
80 s2 : CopyStates |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
81 s3 : CopyStates |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
82 s4 : CopyStates |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
83 s5 : CopyStates |
| 19 | 84 H : CopyStates |
| 17 | 85 |
| 86 | |
| 20 | 87 Copyδ : CopyStates → ℕ → CopyStates × ( Write ℕ ) × Move |
| 139 | 88 Copyδ s1 0 = H , wnone , mnone |
| 89 Copyδ s1 1 = s2 , write 0 , right | |
| 90 Copyδ s2 0 = s3 , write 0 , right | |
| 91 Copyδ s2 1 = s2 , write 1 , right | |
| 92 Copyδ s3 0 = s4 , write 1 , left | |
| 93 Copyδ s3 1 = s3 , write 1 , right | |
| 94 Copyδ s4 0 = s5 , write 0 , left | |
| 95 Copyδ s4 1 = s4 , write 1 , left | |
| 96 Copyδ s5 0 = s1 , write 1 , right | |
| 97 Copyδ s5 1 = s5 , write 1 , left | |
| 98 Copyδ H _ = H , wnone , mnone | |
| 99 Copyδ _ (suc (suc _)) = H , wnone , mnone | |
| 17 | 100 |
| 20 | 101 copyMachine : Turing CopyStates ℕ |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
102 copyMachine = record { |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
103 tδ = Copyδ |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
104 ; tstart = s1 |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
105 ; tend = tend |
| 20 | 106 ; tnone = 0 |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
107 } where |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
108 tend : CopyStates → Bool |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
109 tend H = true |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
110 tend _ = false |
| 17 | 111 |
| 20 | 112 test1 : CopyStates × ( List ℕ ) × ( List ℕ ) |
| 113 test1 = Turing.taccept copyMachine ( 1 ∷ 1 ∷ 0 ∷ 0 ∷ 0 ∷ [] ) | |
| 19 | 114 |
| 20 | 115 test2 : ℕ → CopyStates × ( List ℕ ) × ( List ℕ ) |
| 116 test2 n = loop n (Turing.tstart copyMachine) ( 1 ∷ 1 ∷ 0 ∷ 0 ∷ 0 ∷ [] ) [] | |
| 19 | 117 where |
| 20 | 118 loop : ℕ → CopyStates → ( List ℕ ) → ( List ℕ ) → CopyStates × ( List ℕ ) × ( List ℕ ) |
| 19 | 119 loop zero q L R = ( q , L , R ) |
| 120 loop (suc n) q L R = loop n ( proj₁ t1 ) ( proj₁ ( proj₂ t1 ) ) ( proj₂ ( proj₂ t1 ) ) | |
| 121 where | |
| 39 | 122 t1 = move {CopyStates} {ℕ} {0} {Copyδ} q L R |
| 20 | 123 |
| 164 | 124 -- testn = map (\ n -> test2 n) ( 0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ [] ) |
| 125 | |
| 126 testn : ℕ → List ( CopyStates × ( List ℕ ) × ( List ℕ ) ) | |
| 127 testn 0 = test2 0 ∷ [] | |
| 128 testn (suc n) = test2 n ∷ testn n | |
| 129 |