Mercurial > hg > Members > kono > Proof > automaton
annotate agda/turing.agda @ 89:e919e82e95a2
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 10 Nov 2019 12:21:44 +0900 |
| parents | 964e4bd0272a |
| children | 3be1afb87f82 |
| 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 | |
| 20 | 7 open import Data.Bool using ( Bool ; true ; false ) renaming ( not to negate ) |
| 17 | 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 |
| 20 | 19 data Move : Set where |
| 20 left : Move | |
| 21 right : Move | |
| 22 mnone : Move | |
|
18
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 |
| 39 | 32 {-# TERMINATING #-} |
| 33 move : {Q Σ : Set } → { tone : Σ} → {tδ : Q → Σ → Q × ( Write Σ ) × Move } → (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) | |
| 34 move {Q} {Σ} {tnone} {tδ} q L [] = move {Q} {Σ} {tnone} {tδ} q L ( tnone ∷ [] ) | |
| 35 move {Q} {Σ} {tnone} {tδ} q [] R = move {Q} {Σ} {tnone} {tδ} q ( tnone ∷ [] ) R | |
| 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 ) ) | |
| 43 {-# TERMINATING #-} | |
| 44 move-loop : {Q Σ : Set } → {tend : Q → Bool} → (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) | |
| 45 move-loop {Q} {Σ} {tend} q L R with tend q | |
| 46 ... | true = ( q , L , R ) | |
| 47 ... | flase = move-loop {Q} {Σ} {tend} ( proj₁ next ) ( proj₁ ( proj₂ next ) ) ( proj₂ ( proj₂ next ) ) | |
| 48 where | |
| 46 | 49 next = move {Q} {Σ} {{!!}} {{!!}} q L R |
| 17 | 50 |
| 51 record Turing ( Q : Set ) ( Σ : Set ) | |
| 52 : Set where | |
| 53 field | |
| 20 | 54 tδ : Q → Σ → Q × ( Write Σ ) × Move |
| 17 | 55 tstart : Q |
| 56 tend : Q → Bool | |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
57 tnone : Σ |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
58 {-# TERMINATING #-} |
| 20 | 59 move0 : (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) |
| 60 move0 q L R with tend q | |
| 61 ... | true = ( q , L , R ) | |
| 62 move0 q L [] | false = move0 q L ( tnone ∷ [] ) | |
| 63 move0 q [] R | false = move0 q ( tnone ∷ [] ) R | |
| 64 move0 q ( LH ∷ LT ) ( RH ∷ RT ) | false with tδ q LH | |
| 65 ... | nq , write x , left = move0 nq ( RH ∷ x ∷ LT ) RT | |
| 66 ... | nq , write x , right = move0 nq LT ( x ∷ RH ∷ RT ) | |
| 67 ... | nq , write x , mnone = move0 nq ( x ∷ LT ) ( RH ∷ RT ) | |
| 68 ... | nq , wnone , left = move0 nq ( RH ∷ LH ∷ LT ) RT | |
| 69 ... | nq , wnone , right = move0 nq LT ( LH ∷ RH ∷ RT ) | |
| 70 ... | nq , wnone , mnone = move0 nq ( LH ∷ LT ) ( RH ∷ RT ) | |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
71 taccept : List Σ → ( Q × List Σ × List Σ ) |
| 20 | 72 taccept L = move0 tstart L [] |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
73 |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
74 data CopyStates : Set where |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
75 s1 : CopyStates |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
76 s2 : CopyStates |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
77 s3 : CopyStates |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
78 s4 : CopyStates |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
79 s5 : CopyStates |
| 19 | 80 H : CopyStates |
| 17 | 81 |
| 82 | |
| 20 | 83 Copyδ : CopyStates → ℕ → CopyStates × ( Write ℕ ) × Move |
| 84 Copyδ s1 0 = (H , wnone , mnone ) | |
| 85 Copyδ s1 1 = (s2 , write 0 , right ) | |
| 86 Copyδ s2 0 = (s3 , write 0 , right ) | |
| 87 Copyδ s2 1 = (s2 , write 1 , right ) | |
| 88 Copyδ s3 0 = (s4 , write 1 , left ) | |
| 89 Copyδ s3 1 = (s3 , write 1 , right ) | |
| 90 Copyδ s4 0 = (s5 , write 0 , left ) | |
| 91 Copyδ s4 1 = (s4 , write 1 , left ) | |
| 92 Copyδ s5 0 = (s1 , write 1 , right ) | |
| 93 Copyδ s5 1 = (s5 , write 1 , left ) | |
| 94 Copyδ H _ = (H , wnone , mnone ) | |
| 95 Copyδ _ (suc (suc _)) = (H , wnone , mnone ) | |
| 17 | 96 |
| 20 | 97 copyMachine : Turing CopyStates ℕ |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
98 copyMachine = record { |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
99 tδ = Copyδ |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
100 ; tstart = s1 |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
101 ; tend = tend |
| 20 | 102 ; tnone = 0 |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
103 } where |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
104 tend : CopyStates → Bool |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
105 tend H = true |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
106 tend _ = false |
| 17 | 107 |
| 20 | 108 test1 : CopyStates × ( List ℕ ) × ( List ℕ ) |
| 109 test1 = Turing.taccept copyMachine ( 1 ∷ 1 ∷ 0 ∷ 0 ∷ 0 ∷ [] ) | |
| 19 | 110 |
| 20 | 111 test2 : ℕ → CopyStates × ( List ℕ ) × ( List ℕ ) |
| 112 test2 n = loop n (Turing.tstart copyMachine) ( 1 ∷ 1 ∷ 0 ∷ 0 ∷ 0 ∷ [] ) [] | |
| 19 | 113 where |
| 20 | 114 loop : ℕ → CopyStates → ( List ℕ ) → ( List ℕ ) → CopyStates × ( List ℕ ) × ( List ℕ ) |
| 19 | 115 loop zero q L R = ( q , L , R ) |
| 116 loop (suc n) q L R = loop n ( proj₁ t1 ) ( proj₁ ( proj₂ t1 ) ) ( proj₂ ( proj₂ t1 ) ) | |
| 117 where | |
| 39 | 118 t1 = move {CopyStates} {ℕ} {0} {Copyδ} q L R |
| 20 | 119 |
| 120 | |
| 121 --- | |
| 122 -- utm char | |
| 123 -- head head position | |
| 124 -- send state description end | |
| 125 -- del state delimitor | |
| 126 -- sstart state description start | |
| 127 -- 0 | |
| 128 -- 1 | |
| 129 -- utm state description | |
| 130 -- state-num ℕ ( 0 accept, 1 reject ) | |
| 131 -- print 0 write 0, 1 write 1, 2 none | |
| 132 -- move 0 left , 1 none 2 write | |
| 133 -- utm state | |
| 134 -- head-value : ℕ | |
| 135 -- current-state : ℕ | |
| 136 -- direction : ℕ | |
| 137 -- head-dir : ℕ | |
| 138 -- | |
| 139 -- --------------- head sstart ( state description ) * send input -------------- | |
| 140 -- | |
| 141 -- loop search sstart ( depend on head position ) | |
| 142 -- if state description end reject | |
| 143 -- if state-num eq current state | |
| 144 -- if accept end | |
| 145 -- set current-state, direction and head-value by utm state description | |
| 146 -- goto exec | |
| 147 -- else goto loop | |
| 148 -- exec | |
| 149 -- if head-dir = left | |
| 150 -- search head towrards letf | |
| 151 -- else | |
| 152 -- search head towards write | |
| 153 -- put head-value | |
| 154 -- move head ( considering state description ) | |
| 155 -- back to sstart | |
| 156 -- goto loop | |
| 157 | |
| 158 | |
| 159 | |
| 160 postulate UTM : Turing ℕ ℕ | |
| 161 postulate encode-for-utm : Turing ℕ ℕ → List ℕ | |
| 162 postulate enumerate-tm : Turing ℕ ℕ → ℕ | |
| 163 postulate utm-simulate : ( tm : Turing ℕ ℕ ) → ( In : List ℕ ) → Turing.taccept UTM ((encode-for-utm tm) ++ In) ≡ Turing.taccept tm In | |
| 164 | |
| 165 record Halt : Set where | |
| 166 field | |
| 167 halt : List ℕ → Bool | |
| 168 TM : Turing ℕ ℕ | |
| 169 | |
| 170 open Halt | |
| 171 | |
| 172 record NotHalt ( H : Halt ) : Set where | |
| 173 field | |
| 174 nothalt : List ℕ → Bool | |
| 175 NegTM : Turing ℕ ℕ | |
| 176 neg : (n : List ℕ ) → nothalt n ≡ negate ( halt H n ) | |
| 177 | |
| 178 open NotHalt | |
| 179 | |
| 180 -- neg : ( tm : Turing ℕ ℕ ) → ( h : Halt ) → Bool | |
| 181 -- neg tm h = negate ( halt h ( encode-for-utm tm ) ) | |
| 182 | |
| 183 open import Data.Empty | |
| 184 | |
| 185 lemma1 : (H : Halt ) → (NH : NotHalt H ) → nothalt NH (encode-for-utm ( NegTM NH )) ≡ true → ⊥ | |
| 186 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 )) | |
| 187 ... | true | false | refl = {!!} | |
| 188 ... | false | true | refl = {!!} | |
| 189 | |
| 190 lemma2 : (H : Halt ) → (NH : NotHalt H ) → nothalt NH (encode-for-utm ( NegTM NH )) ≡ false → ⊥ | |
| 191 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 )) | |
| 192 ... | true | false | refl = {!!} | |
| 193 ... | false | true | refl = {!!} |