1app load ["emitLib"]; 
2quietdec := true;
3open pred_setLib pred_setTheory arithmeticTheory;
4quietdec := false;
5
6val tm_ss = list_ss ++ PRED_SET_ss;
7
8val _ = new_theory "turing";
9
10(*---------------------------------------------------------------------------*)
11(* Turing machines, tape infinite in one direction.                          *)
12(*---------------------------------------------------------------------------*)
13
14Hol_datatype `dir = L | R`;
15
16(*---------------------------------------------------------------------------*)
17(* Raw datatype of TMs. The only slightly odd thing may be that the blank is *)
18(* explicitly included. Also, it turns out to facilitate the definition of   *)
19(* executions if the initial value of the current cell is set to a value.    *)
20(* Because having a "left-edge" marker simplifies many TM algorithms, we set *)
21(* aside a particular "star" value for this purpose.                         *)
22(*---------------------------------------------------------------------------*)
23
24Hol_datatype 
25  `TM = <| states     : 'state -> bool ;
26           inputsymbs : 'alpha -> bool ;
27           tapesymbs  : 'alpha -> bool ;
28           init       : 'state ;
29           trans      : 'state -> 'alpha -> 'state # 'alpha # dir;
30           accept     : 'state ;
31           reject     : 'state ;
32           blank      : 'alpha ;
33           star       : 'alpha |>`;
34
35(*---------------------------------------------------------------------------*)
36(* Predicate singling out the real Turing machines. Is in principle an       *)
37(* executable thing, but we don't currently handle (bounded) quantifiers.    *)
38(*---------------------------------------------------------------------------*)
39
40val isTM_def = 
41 Define
42   `isTM (M : ('alpha,'state)TM) =
43      FINITE M.states            /\
44      FINITE M.inputsymbs        /\
45      FINITE M.tapesymbs         /\
46      M.blank IN M.tapesymbs     /\
47      ~(M.blank IN M.inputsymbs) /\
48      M.star IN M.inputsymbs     /\
49      M.inputsymbs SUBSET M.tapesymbs /\
50      M.accept IN M.states       /\
51      M.reject IN M.states       /\
52      ~(M.accept = M.reject)     /\
53      M.init IN M.states         /\
54      !a p q b d. 
55          a IN M.tapesymbs /\ p IN M.states /\ (M.trans p a = (q,b,d)) 
56          ==> q IN M.states /\ b IN M.tapesymbs`;
57
58(*---------------------------------------------------------------------------*)
59(* Is a string built from the input alphabet of the TM?                      *)
60(*---------------------------------------------------------------------------*)
61
62val isInputWord_def = 
63 Define
64   `isInputWord (M:('a,'state)TM) w = !a. MEM a w ==> a IN M.inputsymbs`;
65
66(*---------------------------------------------------------------------------*)
67(* A step of TM computation alters the current configuration. A config.      *)
68(* <|left;cell;state;right|> represents the complete state of the machine.   *)
69(* "left" is the portion of the tape left of the tape pointer, (in reverse   *)
70(* order, so that the head of the "left" is actually the last element of the *)
71(* left part of the tape). "cell" holds the contents of the current cell     *)
72(* operated on by the machine. "state" holds the current state of the        *)
73(* machine. "right" holds the portion of the tape to the right of the        *)
74(* current cell; it is not in reverse order.                                 *)
75(*---------------------------------------------------------------------------*)
76
77Hol_datatype 
78  `config = <| left  : 'a list;
79               cell  : 'a ;
80               state : 'state ;
81               right : 'a list |>`;
82
83(*---------------------------------------------------------------------------*)
84(* The configuration determines the tape contents.                           *)
85(*---------------------------------------------------------------------------*)
86
87val tape_of_def =
88 Define
89   `tape_of (cnfg:('a,'state)config) =
90      REVERSE cnfg.left ++ [cnfg.cell] ++ cnfg.right`;
91
92(*---------------------------------------------------------------------------*)
93(* A transition of the machine. The transition function M.trans              *)
94(*                                                                           *)
95(*    trans : 'state -> 'a -> 'state # 'a # dir                              *)
96(*                                                                           *)
97(* yields the new state, new cell contents, and the direction for the tape   *)
98(* head to move. Given that, we need to know whether or not we are hitting   *)
99(* the left edge of the tape, or, the right edge of the tape. The config. is *)
100(* then updated accordingly.                                                 *)
101(*---------------------------------------------------------------------------*)
102
103val Step_def =
104 Define 
105   `Step (M:('a,'state)TM) (cnfg: ('a,'state) config) =
106     let (q,b,d) = M.trans cnfg.state cnfg.cell in
107     if d = L 
108      then 
109        (case cnfg.left 
110          of [] -> cnfg with  <| cell := b; state := q |>
111          || h::t -> cnfg with <| left := t; cell := h; state := q; 
112                                  right := b::cnfg.right |>)
113      else (* d = R *)
114       (case cnfg.right 
115         of [] -> cnfg with 
116                    <|left := b::cnfg.left; cell := M.blank; state := q |>
117         || h::t -> cnfg with 
118                    <|left := b::cnfg.left; cell := h; 
119                      state:=q; right := t |>)`;
120
121(*---------------------------------------------------------------------------*)
122(* Accepting configuration                                                   *)
123(*---------------------------------------------------------------------------*)
124
125val Accepting_def = 
126 Define
127   `Accepting (M:('a,'state)TM) 
128              (cnfg : ('a,'state) config) = (cnfg.state = M.accept) `;
129
130(*---------------------------------------------------------------------------*)
131(* Rejecting configuration                                                   *)
132(*---------------------------------------------------------------------------*)
133
134val Rejecting_def = 
135 Define
136   `Rejecting (M:('a,'state)TM) 
137              (cnfg : ('a,'state) config) = (cnfg.state = M.reject) `;
138
139(*---------------------------------------------------------------------------*)
140(* Terminal configuration                                                    *)
141(*---------------------------------------------------------------------------*)
142
143val Terminal_def = 
144 Define
145   `Terminal (M:('a,'state)TM) 
146             (cnfg : ('a,'state) config) 
147    = Accepting M cnfg \/ Rejecting M cnfg`;
148
149(*---------------------------------------------------------------------------*)
150(* Initial configuration. Computation starts with M.star in the current cell *)
151(*---------------------------------------------------------------------------*)
152
153val Initial_def = 
154 Define
155   `Initial (M:('a,'state)TM) w =
156      <| left := []; cell := M.star; state := M.init; right := w |>`;
157
158(*---------------------------------------------------------------------------*)
159(* Execution via step index, stopping when a terminal state is hit, or when  *)
160(* the number of prescribed steps is exceeded.                               *)
161(*---------------------------------------------------------------------------*)
162
163(*
164val Run_def =
165 Define 
166  `(Run (M:('a,'state)TM) c 0 = c) /\
167   (Run M c (SUC n) = 
168        if Terminal M c then c 
169        else Run M (Step M c) n)`;
170*)
171
172val Run_def = 
173 Define
174   `Run M c n = 
175      if n = 0 then c 
176      else
177        let c' = Run M c (n-1)
178          in if Terminal M c' then c' 
179             else Step M c'`;
180
181(*---------------------------------------------------------------------------*)
182(* Generate ML code for TMs                                                  *)
183(*---------------------------------------------------------------------------*)
184
185open emitLib;
186
187val elems = 
188 [MLSIG "type num = numML.num",
189  MLSTRUCT "type num = numML.num",
190  OPEN ["num", "list", "combin"],
191  DATATYPE `dir = L | R`,
192  DATATYPE 
193     `TM = <| states     : 'state -> bool ;
194              inputsymbs : 'alpha -> bool ;
195              tapesymbs  : 'alpha -> bool ;
196              init       : 'state ;
197              trans      : 'state -> 'alpha -> 'state # 'alpha # dir;
198              accept     : 'state ;
199              reject     : 'state ;
200              blank      : 'alpha ;
201              star       : 'alpha |>`,
202  DATATYPE 
203     `config = <| left  : 'a list;
204                  cell  : 'a ;
205                  state : 'state ;
206                  right : 'a list |>`,
207  DEFN tape_of_def,
208  DEFN Step_def,
209  DEFN Accepting_def,
210  DEFN Rejecting_def,
211  DEFN Terminal_def,
212  DEFN Initial_def,
213  DEFN Run_def];
214
215val _ = emitML "" ("Turing", elems);
216
217(*---------------------------------------------------------------------------*)
218(* Basic development towards undecidability of HP.                           *)
219(*---------------------------------------------------------------------------*)
220
221val Accepting_lem = Q.prove
222(`!m k M c.
223   isTM M /\ Accepting M (Run M c k) ==> Accepting M (Run M c (m+k))`,
224 Induct THENL
225 [REPEAT STRIP_TAC THEN RW_TAC tm_ss [Once Run_def,Terminal_def] THENL
226  [METIS_TAC [Run_def],
227   RW_TAC tm_ss [] THENL
228   [Q.UNABBREV_TAC `c'` THEN POP_ASSUM MP_TAC THEN 
229     RULE_ASSUM_TAC (ONCE_REWRITE_RULE [Run_def]) THEN
230     BasicProvers.NORM_TAC tm_ss [] THEN 
231     POP_ASSUM MP_TAC THEN RW_TAC tm_ss [Terminal_def,LET_THM],
232    FULL_SIMP_TAC tm_ss [] THEN Q.UNABBREV_TAC `c'` THEN
233     NTAC 2 (POP_ASSUM MP_TAC) THEN
234     RULE_ASSUM_TAC (ONCE_REWRITE_RULE [Run_def]) THEN
235     BasicProvers.NORM_TAC tm_ss [] THEN 
236     POP_ASSUM MP_TAC THEN RW_TAC tm_ss [Terminal_def,LET_THM]]],
237   REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC [Run_def] THEN RW_TAC tm_ss [] THEN
238    FULL_SIMP_TAC bool_ss [DECIDE ``k + SUC m - 1 = m + k``] THEN 
239    `Accepting M c'` by METIS_TAC [] THEN 
240    RW_TAC tm_ss [] THEN METIS_TAC [Terminal_def]]);
241
242val Rejecting_lem = Q.prove
243(`!m k M c.
244   isTM M /\ Rejecting M (Run M c k) ==> Rejecting M (Run M c (m+k))`,
245 Induct THENL
246 [REPEAT STRIP_TAC THEN RW_TAC tm_ss [Once Run_def,Terminal_def] THENL
247  [METIS_TAC [Run_def],
248   RW_TAC tm_ss [] THENL
249   [Q.UNABBREV_TAC `c'` THEN POP_ASSUM MP_TAC THEN 
250     RULE_ASSUM_TAC (ONCE_REWRITE_RULE [Run_def]) THEN
251     BasicProvers.NORM_TAC tm_ss [] THEN 
252     POP_ASSUM MP_TAC THEN RW_TAC tm_ss [Terminal_def,LET_THM],
253    FULL_SIMP_TAC tm_ss [] THEN Q.UNABBREV_TAC `c'` THEN
254     NTAC 2 (POP_ASSUM MP_TAC) THEN 
255     RULE_ASSUM_TAC (ONCE_REWRITE_RULE [Run_def]) THEN 
256     BasicProvers.NORM_TAC tm_ss [] THEN
257     POP_ASSUM MP_TAC THEN RW_TAC tm_ss [Terminal_def,LET_THM]]],
258  REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC [Run_def] THEN RW_TAC tm_ss [] THEN
259   FULL_SIMP_TAC bool_ss [DECIDE ``k + SUC m - 1 = m + k``] THEN 
260   `Rejecting M c'` by METIS_TAC [] THEN RW_TAC tm_ss [] THEN 
261   METIS_TAC [Terminal_def]]);
262
263
264(*---------------------------------------------------------------------------*)
265(* Does a machine M accept or reject a word, or does it loop. It is at this  *)
266(* point that we require the input word be built from M's alphabet.          *)
267(*---------------------------------------------------------------------------*)
268
269val Accepts_def = 
270 Define
271   `Accepts (M:('a,'state)TM) w = 
272      isInputWord M w /\ ?n. Accepting M (Run M (Initial M w) n)`;
273
274val Rejects_def = 
275 Define
276   `Rejects (M:('a,'state)TM) w = 
277      isInputWord M w /\ ?n. Rejecting M (Run M (Initial M w) n)`;
278
279val Loops_def = 
280 Define
281   `Loops (M:('a,'state)TM) w = 
282     isInputWord M w /\ !n. ~Terminal M (Run M (Initial M w) n)`;
283
284val Halts_def =
285 Define
286   `Halts (M:('a,'state)TM,w) = Accepts M w \/ Rejects M w`;
287
288val RunCases = Q.prove
289(`!M w. isInputWord M w ==> Accepts M w \/ Rejects M w \/ Loops M w`,
290 METIS_TAC[Accepts_def, Rejects_def, Loops_def, 
291           Accepting_def, Rejecting_def, Terminal_def]);
292
293val LoopCases = Q.prove
294(`!M w. isInputWord M w ==> Halts (M,w) \/ Loops M w`,
295  METIS_TAC [RunCases,Halts_def]);
296
297val Halts_not_Loops = Q.prove
298(`!M w. isInputWord M w ==> (Halts (M,w) = ~Loops M w)`,
299  METIS_TAC [Loops_def,Halts_def,Terminal_def,Accepts_def, Rejects_def]);
300
301val Not_Accepts_and_Rejects = Q.prove
302(`!M w. isTM M ==> ~(Accepts M w /\ Rejects M w)`,
303 RW_TAC bool_ss [GSYM IMP_DISJ_THM,Accepts_def, Rejects_def] THEN 
304  STRIP_TAC THEN
305  STRIP_ASSUME_TAC (DECIDE ``n < n' \/ (n=n') \/ n' < n``) THENL
306  [`?p. p + n = n'` by METIS_TAC [LESS_ADD] THEN RW_TAC std_ss [] THEN
307   `Accepting M (Run M (Initial M w) (p + n))` by METIS_TAC [Accepting_lem] THEN
308   METIS_TAC [isTM_def, Accepting_def, Rejecting_def],
309   RW_TAC std_ss [] THEN METIS_TAC [isTM_def, Accepting_def, Rejecting_def],
310  `?p. p + n' = n` by METIS_TAC [LESS_ADD] THEN RW_TAC std_ss [] THEN 
311  `Rejecting M (Run M (Initial M w) (p + n'))` by METIS_TAC [Rejecting_lem] THEN
312  METIS_TAC [isTM_def, Accepting_def, Rejecting_def]]);
313
314
315(*---------------------------------------------------------------------------*)
316(* The language defined by a machine is the set of input words on which it   *)
317(* halts and accepts.                                                        *)
318(*---------------------------------------------------------------------------*)
319
320val Lang_of_def = 
321 Define 
322   `Lang_of (M:('a,'state)TM) = {w | Accepts M w}`;
323
324(*---------------------------------------------------------------------------*)
325(* A set s is recognizable, or recursively enumerable (r.e.), if there is a  *)
326(* single machine that accepts all elements in s. For elements not in s, the *)
327(* machine can either reject or loop.                                        *)
328(*---------------------------------------------------------------------------*)
329
330val Recognizable_def = 
331 Define
332   `Recognizable s = ?M:('a,num)TM. isTM M /\ (Lang_of M = s)`;
333
334(*---------------------------------------------------------------------------*)
335(* A set s is decidable if there exists a machine M that accepts elements in *)
336(* s and rejects elements not in s.                                          *)
337(*---------------------------------------------------------------------------*)
338
339val isDecider_def = 
340 Define 
341  `isDecider (M:('a,num)TM) s =
342       isTM M /\ 
343       !w. (w IN s ==> Accepts M w) /\
344           (~(w IN s) ==> Rejects M w)`;
345
346val Decidable_def = 
347 Define
348   `Decidable s = ?M:('a,num)TM. isDecider M s`;
349
350(*---------------------------------------------------------------------------*)
351(* Useful sanity test: if a set and its complement are recognizable then     *)
352(* the set is decidable. Proof interleaves the two recognizers.              *)
353(*---------------------------------------------------------------------------*)
354(*
355g `!s. Recognizable s /\ Recognizable (COMPL s) ==> Decidable s`;
356*)
357
358