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