3 begin |
3 begin |
4 |
4 |
5 section {* Wang coding of input arguments *} |
5 section {* Wang coding of input arguments *} |
6 |
6 |
7 text {* |
7 text {* |
8 The direct compilation of the universal function @{text "rec_F"} can not give us UTM, because @{text "rec_F"} is of arity 2, |
8 The direct compilation of the universal function @{text "rec_F"} can |
9 where the first argument represents the Godel coding of the TM being simulated and the second argument represents the right number (in Wang's coding) of the TM tape. |
9 not give us UTM, because @{text "rec_F"} is of arity 2, where the |
10 (Notice, left number is always @{text "0"} at the very beginning). However, UTM needs to simulate the execution of any TM which may |
10 first argument represents the Godel coding of the TM being simulated |
11 very well take many input arguments. Therefore, a initialization TM needs to run before the TM compiled from @{text "rec_F"}, and the sequential |
11 and the second argument represents the right number (in Wang's |
12 composition of these two TMs will give rise to the UTM we are seeking. The purpose of this initialization TM is to transform the multiple |
12 coding) of the TM tape. (Notice, left number is always @{text "0"} |
13 input arguments of the TM being simulated into Wang's coding, so that it can be consumed by the TM compiled from @{text "rec_F"} as the second |
13 at the very beginning). However, UTM needs to simulate the execution |
14 argument. |
14 of any TM which may very well take many input arguments. Therefore, |
15 |
15 a initialization TM needs to run before the TM compiled from @{text |
16 However, this initialization TM (named @{text "t_wcode"}) can not be constructed by compiling from any resurve function, because every recursive |
16 "rec_F"}, and the sequential composition of these two TMs will give |
17 function takes a fixed number of input arguments, while @{text "t_wcode"} needs to take varying number of arguments and tranform them into |
17 rise to the UTM we are seeking. The purpose of this initialization |
18 Wang's coding. Therefore, this section give a direct construction of @{text "t_wcode"} with just some parts being obtained from recursive functions. |
18 TM is to transform the multiple input arguments of the TM being |
|
19 simulated into Wang's coding, so that it can be consumed by the TM |
|
20 compiled from @{text "rec_F"} as the second argument. |
|
21 |
|
22 However, this initialization TM (named @{text "t_wcode"}) can not be |
|
23 constructed by compiling from any resurve function, because every |
|
24 recursive function takes a fixed number of input arguments, while |
|
25 @{text "t_wcode"} needs to take varying number of arguments and |
|
26 tranform them into Wang's coding. Therefore, this section give a |
|
27 direct construction of @{text "t_wcode"} with just some parts being |
|
28 obtained from recursive functions. |
19 |
29 |
20 \newlength{\basewidth} |
30 \newlength{\basewidth} |
21 \settowidth{\basewidth}{xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx} |
31 \settowidth{\basewidth}{xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx} |
22 \newlength{\baseheight} |
32 \newlength{\baseheight} |
23 \settoheight{\baseheight}{$B:R$} |
33 \settoheight{\baseheight}{$B:R$} |
69 \draw [->, >=latex, thick] (10)+(0, -4\baseheight) -- (10); |
79 \draw [->, >=latex, thick] (10)+(0, -4\baseheight) -- (10); |
70 \end{tikzpicture}} |
80 \end{tikzpicture}} |
71 \caption{The output of TM $prepare$} \label{prepare_output} |
81 \caption{The output of TM $prepare$} \label{prepare_output} |
72 \end{figure} |
82 \end{figure} |
73 |
83 |
74 As shown in Figure \ref{prepare_input}, the input of $prepare$ is the same as the the input |
84 As shown in Figure \ref{prepare_input}, the input of $prepare$ is the |
75 of UTM, where $m$ is the Godel coding of the TM being interpreted and $a_1$ through $a_n$ are the $n$ input arguments of the TM under interpretation. The purpose of $purpose$ is to transform this initial tape layout to the one shown in Figure \ref{prepare_output}, |
85 same as the the input of UTM, where $m$ is the Godel coding of the TM |
76 which is convenient for the generation of Wang's codding of $a_1, \ldots, a_n$. The coding procedure starts from $a_n$ and ends after $a_1$ is encoded. The coding result is stored in an accumulator at the end of the tape (initially represented by the $1$ two blanks right to $a_n$ in Figure \ref{prepare_output}). In Figure \ref{prepare_output}, arguments $a_1, \ldots, a_n$ are separated by two blanks on both ends with the rest so that movement conditions can be implemented conveniently in subsequent TMs, because, by convention, |
86 being interpreted and $a_1$ through $a_n$ are the $n$ input arguments |
77 two consecutive blanks are usually used to signal the end or start of a large chunk of data. The diagram of $prepare$ is given in Figure \ref{prepare_diag}. |
87 of the TM under interpretation. The purpose of $purpose$ is to |
|
88 transform this initial tape layout to the one shown in Figure |
|
89 \ref{prepare_output}, which is convenient for the generation of Wang's |
|
90 codding of $a_1, \ldots, a_n$. The coding procedure starts from $a_n$ |
|
91 and ends after $a_1$ is encoded. The coding result is stored in an |
|
92 accumulator at the end of the tape (initially represented by the $1$ |
|
93 two blanks right to $a_n$ in Figure \ref{prepare_output}). In Figure |
|
94 \ref{prepare_output}, arguments $a_1, \ldots, a_n$ are separated by |
|
95 two blanks on both ends with the rest so that movement conditions can |
|
96 be implemented conveniently in subsequent TMs, because, by convention, |
|
97 two consecutive blanks are usually used to signal the end or start of |
|
98 a large chunk of data. The diagram of $prepare$ is given in Figure |
|
99 \ref{prepare_diag}. |
78 |
100 |
79 |
101 |
80 \begin{figure}[h!] |
102 \begin{figure}[h!] |
81 \centering |
103 \centering |
82 \scalebox{0.9}{ |
104 \scalebox{0.9}{ |
1324 and tm_wf: "tm_wf (ap, 0)" |
1345 and tm_wf: "tm_wf (ap, 0)" |
1325 shows "\<exists> stp. steps0 (Suc 0, l, r) (adjust ap) stp = |
1346 shows "\<exists> stp. steps0 (Suc 0, l, r) (adjust ap) stp = |
1326 (Suc (length ap div 2), l', r')" |
1347 (Suc (length ap div 2), l', r')" |
1327 proof - |
1348 proof - |
1328 have "\<exists> stp. \<not> is_final (steps0 (1, l, r) ap stp) \<and> (steps0 (1, l, r) ap (Suc stp) = (0, l', r'))" |
1349 have "\<exists> stp. \<not> is_final (steps0 (1, l, r) ap stp) \<and> (steps0 (1, l, r) ap (Suc stp) = (0, l', r'))" |
1329 thm before_final using exec |
1350 using exec |
1330 by(erule_tac before_final) |
1351 by(erule_tac before_final) |
1331 then obtain stpa where a: |
1352 then obtain stpa where a: |
1332 "\<not> is_final (steps0 (1, l, r) ap stpa) \<and> (steps0 (1, l, r) ap (Suc stpa) = (0, l', r'))" .. |
1353 "\<not> is_final (steps0 (1, l, r) ap stpa) \<and> (steps0 (1, l, r) ap (Suc stpa) = (0, l', r'))" .. |
1333 obtain sa la ra where b:"steps0 (1, l, r) ap stpa = (sa, la, ra)" by (metis prod_cases3) |
1354 obtain sa la ra where b:"steps0 (1, l, r) ap stpa = (sa, la, ra)" by (metis prod_cases3) |
1334 hence c: "steps0 (Suc 0, l, r) (adjust ap) stpa = (sa, la, ra)" |
1355 hence c: "steps0 (Suc 0, l, r) (adjust ap) stpa = (sa, la, ra)" |
1375 (tm_of abc_twice @ shift (mopup (Suc 0)) ((length (tm_of abc_twice) div 2))) stp = |
1396 (tm_of abc_twice @ shift (mopup (Suc 0)) ((length (tm_of abc_twice) div 2))) stp = |
1376 (0, Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (2 * rs)) @ Bk\<up>(rn))" by blast |
1397 (0, Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (2 * rs)) @ Bk\<up>(rn))" by blast |
1377 hence "\<exists> stp. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n)) |
1398 hence "\<exists> stp. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n)) |
1378 (adjust t_twice_compile) stp |
1399 (adjust t_twice_compile) stp |
1379 = (Suc (length t_twice_compile div 2), Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (2 * rs)) @ Bk\<up>(rn))" |
1400 = (Suc (length t_twice_compile div 2), Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (2 * rs)) @ Bk\<up>(rn))" |
1380 thm adjust_halt_eq |
|
1381 apply(rule_tac stp = stp in adjust_halt_eq) |
1401 apply(rule_tac stp = stp in adjust_halt_eq) |
1382 apply(simp add: t_twice_compile_def, auto) |
1402 apply(simp add: t_twice_compile_def, auto) |
1383 done |
1403 done |
1384 then obtain stpb where |
1404 then obtain stpb where |
1385 "steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n)) |
1405 "steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n)) |
3308 |
3328 |
3309 lemma [intro]: "tm_wf (t_wcode_prepare, 0)" |
3329 lemma [intro]: "tm_wf (t_wcode_prepare, 0)" |
3310 apply(simp add:tm_wf.simps t_wcode_prepare_def) |
3330 apply(simp add:tm_wf.simps t_wcode_prepare_def) |
3311 done |
3331 done |
3312 |
3332 |
3313 (* |
|
3314 lemma t_correct_termi: "t_correct tp \<Longrightarrow> |
|
3315 list_all (\<lambda>(acn, st). (st \<le> Suc (length tp div 2))) (change_termi_state tp)" |
|
3316 apply(auto simp: t_correct.simps List.list_all_length) |
|
3317 apply(erule_tac x = n in allE, simp) |
|
3318 apply(case_tac "tp!n", auto simp: change_termi_state.simps split: if_splits) |
|
3319 done |
|
3320 *) |
|
3321 |
|
3322 lemma t_correct_shift: |
3333 lemma t_correct_shift: |
3323 "list_all (\<lambda>(acn, st). (st \<le> y)) tp \<Longrightarrow> |
3334 "list_all (\<lambda>(acn, st). (st \<le> y)) tp \<Longrightarrow> |
3324 list_all (\<lambda>(acn, st). (st \<le> y + off)) (shift tp off) " |
3335 list_all (\<lambda>(acn, st). (st \<le> y + off)) (shift tp off) " |
3325 apply(auto simp: List.list_all_length) |
3336 apply(auto simp: List.list_all_length) |
3326 apply(erule_tac x = n in allE, simp add: length_shift) |
3337 apply(erule_tac x = n in allE, simp add: length_shift) |
3327 apply(case_tac "tp!n", auto simp: shift.simps) |
3338 apply(case_tac "tp!n", auto simp: shift.simps) |
3328 done |
3339 done |
3329 (* |
|
3330 lemma [intro]: |
|
3331 "t_correct (tm_of abc_twice @ tMp (Suc 0) |
|
3332 (start_of twice_ly (length abc_twice) - Suc 0))" |
|
3333 apply(rule_tac t_compiled_correct, simp_all) |
|
3334 apply(simp add: twice_ly_def) |
|
3335 done |
|
3336 |
|
3337 lemma [intro]: "t_correct (tm_of abc_fourtimes @ tMp (Suc 0) |
|
3338 (start_of fourtimes_ly (length abc_fourtimes) - Suc 0))" |
|
3339 apply(rule_tac t_compiled_correct, simp_all) |
|
3340 apply(simp add: fourtimes_ly_def) |
|
3341 done |
|
3342 *) |
|
3343 |
3340 |
3344 lemma [intro]: "(28 + (length t_twice_compile + length t_fourtimes_compile)) mod 2 = 0" |
3341 lemma [intro]: "(28 + (length t_twice_compile + length t_fourtimes_compile)) mod 2 = 0" |
3345 apply(auto simp: t_twice_compile_def t_fourtimes_compile_def) |
3342 apply(auto simp: t_twice_compile_def t_fourtimes_compile_def) |
3346 by arith |
3343 by arith |
3347 |
3344 |
4663 |
4659 |
4664 definition UTM_pre :: "instr list" |
4660 definition UTM_pre :: "instr list" |
4665 where |
4661 where |
4666 "UTM_pre = t_wcode |+| t_utm" |
4662 "UTM_pre = t_wcode |+| t_utm" |
4667 |
4663 |
4668 (* |
|
4669 lemma F_abc_halt_eq: |
|
4670 "\<lbrakk>Turing.t_correct tp; |
|
4671 length lm = k; |
|
4672 steps (Suc 0, Bk\<up>(l), <lm>) tp stp = (0, Bk\<up>(m), Oc\<up>(rs)@Bk\<up>(n)); |
|
4673 rs > 0\<rbrakk> |
|
4674 \<Longrightarrow> \<exists> stp m. abc_steps_l (0, [code tp, bl2wc (<lm>)]) (F_aprog) stp = |
|
4675 (length (F_aprog), code tp # bl2wc (<lm>) # (rs - 1) # 0\<up>(m))" |
|
4676 apply(drule_tac F_t_halt_eq, simp, simp, simp) |
|
4677 apply(case_tac "rec_ci rec_F") |
|
4678 apply(frule_tac abc_append_dummy_complie, simp, simp, erule_tac exE, |
|
4679 erule_tac exE) |
|
4680 apply(rule_tac x = stp in exI, rule_tac x = m in exI) |
|
4681 apply(simp add: F_aprog_def dummy_abc_def) |
|
4682 done |
|
4683 |
|
4684 lemma F_abc_utm_halt_eq: |
|
4685 "\<lbrakk>rs > 0; |
|
4686 abc_steps_l (0, [code tp, bl2wc (<lm>)]) F_aprog stp = |
|
4687 (length F_aprog, code tp # bl2wc (<lm>) # (rs - 1) # 0\<up>(m))\<rbrakk> |
|
4688 \<Longrightarrow> \<exists>stp m n.(steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) t_utm stp = |
|
4689 (0, Bk\<up>(m), Oc\<up>(rs) @ Bk\<up>(n)))" |
|
4690 thm abacus_turing_eq_halt |
|
4691 using abacus_turing_eq_halt |
|
4692 [of "layout_of F_aprog" "F_aprog" "F_tprog" "length (F_aprog)" |
|
4693 "[code tp, bl2wc (<lm>)]" stp "code tp # bl2wc (<lm>) # (rs - 1) # 0\<up>(m)" "Suc (Suc 0)" |
|
4694 "start_of (layout_of (F_aprog)) (length (F_aprog))" "[]" 0] |
|
4695 apply(simp add: F_tprog_def t_utm_def abc_lm_v.simps nth_append) |
|
4696 apply(erule_tac exE)+ |
|
4697 apply(rule_tac x = stpa in exI, rule_tac x = "Suc (Suc ma)" in exI, |
|
4698 rule_tac x = l in exI, simp add: exp_ind) |
|
4699 done |
|
4700 |
|
4701 declare tape_of_nl_abv_cons[simp del] |
|
4702 |
|
4703 lemma t_utm_halt_eq': |
|
4704 "\<lbrakk>Turing.t_correct tp; |
|
4705 0 < rs; |
|
4706 steps (Suc 0, Bk\<up>(l), <lm::nat list>) tp stp = (0, Bk\<up>(m), Oc\<up>(rs)@Bk\<up>(n))\<rbrakk> |
|
4707 \<Longrightarrow> \<exists>stp m n. steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) t_utm stp = |
|
4708 (0, Bk\<up>(m), Oc\<up>(rs) @ Bk\<up>(n))" |
|
4709 apply(drule_tac l = l in F_abc_halt_eq, simp, simp, simp) |
|
4710 apply(erule_tac exE, erule_tac exE) |
|
4711 apply(rule_tac F_abc_utm_halt_eq, simp_all) |
|
4712 done |
|
4713 *) |
|
4714 (* |
|
4715 lemma [simp]: "tinres xs (xs @ Bk\<up>(i))" |
|
4716 apply(auto simp: tinres_def) |
|
4717 done |
|
4718 |
|
4719 lemma [elim]: "\<lbrakk>rs > 0; Oc\<up>(rs) @ Bk\<up>(na) = c @ Bk\<up>(n)\<rbrakk> |
|
4720 \<Longrightarrow> \<exists>n. c = Oc\<up>(rs) @ Bk\<up>(n)" |
|
4721 apply(case_tac "na > n") |
|
4722 apply(subgoal_tac "\<exists> d. na = d + n", auto simp: exp_add) |
|
4723 apply(rule_tac x = "na - n" in exI, simp) |
|
4724 apply(subgoal_tac "\<exists> d. n = d + na", auto simp: exp_add) |
|
4725 apply(case_tac rs, simp_all add: exp_ind, case_tac d, |
|
4726 simp_all add: exp_ind) |
|
4727 apply(rule_tac x = "n - na" in exI, simp) |
|
4728 done |
|
4729 *) |
|
4730 (* |
|
4731 lemma t_utm_halt_eq'': |
|
4732 "\<lbrakk>Turing.t_correct tp; |
|
4733 0 < rs; |
|
4734 steps (Suc 0, Bk\<up>(l), <lm::nat list>) tp stp = (0, Bk\<up>(m), Oc\<up>(rs)@Bk\<up>(n))\<rbrakk> |
|
4735 \<Longrightarrow> \<exists>stp m n. steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>(i)) t_utm stp = |
|
4736 (0, Bk\<up>(m), Oc\<up>(rs) @ Bk\<up>(n))" |
|
4737 apply(drule_tac t_utm_halt_eq', simp_all) |
|
4738 apply(erule_tac exE)+ |
|
4739 proof - |
|
4740 fix stpa ma na |
|
4741 assume "steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) t_utm stpa = (0, Bk\<up>(ma), Oc\<up>(rs) @ Bk\<up>(na))" |
|
4742 and gr: "rs > 0" |
|
4743 thus "\<exists>stp m n. steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>(i)) t_utm stp = (0, Bk\<up>(m), Oc\<up>(rs) @ Bk\<up>(n))" |
|
4744 apply(rule_tac x = stpa in exI, rule_tac x = ma in exI, simp) |
|
4745 proof(case_tac "steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>(i)) t_utm stpa", simp) |
|
4746 fix a b c |
|
4747 assume "steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) t_utm stpa = (0, Bk\<up>(ma), Oc\<up>(rs) @ Bk\<up>(na))" |
|
4748 "steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>(i)) t_utm stpa = (a, b, c)" |
|
4749 thus " a = 0 \<and> b = Bk\<up>(ma) \<and> (\<exists>n. c = Oc\<up>(rs) @ Bk\<up>(n))" |
|
4750 using tinres_steps2[of "<[code tp, bl2wc (<lm>)]>" "<[code tp, bl2wc (<lm>)]> @ Bk\<up>(i)" |
|
4751 "Suc 0" " [Bk, Bk]" t_utm stpa 0 "Bk\<up>(ma)" "Oc\<up>(rs) @ Bk\<up>(na)" a b c] |
|
4752 apply(simp) |
|
4753 using gr |
|
4754 apply(simp only: tinres_def, auto) |
|
4755 apply(rule_tac x = "na + n" in exI, simp add: exp_add) |
|
4756 done |
|
4757 qed |
|
4758 qed |
|
4759 |
|
4760 lemma [simp]: "tinres [Bk, Bk] [Bk]" |
|
4761 apply(auto simp: tinres_def) |
|
4762 done |
|
4763 |
|
4764 lemma [elim]: "Bk\<up>(ma) = b @ Bk\<up>(n) \<Longrightarrow> \<exists>m. b = Bk\<up>(m)" |
|
4765 apply(subgoal_tac "ma = length b + n") |
|
4766 apply(rule_tac x = "ma - n" in exI, simp add: exp_add) |
|
4767 apply(drule_tac length_equal) |
|
4768 apply(simp) |
|
4769 done |
|
4770 *) |
|
4771 |
|
4772 |
|
4773 |
|
4774 lemma tinres_step1: |
4664 lemma tinres_step1: |
4775 "\<lbrakk>tinres l l'; step (ss, l, r) (t, 0) = (sa, la, ra); |
4665 "\<lbrakk>tinres l l'; step (ss, l, r) (t, 0) = (sa, la, ra); |
4776 step (ss, l', r) (t, 0) = (sb, lb, rb)\<rbrakk> |
4666 step (ss, l', r) (t, 0) = (sb, lb, rb)\<rbrakk> |
4777 \<Longrightarrow> tinres la lb \<and> ra = rb \<and> sa = sb" |
4667 \<Longrightarrow> tinres la lb \<and> ra = rb \<and> sa = sb" |
4778 apply(case_tac ss, case_tac [!]r, case_tac [!] "a::cell") |
4668 apply(case_tac ss, case_tac [!]r, case_tac [!] "a::cell") |