Read-back: PvsNP.P_subset_NP

The statement. The declaration asserts the set inclusion

$$\mathsf{P} \subseteq \mathsf{NP},$$

where $\mathsf{P}$ and $\mathsf{NP}$ are two specific sets of languages over the alphabet $\{\mathrm{false},\mathrm{true}\}$ defined in the accompanying bundle (unfolded below). A "language" here is any set $L$ of finite bit-strings (finite lists of Booleans; the empty string is allowed). Concretely the theorem says: for every set of bit-strings $L$, if $L$ satisfies the membership condition of $\mathsf{P}$ below, then $L$ satisfies the membership condition of $\mathsf{NP}$ below. There are no other hypotheses, no free variables, and no typeclass assumptions. (The declaration is stated with a sorry in place of a proof; the read-back describes only what is claimed.)

Throughout, $\Sigma^*$ denotes the set of finite bit-strings, $|w|$ the length of a string $w$, and $\mathbb{N}$ includes $0$.

---

The machine model shared by both definitions

Both $\mathsf{P}$ and $\mathsf{NP}$ are phrased in terms of Mathlib's bundled stack machine ("TM2") with the following data and conditions. For a function $f : A \to B$, an "input encoding" $e_A : A \to \Gamma_0^{*}$ and an "output encoding" $e_B : B \to \Gamma_1^{*}$ (lists over alphabets $\Gamma_0,\Gamma_1$), the assertion "$f$ is computable in polynomial time relative to $(e_A, e_B)$" means that the following structure is nonempty (this is merely a proposition; no particular machine is fixed):

• A machine $M$ consisting of:
  • a finite index type $K$ of stacks, with decidable equality;
  • two distinguished stack indices $k_0$ (input stack) and $k_1$ (output stack) in $K$ — they are allowed to coincide;
  • for each $k \in K$ a type $\Gamma_k$ of stack symbols (arbitrary types; only $\Gamma_{k_0}$ is required to be finite by the structure itself, though the bijections below force $\Gamma_{k_0}$ and $\Gamma_{k_1}$ to be finite anyway);
  • a finite type $\Lambda$ of program labels and a distinguished "main" label $\lambda_0 \in \Lambda$;
  • a finite type $S$ of internal states and a distinguished initial state $s_0 \in S$;
  • a program $m : \Lambda \to \mathrm{Stmt}$, assigning to each label a statement built from the constructors push (onto stack $k$ a symbol computed from the internal state), peek (update the internal state from the top of stack $k$, if any), pop (same, and remove the top), load (update the internal state), branch (on a Boolean of the internal state), goto (jump to a label computed from the internal state), and halt.
• Bijections $\iota_0 : \Gamma_{k_0} \simeq \Gamma_0$ and $\iota_1 : \Gamma_{k_1} \simeq \Gamma_1$ identifying the input and output stack alphabets with $\Gamma_0$, $\Gamma_1$ respectively.
• A polynomial $p \in \mathbb{N}[X]$ with natural-number coefficients (the "time bound").
• For every input $a \in A$, a witness that the machine, started in the configuration

$$C_{\mathrm{init}}(a) := \bigl(\text{label } \lambda_0,\ \text{state } s_0,\ \text{stack } k_0 = \iota_0^{-1}\text{ applied symbolwise to } e_A(a),\ \text{all other stacks empty}\bigr),$$

reaches, after exactly some number $t$ of iterations of the one-step transition function (with $t \le p(|e_A(a)|)$, where $|e_A(a)|$ is the length of the encoded input), the configuration

$$C_{\mathrm{halt}}(f(a)) := \bigl(\text{label } \bot\ (\text{halted}),\ \text{state } s_0,\ \text{stack } k_1 = \iota_1^{-1}\text{ applied symbolwise to } e_B(f(a)),\ \text{all other stacks empty}\bigr).$$

