theory Standard_Results imports Universal begin section ‹Kleene normal form and the number of $\mu$-operations› text ‹Kleene's original normal form theorem~\<^cite>‹"Kleene43"› states that every partial recursive $f$ can be expressed as $f(x) = u(\mu y[t(i, x, y) = 0]$ for some $i$, where $u$ and $t$ are specially crafted primitive recursive functions tied to Kleene's definition of partial recursive functions. Rogers~\<^cite>‹‹p.~29f.› in "Rogers87"› relaxes the theorem by allowing $u$ and $t$ to be any primitive recursive functions of arity one and three, respectively. Both versions require a separate $t$-predicate for every arity. We will show a unified version for all arities by treating $x$ as an encoded list of arguments. Our universal function @{thm[display,names_short] "r_univ_def"} can represent all partial recursive functions (see theorem @{thm[source] r_univ}). Moreover @{term "r_result"}, @{term "r_dec"}, and @{term "r_not"} are primitive recursive. As such @{term r_univ} could almost serve as the right-hand side $u(\mu y[t(i, x, y) = 0]$. Its only flaw is that the outer function, the composition of @{term r_dec} and @{term r_result}, is ternary rather than unary.› lemma r_univ_almost_kleene_nf: "r_univ ≃ (let u = Cn 3 r_dec [r_result]; t = Cn 3 r_not [r_result] in Cn 2 u [Mn 2 t, Id 2 0, Id 2 1])" unfolding r_univ_def by (rule exteqI) simp_all text ‹We can remedy the wrong arity with some encoding and projecting.› definition r_nf_t :: recf where "r_nf_t ≡ Cn 3 r_and [Cn 3 r_eq [Cn 3 r_pdec2 [Id 3 0], Cn 3 r_prod_encode [Id 3 1, Id 3 2]], Cn 3 r_not [Cn 3 r_result [Cn 3 r_pdec1 [Id 3 0], Cn 3 r_pdec12 [Id 3 0], Cn 3 r_pdec22 [Id 3 0]]]]" lemma r_nf_t_prim: "prim_recfn 3 r_nf_t" unfolding r_nf_t_def by simp definition r_nf_u :: recf where "r_nf_u ≡ Cn 1 r_dec [Cn 1 r_result [r_pdec1, r_pdec12, r_pdec22]]" lemma r_nf_u_prim: "prim_recfn 1 r_nf_u" unfolding r_nf_u_def by simp lemma r_nf_t_0: assumes "eval r_result [pdec1 y, pdec12 y, pdec22 y] ↓≠ 0" and "pdec2 y = prod_encode (i, x)" shows "eval r_nf_t [y, i, x] ↓= 0" unfolding r_nf_t_def using assms by auto lemma r_nf_t_1: assumes "eval r_result [pdec1 y, pdec12 y, pdec22 y] ↓= 0 ∨ pdec2 y ≠ prod_encode (i, x)" shows "eval r_nf_t [y, i, x] ↓= 1" unfolding r_nf_t_def using assms r_result_total by auto text ‹The next function is just as universal as @{term r_univ}, but satisfies the conditions of the Kleene normal form theorem because the outer funtion @{term r_nf_u} is unary.› definition "r_normal_form ≡ Cn 2 r_nf_u [Mn 2 r_nf_t]" lemma r_normal_form_recfn: "recfn 2 r_normal_form" unfolding r_normal_form_def using r_nf_u_prim r_nf_t_prim by simp lemma r_univ_exteq_r_normal_form: "r_univ ≃ r_normal_form" proof (rule exteqI) show arity: "arity r_univ = arity r_normal_form" using r_normal_form_recfn by simp show "eval r_univ xs = eval r_normal_form xs" if "length xs = arity r_univ" for xs proof - have "length xs = 2" using that by simp then obtain i x where ix: "[i, x] = xs" by (smt Suc_length_conv length_0_conv numeral_2_eq_2) have "eval r_univ [i, x] = eval r_normal_form [i, x]" proof (cases "∀t. eval r_result [t, i, x] ↓= 0") case True then have "eval r_univ [i, x] ↑" unfolding r_univ_def by simp moreover have "eval r_normal_form [i, x] ↑" proof - have "eval r_nf_t [y, i, x] ↓= 1" for y using True r_nf_t_1[of y i x] by fastforce then show ?thesis unfolding r_normal_form_def using r_nf_u_prim r_nf_t_prim by simp qed ultimately show ?thesis by simp next case False then have "∃t. eval r_result [t, i, x] ↓≠ 0" by (simp add: r_result_total) then obtain t where "eval r_result [t, i, x] ↓≠ 0" by auto then have "eval r_nf_t [triple_encode t i x, i, x] ↓= 0" using r_nf_t_0 by simp then obtain y where y: "eval (Mn 2 r_nf_t) [i, x] ↓= y" using r_nf_t_prim Mn_free_imp_total by fastforce then have "eval r_nf_t [y, i, x] ↓= 0" using r_nf_t_prim Mn_free_imp_total eval_Mn_convergE(2)[of 2 r_nf_t "[i, x]" y] by simp then have r_result: "eval r_result [pdec1 y, pdec12 y, pdec22 y] ↓≠ 0" and pdec2: "pdec2 y = prod_encode (i, x)" using r_nf_t_0[of y i x] r_nf_t_1[of y i x] r_result_total by auto then have "eval r_result [pdec1 y, i, x] ↓≠ 0" by simp then obtain v where v: "eval r_univ [pdec12 y, pdec22 y] ↓= v" "eval r_result [pdec1 y, pdec12 y, pdec22 y] ↓= Suc v" using r_result r_result_bivalent'[of "pdec12 y" "pdec22 y" _ "pdec1 y"] r_result_diverg'[of "pdec12 y" "pdec22 y" "pdec1 y"] by auto have "eval r_normal_form [i, x] = eval r_nf_u [y]" unfolding r_normal_form_def using y r_nf_t_prim r_nf_u_prim by simp also have "... = eval r_dec [the (eval (Cn 1 r_result [r_pdec1, r_pdec12, r_pdec22]) [y])]" unfolding r_nf_u_def using r_result by simp also have "... = eval r_dec [Suc v]" using v by simp also have "... ↓= v" by simp finally have "eval r_normal_form [i, x] ↓= v" . moreover have "eval r_univ [i, x] ↓= v" using v(1) pdec2 by simp ultimately show ?thesis by simp qed with ix show ?thesis by simp qed qed theorem normal_form: assumes "recfn n f" obtains i where "∀x. e_length x = n ⟶ eval r_normal_form [i, x] = eval f (list_decode x)" proof - have "eval r_normal_form [encode f, x] = eval f (list_decode x)" if "e_length x = n" for x using r_univ_exteq_r_normal_form assms that exteq_def r_univ' by auto then show ?thesis using that by auto qed text ‹As a consequence of the normal form theorem every partial recursive function can be represented with exactly one application of the $\mu$-operator.› fun count_Mn :: "recf ⇒ nat" where "count_Mn Z = 0" | "count_Mn S = 0" | "count_Mn (Id m n) = 0" | "count_Mn (Cn n f gs) = count_Mn f + sum_list (map count_Mn gs)" | "count_Mn (Pr n f g) = count_Mn f + count_Mn g" | "count_Mn (Mn n f) = Suc (count_Mn f)" lemma count_Mn_zero_iff_prim: "count_Mn f = 0 ⟷ Mn_free f" by (induction f) auto text ‹The normal form has only one $\mu$-recursion.› lemma count_Mn_normal_form: "count_Mn r_normal_form = 1" unfolding r_normal_form_def r_nf_u_def r_nf_t_def using count_Mn_zero_iff_prim by simp lemma one_Mn_suffices: assumes "recfn n f" shows "∃g. count_Mn g = 1 ∧ g ≃ f" proof - have "n > 0" using assms wellf_arity_nonzero by auto obtain i where i: "∀x. e_length x = n ⟶ eval r_normal_form [i, x] = eval f (list_decode x)" using normal_form[OF assms(1)] by auto define g where "g ≡ Cn n r_normal_form [r_constn (n - 1) i, r_list_encode (n - 1)]" then have "recfn n g" using r_normal_form_recfn ‹n > 0› by simp then have "g ≃ f" using g_def r_list_encode i assms by (intro exteqI) simp_all moreover have "count_Mn g = 1" unfolding g_def using count_Mn_normal_form count_Mn_zero_iff_prim by simp ultimately show ?thesis by auto qed text ‹The previous lemma could have been obtained without @{term "r_normal_form"} directly from @{term "r_univ"}.› section ‹The $s$-$m$-$n$ theorem› text ‹For all $m, n > 0$ there is an $(m + 1)$-ary primitive recursive function $s^m_n$ with \[ \varphi_p^{(m + n)}(c_1, \dots,c_m, x_1, \dots, x_n) = \varphi_{s^m_n(p, c_1, \dots,c_m)}^{(n)}(x_1, \dots, x_n) \] for all $p, c_1, \ldots, c_m, x_1, \ldots, x_n$. Here, $\varphi^{(n)}$ is a function universal for $n$-ary partial recursive functions, which we will represent by @{term "r_universal n"}› text ‹The $s^m_n$ functions compute codes of functions. We start simple: computing codes of the unary constant functions.› fun code_const1 :: "nat ⇒ nat" where "code_const1 0 = 0" | "code_const1 (Suc c) = quad_encode 3 1 1 (singleton_encode (code_const1 c))" lemma code_const1: "code_const1 c = encode (r_const c)" by (induction c) simp_all definition "r_code_const1_aux ≡ Cn 3 r_prod_encode [r_constn 2 3, Cn 3 r_prod_encode [r_constn 2 1, Cn 3 r_prod_encode [r_constn 2 1, Cn 3 r_singleton_encode [Id 3 1]]]]" lemma r_code_const1_aux_prim: "prim_recfn 3 r_code_const1_aux" by (simp_all add: r_code_const1_aux_def) lemma r_code_const1_aux: "eval r_code_const1_aux [i, r, c] ↓= quad_encode 3 1 1 (singleton_encode r)" by (simp add: r_code_const1_aux_def) definition "r_code_const1 ≡ r_shrink (Pr 1 Z r_code_const1_aux)" lemma r_code_const1_prim: "prim_recfn 1 r_code_const1" by (simp_all add: r_code_const1_def r_code_const1_aux_prim) lemma r_code_const1: "eval r_code_const1 [c] ↓= code_const1 c" proof - let ?h = "Pr 1 Z r_code_const1_aux" have "eval ?h [c, x] ↓= code_const1 c" for x using r_code_const1_aux r_code_const1_def by (induction c) (simp_all add: r_code_const1_aux_prim) then show ?thesis by (simp add: r_code_const1_def r_code_const1_aux_prim) qed text ‹Functions that compute codes of higher-arity constant functions:› definition code_constn :: "nat ⇒ nat ⇒ nat" where "code_constn n c ≡ if n = 1 then code_const1 c else quad_encode 3 n (code_const1 c) (singleton_encode (triple_encode 2 n 0))" lemma code_constn: "code_constn (Suc n) c = encode (r_constn n c)" unfolding code_constn_def using code_const1 r_constn_def by (cases "n = 0") simp_all definition r_code_constn :: "nat ⇒ recf" where "r_code_constn n ≡ if n = 1 then r_code_const1 else Cn 1 r_prod_encode [r_const 3, Cn 1 r_prod_encode [r_const n, Cn 1 r_prod_encode [r_code_const1, Cn 1 r_singleton_encode [Cn 1 r_prod_encode [r_const 2, Cn 1 r_prod_encode [r_const n, Z]]]]]]" lemma r_code_constn_prim: "prim_recfn 1 (r_code_constn n)" by (simp_all add: r_code_constn_def r_code_const1_prim) lemma r_code_constn: "eval (r_code_constn n) [c] ↓= code_constn n c" by (auto simp add: r_code_constn_def r_code_const1 code_constn_def r_code_const1_prim) text ‹Computing codes of $m$-ary projections:› definition code_id :: "nat ⇒ nat ⇒ nat" where "code_id m n ≡ triple_encode 2 m n" lemma code_id: "encode (Id m n) = code_id m n" unfolding code_id_def by simp text ‹The functions $s^m_n$ are represented by the following function. The value $m$ corresponds to the length of @{term "cs"}.› definition smn :: "nat ⇒ nat ⇒ nat list ⇒ nat" where "smn n p cs ≡ quad_encode 3 n (encode (r_universal (n + length cs))) (list_encode (code_constn n p # map (code_constn n) cs @ map (code_id n) [0..<n]))" lemma smn: assumes "n > 0" shows "smn n p cs = encode (Cn n (r_universal (n + length cs)) (r_constn (n - 1) p # map (r_constn (n - 1)) cs @ (map (Id n) [0..<n])))" proof - let ?p = "r_constn (n - 1) p" let ?gs1 = "map (r_constn (n - 1)) cs" let ?gs2 = "map (Id n) [0..<n]" let ?gs = "?p # ?gs1 @ ?gs2" have "map encode ?gs1 = map (code_constn n) cs" by (intro nth_equalityI; auto; metis code_constn assms Suc_pred) moreover have "map encode ?gs2 = map (code_id n) [0..<n]" by (rule nth_equalityI) (auto simp add: code_id_def) moreover have "encode ?p = code_constn n p" using assms code_constn[of "n - 1" p] by simp ultimately have "map encode ?gs = code_constn n p # map (code_constn n) cs @ map (code_id n) [0..<n]" by simp then show ?thesis unfolding smn_def using assms encode.simps(4) by presburger qed text ‹The next function is to help us define @{typ recf}s corresponding to the $s^m_n$ functions. It maps $m + 1$ arguments $p, c_1, \ldots, c_m$ to an encoded list of length $m + n + 1$. The list comprises the $m + 1$ codes of the $n$-ary constants $p, c_1, \ldots, c_m$ and the $n$ codes for all $n$-ary projections.› definition r_smn_aux :: "nat ⇒ nat ⇒ recf" where "r_smn_aux n m ≡ Cn (Suc m) (r_list_encode (m + n)) (map (λi. Cn (Suc m) (r_code_constn n) [Id (Suc m) i]) [0..<Suc m] @ map (λi. r_constn m (code_id n i)) [0..<n])" lemma r_smn_aux_prim: "n > 0 ⟹ prim_recfn (Suc m) (r_smn_aux n m)" by (auto simp add: r_smn_aux_def r_code_constn_prim) lemma r_smn_aux: assumes "n > 0" and "length cs = m" shows "eval (r_smn_aux n m) (p # cs) ↓= list_encode (map (code_constn n) (p # cs) @ map (code_id n) [0..<n])" proof - let ?xs = "map (λi. Cn (Suc m) (r_code_constn n) [Id (Suc m) i]) [0..<Suc m]" let ?ys = "map (λi. r_constn m (code_id n i)) [0..<n]" have len_xs: "length ?xs = Suc m" by simp have map_xs: "map (λg. eval g (p # cs)) ?xs = map Some (map (code_constn n) (p # cs))" proof (intro nth_equalityI) show len: "length (map (λg. eval g (p # cs)) ?xs) = length (map Some (map (code_constn n) (p # cs)))" by (simp add: assms(2)) have "map (λg. eval g (p # cs)) ?xs ! i = map Some (map (code_constn n) (p # cs)) ! i" if "i < Suc m" for i proof - have "map (λg. eval g (p # cs)) ?xs ! i = (λg. eval g (p # cs)) (?xs ! i)" using len_xs that by (metis nth_map) also have "... = eval (Cn (Suc m) (r_code_constn n) [Id (Suc m) i]) (p # cs)" using that len_xs by (metis (no_types, lifting) add.left_neutral length_map nth_map nth_upt) also have "... = eval (r_code_constn n) [the (eval (Id (Suc m) i) (p # cs))]" using r_code_constn_prim assms(2) that by simp also have "... = eval (r_code_constn n) [(p # cs) ! i]" using len that by simp finally have "map (λg. eval g (p # cs)) ?xs ! i ↓= code_constn n ((p # cs) ! i)" using r_code_constn by simp then show ?thesis using len_xs len that by (metis length_map nth_map) qed moreover have "length (map (λg. eval g (p # cs)) ?xs) = Suc m" by simp ultimately show "⋀i. i < length (map (λg. eval g (p # cs)) ?xs) ⟹ map (λg. eval g (p # cs)) ?xs ! i = map Some (map (code_constn n) (p # cs)) ! i" by simp qed moreover have "map (λg. eval g (p # cs)) ?ys = map Some (map (code_id n) [0..<n])" using assms(2) by (intro nth_equalityI; auto) ultimately have "map (λg. eval g (p # cs)) (?xs @ ?ys) = map Some (map (code_constn n) (p # cs) @ map (code_id n) [0..<n])" by (metis map_append) moreover have "map (λx. the (eval x (p # cs))) (?xs @ ?ys) = map the (map (λx. eval x (p # cs)) (?xs @ ?ys))" by simp ultimately have *: "map (λg. the (eval g (p # cs))) (?xs @ ?ys) = (map (code_constn n) (p # cs) @ map (code_id n) [0..<n])" by simp have "∀i<length ?xs. eval (?xs ! i) (p # cs) = map (λg. eval g (p # cs)) ?xs ! i" by (metis nth_map) then have "∀i<length ?xs. eval (?xs ! i) (p # cs) = map Some (map (code_constn n) (p # cs)) ! i" using map_xs by simp then have "∀i<length ?xs. eval (?xs ! i) (p # cs) ↓" using assms map_xs by (metis length_map nth_map option.simps(3)) then have xs_converg: "∀z∈set ?xs. eval z (p # cs) ↓" by (metis in_set_conv_nth) have "∀i<length ?ys. eval (?ys ! i) (p # cs) = map (λx. eval x (p # cs)) ?ys ! i" by simp then have "∀i<length ?ys. eval (?ys ! i) (p # cs) = map Some (map (code_id n) [0..<n]) ! i" using assms(2) by simp then have "∀i<length ?ys. eval (?ys ! i) (p # cs) ↓" by simp then have "∀z∈set (?xs @ ?ys). eval z (p # cs) ↓" using xs_converg by auto moreover have "recfn (length (p # cs)) (Cn (Suc m) (r_list_encode (m + n)) (?xs @ ?ys))" using assms r_code_constn_prim by auto ultimately have "eval (r_smn_aux n m) (p # cs) = eval (r_list_encode (m + n)) (map (λg. the (eval g (p # cs))) (?xs @ ?ys))" unfolding r_smn_aux_def using assms by simp then have "eval (r_smn_aux n m) (p # cs) = eval (r_list_encode (m + n)) (map (code_constn n) (p # cs) @ map (code_id n) [0..<n])" using * by metis moreover have "length (?xs @ ?ys) = Suc (m + n)" by simp ultimately show ?thesis using r_list_encode * assms(1) by (metis (no_types, lifting) length_map) qed text ‹For all $m, n > 0$, the @{typ recf} corresponding to $s^m_n$ is given by the next function.› definition r_smn :: "nat ⇒ nat ⇒ recf" where "r_smn n m ≡ Cn (Suc m) r_prod_encode [r_constn m 3, Cn (Suc m) r_prod_encode [r_constn m n, Cn (Suc m) r_prod_encode [r_constn m (encode (r_universal (n + m))), r_smn_aux n m]]]" lemma r_smn_prim [simp]: "n > 0 ⟹ prim_recfn (Suc m) (r_smn n m)" by (simp_all add: r_smn_def r_smn_aux_prim) lemma r_smn: assumes "n > 0" and "length cs = m" shows "eval (r_smn n m) (p # cs) ↓= smn n p cs" using assms r_smn_def r_smn_aux smn_def r_smn_aux_prim by simp lemma map_eval_Some_the: assumes "map (λg. eval g xs) gs = map Some ys" shows "map (λg. the (eval g xs)) gs = ys" using assms by (metis (no_types, lifting) length_map nth_equalityI nth_map option.sel) text ‹The essential part of the $s$-$m$-$n$ theorem: For all $m, n > 0$ the function $s^m_n$ satisfies \[ \varphi_p^{(m + n)}(c_1, \dots,c_m, x_1, \dots, x_n) = \varphi_{s^m_n(p, c_1, \dots,c_m)}^{(n)}(x_1, \dots, x_n) \] for all $p, c_i, x_j$.› lemma smn_lemma: assumes "n > 0" and len_cs: "length cs = m" and len_xs: "length xs = n" shows "eval (r_universal (m + n)) (p # cs @ xs) = eval (r_universal n) ((the (eval (r_smn n m) (p # cs))) # xs)" proof - let ?s = "r_smn n m" let ?f = "Cn n (r_universal (n + length cs)) (r_constn (n - 1) p # map (r_constn (n - 1)) cs @ (map (Id n) [0..<n]))" have "eval ?s (p # cs) ↓= smn n p cs" using assms r_smn by simp then have eval_s: "eval ?s (p # cs) ↓= encode ?f" by (simp add: assms(1) smn) have "recfn n ?f" using len_cs assms by auto then have *: "eval (r_universal n) ((encode ?f) # xs) = eval ?f xs" using r_universal[of ?f n, OF _ len_xs] by simp let ?gs = "r_constn (n - 1) p # map (r_constn (n - 1)) cs @ map (Id n) [0..<n]" have "∀g∈set ?gs. eval g xs ↓" using len_cs len_xs assms by auto then have "eval ?f xs = eval (r_universal (n + length cs)) (map (λg. the (eval g xs)) ?gs)" using len_cs len_xs assms ‹recfn n ?f› by simp then have "eval ?f xs = eval (r_universal (m + n)) (map (λg. the (eval g xs)) ?gs)" by (simp add: len_cs add.commute) then have "eval (r_universal n) ((the (eval ?s (p # cs))) # xs) = eval (r_universal (m + n)) (map (λg. the (eval g xs)) ?gs)" using eval_s * by simp moreover have "map (λg. the (eval g xs)) ?gs = p # cs @ xs" proof (intro nth_equalityI) show "length (map (λg. the (eval g xs)) ?gs) = length (p # cs @ xs)" by (simp add: len_xs) have len: "length (map (λg. the (eval g xs)) ?gs) = Suc (m + n)" by (simp add: len_cs) moreover have "map (λg. the (eval g xs)) ?gs ! i = (p # cs @ xs) ! i" if "i < Suc (m + n)" for i proof - from that consider "i = 0" | "i > 0 ∧ i < Suc m" | "Suc m ≤ i ∧ i < Suc (m + n)" using not_le_imp_less by auto then show ?thesis proof (cases) case 1 then show ?thesis using assms(1) len_xs by simp next case 2 then have "?gs ! i = (map (r_constn (n - 1)) cs) ! (i - 1)" using len_cs by (metis One_nat_def Suc_less_eq Suc_pred length_map less_numeral_extra(3) nth_Cons' nth_append) then have "map (λg. the (eval g xs)) ?gs ! i = (λg. the (eval g xs)) ((map (r_constn (n - 1)) cs) ! (i - 1))" using len by (metis length_map nth_map that) also have "... = the (eval ((r_constn (n - 1) (cs ! (i - 1)))) xs)" using 2 len_cs by auto also have "... = cs ! (i - 1)" using r_constn len_xs assms(1) by simp also have "... = (p # cs @ xs) ! i" using 2 len_cs by (metis diff_Suc_1 less_Suc_eq_0_disj less_numeral_extra(3) nth_Cons' nth_append) finally show ?thesis . next case 3 then have "?gs ! i = (map (Id n) [0..<n]) ! (i - Suc m)" using len_cs by (simp; metis (no_types, lifting) One_nat_def Suc_less_eq add_leE plus_1_eq_Suc diff_diff_left length_map not_le nth_append ordered_cancel_comm_monoid_diff_class.add_diff_inverse) then have "map (λg. the (eval g xs)) ?gs ! i = (λg. the (eval g xs)) ((map (Id n) [0..<n]) ! (i - Suc m))" using len by (metis length_map nth_map that) also have "... = the (eval ((Id n (i - Suc m))) xs)" using 3 len_cs by auto also have "... = xs ! (i - Suc m)" using len_xs 3 by auto also have "... = (p # cs @ xs) ! i" using len_cs len_xs 3 by (metis diff_Suc_1 diff_diff_left less_Suc_eq_0_disj not_le nth_Cons' nth_append plus_1_eq_Suc) finally show ?thesis . qed qed ultimately show "map (λg. the (eval g xs)) ?gs ! i = (p # cs @ xs) ! i" if "i < length (map (λg. the (eval g xs)) ?gs)" for i using that by simp qed ultimately show ?thesis by simp qed theorem smn_theorem: assumes "n > 0" shows "∃s. prim_recfn (Suc m) s ∧ (∀p cs xs. length cs = m ∧ length xs = n ⟶ eval (r_universal (m + n)) (p # cs @ xs) = eval (r_universal n) ((the (eval s (p # cs))) # xs))" using smn_lemma exI[of _ "r_smn n m"] assms by simp text ‹For every numbering, that is, binary partial recursive function, $\psi$ there is a total recursive function $c$ that translates $\psi$-indices into $\varphi$-indices.› lemma numbering_translation: assumes "recfn 2 psi" obtains c where "recfn 1 c" "total c" "∀i x. eval psi [i, x] = eval r_phi [the (eval c [i]), x]" proof - let ?p = "encode psi" define c where "c = Cn 1 (r_smn 1 1) [r_const ?p, Id 1 0]" then have "prim_recfn 1 c" by simp moreover from this have "total c" by auto moreover have "eval r_phi [the (eval c [i]), x] = eval psi [i, x]" for i x proof - have "eval c [i] = eval (r_smn 1 1) [?p, i]" using c_def by simp then have "eval (r_universal 1) [the (eval c [i]), x] = eval (r_universal 1) [the (eval (r_smn 1 1) [?p, i]), x]" by simp also have "... = eval (r_universal (1 + 1)) (?p # [i] @ [x])" using smn_lemma[of 1 "[i]" 1 "[x]" ?p] by simp also have "... = eval (r_universal 2) [?p, i, x]" by (metis append_eq_Cons_conv nat_1_add_1) also have "... = eval psi [i, x]" using r_universal[OF assms, of "[i, x]"] by simp finally have "eval (r_universal 1) [the (eval c [i]), x] = eval psi [i, x]" . then show ?thesis using r_phi_def by simp qed ultimately show ?thesis using that by auto qed section ‹Fixed-point theorems› text ‹Fixed-point theorems (also known as recursion theorems) come in many shapes. We prove the minimum we need for Chapter~\ref{c:iirf}.› subsection ‹Rogers's fixed-point theorem› text ‹In this section we prove a theorem that Rogers~\<^cite>‹"Rogers87"› credits to Kleene, but admits that it is a special case and not the original formulation. We follow Wikipedia~\<^cite>‹"wiki-krt"› and call it the Rogers's fixed-point theorem.› lemma s11_inj: "inj (λx. smn 1 p [x])" proof fix x⇩_{1}x⇩_{2}:: nat assume "smn 1 p [x⇩_{1}] = smn 1 p [x⇩_{2}]" then have "list_encode [code_constn 1 p, code_constn 1 x⇩_{1}, code_id 1 0] = list_encode [code_constn 1 p, code_constn 1 x⇩_{2}, code_id 1 0]" using smn_def by (simp add: prod_encode_eq) then have "[code_constn 1 p, code_constn 1 x⇩_{1}, code_id 1 0] = [code_constn 1 p, code_constn 1 x⇩_{2}, code_id 1 0]" using list_decode_encode by metis then have "code_constn 1 x⇩_{1}= code_constn 1 x⇩_{2}" by simp then show "x⇩_{1}= x⇩_{2}" using code_const1 code_constn code_constn_def encode_injective r_constn by (metis One_nat_def length_Cons list.size(3) option.simps(1)) qed definition "r_univuniv ≡ Cn 2 r_phi [Cn 2 r_phi [Id 2 0, Id 2 0], Id 2 1]" lemma r_univuniv_recfn: "recfn 2 r_univuniv" by (simp add: r_univuniv_def) lemma r_univuniv_converg: assumes "eval r_phi [x, x] ↓" shows "eval r_univuniv [x, y] = eval r_phi [the (eval r_phi [x, x]), y]" unfolding r_univuniv_def using assms r_univuniv_recfn r_phi_recfn by simp text ‹Strictly speaking this is a generalization of Rogers's theorem in that it shows the existence of infinitely many fixed-points. In conventional terms it says that for every total recursive $f$ and $k \in \mathbb{N}$ there is an $n \geq k$ with $\varphi_n = \varphi_{f(n)}$.› theorem rogers_fixed_point_theorem: fixes k :: nat assumes "recfn 1 f" and "total f" shows "∃n≥k. ∀x. eval r_phi [n, x] = eval r_phi [the (eval f [n]), x]" proof - let ?p = "encode r_univuniv" define h where "h = Cn 1 (r_smn 1 1) [r_const ?p, Id 1 0]" then have "prim_recfn 1 h" by simp then have "total h" by blast have "eval h [x] = eval (Cn 1 (r_smn 1 1) [r_const ?p, Id 1 0]) [x]" for x unfolding h_def by simp then have h: "the (eval h [x]) = smn 1 ?p [x]" for x by (simp add: r_smn) have "eval r_phi [the (eval h [x]), y] = eval r_univuniv [x, y]" for x y proof - have "eval r_phi [the (eval h [x]), y] = eval r_phi [smn 1 ?p [x], y]" using h by simp also have "... = eval r_phi [the (eval (r_smn 1 1) [?p, x]), y]" by (simp add: r_smn) also have "... = eval (r_universal 2) [?p, x, y]" using r_phi_def smn_lemma[of 1 "[x]" 1 "[y]" ?p] by (metis Cons_eq_append_conv One_nat_def Suc_1 length_Cons less_numeral_extra(1) list.size(3) plus_1_eq_Suc) finally show "eval r_phi [the (eval h [x]), y] = eval r_univuniv [x, y]" using r_universal r_univuniv_recfn by simp qed then have *: "eval r_phi [the (eval h [x]), y] = eval r_phi [the (eval r_phi [x, x]), y]" if "eval r_phi [x, x] ↓" for x y using r_univuniv_converg that by simp let ?fh = "Cn 1 f [h]" have "recfn 1 ?fh" using ‹prim_recfn 1 h› assms by simp then have "infinite {r. recfn 1 r ∧ r ≃ ?fh}" using exteq_infinite[of ?fh 1] by simp then have "infinite (encode ` {r. recfn 1 r ∧ r ≃ ?fh})" (is "infinite ?E") using encode_injective by (meson finite_imageD inj_onI) then have "infinite ((λx. smn 1 ?p [x]) ` ?E)" using s11_inj[of ?p] by (simp add: finite_image_iff inj_on_subset) moreover have "(λx. smn 1 ?p [x]) ` ?E = {smn 1 ?p [encode r] |r. recfn 1 r ∧ r ≃ ?fh}" by auto ultimately have "infinite {smn 1 ?p [encode r] |r. recfn 1 r ∧ r ≃ ?fh}" by simp then obtain n where "n ≥ k" "n ∈ {smn 1 ?p [encode r] |r. recfn 1 r ∧ r ≃ ?fh}" by (meson finite_nat_set_iff_bounded_le le_cases) then obtain r where r: "recfn 1 r" "n = smn 1 ?p [encode r]" "recfn 1 r ∧ r ≃ ?fh" by auto then have eval_r: "eval r [encode r] = eval ?fh [encode r]" by (simp add: exteq_def) then have eval_r': "eval r [encode r] = eval f [the (eval h [encode r])]" using assms ‹total h› ‹prim_recfn 1 h› by simp then have "eval r [encode r] ↓" using ‹prim_recfn 1 h› assms(1,2) by simp then have "eval r_phi [encode r, encode r] ↓" by (simp add: ‹recfn 1 r› r_phi) then have "eval r_phi [the (eval h [encode r]), y] = eval r_phi [(the (eval r_phi [encode r, encode r])), y]" for y using * by simp then have "eval r_phi [the (eval h [encode r]), y] = eval r_phi [(the (eval r [encode r])), y]" for y by (simp add: ‹recfn 1 r› r_phi) moreover have "n = the (eval h [encode r])" by (simp add: h r(2)) ultimately have "eval r_phi [n, y] = eval r_phi [the (eval r [encode r]), y]" for y by simp then have "eval r_phi [n, y] = eval r_phi [the (eval ?fh [encode r]), y]" for y using r by (simp add: eval_r) moreover have "eval ?fh [encode r] = eval f [n]" using eval_r eval_r' ‹n = the (eval h [encode r])› by auto ultimately have "eval r_phi [n, y] = eval r_phi [the (eval f [n]), y]" for y by simp with ‹n ≥ k› show ?thesis by auto qed subsection ‹Kleene's fixed-point theorem› text ‹The next theorem is what Rogers~\<^cite>‹‹p.~214› in "Rogers87"› calls Kleene's version of what we call Rogers's fixed-point theorem. More precisely this would be Kleene's \emph{second} fixed-point theorem, but since we do not cover the first one, we leave out the number.› theorem kleene_fixed_point_theorem: fixes k :: nat assumes "recfn 2 psi" shows "∃n≥k. ∀x. eval r_phi [n, x] = eval psi [n, x]" proof - from numbering_translation[OF assms] obtain c where c: "recfn 1 c" "total c" "∀i x. eval psi [i, x] = eval r_phi [the (eval c [i]), x]" by auto then obtain n where "n ≥ k" and "∀x. eval r_phi [n, x] = eval r_phi [the (eval c [n]), x]" using rogers_fixed_point_theorem by blast with c(3) have "∀x. eval r_phi [n, x] = eval psi [n, x]" by simp with ‹n ≥ k› show ?thesis by auto qed text ‹Kleene's fixed-point theorem can be generalized to arbitrary arities. But we need to generalize it only to binary functions in order to show Smullyan's double fixed-point theorem in Section~\ref{s:smullyan}.› definition "r_univuniv2 ≡ Cn 3 r_phi [Cn 3 (r_universal 2) [Id 3 0, Id 3 0, Id 3 1], Id 3 2]" lemma r_univuniv2_recfn: "recfn 3 r_univuniv2" by (simp add: r_univuniv2_def) lemma r_univuniv2_converg: assumes "eval (r_universal 2) [u, u, x] ↓" shows "eval r_univuniv2 [u, x, y] = eval r_phi [the (eval (r_universal 2) [u, u, x]), y]" unfolding r_univuniv2_def using assms r_univuniv2_recfn by simp theorem kleene_fixed_point_theorem_2: assumes "recfn 2 f" and "total f" shows "∃n. recfn 1 n ∧ total n ∧ (∀x y. eval r_phi [(the (eval n [x])), y] = eval r_phi [(the (eval f [the (eval n [x]), x])), y])" proof - let ?p = "encode r_univuniv2" let ?s = "r_smn 1 2" define h where "h = Cn 2 ?s [r_dummy 1 (r_const ?p), Id 2 0, Id 2 1]" then have [simp]: "prim_recfn 2 h" by simp { fix u x y have "eval h [u, x] = eval (Cn 2 ?s [r_dummy 1 (r_const ?p), Id 2 0, Id 2 1]) [u, x]" using h_def by simp then have "the (eval h [u, x]) = smn 1 ?p [u, x]" by (simp add: r_smn) then have "eval r_phi [the (eval h [u, x]), y] = eval r_phi [smn 1 ?p [u, x], y]" by simp also have "... = eval r_phi [encode (Cn 1 (r_universal 3) (r_constn 0 ?p # r_constn 0 u # r_constn 0 x # [Id 1 0])), y]" using smn[of 1 ?p "[u, x]"] by (simp add: numeral_3_eq_3) also have "... = eval r_phi [encode (Cn 1 (r_universal 3) (r_const ?p # r_const u # r_const x # [Id 1 0])), y]" (is "_ = eval r_phi [encode ?f, y]") by (simp add: r_constn_def) also have "... = eval ?f [y]" using r_phi'[of ?f] by auto also have "... = eval (r_universal 3) [?p, u, x, y]" using r_univuniv2_recfn r_universal r_phi by auto also have "... = eval r_univuniv2 [u, x, y]" using r_universal by (simp add: r_universal r_univuniv2_recfn) finally have "eval r_phi [the (eval h [u, x]), y] = eval r_univuniv2 [u, x, y]" . } then have *: "eval r_phi [the (eval h [u, x]), y] = eval r_phi [the (eval (r_universal 2) [u, u, x]), y]" if "eval (r_universal 2) [u, u, x] ↓" for u x y using r_univuniv2_converg that by simp let ?fh = "Cn 2 f [h, Id 2 1]" let ?e = "encode ?fh" have "recfn 2 ?fh" using assms by simp have "total h" by auto then have "total ?fh" using assms Cn_total totalI2[of ?fh] by fastforce let ?n = "Cn 1 h [r_const ?e, Id 1 0]" have "recfn 1 ?n" using assms by simp moreover have "total ?n" using ‹total h› totalI1[of ?n] by simp moreover { fix x y have "eval r_phi [(the (eval ?n [x])), y] = eval r_phi [(the (eval h [?e, x])), y]" by simp also have "... = eval r_phi [the (eval (r_universal 2) [?e, ?e, x]), y]" using * r_universal[of _ 2] totalE[of ?fh 2] ‹total ?fh› ‹recfn 2 ?fh› by (metis length_Cons list.size(3) numeral_2_eq_2) also have "... = eval r_phi [the (eval f [the (eval h [?e, x]), x]), y]" proof - have "eval (r_universal 2) [?e, ?e, x] ↓" using totalE[OF ‹total ?fh›] ‹recfn 2 ?fh› r_universal by (metis length_Cons list.size(3) numeral_2_eq_2) moreover have "eval (r_universal 2) [?e, ?e, x] = eval ?fh [?e, x]" by (metis ‹recfn 2 ?fh› length_Cons list.size(3) numeral_2_eq_2 r_universal) then show ?thesis using assms ‹total h› by simp qed also have "... = eval r_phi [(the (eval f [the (eval ?n [x]), x])), y]" by simp finally have "eval r_phi [(the (eval ?n [x])), y] = eval r_phi [(the (eval f [the (eval ?n [x]), x])), y]" . } ultimately show ?thesis by blast qed subsection ‹Smullyan's double fixed-point theorem\label{s:smullyan}› theorem smullyan_double_fixed_point_theorem: assumes "recfn 2 g" and "total g" and "recfn 2 h" and "total h" shows "∃m n. (∀x. eval r_phi [m, x] = eval r_phi [the (eval g [m, n]), x]) ∧ (∀x. eval r_phi [n, x] = eval r_phi [the (eval h [m, n]), x])" proof - obtain m where "recfn 1 m" and "total m" and m: "∀x y. eval r_phi [the (eval m [x]), y] = eval r_phi [the (eval g [the (eval m [x]), x]), y]" using kleene_fixed_point_theorem_2[of g] assms(1,2) by auto define k where "k = Cn 1 h [m, Id 1 0]" then have "recfn 1 k" using ‹recfn 1 m› assms(3) by simp have "total (Id 1 0)" by (simp add: Mn_free_imp_total) then have "total k" using ‹total m› assms(4) Cn_total k_def ‹recfn 1 k› by simp obtain n where n: "∀x. eval r_phi [n, x] = eval r_phi [the (eval k [n]), x]" using rogers_fixed_point_theorem[of k] ‹recfn 1 k› ‹total k› by blast obtain mm where mm: "eval m [n] ↓= mm" using ‹total m› ‹recfn 1 m› by fastforce then have "∀x. eval r_phi [mm, x] = eval r_phi [the (eval g [mm, n]), x]" by (metis m option.sel) moreover have "∀x. eval r_phi [n, x] = eval r_phi [the (eval h [mm, n]), x]" using k_def assms(3) ‹total m› ‹recfn 1 m› mm n by simp ultimately show ?thesis by blast qed section ‹Decidable and recursively enumerable sets\label{s:decidable}› text ‹We defined @{term decidable} already back in Section~\ref{s:halting}: @{thm[display] decidable_def}› text ‹The next theorem is adapted from @{thm[source] halting_problem_undecidable}.› theorem halting_problem_phi_undecidable: "¬ decidable {x. eval r_phi [x, x] ↓}" (is "¬ decidable ?K") proof assume "decidable ?K" then obtain f where "recfn 1 f" and f: "∀x. eval f [x] ↓= (if x ∈ ?K then 1 else 0)" using decidable_def by auto define g where "g ≡ Cn 1 r_ifeq_else_diverg [f, Z, Z]" then have "recfn 1 g" using ‹recfn 1 f› r_ifeq_else_diverg_recfn by simp then obtain i where i: "eval r_phi [i, x] = eval g [x]" for x using r_phi' by auto from g_def have "eval g [x] = (if x ∉ ?K then Some 0 else None)" for x using r_ifeq_else_diverg_recfn ‹recfn 1 f› f by simp then have "eval g [i] ↓ ⟷ i ∉ ?K" by simp also have "... ⟷ eval r_phi [i, i] ↑" by simp also have "... ⟷ eval g [i] ↑" using i by simp finally have "eval g [i] ↓ ⟷ eval g [i] ↑" . then show False by auto qed lemma decidable_complement: "decidable X ⟹ decidable (- X)" proof - assume "decidable X" then obtain f where f: "recfn 1 f" "∀x. eval f [x] ↓= (if x ∈ X then 1 else 0)" using decidable_def by auto define g where "g = Cn 1 r_not [f]" then have "recfn 1 g" by (simp add: f(1)) moreover have "eval g [x] ↓= (if x ∈ X then 0 else 1)" for x by (simp add: g_def f) ultimately show ?thesis using decidable_def by auto qed text ‹Finite sets are decidable.› fun r_contains :: "nat list ⇒ recf" where "r_contains [] = Z" | "r_contains (x # xs) = Cn 1 r_ifeq [Id 1 0, r_const x, r_const 1, r_contains xs]" lemma r_contains_prim: "prim_recfn 1 (r_contains xs)" by (induction xs) auto lemma r_contains: "eval (r_contains xs) [x] ↓= (if x ∈ set xs then 1 else 0)" proof (induction xs arbitrary: x) case Nil then show ?case by simp next case (Cons a xs) have "eval (r_contains (a # xs)) [x] = eval r_ifeq [x, a, 1, the (eval (r_contains xs) [x])]" using r_contains_prim prim_recfn_total by simp also have "... ↓= (if x = a then 1 else if x ∈ set xs then 1 else 0)" using Cons.IH by simp also have "... ↓= (if x = a ∨ x ∈ set xs then 1 else 0)" by simp finally show ?case by simp qed lemma finite_set_decidable: "finite X ⟹ decidable X" proof - fix X :: "nat set" assume "finite X" then obtain xs where "X = set xs" using finite_list by auto then have "∀x. eval (r_contains xs) [x] ↓= (if x ∈ X then 1 else 0)" using r_contains by simp then show "decidable X" using decidable_def r_contains_prim by blast qed definition semidecidable :: "nat set ⇒ bool" where "semidecidable X ≡ (∃f. recfn 1 f ∧ (∀x. eval f [x] = (if x ∈ X then Some 1 else None)))" text ‹The semidecidable sets are the domains of partial recursive functions.› lemma semidecidable_iff_domain: "semidecidable X ⟷ (∃f. recfn 1 f ∧ (∀x. eval f [x] ↓ ⟷ x ∈ X))" proof show "semidecidable X ⟹ ∃f. recfn 1 f ∧ (∀x. (eval f [x] ↓) = (x ∈ X))" using semidecidable_def by (metis option.distinct(1)) show "semidecidable X" if "∃f. recfn 1 f ∧ (∀x. (eval f [x] ↓) = (x ∈ X))" for X proof - from that obtain f where f: "recfn 1 f" "∀x. (eval f [x] ↓) = (x ∈ X)" by auto let ?g = "Cn 1 (r_const 1) [f]" have "recfn 1 ?g" using f(1) by simp moreover have "∀x. eval ?g [x] = (if x ∈ X then Some 1 else None)" using f by simp ultimately show "semidecidable X" using semidecidable_def by blast qed qed lemma decidable_imp_semidecidable: "decidable X ⟹ semidecidable X" proof - assume "decidable X" then obtain f where f: "recfn 1 f" "∀x. eval f [x] ↓= (if x ∈ X then 1 else 0)" using decidable_def by auto define g where "g = Cn 1 r_ifeq_else_diverg [f, r_const 1, r_const 1]" then have "recfn 1 g" by (simp add: f(1)) have "eval g [x] = eval r_ifeq_else_diverg [if x ∈ X then 1 else 0, 1, 1]" for x by (simp add: g_def f) then have "⋀x. x ∈ X ⟹ eval g [x] ↓= 1" and "⋀x. x ∉ X ⟹ eval g [x] ↑" by simp_all then show ?thesis using ‹recfn 1 g› semidecidable_def by auto qed text ‹A set is recursively enumerable if it is empty or the image of a total recursive function.› definition recursively_enumerable :: "nat set ⇒ bool" where "recursively_enumerable X ≡ X = {} ∨ (∃f. recfn 1 f ∧ total f ∧ X = {the (eval f [x]) |x. x ∈ UNIV})" theorem recursively_enumerable_iff_semidecidable: "recursively_enumerable X ⟷ semidecidable X" proof show "semidecidable X" if "recursively_enumerable X" for X proof (cases) assume "X = {}" then show ?thesis using finite_set_decidable decidable_imp_semidecidable recursively_enumerable_def semidecidable_def by blast next assume "X ≠ {}" with that obtain f where f: "recfn 1 f" "total f" "X = {the (eval f [x]) |x. x ∈ UNIV}" using recursively_enumerable_def by blast define h where "h = Cn 2 r_eq [Cn 2 f [Id 2 0], Id 2 1]" then have "recfn 2 h" using f(1) by simp from h_def have h: "eval h [x, y] ↓= 0 ⟷ the (eval f [x]) = y" for x y using f(1,2) by simp from h_def ‹recfn 2 h› totalI2 f(2) have "total h" by simp define g where "g = Mn 1 h" then have "recfn 1 g" using h_def f(1) by simp then have "eval g [y] = (if (∃x. eval h [x, y] ↓= 0 ∧ (∀x'<x. eval h [x', y] ↓)) then Some (LEAST x. eval h [x, y] ↓= 0) else None)" for y using g_def ‹total h› f(2) by simp then have "eval g [y] = (if ∃x. eval h [x, y] ↓= 0 then Some (LEAST x. eval h [x, y] ↓= 0) else None)" for y using ‹total h› ‹recfn 2 h› by simp then have "eval g [y] ↓ ⟷ (∃x. eval h [x, y] ↓= 0)" for y by simp with h have "eval g [y] ↓ ⟷ (∃x. the (eval f [x]) = y)" for y by simp with f(3) have "eval g [y] ↓ ⟷ y ∈ X" for y by auto with ‹recfn 1 g› semidecidable_iff_domain show ?thesis by auto qed show "recursively_enumerable X" if "semidecidable X" for X proof (cases) assume "X = {}" then show ?thesis using recursively_enumerable_def by simp next assume "X ≠ {}" then obtain x⇩_{0}where "x⇩_{0}∈ X" by auto from that semidecidable_iff_domain obtain f where f: "recfn 1 f" "∀x. eval f [x] ↓ ⟷ x ∈ X" by auto let ?i = "encode f" have i: "⋀x. eval f [x] = eval r_phi [?i, x]" using r_phi' f(1) by simp with ‹x⇩_{0}∈ X› f(2) have "eval r_phi [?i, x⇩_{0}] ↓" by simp then obtain g where g: "recfn 1 g" "total g" "∀x. eval r_phi [?i, x] ↓ = (∃y. eval g [y] ↓= x)" using f(1) nonempty_domain_enumerable by blast with f(2) i have "∀x. x ∈ X = (∃y. eval g [y] ↓= x)" by simp then have "∀x. x ∈ X = (∃y. the (eval g [y]) = x)" using totalE[OF g(2) g(1)] by (metis One_nat_def length_Cons list.size(3) option.collapse option.sel) then have "X = {the (eval g [y]) |y. y ∈ UNIV}" by auto with g(1,2) show ?thesis using recursively_enumerable_def by auto qed qed text ‹The next goal is to show that a set is decidable iff. it and its complement are semidecidable. For this we use the concurrent evaluation function.› lemma semidecidable_decidable: assumes "semidecidable X" and "semidecidable (- X)" shows "decidable X" proof - obtain f where f: "recfn 1 f ∧ (∀x. eval f [x] ↓ ⟷ x ∈ X)" using assms(1) semidecidable_iff_domain by auto let ?i = "encode f" obtain g where g: "recfn 1 g ∧ (∀x. eval g [x] ↓ ⟷ x ∈ (- X))" using assms(2) semidecidable_iff_domain by auto let ?j = "encode g" define d where "d = Cn 1 r_pdec1 [Cn 1 r_parallel [r_const ?j, r_const ?i, Id 1 0]]" then have "recfn 1 d" by (simp add: d_def) have *: "⋀x. eval r_phi [?i, x] = eval f [x]" "⋀x. eval r_phi [?j, x] = eval g [x]" using f g r_phi' by simp_all have "eval d [x] ↓= 1" if "x ∈ X" for x proof - have "eval f [x] ↓" using f that by simp moreover have "eval g [x] ↑" using g that by blast ultimately have "eval r_parallel [?j, ?i, x] ↓= prod_encode (1, the (eval f [x]))" using * r_parallel(3) by simp with d_def show ?thesis by simp qed moreover have "eval d [x] ↓= 0" if "x ∉ X" for x proof - have "eval g [x] ↓" using g that by simp moreover have "eval f [x] ↑" using f that by blast ultimately have "eval r_parallel [?j, ?i, x] ↓= prod_encode (0, the (eval g [x]))" using * r_parallel(2) by blast with d_def show ?thesis by simp qed ultimately show ?thesis using decidable_def ‹recfn 1 d› by auto qed theorem decidable_iff_semidecidable_complement: "decidable X ⟷ semidecidable X ∧ semidecidable (- X)" using semidecidable_decidable decidable_imp_semidecidable decidable_complement by blast section ‹Rice's theorem› definition index_set :: "nat set ⇒ bool" where "index_set I ≡ ∀i j. i ∈ I ∧ (∀x. eval r_phi [i, x] = eval r_phi [j, x]) ⟶ j ∈ I" lemma index_set_closed_in: assumes "index_set I" and "i ∈ I" and "∀x. eval r_phi [i, x] = eval r_phi [j, x]" shows "j ∈ I" using index_set_def assms by simp lemma index_set_closed_not_in: assumes "index_set I" and "i ∉ I" and "∀x. eval r_phi [i, x] = eval r_phi [j, x]" shows "j ∉ I" using index_set_def assms by metis theorem rice_theorem: assumes "index_set I" and "I ≠ UNIV" and "I ≠ {}" shows "¬ decidable I" proof assume "decidable I" then obtain d where d: "recfn 1 d" "∀i. eval d [i] ↓= (if i ∈ I then 1 else 0)" using decidable_def by auto obtain j⇩_{1}j⇩_{2}where "j⇩_{1}∉ I" and "j⇩_{2}∈ I" using assms(2,3) by auto let ?if = "Cn 2 r_ifz [Cn 2 d [Id 2 0], r_dummy 1 (r_const j⇩_{2}), r_dummy 1 (r_const j⇩_{1})]" define psi where "psi = Cn 2 r_phi [?if, Id 2 1] " then have "recfn 2 psi" by (simp add: d) have "eval ?if [x, y] = Some (if x ∈ I then j⇩_{1}else j⇩_{2})" for x y by (simp add: d) moreover have "eval psi [x, y] = eval (Cn 2 r_phi [?if, Id 2 1]) [x, y]" for x y using psi_def by simp ultimately have psi: "eval psi [x, y] = eval r_phi [if x ∈ I then j⇩_{1}else j⇩_{2}, y]" for x y by (simp add: d) then have in_I: "eval psi [x, y] = eval r_phi [j⇩_{1}, y]" if "x ∈ I" for x y by (simp add: that) have not_in_I: "eval psi [x, y] = eval r_phi [j⇩_{2}, y]" if "x ∉ I" for x y by (simp add: psi that) obtain n where n: "∀x. eval r_phi [n, x] = eval psi [n, x]" using kleene_fixed_point_theorem[OF ‹recfn 2 psi›] by auto show False proof cases assume "n ∈ I" then have "∀x. eval r_phi [n, x] = eval r_phi [j⇩_{1}, x]" using n in_I by simp then have "n ∉ I" using ‹j⇩_{1}∉ I› index_set_closed_not_in[OF assms(1)] by simp with ‹n ∈ I› show False by simp next assume "n ∉ I" then have "∀x. eval r_phi [n, x] = eval r_phi [j⇩_{2}, x]" using n not_in_I by simp then have "n ∈ I" using ‹j⇩_{2}∈ I› index_set_closed_in[OF assms(1)] by simp with ‹n ∉ I› show False by simp qed qed section ‹Partial recursive functions as actual functions\label{s:alternative}› text ‹A well-formed @{typ recf} describes an algorithm. Usually, however, partial recursive functions are considered to be partial functions, that is, right-unique binary relations. This distinction did not matter much until now, because we were mostly concerned with the \emph{existence} of partial recursive functions, which is equivalent to the existence of algorithms. Whenever it did matter, we could use the extensional equivalence @{term "exteq"}. In Chapter~\ref{c:iirf}, however, we will deal with sets of functions and sets of sets of functions. For illustration consider the singleton set containing only the unary zero function. It could be expressed by @{term "{Z}"}, but this would not contain @{term[names_short] "Cn 1 (Id 1 0) [Z]"}, which computes the same function. The alternative representation as @{term "{f. f ≃ Z}"} is not a singleton set. Another alternative would be to identify partial recursive functions with the equivalence classes of @{term "exteq"}. This would work for all arities. But since we will only need unary and binary functions, we can go for the less general but simpler alternative of regarding partial recursive functions as certain functions of types @{typ "nat ⇒ nat option"} and @{typ "nat ⇒ nat ⇒ nat option"}. With this notation we can represent the aforementioned set by @{term "{λ_. Some (0::nat)}"} and express that the function @{term "λ_. Some (0::nat)"} is total recursive. In addition terms get shorter, for instance, @{term "eval r_func [i, x]"} becomes @{term "func i x"}.› subsection ‹The definitions› type_synonym partial1 = "nat ⇒ nat option" type_synonym partial2 = "nat ⇒ nat ⇒ nat option" definition total1 :: "partial1 ⇒ bool" where "total1 f ≡ ∀x. f x ↓" definition total2 :: "partial2 ⇒ bool" where "total2 f ≡ ∀x y. f x y ↓" lemma total1I [intro]: "(⋀x. f x ↓) ⟹ total1 f" using total1_def by simp lemma total2I [intro]: "(⋀x y. f x y ↓) ⟹ total2 f" using total2_def by simp lemma total1E [dest, simp]: "total1 f ⟹ f x ↓" using total1_def by simp lemma total2E [dest, simp]: "total2 f ⟹ f x y ↓" using total2_def by simp definition P1 :: "partial1 set" ("𝒫") where "𝒫 ≡ {λx. eval r [x] |r. recfn 1 r}" definition P2 :: "partial2 set" ("𝒫⇧^{2}") where "𝒫⇧^{2}≡ {λx y. eval r [x, y] |r. recfn 2 r}" definition R1 :: "partial1 set" ("ℛ") where "ℛ ≡ {λx. eval r [x] |r. recfn 1 r ∧ total r}" definition R2 :: "partial2 set" ("ℛ⇧^{2}") where "ℛ⇧^{2}≡ {λx y. eval r [x, y] |r. recfn 2 r ∧ total r}" definition Prim1 :: "partial1 set" where "Prim1 ≡ {λx. eval r [x] |r. prim_recfn 1 r}" definition Prim2 :: "partial2 set" where "Prim2 ≡ {λx y. eval r [x, y] |r. prim_recfn 2 r}" lemma R1_imp_P1 [simp, elim]: "f ∈ ℛ ⟹ f ∈ 𝒫" using R1_def P1_def by auto lemma R2_imp_P2 [simp, elim]: "f ∈ ℛ⇧^{2}⟹ f ∈ 𝒫⇧^{2}" using R2_def P2_def by auto lemma Prim1_imp_R1 [simp, elim]: "f ∈ Prim1 ⟹ f ∈ ℛ" unfolding Prim1_def R1_def by auto lemma Prim2_imp_R2 [simp, elim]: "f ∈ Prim2 ⟹ f ∈ ℛ⇧^{2}" unfolding Prim2_def R2_def by auto lemma P1E [elim]: assumes "f ∈ 𝒫" obtains r where "recfn 1 r" and "∀x. eval r [x] = f x" using assms P1_def by force lemma P2E [elim]: assumes "f ∈ 𝒫⇧^{2}" obtains r where "recfn 2 r" and "∀x y. eval r [x, y] = f x y" using assms P2_def by force lemma P1I [intro]: assumes "recfn 1 r" and "(λx. eval r [x]) = f" shows "f ∈ 𝒫" using assms P1_def by auto lemma P2I [intro]: assumes "recfn 2 r" and "⋀x y. eval r [x, y] = f x y" shows "f ∈ 𝒫⇧^{2}" proof - have "(λx y. eval r [x, y]) = f" using assms(2) by simp then show ?thesis using assms(1) P2_def by auto qed lemma R1I [intro]: assumes "recfn 1 r" and "total r" and "⋀x. eval r [x] = f x" shows "f ∈ ℛ" unfolding R1_def using CollectI[of "λf. ∃r. f = (λx. eval r [x]) ∧ recfn 1 r ∧ total r" f] assms by metis lemma R1E [elim]: assumes "f ∈ ℛ" obtains r where "recfn 1 r" and "total r" and "f = (λx. eval r [x])" using assms R1_def by auto lemma R2I [intro]: assumes "recfn 2 r" and "total r" and "⋀x y. eval r [x, y] = f x y" shows "f ∈ ℛ⇧^{2}" unfolding R2_def using CollectI[of "λf. ∃r. f = (λx y. eval r [x, y]) ∧ recfn 2 r ∧ total r" f] assms by metis lemma R1_SOME: assumes "f ∈ ℛ" and "r = (SOME r'. recfn 1 r' ∧ total r' ∧ f = (λx. eval r' [x]))" (is "r = (SOME r'. ?P r')") shows "recfn 1 r" and "⋀x. eval r [x] ↓" and "⋀x. f x = eval r [x]" and "f = (λx. eval r [x])" proof - obtain r' where "?P r'" using R1E[OF assms(1)] by auto then show "recfn 1 r" "⋀b. eval r [b] ↓" "⋀x. f x = eval r [x]" using someI[of ?P r'] assms(2) totalE[of r] by (auto, metis) then show "f = (λx. eval r [x])" by auto qed lemma R2E [elim]: assumes "f ∈ ℛ⇧^{2}" obtains r where "recfn 2 r" and "total r" and "f = (λx⇩_{1}x⇩_{2}. eval r [x⇩_{1}, x⇩_{2}])" using assms R2_def by auto lemma R1_imp_total1 [simp]: "f ∈ ℛ ⟹ total1 f" using total1I by fastforce lemma R2_imp_total2 [simp]: "f ∈ ℛ⇧^{2}⟹ total2 f" using totalE by fastforce lemma Prim1I [intro]: assumes "prim_recfn 1 r" and "⋀x. f x = eval r [x]" shows "f ∈ Prim1" using assms Prim1_def by blast lemma Prim2I [intro]: assumes "prim_recfn 2 r" and "⋀x y. f x y = eval r [x, y]" shows "f ∈ Prim2" using assms Prim2_def by blast lemma P1_total_imp_R1 [intro]: assumes "f ∈ 𝒫" and "total1 f" shows "f ∈ ℛ" using assms totalI1 by force lemma P2_total_imp_R2 [intro]: assumes "f ∈ 𝒫⇧^{2}" and "total2 f" shows "f ∈ ℛ⇧^{2}" using assms totalI2 by force subsection ‹Some simple properties› text ‹In order to show that a @{typ partial1} or @{typ partial2} function is in @{term "𝒫"}, @{term "𝒫⇧^{2}"}, @{term "ℛ"}, @{term "ℛ⇧^{2}"}, @{term "Prim1"}, or @{term "Prim2"} we will usually have to find a suitable @{typ recf}. But for some simple or frequent cases this section provides shortcuts.› lemma identity_in_R1: "Some ∈ ℛ" proof - have "∀x. eval (Id 1 0) [x] ↓= x" by simp moreover have "recfn 1 (Id 1 0)" by simp moreover have "total (Id 1 0)" by (simp add: totalI1) ultimately show ?thesis by blast qed lemma P2_proj_P1 [simp, elim]: assumes "ψ ∈ 𝒫⇧^{2}" shows "ψ i ∈ 𝒫" proof - from assms obtain u where u: "recfn 2 u" "(λx⇩_{1}x⇩_{2}. eval u [x⇩_{1}, x⇩_{2}]) = ψ" by auto define v where "v ≡ Cn 1 u [r_const i, Id 1 0]" then have "recfn 1 v" "(λx. eval v [x]) = ψ i" using u by auto then show ?thesis by auto qed lemma R2_proj_R1 [simp, elim]: assumes "ψ ∈ ℛ⇧^{2}" shows "ψ i ∈ ℛ" proof - from assms have "ψ ∈ 𝒫⇧^{2}" by simp then have "ψ i ∈ 𝒫" by auto moreover have "total1 (ψ i)" using assms by (simp add: total1I) ultimately show ?thesis by auto qed lemma const_in_Prim1: "(λ_. Some c) ∈ Prim1" proof - define r where "r = r_const c" then have "⋀x. eval r [x] = Some c" by simp moreover have "recfn 1 r" "Mn_free r" using r_def by simp_all ultimately show ?thesis by auto qed lemma concat_P1_P1: assumes "f ∈ 𝒫" and "g ∈ 𝒫" shows "(λx. if g x ↓ ∧ f (the (g x)) ↓ then Some (the (f (the (g x)))) else None) ∈ 𝒫" (is "?h ∈ 𝒫") proof - obtain rf where rf: "recfn 1 rf" "∀x. eval rf [x] = f x" using assms(1) by auto obtain rg where rg: "recfn 1 rg" "∀x. eval rg [x] = g x" using assms(2) by auto let ?rh = "Cn 1 rf [rg]" have "recfn 1 ?rh" using rf(1) rg(1) by simp moreover have "eval ?rh [x] = ?h x" for x using rf rg by simp ultimately show ?thesis by blast qed lemma P1_update_P1: assumes "f ∈ 𝒫" shows "f(x:=z) ∈ 𝒫" proof (cases z) case None define re where "re ≡ Mn 1 (r_constn 1 1)" from assms obtain r where r: "recfn 1 r" "(λu. eval r [u]) = f" by auto define r' where "r' = Cn 1 (r_lifz re r) [Cn 1 r_eq [Id 1 0, r_const x], Id 1 0]" have "recfn 1 r'" using r(1) r'_def re_def by simp then have "eval r' [u] = eval (r_lifz re r) [if u = x then 0 else 1, u]" for u using r'_def by simp with r(1) have "eval r' [u] = (if u = x then None else eval r [u])" for u using re_def re_def by simp with r(2) have "eval r' [u] = (f(x:=None)) u" for u by auto then have "(λu. eval r' [u]) = f(x:=None)" by auto with None ‹recfn 1 r'› show ?thesis by auto next case (Some y) from assms obtain r where r: "recfn 1 r" "(λu. eval r [u])