Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/turing.agda @ 407:c7ad8d2dc157
safe halt.agda
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 09 Nov 2023 18:04:55 +0900 |
| parents | 6f3636fbc481 |
| children |
| rev | line source |
|---|---|
| 407 | 1 {-# OPTIONS --cubical-compatible --safe #-} |
| 2 -- {-# OPTIONS --allow-unsolved-metas #-} | |
| 17 | 3 module turing where |
| 4 | |
| 5 open import Level renaming ( suc to succ ; zero to Zero ) | |
| 139 | 6 open import Data.Nat -- hiding ( erase ) |
| 17 | 7 open import Data.List |
| 164 | 8 open import Data.Maybe hiding ( map ) |
| 318 | 9 -- open import Data.Bool using ( Bool ; true ; false ) renaming ( not to negate ) |
| 17 | 10 open import Relation.Binary.PropositionalEquality hiding ( [_] ) |
| 11 open import Relation.Nullary using (¬_; Dec; yes; no) | |
| 12 open import Level renaming ( suc to succ ; zero to Zero ) | |
| 164 | 13 open import Data.Product hiding ( map ) |
| 318 | 14 open import logic |
| 17 | 15 |
| 16 | |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
17 data Write ( Σ : Set ) : Set where |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
18 write : Σ → Write Σ |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
19 wnone : Write Σ |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
20 -- erase write tnone |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
21 |
| 20 | 22 data Move : Set where |
| 23 left : Move | |
| 24 right : Move | |
| 25 mnone : Move | |
|
18
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 -- 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
|
28 |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
29 -- 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
|
30 -- erase push SL , push tone |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
31 -- none push SL , push SR |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
32 -- left push SR , pop |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
33 -- right pop , push SL |
| 17 | 34 |
| 139 | 35 move : {Q Σ : Set } → { tnone : Σ} → {tδ : Q → Σ → Q × ( Write Σ ) × Move } → (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) |
| 39 | 36 move {Q} {Σ} {tnone} {tδ} q ( LH ∷ LT ) ( RH ∷ RT ) with tδ q LH |
| 37 ... | nq , write x , left = ( nq , ( RH ∷ x ∷ LT ) , RT ) | |
| 38 ... | nq , write x , right = ( nq , LT , ( x ∷ RH ∷ RT ) ) | |
| 39 ... | nq , write x , mnone = ( nq , ( x ∷ LT ) , ( RH ∷ RT ) ) | |
| 40 ... | nq , wnone , left = ( nq , ( RH ∷ LH ∷ LT ) , RT ) | |
| 41 ... | nq , wnone , right = ( nq , LT , ( LH ∷ RH ∷ RT ) ) | |
| 42 ... | nq , wnone , mnone = ( nq , ( LH ∷ LT ) , ( RH ∷ RT ) ) | |
| 407 | 43 move {Q} {Σ} {tnone} {tδ} q ( LH ∷ LT ) [] with tδ q LH |
| 44 ... | nq , write x , left = ( nq , ( tnone ∷ x ∷ LT ) , [] ) | |
| 45 ... | nq , write x , right = ( nq , LT , ( x ∷ tnone ∷ [] ) ) | |
| 46 ... | nq , write x , mnone = ( nq , ( x ∷ LT ) , ( tnone ∷ [] ) ) | |
| 47 ... | nq , wnone , left = ( nq , ( tnone ∷ LH ∷ LT ) , [] ) | |
| 48 ... | nq , wnone , right = ( nq , LT , ( LH ∷ tnone ∷ [] ) ) | |
| 49 ... | nq , wnone , mnone = ( nq , ( LH ∷ LT ) , ( tnone ∷ [] ) ) | |
| 50 move {Q} {Σ} {tnone} {tδ} q [] ( RH ∷ RT ) with tδ q tnone | |
| 51 ... | nq , write x , left = ( nq , ( RH ∷ x ∷ [] ) , RT ) | |
| 52 ... | nq , write x , right = ( nq , [] , ( x ∷ RH ∷ RT ) ) | |
| 53 ... | nq , write x , mnone = ( nq , ( x ∷ [] ) , ( RH ∷ RT ) ) | |
| 54 ... | nq , wnone , left = ( nq , ( RH ∷ tnone ∷ [] ) , RT ) | |
| 55 ... | nq , wnone , right = ( nq , [] , ( tnone ∷ RH ∷ RT ) ) | |
| 56 ... | nq , wnone , mnone = ( nq , ( tnone ∷ [] ) , ( RH ∷ RT ) ) | |
| 57 move {Q} {Σ} {tnone} {tδ} q [] [] with tδ q tnone | |
| 58 ... | nq , write x , left = ( nq , ( tnone ∷ x ∷ [] ) , [] ) | |
| 59 ... | nq , write x , right = ( nq , [] , ( x ∷ tnone ∷ [] ) ) | |
| 60 ... | nq , write x , mnone = ( nq , ( x ∷ [] ) , ( tnone ∷ [] ) ) | |
| 61 ... | nq , wnone , left = ( nq , ( tnone ∷ tnone ∷ [] ) , [] ) | |
| 62 ... | nq , wnone , right = ( nq , [] , ( tnone ∷ tnone ∷ [] ) ) | |
| 63 ... | nq , wnone , mnone = ( nq , ( tnone ∷ [] ) , ( tnone ∷ [] ) ) | |
| 64 | |
| 65 move-loop : (i : ℕ) {Q Σ : Set } → {tend : Q → Bool} → { tnone : Σ} → {tδ : Q → Σ → Q × ( Write Σ ) × Move } | |
| 139 | 66 → (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) |
| 407 | 67 move-loop zero {Q} {Σ} {tend} {tnone} {tδ} q L R = ( q , L , R ) |
| 68 move-loop (suc i) {Q} {Σ} {tend} {tnone} {tδ} q L R with tend q | |
| 39 | 69 ... | true = ( q , L , R ) |
| 407 | 70 ... | flase = move-loop i {Q} {Σ} {tend} {tnone} {tδ} ( proj₁ next ) ( proj₁ ( proj₂ next ) ) ( proj₂ ( proj₂ next ) ) |
| 39 | 71 where |
| 139 | 72 next = move {Q} {Σ} {tnone} {tδ} q L R |
| 73 | |
| 74 move0 : {Q Σ : Set } ( tend : Q → Bool ) (tnone : Σ ) (tδ : Q → Σ → Q × ( Write Σ ) × Move) | |
| 75 (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) | |
| 407 | 76 move0 tend tnone tδ q ( LH ∷ LT ) ( RH ∷ RT ) with tδ q LH |
| 77 ... | nq , write x , left = nq , ( RH ∷ x ∷ LT ) , RT | |
| 78 ... | nq , write x , right = nq , LT , ( x ∷ RH ∷ RT ) | |
| 79 ... | nq , write x , mnone = nq , ( x ∷ LT ) , ( RH ∷ RT ) | |
| 80 ... | nq , wnone , left = nq , ( RH ∷ LH ∷ LT ) , RT | |
| 81 ... | nq , wnone , right = nq , LT , ( LH ∷ RH ∷ RT ) | |
| 82 ... | nq , wnone , mnone = ( q , ( LH ∷ LT ) , ( RH ∷ RT ) ) | |
| 83 move0 tend tnone tδ q ( LH ∷ LT ) [] with tδ q LH | |
| 84 ... | nq , write x , left = nq , ( tnone ∷ x ∷ LT ) , [] | |
| 85 ... | nq , write x , right = nq , LT , ( x ∷ tnone ∷ [] ) | |
| 86 ... | nq , write x , mnone = nq , ( x ∷ LT ) , ( tnone ∷ [] ) | |
| 87 ... | nq , wnone , left = nq , ( tnone ∷ LH ∷ LT ) , [] | |
| 88 ... | nq , wnone , right = nq , LT , ( LH ∷ tnone ∷ [] ) | |
| 89 ... | nq , wnone , mnone = nq , ( LH ∷ LT ) , ( tnone ∷ [] ) | |
| 90 move0 tend tnone tδ q [] ( RH ∷ RT ) with tδ q tnone | |
| 91 ... | nq , write x , left = nq , ( RH ∷ x ∷ [] ) , RT | |
| 92 ... | nq , write x , right = nq , [] , ( x ∷ RH ∷ RT ) | |
| 93 ... | nq , write x , mnone = nq , ( x ∷ [] ) , ( RH ∷ RT ) | |
| 94 ... | nq , wnone , left = nq , ( RH ∷ tnone ∷ [] ) , RT | |
| 95 ... | nq , wnone , right = nq , [] , ( tnone ∷ RH ∷ RT ) | |
| 96 ... | nq , wnone , mnone = nq , ( tnone ∷ [] ) , ( RH ∷ RT ) | |
| 97 move0 tend tnone tδ q [] [] with tδ q tnone | |
| 98 ... | nq , write x , left = nq , ( tnone ∷ x ∷ [] ) , [] | |
| 99 ... | nq , write x , right = nq , [] , ( x ∷ tnone ∷ [] ) | |
| 100 ... | nq , write x , mnone = nq , ( x ∷ [] ) , ( tnone ∷ [] ) | |
| 101 ... | nq , wnone , left = nq , ( tnone ∷ tnone ∷ [] ) , [] | |
| 102 ... | nq , wnone , right = nq , [] , ( tnone ∷ tnone ∷ [] ) | |
| 103 ... | nq , wnone , mnone = nq , ( tnone ∷ [] ) , ( tnone ∷ [] ) | |
| 17 | 104 |
| 105 record Turing ( Q : Set ) ( Σ : Set ) | |
| 106 : Set where | |
| 107 field | |
| 20 | 108 tδ : Q → Σ → Q × ( Write Σ ) × Move |
| 17 | 109 tstart : Q |
| 110 tend : Q → Bool | |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
111 tnone : Σ |
| 407 | 112 taccept : (i : ℕ ) → List Σ → ( Q × List Σ × List Σ ) |
| 113 taccept i L = tloop i tstart [] [] where | |
| 114 tloop : (i : ℕ) (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) | |
| 115 tloop zero q L R = ( q , L , R ) | |
| 116 tloop (suc i) q L R with tend q | |
| 117 ... | true = ( q , L , R ) | |
| 118 ... | false with move0 tend tnone tδ q L R | |
| 119 ... | nq , L , R = tloop i nq L R | |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
120 |
| 318 | 121 open import automaton |
| 332 | 122 |
| 123 -- ATuring : {Σ : Set } → Automaton (List Σ) Σ | |
| 124 -- ATuring = record { δ = {!!} ; aend = {!!} } | |
| 125 | |
| 126 open import automaton | |
| 318 | 127 open Automaton |
| 128 | |
| 407 | 129 move1 : {Q Σ : Set } (tnone : Σ ) (δ : Q → Σ → Q ) (tδ : Q → Σ → Write Σ × Move) |
| 318 | 130 (q : Q ) ( L : List Σ ) ( R : List Σ ) → Q × List Σ × List Σ |
| 407 | 131 move1 tnone δ tδ q ( LH ∷ LT ) ( RH ∷ RT ) with tδ (δ q LH) LH |
| 132 ... | write x , left = (δ q LH) , ( RH ∷ x ∷ LT ) , RT | |
| 133 ... | write x , right = (δ q LH) , LT , ( x ∷ RH ∷ RT ) | |
| 134 ... | write x , mnone = (δ q LH) , ( x ∷ LT ) , ( RH ∷ RT ) | |
| 135 ... | wnone , left = (δ q LH) , ( RH ∷ LH ∷ LT ) , RT | |
| 136 ... | wnone , right = (δ q LH) , LT , ( LH ∷ RH ∷ RT ) | |
| 137 ... | wnone , mnone = (δ q LH) , ( LH ∷ LT ) , ( RH ∷ RT ) | |
| 138 move1 tnone δ tδ q ( LH ∷ LT ) [] with tδ (δ q LH) LH | |
| 139 ... | write x , left = (δ q LH) , ( tnone ∷ x ∷ LT ) , [] | |
| 140 ... | write x , right = (δ q LH) , LT , ( x ∷ tnone ∷ [] ) | |
| 141 ... | write x , mnone = (δ q LH) , ( x ∷ LT ) , ( tnone ∷ [] ) | |
| 142 ... | wnone , left = (δ q LH) , ( tnone ∷ LH ∷ LT ) , [] | |
| 143 ... | wnone , right = (δ q LH) , LT , ( LH ∷ tnone ∷ [] ) | |
| 144 ... | wnone , mnone = (δ q LH) , ( LH ∷ LT ) , ( tnone ∷ [] ) | |
| 145 move1 tnone δ tδ q [] ( RH ∷ RT ) with tδ (δ q tnone) tnone | |
| 146 ... | write x , left = (δ q tnone) , ( RH ∷ x ∷ [] ) , RT | |
| 147 ... | write x , right = (δ q tnone) , [] , ( x ∷ RH ∷ RT ) | |
| 148 ... | write x , mnone = (δ q tnone) , ( x ∷ [] ) , ( RH ∷ RT ) | |
| 149 ... | wnone , left = (δ q tnone) , ( RH ∷ tnone ∷ [] ) , RT | |
| 150 ... | wnone , right = (δ q tnone) , [] , ( tnone ∷ RH ∷ RT ) | |
| 151 ... | wnone , mnone = (δ q tnone) , ( tnone ∷ [] ) , ( RH ∷ RT ) | |
| 152 move1 tnone δ tδ q [] [] with tδ (δ q tnone) tnone | |
| 153 ... | write x , left = (δ q tnone) , ( tnone ∷ x ∷ [] ) , [] | |
| 154 ... | write x , right = (δ q tnone) , [] , ( x ∷ tnone ∷ [] ) | |
| 155 ... | write x , mnone = (δ q tnone) , ( x ∷ [] ) , ( tnone ∷ [] ) | |
| 156 ... | wnone , left = (δ q tnone) , ( tnone ∷ tnone ∷ [] ) , [] | |
| 157 ... | wnone , right = (δ q tnone) , [] , ( tnone ∷ tnone ∷ [] ) | |
| 158 ... | wnone , mnone = (δ q tnone) , ( tnone ∷ [] ) , ( tnone ∷ [] ) | |
| 318 | 159 |
| 160 record TM ( Q : Set ) ( Σ : Set ) | |
| 161 : Set where | |
| 162 field | |
| 163 automaton : Automaton Q Σ | |
| 164 tδ : Q → Σ → Write Σ × Move | |
| 165 tnone : Σ | |
| 407 | 166 taccept : (i : ℕ) → Q → List Σ → ( Q × List Σ × List Σ ) |
| 167 taccept i q L = tloop i q L [] where | |
| 168 tloop : (i : ℕ) → (q : Q ) ( L : List Σ ) ( R : List Σ ) → Q × List Σ × List Σ | |
| 169 tloop i q L R with aend automaton q | |
| 170 ... | true = ( q , L , R ) | |
| 171 tloop zero q L R | false = ( q , L , R ) | |
| 172 tloop (suc i) q L R | false with move1 tnone (δ automaton) tδ q L R | |
| 173 ... | q' , L' , R' = tloop i q' L' R' | |
| 318 | 174 |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
175 data CopyStates : Set where |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
176 s1 : CopyStates |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
177 s2 : CopyStates |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
178 s3 : CopyStates |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
179 s4 : CopyStates |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
180 s5 : CopyStates |
| 19 | 181 H : CopyStates |
| 17 | 182 |
| 183 | |
| 20 | 184 Copyδ : CopyStates → ℕ → CopyStates × ( Write ℕ ) × Move |
| 139 | 185 Copyδ s1 0 = H , wnone , mnone |
| 186 Copyδ s1 1 = s2 , write 0 , right | |
| 187 Copyδ s2 0 = s3 , write 0 , right | |
| 188 Copyδ s2 1 = s2 , write 1 , right | |
| 189 Copyδ s3 0 = s4 , write 1 , left | |
| 190 Copyδ s3 1 = s3 , write 1 , right | |
| 191 Copyδ s4 0 = s5 , write 0 , left | |
| 192 Copyδ s4 1 = s4 , write 1 , left | |
| 193 Copyδ s5 0 = s1 , write 1 , right | |
| 194 Copyδ s5 1 = s5 , write 1 , left | |
| 195 Copyδ H _ = H , wnone , mnone | |
| 196 Copyδ _ (suc (suc _)) = H , wnone , mnone | |
| 17 | 197 |
| 20 | 198 copyMachine : Turing CopyStates ℕ |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
199 copyMachine = record { |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
200 tδ = Copyδ |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
201 ; tstart = s1 |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
202 ; tend = tend |
| 20 | 203 ; tnone = 0 |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
204 } where |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
205 tend : CopyStates → Bool |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
206 tend H = true |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
207 tend _ = false |
| 17 | 208 |
| 318 | 209 copyTM : TM CopyStates ℕ |
| 210 copyTM = record { | |
| 211 automaton = record { δ = λ q i → proj₁ (Copyδ q i) ; aend = tend } | |
| 212 ; tδ = λ q i → proj₂ (Copyδ q i ) | |
| 213 ; tnone = 0 | |
| 214 } where | |
| 215 tend : CopyStates → Bool | |
| 216 tend H = true | |
| 217 tend _ = false | |
| 218 | |
| 20 | 219 test1 : CopyStates × ( List ℕ ) × ( List ℕ ) |
| 407 | 220 test1 = Turing.taccept copyMachine 10 ( 1 ∷ 1 ∷ 0 ∷ 0 ∷ 0 ∷ [] ) |
| 19 | 221 |
| 20 | 222 test2 : ℕ → CopyStates × ( List ℕ ) × ( List ℕ ) |
| 223 test2 n = loop n (Turing.tstart copyMachine) ( 1 ∷ 1 ∷ 0 ∷ 0 ∷ 0 ∷ [] ) [] | |
| 19 | 224 where |
| 20 | 225 loop : ℕ → CopyStates → ( List ℕ ) → ( List ℕ ) → CopyStates × ( List ℕ ) × ( List ℕ ) |
| 19 | 226 loop zero q L R = ( q , L , R ) |
| 227 loop (suc n) q L R = loop n ( proj₁ t1 ) ( proj₁ ( proj₂ t1 ) ) ( proj₂ ( proj₂ t1 ) ) | |
| 228 where | |
| 39 | 229 t1 = move {CopyStates} {ℕ} {0} {Copyδ} q L R |
| 20 | 230 |
| 164 | 231 -- testn = map (\ n -> test2 n) ( 0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ [] ) |
| 232 | |
| 233 testn : ℕ → List ( CopyStates × ( List ℕ ) × ( List ℕ ) ) | |
| 234 testn 0 = test2 0 ∷ [] | |
| 235 testn (suc n) = test2 n ∷ testn n | |
| 236 |