Here one iteration of the transition function on a configuration with label $\ell \in \Lambda$ executes the statement $m(\ell)$ to completion (a whole statement counts as one step regardless of how many push/pop/etc. operations it contains) yielding a new configuration, and on a halted configuration (label $\bot$) yields "no configuration". Iteration is performed in the option monad, so once "no configuration" is produced it persists; hence the requirement that the $t$-th iterate equals $C_{\mathrm{halt}}(f(a))$ forces the run not to have halted strictly earlier than step $t$, and forces the halting configuration to have the internal state equal to the initial state $s_0$ and all stacks other than $k_1$ empty (if $k_0 = k_1$, the single stack must hold exactly the encoded output). The bound $t \le p(|e_A(a)|)$ is $\le$, not $<$.

The set $\mathsf{P}$

A language $L \subseteq \Sigma^*$ belongs to $\mathsf{P}$ if and only if there exists a function $\chi : \Sigma^* \to \{\mathrm{false},\mathrm{true}\}$ such that

1. $\chi$ is computable in polynomial time, in the sense above, relative to the input encoding $e_A = \mathrm{id}$ (a bit-string is fed in as itself, so $\Gamma_0 = \{\mathrm{false},\mathrm{true}\}$ and the input length is $|w|$) and the output encoding $e_B(b) = [\,b\,]$ (the one-symbol string consisting of $b$; so $\Gamma_1 = \{\mathrm{false},\mathrm{true}\}$); and
2. for every bit-string $w$ (including the empty string): $w \in L \iff \chi(w) = \mathrm{true}$.

The set $\mathsf{NP}$

A language $L \subseteq \Sigma^*$ belongs to $\mathsf{NP}$ if and only if there exist a function $R : \Sigma^* \times \Sigma^* \to \{\mathrm{false},\mathrm{true}\}$ and a natural number $k \in \mathbb{N}$ (possibly $k = 0$) such that

1. $R$ is computable in polynomial time, in the sense above, relative to the input encoding

$$e_A(x, y) := \bigl[\mathrm{inl}(x_1), \dots, \mathrm{inl}(x_{|x|})\bigr] \mathbin{+\!\!+} \bigl[\mathrm{inr}(y_1), \dots, \mathrm{inr}(y_{|y|})\bigr]$$

over the four-symbol alphabet $\Gamma_0 = \{\mathrm{false},\mathrm{true}\} \sqcup \{\mathrm{false},\mathrm{true}\}$ (the first string's bits tagged "left", followed by the second string's bits tagged "right"; the encoded length is $|x| + |y|$, so the time bound is $p(|x|+|y|)$), and the output encoding $e_B(b) = [\,b\,]$ as before; and 2. for every bit-string $w$ (including the empty string):

$$w \in L \iff \exists\, y \in \Sigma^* \text{ with } |y| \le |w|^{k} \text{ and } R(w, y) = \mathrm{true}.$$

Here $|w|^k$ is natural-number exponentiation with $0^0 = 1$; in particular if $k = 0$ the witness $y$ must have length $\le 1$ for every $w$, and if $k \ge 1$ and $w$ is the empty string then $y$ must be the empty string.

What the theorem claims, fully unfolded

For every set of bit-strings $L$: if there is a Boolean-valued function $\chi$ on bit-strings, computed (identity input encoding, one-bit output encoding) by some finite stack machine as above within a number of statement-executions bounded by a fixed polynomial in $|w|$ and halting in the exact halting configuration described, with $L = \{ w : \chi(w) = \mathrm{true} \}$, then there are a Boolean-valued function $R$ on pairs of bit-strings and a $k \in \mathbb{N}$, with $R$ computed (tagged-concatenation input encoding over a four-symbol alphabet, one-bit output encoding) by some finite stack machine within a fixed polynomial in $|w|+|y|$ statement-executions and halting in the exact halting configuration described, such that $L = \{ w : \exists y,\ |y| \le |w|^k \wedge R(w,y) = \mathrm{true} \}$.