Theory NP
chapter ‹Time complexity\label{s:TC}›
theory NP
imports Elementary Composing Symbol_Ops
begin
text ‹
In order to formulate the Cook-Levin theorem we need to formalize \SAT{} and
$\NP$-completeness. This chapter is devoted to the latter and hence introduces
the complexity class $\NP$ and the concept of polynomial-time many-one
reduction. Moreover, although not required for the Cook-Levin theorem, it
introduces the class $\mathcal{P}$ and contains a proof of $\mathcal{P}
\subseteq \NP$ (see Section~\ref{s:TC-subseteq}). The chapter concludes with
some easy results about $\mathcal{P}$, $\NP$ and reducibility in
Section~\ref{s:TC-more}.
›
section ‹The time complexity classes DTIME, $\mathcal{P}$, and $\NP$\label{s:TC-NP}›
text ‹
Arora and Barak~\cite[Definitions 1.12, 1.13]{ccama} define
$\mathrm{DTIME}(T(n))$ as the set of all languages that can be decided in time
$c \cdot T(n)$ for some $c > 0$ and $\mathcal{P} =
\bigcup_{c\geq1}\mathrm{DTIME}(n^c)$. However since $0^c = 0$ for $c\geq 1$,
this means that for a language $L$ to be in $\mathcal{P}$, the Turing machine
deciding $L$ must check the empty string in zero steps. For a Turing machine to
halt in zero steps, it must start in the halting state, which limits its
usefulness. Because of this technical issue we define $\mathrm{DTIME}(T(n))$ as
the set of all languages that can be decided with a running time in $O(T(n))$,
which seems a common enough alternative~\cite{lv-aikc,sipser2006,cz-dtime}.
›
text ‹
Languages are sets of strings, and deciding a language means computing its
characteristic function.
›
type_synonym language = "string set"
definition characteristic :: "language ⇒ (string ⇒ string)" where
"characteristic L ≡ (λx. [x ∈ L])"
definition DTIME :: "(nat ⇒ nat) ⇒ language set" where
"DTIME T ≡ {L. ∃k G M T'.
turing_machine k G M ∧
big_oh T' T ∧
computes_in_time k M (characteristic L) T'}"
definition complexity_class_P :: "language set" (‹𝒫›) where
"𝒫 ≡ ⋃c∈{1..}. DTIME (λn. n ^ c)"
text ‹
A language $L$ is in $\NP$ if there is a polynomial $p$ and a polynomial-time
Turing machine, called the \emph{verifier}, such that for all strings
$x\in\bbOI^*$,
\[
x\in L \longleftrightarrow
\exists u\in\bbOI^{p(|x|)}: M(\langle x, u\rangle) = \bbbI.
\]
The string $u$ does not seem to have a name in general, but in case the verifier
outputs $\bbbI$ on input $\langle x, u\rangle$ it is called a
\emph{certificate} for $x$~\cite[Definition~2.1]{ccama}.
›
definition complexity_class_NP :: "language set" (‹𝒩𝒫›) where
"𝒩𝒫 ≡ {L. ∃k G M p T fverify.
turing_machine k G M ∧
polynomial p ∧
big_oh_poly T ∧
computes_in_time k M fverify T ∧
(∀x. x ∈ L ⟷ (∃u. length u = p (length x) ∧ fverify ⟨x, u⟩ = [𝕀]))}"
text ‹
The definition of $\NP$ is the one place where we need an actual polynomial
function, namely $p$, rather than a function that is merely bounded by a
polynomial. This raises the question as to the definition of a polynomial
function. Arora and Barak~\cite{ccama} do not seem to give a definition in the
context of $\NP$ but explicitly state that polynomial functions are mappings
$\nat \to \nat$. Presumably they also have the form $f(n) = \sum_{i=0}^d
a_i\cdot n^i$, as polynomials do. We have filled in the gap in this definition
in Section~\ref{s:tm-basic-bigoh} by letting the coefficients $a_i$ be natural
numbers.
Regardless of whether this is the meaning intended by Arora and Barak, the
choice is justified because with it the verifier-based definition of $\NP$ is
equivalent to the original definition via nondeterministic Turing machines
(NTMs). In the usual equivalence proof (for example, Arora and
Barak~\cite[Theorem~2.6]{ccama}) a verifier TM and an NTM are constructed.
For the one direction, if a language is decided by a polynomial-time NTM then a
verifier TM can be constructed that simulates the NTM on input $x$ by using the
bits in the string $u$ for the nondeterministic choices. The strings $u$ have
the length $p(|x|)$. So for this construction to work, there must be a polynomial
$p$ that bounds the running time of the NTM. Clearly, a polynomial function with
natural coefficients exists with that property.
For the other direction, assume a language has a verifier TM where $p$ is a
polynomial function with natural coefficients. An NTM deciding this language
receives $x$ as input, then ``guesses'' a string $u$ of length $p(|x|)$, and
then runs the verifier on the pair $\langle x, u\rangle$. For this NTM to run in
polynomial time, $p$ must be computable in time polynomial in $|x|$. We have
shown this to be the case in lemma @{thm [source] transforms_tm_polynomialI} in
Section~\ref{s:tm-arithmetic-poly}.
›
text ‹
A language $L_1$ is polynomial-time many-one reducible to a language $L_2$ if
there is a polynomial-time computable function $f_\mathit{reduce}$ such that for all
$x$, $x\in L_1$ iff.\ $f_\mathit{reduce}(x) \in L_2$.
›
definition reducible (infix ‹≤⇩p› 50) where
"L⇩1 ≤⇩p L⇩2 ≡ ∃k G M T freduce.
turing_machine k G M ∧
big_oh_poly T ∧
computes_in_time k M freduce T ∧
(∀x. x ∈ L⇩1 ⟷ freduce x ∈ L⇩2)"
abbreviation NP_hard :: "language ⇒ bool" where
"NP_hard L ≡ ∀L'∈𝒩𝒫. L' ≤⇩p L"
definition NP_complete :: "language ⇒ bool" where
"NP_complete L ≡ L ∈ 𝒩𝒫 ∧ NP_hard L"
text ‹
Requiring $c \geq 1$ in the definition of $\mathcal{P}$ is not essential:
›
lemma in_P_iff: "L ∈ 𝒫 ⟷ (∃c. L ∈ DTIME (λn. n ^ c))"
proof
assume "L ∈ 𝒫"
then show "∃c. L ∈ DTIME (λn. n ^ c)"
unfolding complexity_class_P_def using Suc_le_eq by auto
next
assume "∃c. L ∈ DTIME (λn. n ^ c)"
then obtain c where "L ∈ DTIME (λn. n ^ c)"
by auto
then obtain k G M T where M:
"turing_machine k G M"
"big_oh T (λn. n ^ c)"
"computes_in_time k M (characteristic L) T"
using DTIME_def by auto
moreover have "big_oh T (λn. n ^ Suc c)"
proof -
obtain c0 n0 :: nat where c0n0: "∀n>n0. T n ≤ c0 * n ^ c"
using M(2) big_oh_def by auto
have "∀n>n0. T n ≤ c0 * n ^ Suc c"
proof standard+
fix n assume "n0 < n"
then have "n ^ c ≤ n ^ Suc c"
using pow_mono by simp
then show "T n ≤ c0 * n ^ Suc c"
using c0n0 by (metis ‹n0 < n› add.commute le_Suc_ex mult_le_mono2 trans_le_add2)
qed
then show ?thesis
using big_oh_def by auto
qed
ultimately have "∃c>0. L ∈ DTIME (λn. n ^ c)"
using DTIME_def by blast
then show "L ∈ 𝒫"
unfolding complexity_class_P_def by auto
qed
section ‹Restricting verifiers to one-bit output\label{s:np-alt}›
text ‹
The verifier Turing machine in the definition of $\NP$ can output any symbol
sequence. In this section we restrict it to outputting only the symbol sequence
\textbf{1} or \textbf{0}. This is equivalent to the definition because it is
easy to check if a symbol sequence differs from \textbf{1} and if so change it
to \textbf{0}, as we show below.
The advantage of this restriction is that if we can make the TM halt with the
output tape head on cell number~1, the output tape symbol read in the final step
equals the output of the TM. We will exploit this in Chapter~\ref{s:Reducing},
where we show how to reduce any language $L\in\NP$ to \SAT{}.
The next Turing machine checks if the symbol sequence on tape $j$ differs from
the one-symbol sequence \textbf{1} and if so turns it into \textbf{0}. It thus
ensures that the tape contains only one bit symbol.
\null
›
definition tm_make_bit :: "tapeidx ⇒ machine" where
"tm_make_bit j ≡
tm_cr j ;;
IF λrs. rs ! j = 𝟭 THEN
tm_right j ;;
IF λrs. rs ! j = □ THEN
[]
ELSE
tm_set j [𝟬]
ENDIF
ELSE
tm_set j [𝟬]
ENDIF"
lemma tm_make_bit_tm:
assumes "G ≥ 4" and "0 < j" and "j < k"
shows "turing_machine k G (tm_make_bit j)"
unfolding tm_make_bit_def
using assms tm_right_tm tm_set_tm tm_cr_tm Nil_tm turing_machine_branch_turing_machine
by simp
locale turing_machine_make_bit =
fixes j :: tapeidx
begin
definition "tm1 ≡ tm_cr j"
definition "tmT1 ≡ tm_right j"
definition "tmT12 ≡ IF λrs. rs ! j = □ THEN [] ELSE tm_set j [𝟬] ENDIF"
definition "tmT2 ≡ tmT1 ;; tmT12"
definition "tm12 ≡ IF λrs. rs ! j = 𝟭 THEN tmT2 ELSE tm_set j [𝟬] ENDIF"
definition "tm2 ≡ tm1 ;; tm12"
lemma tm2_eq_tm_make_bit: "tm2 ≡ tm_make_bit j"
unfolding tm_make_bit_def tm2_def tm12_def tmT2_def tmT12_def tmT1_def tm1_def by simp
context
fixes tps0 :: "tape list" and zs :: "symbol list"
assumes jk: "j < length tps0"
and zs: "proper_symbols zs"
assumes tps0: "tps0 ::: j = ⌊zs⌋"
begin
lemma clean: "clean_tape (tps0 ! j)"
using zs tps0 contents_clean_tape' by simp
definition "tps1 ≡ tps0[j := (⌊zs⌋, 1)]"
lemma tm1 [transforms_intros]:
assumes "ttt = tps0 :#: j + 2"
shows "transforms tm1 tps0 ttt tps1"
unfolding tm1_def by (tform tps: assms jk clean tps0 tps1_def)
definition "tpsT1 ≡ tps0[j := (⌊zs⌋, 2)]"
lemma tmT1 [transforms_intros]:
assumes "ttt = 1"
shows "transforms tmT1 tps1 ttt tpsT1"
unfolding tmT1_def
proof (tform tps: assms tps1_def jk)
show "tpsT1 = tps1[j := tps1 ! j |+| 1] "
using tps1_def tpsT1_def jk
by (metis Suc_1 fst_conv list_update_overwrite nth_list_update_eq plus_1_eq_Suc snd_conv)
qed
definition "tpsT2 ≡ tps0
[j := if length zs ≤ 1 then (⌊zs⌋, 2) else (⌊[𝟬]⌋, 1)]"
lemma tmT12 [transforms_intros]:
assumes "ttt = 14 + 2 * length zs"
shows "transforms tmT12 tpsT1 ttt tpsT2"
unfolding tmT12_def
proof (tform tps: assms tpsT1_def tps0 jk zs)
show "8 + tpsT1 :#: j + 2 * length zs + Suc (2 * length [𝟬]) + 1 ≤ ttt"
using tpsT1_def jk assms by simp
have "read tpsT1 ! j = ⌊zs⌋ 2"
using tpsT1_def jk tapes_at_read' by (metis fst_conv length_list_update nth_list_update_eq snd_conv)
moreover have "⌊zs⌋ 2 = □ ⟷ length zs ≤ 1"
using zs contents_def
by (metis Suc_1 diff_Suc_1 less_imp_le_nat linorder_le_less_linear not_less_eq_eq zero_neq_numeral)
ultimately have "read tpsT1 ! j = □ ⟷ length zs ≤ 1"
by simp
then show
"read tpsT1 ! j ≠ □ ⟹ tpsT2 = tpsT1[j := (⌊[𝟬]⌋, 1)]"
"read tpsT1 ! j = □ ⟹ tpsT2 = tpsT1"
using tpsT1_def tpsT2_def jk by simp_all
qed
lemma tmT2 [transforms_intros]:
assumes "ttt = 15 + 2 * length zs"
shows "transforms tmT2 tps1 ttt tpsT2"
unfolding tmT2_def by (tform time: assms)
definition "tps2 ≡ tps0
[j := if zs = [𝟭] then (⌊zs⌋, 2) else (⌊[𝟬]⌋, 1)]"
lemma tm12 [transforms_intros]:
assumes "ttt = 17 + 2 * length zs"
shows "transforms tm12 tps1 ttt tps2"
unfolding tm12_def
proof (tform tps: assms tps0 jk zs tps1_def)
have "read tps1 ! j = ⌊zs⌋ 1"
using tps1_def jk tapes_at_read' by (metis fst_conv length_list_update nth_list_update_eq snd_conv)
then have *: "read tps1 ! j = 𝟭 ⟷ ⌊zs⌋ 1 = 𝟭"
by simp
show "read tps1 ! j ≠ 𝟭 ⟹ tps2 = tps1[j := (⌊[𝟬]⌋, 1)]"
using * tps2_def tps1_def by auto
show "tps2 = tpsT2" if "read tps1 ! j = 𝟭"
proof (cases "zs = [𝟭]")
case True
then show ?thesis
using * tps2_def tpsT2_def by simp
next
case False
then have "⌊zs⌋ 1 = 𝟭"
using * that by simp
then have "length zs > 1"
using False contents_def contents_outofbounds
by (metis One_nat_def Suc_length_conv diff_Suc_1 length_0_conv linorder_neqE_nat nth_Cons_0 zero_neq_numeral)
then show ?thesis
using * tps2_def tpsT2_def by auto
qed
show "8 + tps1 :#: j + 2 * length zs + Suc (2 * length [𝟬]) + 1 ≤ ttt"
using tps1_def jk assms by simp
qed
lemma tm2:
assumes "ttt = 19 + 2 * length zs + tps0 :#: j"
shows "transforms tm2 tps0 ttt tps2"
unfolding tm2_def by (tform tps: assms tps0 jk zs tps1_def)
end
end
lemma transforms_tm_make_bitI [transforms_intros]:
fixes j :: tapeidx
fixes tps tps' :: "tape list" and zs :: "symbol list" and ttt :: nat
assumes "j < length tps" and "proper_symbols zs"
assumes "tps ::: j = ⌊zs⌋"
assumes "ttt = 19 + 2 * length zs + tps :#: j"
assumes "tps' = tps
[j := if zs = [𝟭] then (⌊zs⌋, 2) else (⌊[𝟬]⌋, 1)]"
shows "transforms (tm_make_bit j) tps ttt tps'"
proof -
interpret loc: turing_machine_make_bit j .
show ?thesis
using assms loc.tps2_def loc.tm2 loc.tm2_eq_tm_make_bit by simp
qed
lemma output_length_le_time:
assumes "turing_machine k G M"
and "tps ::: 1 = ⌊zs⌋"
and "proper_symbols zs"
and "transforms M (snd (start_config k xs)) t tps"
shows "length zs ≤ t"
proof -
have 1: "execute M (start_config k xs) t = (length M, tps)"
using assms transforms_def transits_def
by (metis (no_types, lifting) execute_after_halting_ge fst_conv start_config_def sndI)
moreover have "k > 1"
using assms(1) turing_machine_def by simp
ultimately have "((execute M (start_config k xs) t) <:> 1) i = □" if "i > t" for i
using assms blank_after_time that by (meson zero_less_one)
then have "(tps ::: 1) i = □" if "i > t" for i
using 1 that by simp
then have *: "⌊zs⌋ i = □" if "i > t" for i
using assms(2) that by simp
show ?thesis
proof (rule ccontr)
assume "¬ length zs ≤ t"
then have "length zs > t"
by simp
then have "⌊zs⌋ (Suc t) ≠ □"
using contents_inbounds assms(3) contents_def proper_symbols_ne0 by simp
then show False
using * by simp
qed
qed
text ‹
This is the alternative definition of $\NP$, which restricts the verifier
to output only strings of length one:
›
lemma NP_output_len_1:
"𝒩𝒫 = {L. ∃k G M p T fverify.
turing_machine k G M ∧
polynomial p ∧
big_oh_poly T ∧
computes_in_time k M fverify T ∧
(∀y. length (fverify y) = 1) ∧
(∀x. x ∈ L ⟷ (∃u. length u = p (length x) ∧ fverify ⟨x, u⟩ = [𝕀]))}"
(is "_ = ?M")
proof
show "?M ⊆ 𝒩𝒫"
using complexity_class_NP_def by fast
define Q where "Q = (λL k G M p T fverify.
turing_machine k G M ∧
polynomial p ∧
big_oh_poly T ∧
computes_in_time k M fverify T ∧
(∀x. (x ∈ L) = (∃u. length u = p (length x) ∧ fverify ⟨x, u⟩ = [𝕀])))"
have alt: "complexity_class_NP = {L::language. ∃k G M p T fverify. Q L k G M p T fverify}"
unfolding complexity_class_NP_def Q_def by simp
show "𝒩𝒫 ⊆ ?M"
proof
fix L assume "L ∈ 𝒩𝒫"
then obtain k G M p T fverify where "Q L k G M p T fverify"
using alt by blast
then have ex:
"turing_machine k G M ∧
polynomial p ∧
big_oh_poly T ∧
computes_in_time k M fverify T ∧
(∀x. (x ∈ L) = (∃u. length u = p (length x) ∧ fverify ⟨x, u⟩ = [𝕀]))"
using Q_def by simp
have "k ≥ 2" and "G ≥ 4"
using ex turing_machine_def by simp_all
define M' where "M' = M ;; tm_make_bit 1"
define f' where "f' = (λy. if fverify y = [𝕀] then [𝕀] else [𝕆])"
define T' where "T' = (λn. 19 + 4 * T n)"
have "turing_machine k G M'"
unfolding M'_def using ‹2 ≤ k› ‹4 ≤ G› ex tm_make_bit_tm by simp
moreover have "polynomial p"
using ex by simp
moreover have "big_oh_poly T'"
using T'_def ex big_oh_poly_const big_oh_poly_prod big_oh_poly_sum by simp
moreover have "computes_in_time k M' f' T'"
proof
fix y
let ?cfg = "start_config k (string_to_symbols y)"
obtain tps where
1: "tps ::: 1 = string_to_contents (fverify y)" and
2: "transforms M (snd ?cfg) (T (length y)) tps"
using ex computes_in_timeD by blast
have len_tps: "length tps ≥ 2"
by (smt (verit) "2" ‹2 ≤ k› ex execute_num_tapes start_config_length less_le_trans numeral_2_eq_2
prod.sel(2) transforms_def transits_def zero_less_Suc)
define zs where "zs = string_to_symbols (fverify y)"
then have zs: "tps ::: 1 = ⌊zs⌋" "proper_symbols zs"
using 1 by auto
have transforms_MI [transforms_intros]: "transforms M (snd ?cfg) (T (length y)) tps"
using 2 by simp
define tps' where
"tps' = tps[1 := if zs = [𝟭] then (⌊zs⌋, 2) else (⌊[𝟬]⌋, 1)]"
have "transforms M' (snd ?cfg) (T (length y) + (19 + (tps :#: Suc 0 + 2 * length zs))) tps'"
unfolding M'_def by (tform tps: zs len_tps tps'_def)
moreover have "T (length y) + (19 + (tps :#: Suc 0 + 2 * length zs)) ≤ T' (length y)"
proof -
have "tps :#: Suc 0 ≤ T (length y)"
using 2 transforms_def transits_def start_config_def ex head_pos_le_time `2 ≤ k`
by (smt (verit, ccfv_threshold) One_nat_def Suc_1 Suc_le_lessD leD linorder_le_less_linear
order_less_le_trans prod.sel(2))
moreover have "length zs ≤ T (length y)"
using zs 2 ex output_length_le_time by auto
ultimately show ?thesis
using T'_def 1 2 by simp
qed
ultimately have *: "transforms M' (snd ?cfg) (T' (length y)) tps'"
using transforms_monotone by simp
have "tps' ::: 1 = (if zs = [𝟭] then tps ::: 1 else ⌊[𝟬]⌋)"
using tps'_def len_tps zs(1) by simp
also have "... = (if zs = [𝟭] then ⌊[𝟭]⌋ else ⌊[𝟬]⌋)"
using zs(1) by simp
also have "... = (if string_to_symbols (fverify y) = [3] then ⌊[3]⌋ else ⌊[2]⌋)"
using zs_def by simp
also have "... = (if fverify y = [𝕀] then ⌊[𝟭]⌋ else ⌊[𝟬]⌋)"
by auto
also have "... = (if fverify y = [𝕀] then string_to_contents [𝕀] else string_to_contents [𝕆])"
by auto
also have "... = string_to_contents (if fverify y = [𝕀] then [𝕀] else [𝕆])"
by simp
also have "... = string_to_contents (f' y)"
using f'_def by auto
finally have "tps' ::: 1 = string_to_contents (f' y)" .
then show "∃tps'. tps' ::: 1 = string_to_contents (f' y) ∧
transforms M' (snd ?cfg) (T' (length y)) tps'"
using * by auto
qed
moreover have "∀y. length (f' y) = 1"
using f'_def by simp
moreover have "(∀x. x ∈ L ⟷ (∃u. length u = p (length x) ∧ f' ⟨x, u⟩ = [𝕀]))"
using ex f'_def by auto
ultimately show "L ∈ ?M"
by blast
qed
qed
section ‹$\mathcal{P}$ is a subset of $\NP$\label{s:TC-subseteq}›
text ‹
Let $L\in\mathcal{P}$ be a language and $M$ a Turing machine that decides $L$ in
polynomial time. To show $L\in\NP$ we could use a TM that extracts the first
element from the input $\langle x, u\rangle$ and runs $M$ on $x$. We do not have
to construct such a TM explicitly because we have shown that the extraction of
the first pair element is computable in polynomial time (lemma~@{thm [source]
tm_first_computes}), and by assumption the characteristic function of $L$ is
computable in polynomial time, too. The composition of these two functions is
the verifier function required by the definition of $\NP$. And by lemma~@{thm
[source] computes_composed_poly} the composition of polynomial-time functions is
polynomial-time, too.
\null
›
theorem P_subseteq_NP: "𝒫 ⊆ 𝒩𝒫"
proof
fix L :: language
assume "L ∈ 𝒫"
then obtain c where c: "L ∈ DTIME (λn. n ^ c)"
using complexity_class_P_def by auto
then obtain k G M T' where M:
"turing_machine k G M"
"computes_in_time k M (characteristic L) T'"
"big_oh T' (λn. n ^ c)"
using DTIME_def by auto
then have 4: "big_oh_poly T'"
using big_oh_poly_def by auto
define f where "f = (λx. symbols_to_string (first (bindecode (string_to_symbols x))))"
define T :: "nat ⇒ nat" where "T = (λn. 9 + 4 * n)"
have 1: "turing_machine 3 6 tm_first"
by (simp add: tm_first_tm)
have 2: "computes_in_time 3 tm_first f T"
using f_def T_def tm_first_computes by simp
have 3: "big_oh_poly T"
proof -
have "big_oh_poly (λn. 9)"
using big_oh_poly_const by simp
moreover have "big_oh_poly (λn. 4 * n)"
using big_oh_poly_const big_oh_poly_prod big_oh_poly_poly[of 1] by simp
ultimately show ?thesis
using big_oh_poly_sum T_def by simp
qed
define fverify where "fverify = characteristic L ∘ f"
then have *: "∃T k G M. big_oh_poly T ∧ turing_machine k G M ∧ computes_in_time k M fverify T"
using M 1 2 3 4 computes_composed_poly by simp
then have fverify: "fverify ⟨x, u⟩ = [x ∈ L]" for x u
using f_def first_pair symbols_to_string_to_symbols fverify_def characteristic_def
by simp
define p :: "nat ⇒ nat" where "p = (λ_. 0)"
then have "polynomial p"
using const_polynomial by simp
moreover have "∀x. x ∈ L ⟷ (∃u. length u = p (length x) ∧ fverify ⟨x, u⟩ = [𝕀])"
using fverify p_def by simp
ultimately show "L ∈ 𝒩𝒫"
using * complexity_class_NP_def by fast
qed
section ‹More about $\mathcal{P}$, $\NP$, and reducibility\label{s:TC-more}›
text ‹
We prove some low-hanging fruits about the concepts introduced in this chapter.
None of the results are needed to show the Cook-Levin theorem.
›
text ‹
A language can be reduced to itself by the identity function. Hence reducibility
is a reflexive relation.
\null
›
lemma reducible_refl: "L ≤⇩p L"
proof -
let ?M = "tm_id"
let ?T = "λn. Suc (Suc n)"
have "turing_machine 2 4 ?M"
using tm_id_tm by simp
moreover have "big_oh_poly ?T"
proof -
have "big_oh_poly (λn. n + 2)"
using big_oh_poly_const big_oh_poly_id big_oh_poly_sum by blast
then show ?thesis
by simp
qed
moreover have "computes_in_time 2 ?M id ?T"
using computes_id by simp
moreover have "∀x. x ∈ L ⟷ id x ∈ L"
by simp
ultimately show "L ≤⇩p L"
using reducible_def by metis
qed
text ‹
Reducibility is also transitive. If $L_1 \leq_p L_2$ by a TM $M_1$ and $L_2
\leq_p L_3$ by a TM $M_2$ we merely have to run $M_2$ on the output of $M_1$ to
show that $L_1 \leq_p L_3$. Again this is merely the composition of two
polynomial-time computable functions.
›
lemma reducible_trans:
assumes "L⇩1 ≤⇩p L⇩2" and "L⇩2 ≤⇩p L⇩3"
shows "L⇩1 ≤⇩p L⇩3"
proof -
obtain k1 G1 M1 T1 f1 where 1:
"turing_machine k1 G1 M1 ∧
big_oh_poly T1 ∧
computes_in_time k1 M1 f1 T1 ∧
(∀x. x ∈ L⇩1 ⟷ f1 x ∈ L⇩2)"
using assms(1) reducible_def by metis
moreover obtain k2 G2 M2 T2 f2 where 2:
"turing_machine k2 G2 M2 ∧
big_oh_poly T2 ∧
computes_in_time k2 M2 f2 T2 ∧
(∀x. x ∈ L⇩2 ⟷ f2 x ∈ L⇩3)"
using assms(2) reducible_def by metis
ultimately obtain T k G M where
"big_oh_poly T ∧ turing_machine k G M ∧ computes_in_time k M (f2 ∘ f1) T"
using computes_composed_poly by metis
moreover have "∀x. x ∈ L⇩1 ⟷ f2 (f1 x) ∈ L⇩3"
using 1 2 by simp
ultimately show ?thesis
using reducible_def by fastforce
qed
text ‹
The usual way to show that a language is $\NP$-hard is to reduce another $\NP$-hard
language to it.
›
lemma ex_reducible_imp_NP_hard:
assumes "NP_hard L'" and "L' ≤⇩p L"
shows "NP_hard L"
using reducible_trans assms by auto
text ‹
The converse is also true because reducibility is a reflexive relation.
›
lemma NP_hard_iff_reducible: "NP_hard L ⟷ (∃L'. NP_hard L' ∧ L' ≤⇩p L)"
proof
show "NP_hard L ⟹ ∃L'. NP_hard L' ∧ L' ≤⇩p L"
using reducible_refl by auto
show "∃L'. NP_hard L' ∧ L' ≤⇩p L ⟹ NP_hard L"
using ex_reducible_imp_NP_hard by blast
qed
lemma NP_complete_reducible:
assumes "NP_complete L'" and "L ∈ 𝒩𝒫" and "L' ≤⇩p L"
shows "NP_complete L"
using assms NP_complete_def reducible_trans by blast
text ‹
In a sense the complexity class $\mathcal{P}$ is closed under reduction.
›
lemma P_closed_reduction:
assumes "L ∈ 𝒫" and "L' ≤⇩p L"
shows "L' ∈ 𝒫"
proof -
obtain c where c: "L ∈ DTIME (λn. n ^ c)"
using assms(1) complexity_class_P_def by auto
then obtain k G M T where M:
"turing_machine k G M"
"computes_in_time k M (characteristic L) T"
"big_oh T (λn. n ^ c)"
using DTIME_def by auto
then have T: "big_oh_poly T"
using big_oh_poly_def by auto
obtain k' G' M' T' freduce where M':
"turing_machine k' G' M'"
"big_oh_poly T'"
"computes_in_time k' M' freduce T'"
"(∀x. x ∈ L' ⟷ freduce x ∈ L)"
using reducible_def assms(2) by auto
obtain T2 k2 G2 M2 where M2:
"big_oh_poly T2"
"turing_machine k2 G2 M2"
"computes_in_time k2 M2 (characteristic L ∘ freduce) T2"
using M T M' computes_composed_poly by metis
obtain d where d: "big_oh T2 (λn. n ^ d)"
using big_oh_poly_def M2(1) by auto
have "characteristic L ∘ freduce = characteristic L'"
using characteristic_def M'(4) by auto
then have "∃k G M T'. turing_machine k G M ∧ big_oh T' (λn. n ^ d) ∧ computes_in_time k M (characteristic L') T'"
using M2 d by auto
then have "L' ∈ DTIME (λn. n ^ d)"
using DTIME_def by simp
then show ?thesis
using in_P_iff by auto
qed
text ‹
The next lemmas are items~2 and~3 of Theorem~2.8 of the textbook~\cite{ccama}.
Item~1 is the transitivity of the reduction, already proved in lemma @{thm
[source] reducible_trans}.
›
lemma P_eq_NP:
assumes "NP_hard L" and "L ∈ 𝒫"
shows "𝒫 = 𝒩𝒫"
using assms P_closed_reduction P_subseteq_NP by auto
lemma NP_complete_imp:
assumes "NP_complete L"
shows "L ∈ 𝒫 ⟷ 𝒫 = 𝒩𝒫"
using assms NP_complete_def P_eq_NP by auto
end