Mercurial > hg > Members > kono > Proof > automaton
annotate agda/turing.agda @ 139:3be1afb87f82
add utm
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 14 Mar 2020 17:34:54 +0900 |
| parents | 964e4bd0272a |
| children | b3f05cd08d24 |
| 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 |
| 7 open import Data.Maybe | |
| 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 ) | |
| 12 open import Data.Product | |
| 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 |
| 124 | |
| 125 --- | |
| 126 -- utm char | |
| 127 -- head head position | |
| 128 -- send state description end | |
| 129 -- del state delimitor | |
| 130 -- sstart state description start | |
| 131 -- 0 | |
| 132 -- 1 | |
| 133 -- utm state description | |
| 134 -- state-num ℕ ( 0 accept, 1 reject ) | |
| 135 -- print 0 write 0, 1 write 1, 2 none | |
| 136 -- move 0 left , 1 none 2 write | |
| 137 -- utm state | |
| 138 -- head-value : ℕ | |
| 139 -- current-state : ℕ | |
| 140 -- direction : ℕ | |
| 141 -- head-dir : ℕ | |
| 142 -- | |
| 143 -- --------------- head sstart ( state description ) * send input -------------- | |
| 144 -- | |
| 145 -- loop search sstart ( depend on head position ) | |
| 146 -- if state description end reject | |
| 147 -- if state-num eq current state | |
| 148 -- if accept end | |
| 149 -- set current-state, direction and head-value by utm state description | |
| 150 -- goto exec | |
| 151 -- else goto loop | |
| 152 -- exec | |
| 153 -- if head-dir = left | |
| 154 -- search head towrards letf | |
| 155 -- else | |
| 156 -- search head towards write | |
| 157 -- put head-value | |
| 158 -- move head ( considering state description ) | |
| 159 -- back to sstart | |
| 160 -- goto loop | |
| 161 | |
| 162 | |
| 163 | |
| 164 postulate UTM : Turing ℕ ℕ | |
| 165 postulate encode-for-utm : Turing ℕ ℕ → List ℕ | |
| 166 postulate enumerate-tm : Turing ℕ ℕ → ℕ | |
| 167 postulate utm-simulate : ( tm : Turing ℕ ℕ ) → ( In : List ℕ ) → Turing.taccept UTM ((encode-for-utm tm) ++ In) ≡ Turing.taccept tm In | |
| 168 | |
| 169 record Halt : Set where | |
| 170 field | |
| 171 halt : List ℕ → Bool | |
| 172 TM : Turing ℕ ℕ | |
| 173 | |
| 174 open Halt | |
| 175 | |
| 176 record NotHalt ( H : Halt ) : Set where | |
| 177 field | |
| 178 nothalt : List ℕ → Bool | |
| 179 NegTM : Turing ℕ ℕ | |
| 180 neg : (n : List ℕ ) → nothalt n ≡ negate ( halt H n ) | |
| 181 | |
| 182 open NotHalt | |
| 183 | |
| 184 -- neg : ( tm : Turing ℕ ℕ ) → ( h : Halt ) → Bool | |
| 185 -- neg tm h = negate ( halt h ( encode-for-utm tm ) ) | |
| 186 | |
| 187 open import Data.Empty | |
| 188 | |
| 189 lemma1 : (H : Halt ) → (NH : NotHalt H ) → nothalt NH (encode-for-utm ( NegTM NH )) ≡ true → ⊥ | |
| 190 lemma1 h nh negneg=1 with halt h (encode-for-utm ( NegTM nh )) | nothalt nh (encode-for-utm ( NegTM nh )) | neg nh (encode-for-utm ( NegTM nh )) | |
| 191 ... | true | false | refl = {!!} | |
| 192 ... | false | true | refl = {!!} | |
| 193 | |
| 194 lemma2 : (H : Halt ) → (NH : NotHalt H ) → nothalt NH (encode-for-utm ( NegTM NH )) ≡ false → ⊥ | |
| 195 lemma2 h nh negneg=1 with halt h (encode-for-utm ( NegTM nh )) | nothalt nh (encode-for-utm ( NegTM nh )) | neg nh (encode-for-utm ( NegTM nh )) | |
| 196 ... | true | false | refl = {!!} | |
| 197 ... | false | true | refl = {!!} |