|
139
|
1 module utm where
|
|
|
2
|
|
|
3 open import turing
|
|
|
4 open import Data.Product
|
|
319
|
5 -- open import Data.Bool
|
|
139
|
6 open import Data.List
|
|
|
7 open import Data.Nat
|
|
319
|
8 open import logic
|
|
139
|
9
|
|
|
10 data utmStates : Set where
|
|
140
|
11 reads : utmStates
|
|
139
|
12 read0 : utmStates
|
|
|
13 read1 : utmStates
|
|
|
14 read2 : utmStates
|
|
|
15 read3 : utmStates
|
|
|
16 read4 : utmStates
|
|
|
17 read5 : utmStates
|
|
|
18 read6 : utmStates
|
|
|
19
|
|
|
20 loc0 : utmStates
|
|
|
21 loc1 : utmStates
|
|
|
22 loc2 : utmStates
|
|
|
23 loc3 : utmStates
|
|
|
24 loc4 : utmStates
|
|
|
25 loc5 : utmStates
|
|
|
26 loc6 : utmStates
|
|
|
27
|
|
|
28 fetch0 : utmStates
|
|
|
29 fetch1 : utmStates
|
|
|
30 fetch2 : utmStates
|
|
|
31 fetch3 : utmStates
|
|
|
32 fetch4 : utmStates
|
|
|
33 fetch5 : utmStates
|
|
|
34 fetch6 : utmStates
|
|
|
35 fetch7 : utmStates
|
|
|
36
|
|
|
37 print0 : utmStates
|
|
|
38 print1 : utmStates
|
|
|
39 print2 : utmStates
|
|
|
40 print3 : utmStates
|
|
|
41 print4 : utmStates
|
|
|
42 print5 : utmStates
|
|
|
43 print6 : utmStates
|
|
|
44 print7 : utmStates
|
|
|
45
|
|
|
46 mov0 : utmStates
|
|
|
47 mov1 : utmStates
|
|
|
48 mov2 : utmStates
|
|
|
49 mov3 : utmStates
|
|
|
50 mov4 : utmStates
|
|
|
51 mov5 : utmStates
|
|
|
52 mov6 : utmStates
|
|
|
53
|
|
|
54 tidy0 : utmStates
|
|
|
55 tidy1 : utmStates
|
|
|
56 halt : utmStates
|
|
|
57
|
|
|
58 data utmΣ : Set where
|
|
|
59 ０ : utmΣ
|
|
|
60 １ : utmΣ
|
|
|
61 B : utmΣ
|
|
|
62 * : utmΣ
|
|
|
63 $ : utmΣ
|
|
|
64 ^ : utmΣ
|
|
|
65 X : utmΣ
|
|
|
66 Y : utmΣ
|
|
|
67 Z : utmΣ
|
|
|
68 ＠ : utmΣ
|
|
|
69 b : utmΣ
|
|
|
70
|
|
|
71 utmδ : utmStates → utmΣ → utmStates × (Write utmΣ) × Move
|
|
140
|
72 utmδ reads x = read0 , wnone , mnone
|
|
139
|
73 utmδ read0 * = read1 , write * , left
|
|
|
74 utmδ read0 x = read0 , write x , right
|
|
|
75 utmδ read1 x = read2 , write ＠ , right
|
|
|
76 utmδ read2 ^ = read3 , write ^ , right
|
|
|
77 utmδ read2 x = read2 , write x , right
|
|
|
78 utmδ read3 ０ = read4 , write ０ , left
|
|
|
79 utmδ read3 １ = read5 , write １ , left
|
|
|
80 utmδ read3 b = read6 , write b , left
|
|
|
81 utmδ read4 ＠ = loc0 , write ０ , right
|
|
|
82 utmδ read4 x = read4 , write x , left
|
|
|
83 utmδ read5 ＠ = loc0 , write １ , right
|
|
|
84 utmδ read5 x = read5 , write x , left
|
|
|
85 utmδ read6 ＠ = loc0 , write B , right
|
|
|
86 utmδ read6 x = read6 , write x , left
|
|
|
87 utmδ loc0 ０ = loc0 , write X , left
|
|
|
88 utmδ loc0 １ = loc0 , write Y , left
|
|
|
89 utmδ loc0 B = loc0 , write Z , left
|
|
|
90 utmδ loc0 $ = loc1 , write $ , right
|
|
|
91 utmδ loc0 x = loc0 , write x , left
|
|
|
92 utmδ loc1 X = loc2 , write ０ , right
|
|
|
93 utmδ loc1 Y = loc3 , write １ , right
|
|
|
94 utmδ loc1 Z = loc4 , write B , right
|
|
|
95 utmδ loc1 * = fetch0 , write * , right
|
|
|
96 utmδ loc1 x = loc1 , write x , right
|
|
|
97 utmδ loc2 ０ = loc5 , write X , right
|
|
|
98 utmδ loc2 １ = loc6 , write Y , right
|
|
|
99 utmδ loc2 B = loc6 , write Z , right
|
|
|
100 utmδ loc2 x = loc2 , write x , right
|
|
|
101 utmδ loc3 １ = loc5 , write Y , right
|
|
|
102 utmδ loc3 ０ = loc6 , write X , right
|
|
|
103 utmδ loc3 B = loc6 , write Z , right
|
|
|
104 utmδ loc3 x = loc3 , write x , right
|
|
|
105 utmδ loc4 B = loc5 , write Z , right
|
|
|
106 utmδ loc4 ０ = loc6 , write X , right
|
|
|
107 utmδ loc4 １ = loc6 , write Y , right
|
|
|
108 utmδ loc4 x = loc4 , write x , right
|
|
|
109 utmδ loc5 $ = loc1 , write $ , right
|
|
|
110 utmδ loc5 x = loc5 , write x , left
|
|
|
111 utmδ loc6 $ = halt , write $ , right
|
|
|
112 utmδ loc6 * = loc0 , write * , left
|
|
|
113 utmδ loc6 x = loc6 , write x , right
|
|
|
114 utmδ fetch0 ０ = fetch1 , write X , left
|
|
|
115 utmδ fetch0 １ = fetch2 , write Y , left
|
|
|
116 utmδ fetch0 B = fetch3 , write Z , left
|
|
|
117 utmδ fetch0 x = fetch0 , write x , right
|
|
|
118 utmδ fetch1 $ = fetch4 , write $ , right
|
|
|
119 utmδ fetch1 x = fetch1 , write x , left
|
|
|
120 utmδ fetch2 $ = fetch5 , write $ , right
|
|
|
121 utmδ fetch2 x = fetch2 , write x , left
|
|
|
122 utmδ fetch3 $ = fetch6 , write $ , right
|
|
|
123 utmδ fetch3 x = fetch3 , write x , left
|
|
|
124 utmδ fetch4 ０ = fetch7 , write X , right
|
|
|
125 utmδ fetch4 １ = fetch7 , write X , right
|
|
|
126 utmδ fetch4 B = fetch7 , write X , right
|
|
|
127 utmδ fetch4 * = print0 , write * , left
|
|
|
128 utmδ fetch4 x = fetch4 , write x , right
|
|
|
129 utmδ fetch5 ０ = fetch7 , write Y , right
|
|
|
130 utmδ fetch5 １ = fetch7 , write Y , right
|
|
|
131 utmδ fetch5 B = fetch7 , write Y , right
|
|
|
132 utmδ fetch5 * = print0 , write * , left
|
|
|
133 utmδ fetch5 x = fetch5 , write x , right
|
|
|
134 utmδ fetch6 ０ = fetch7 , write Z , right
|
|
|
135 utmδ fetch6 １ = fetch7 , write Z , right
|
|
|
136 utmδ fetch6 B = fetch7 , write Z , right
|
|
|
137 utmδ fetch6 * = print0 , write * , left
|
|
|
138 utmδ fetch6 x = fetch6 , write x , right
|
|
|
139 utmδ fetch7 * = fetch0 , write * , right
|
|
|
140 utmδ fetch7 x = fetch7 , write x , right
|
|
|
141 utmδ print0 X = print1 , write X , right
|
|
|
142 utmδ print0 Y = print2 , write Y , right
|
|
|
143 utmδ print0 Z = print3 , write Z , right
|
|
|
144 utmδ print1 ^ = print4 , write ^ , right
|
|
|
145 utmδ print1 x = print1 , write x , right
|
|
|
146 utmδ print2 ^ = print5 , write ^ , right
|
|
|
147 utmδ print2 x = print2 , write x , right
|
|
|
148 utmδ print3 ^ = print6 , write ^ , right
|
|
|
149 utmδ print3 x = print3 , write x , right
|
|
|
150 utmδ print4 x = print7 , write ０ , left
|
|
|
151 utmδ print5 x = print7 , write １ , left
|
|
|
152 utmδ print6 x = print7 , write B , left
|
|
|
153 utmδ print7 X = mov0 , write X , right
|
|
|
154 utmδ print7 Y = mov1 , write Y , right
|
|
|
155 utmδ print7 x = print7 , write x , left
|
|
|
156 utmδ mov0 ^ = mov2 , write ^ , left
|
|
|
157 utmδ mov0 x = mov0 , write x , right
|
|
|
158 utmδ mov1 ^ = mov3 , write ^ , right
|
|
|
159 utmδ mov1 x = mov1 , write x , right
|
|
|
160 utmδ mov2 ０ = mov4 , write ^ , right
|
|
|
161 utmδ mov2 １ = mov5 , write ^ , right
|
|
|
162 utmδ mov2 B = mov6 , write ^ , right
|
|
|
163 utmδ mov3 ０ = mov4 , write ^ , left
|
|
|
164 utmδ mov3 １ = mov5 , write ^ , left
|
|
|
165 utmδ mov3 B = mov6 , write ^ , left
|
|
|
166 utmδ mov4 ^ = tidy0 , write ０ , left
|
|
|
167 utmδ mov5 ^ = tidy0 , write １ , left
|
|
|
168 utmδ mov6 ^ = tidy0 , write B , left
|
|
|
169 utmδ tidy0 $ = tidy1 , write $ , left
|
|
|
170 utmδ tidy0 x = tidy0 , write x , left
|
|
|
171 utmδ tidy1 X = tidy1 , write ０ , left
|
|
|
172 utmδ tidy1 Y = tidy1 , write １ , left
|
|
|
173 utmδ tidy1 Z = tidy1 , write B , left
|
|
141
|
174 utmδ tidy1 $ = reads , write $ , right
|
|
139
|
175 utmδ tidy1 x = tidy1 , write x , left
|
|
|
176 utmδ _ x = halt , write x , mnone
|
|
|
177
|
|
|
178 U-TM : Turing utmStates utmΣ
|
|
|
179 U-TM = record {
|
|
|
180 tδ = utmδ
|
|
|
181 ; tstart = read0
|
|
|
182 ; tend = tend
|
|
|
183 ; tnone = b
|
|
|
184 } where
|
|
|
185 tend : utmStates → Bool
|
|
|
186 tend halt = true
|
|
|
187 tend _ = false
|
|
|
188
|
|
|
189 -- Copyδ : CopyStates → ℕ → CopyStates × ( Write ℕ ) × Move
|
|
|
190 -- Copyδ s1 0 = H , wnone , mnone
|
|
|
191 -- Copyδ s1 1 = s2 , write 0 , right
|
|
|
192 -- Copyδ s2 0 = s3 , write 0 , right
|
|
|
193 -- Copyδ s2 1 = s2 , write 1 , right
|
|
|
194 -- Copyδ s3 0 = s4 , write 1 , left
|
|
|
195 -- Copyδ s3 1 = s3 , write 1 , right
|
|
|
196 -- Copyδ s4 0 = s5 , write 0 , left
|
|
|
197 -- Copyδ s4 1 = s4 , write 1 , left
|
|
|
198 -- Copyδ s5 0 = s1 , write 1 , right
|
|
|
199 -- Copyδ s5 1 = s5 , write 1 , left
|
|
|
200 -- Copyδ H _ = H , wnone , mnone
|
|
|
201 -- Copyδ _ (suc (suc _)) = H , wnone , mnone
|
|
|
202
|
|
|
203 Copyδ-encode : List utmΣ
|
|
|
204 Copyδ-encode =
|
|
|
205 ０ ∷ ０ ∷ １ ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ ０ ∷ -- s1 0 = H , wnone , mnone
|
|
|
206 * ∷ ０ ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ １ ∷ -- s1 1 = s2 , write 0 , right
|
|
|
207 * ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ ０ ∷ １ ∷ -- s2 0 = s3 , write 0 , right
|
|
|
208 * ∷ ０ ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ １ ∷ -- s2 1 = s2 , write 1 , right
|
|
|
209 * ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ -- s3 0 = s4 , write 1 , left
|
|
|
210 * ∷ ０ ∷ １ ∷ １ ∷ １ ∷ ０ ∷ １ ∷ １ ∷ １ ∷ ０ ∷ １ ∷ -- s3 1 = s3 , write 1 , right
|
|
|
211 * ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ -- s4 0 = s5 , write 0 , left
|
|
|
212 * ∷ １ ∷ ０ ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ -- s4 1 = s4 , write 1 , left
|
|
|
213 * ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ １ ∷ -- s5 0 = s1 , write 1 , right
|
|
|
214 * ∷ １ ∷ ０ ∷ １ ∷ １ ∷ １ ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ ０ ∷ -- s5 1 = s5 , write 1 , left
|
|
|
215 []
|
|
|
216
|
|
|
217
|
|
|
218 input-encode : List utmΣ
|
|
|
219 input-encode = １ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ []
|
|
|
220
|
|
|
221 input+Copyδ : List utmΣ
|
|
|
222 input+Copyδ = ( $ ∷ ０ ∷ ０ ∷ ０ ∷ ０ ∷ * ∷ [] ) -- start state
|
|
|
223 ++ Copyδ-encode
|
|
|
224 ++ ( $ ∷ ^ ∷ input-encode )
|
|
|
225
|
|
140
|
226 short-input : List utmΣ
|
|
|
227 short-input = $ ∷ ０ ∷ ０ ∷ ０ ∷ * ∷
|
|
|
228 ０ ∷ ０ ∷ ０ ∷ １ ∷ ０ ∷ １ ∷ １ ∷ * ∷
|
|
|
229 ０ ∷ ０ ∷ １ ∷ ０ ∷ １ ∷ １ ∷ １ ∷ * ∷
|
|
|
230 ０ ∷ １ ∷ B ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ * ∷
|
|
|
231 １ ∷ ０ ∷ ０ ∷ ０ ∷ １ ∷ １ ∷ １ ∷ $ ∷
|
|
|
232 ^ ∷ ０ ∷ ０ ∷ １ ∷ １ ∷ []
|
|
139
|
233
|
|
140
|
234 utm-test1 : List utmΣ → utmStates × ( List utmΣ ) × ( List utmΣ )
|
|
|
235 utm-test1 inp = Turing.taccept U-TM inp
|
|
|
236
|
|
|
237 {-# TERMINATING #-}
|
|
|
238 utm-test2 : ℕ → List utmΣ → utmStates × ( List utmΣ ) × ( List utmΣ )
|
|
|
239 utm-test2 n inp = loop n (Turing.tstart U-TM) inp []
|
|
139
|
240 where
|
|
|
241 loop : ℕ → utmStates → ( List utmΣ ) → ( List utmΣ ) → utmStates × ( List utmΣ ) × ( List utmΣ )
|
|
|
242 loop zero q L R = ( q , L , R )
|
|
140
|
243 loop (suc n) q L R with move {utmStates} {utmΣ} {０} {utmδ} q L R | q
|
|
|
244 ... | nq , nL , nR | reads = loop n nq nL nR
|
|
|
245 ... | nq , nL , nR | _ = loop (suc n) nq nL nR
|
|
139
|
246
|
|
140
|
247 t1 = utm-test2 20 short-input
|
|
|
248
|
|
|
249 t : (n : ℕ) → utmStates × ( List utmΣ ) × ( List utmΣ )
|
|
141
|
250 -- t n = utm-test2 n input+Copyδ
|
|
|
251 t n = utm-test2 n short-input
|
