# Is this statement of P = NP in Agda correct?

Looking for a self-contained statement of P = NP in type theory, I stumbled upon this short Agda formalization (a cleaned up version is reproduced below).

The statement here does seem to express the problem correctly but I'm not entirely sure as the code is not well-commented. So my question is: is this an accurate statement of P = NP and if not how would one fix it?


open import Data.Nat                              using    (ℕ; suc; zero; _+_; _*_; _≤_; _^_)
open import Data.Bool                             using    (Bool; true; false; if_then_else_; _∨_)
open import Data.List                             using    (List; _∷_; []; length)
open import Data.Vec                              using    (Vec; _∷_; [])
open import Data.Product                          using    (Σ-syntax; _,_)
open import Data.Sum                              using    (_⊎_; inj₁; inj₂)
open import Data.Empty                            using    (⊥)
open import Relation.Binary.PropositionalEquality using    (_≡_; refl)

iterate : {A : Set} → ℕ → A → (A → A) → A
iterate zero    z s = z
iterate (suc n) z s = s (iterate n z s)

is-poly : (ℕ → ℕ) → Set
is-poly f = Σ[ m ∈ ℕ ] ((n : ℕ) → f n ≤ 2 ^ m)

is-inj₂ : {A B : Set} → A ⊎ B → Bool
is-inj₂ (inj₁  _) = false
is-inj₂ (inj₂ _) = true

data fn : ℕ → Set where
fz : {n : ℕ} → fn (suc n)
fs : {n : ℕ} → fn n → fn (suc n)

ref : {A : Set} {n : ℕ} → fn n → Vec A n → A
ref fz (a ∷ _) = a
ref (fs m) (_ ∷ rest) = ref m rest

subs : {A : Set} {n : ℕ} → fn n → A → Vec A n → Vec A n
subs fz a (_ ∷ rest) = a ∷ rest
subs (fs m) a (b ∷ rest) = b ∷ subs m a rest

replicate : {A : Set} → (n : ℕ) → A → Vec A n
replicate zero a = []
replicate (suc n) a = a ∷ replicate n a

data command (stacks : ℕ) (states : ℕ) : Set where
push   : fn stacks → Bool → fn states → command stacks states
pop    : fn stacks → fn states → fn states → fn states
→ command stacks states
return : Bool → command stacks states

record machine : Set where
field
stacks : ℕ
states : ℕ
commands : Vec (command stacks states) states
initial-command : fn states

command-mach : machine → Set
command-mach m = command (machine.stacks m) (machine.states m)

record state (m : machine) : Set where
constructor mkState
field
stacks : Vec (List Bool) (machine.stacks m)
current : fn (machine.states m)

step : (m : machine) → state m → (state m) ⊎ Bool
exec : {m : machine} → command-mach m → state m → (state m) ⊎ Bool

step m s = exec (ref (state.current s) (machine.commands m)) s
exec (return b) _ = inj₂ b
exec (push i b c) s =
let
prev-stack : List Bool
prev-stack = ref i (state.stacks s)
in
inj₁ (mkState (subs i (b ∷ prev-stack) (state.stacks s)) c)

exec (pop i ct cf ce) s with ref i (state.stacks s)
... | []           = inj₁ (mkState (state.stacks s) ce)
... | true  ∷ rest = inj₁ (mkState (subs i rest (state.stacks s)) ct)
... | false ∷ rest = inj₁ (mkState (subs i rest (state.stacks s)) cf)

step-or-halted : (m : machine) → (state m) ⊎ Bool → (state m) ⊎ Bool
step-or-halted m (inj₂ b) = inj₂ b
step-or-halted m (inj₁ s) = step m s

nsteps : {m : machine} → ℕ → state m → (state m) ⊎ Bool
nsteps {m} n s = iterate n (inj₁ s) (step-or-halted m)

initial-state : (m : machine) → List Bool → state m
initial-state m l =
mkState (replicate (machine.stacks m) l) (machine.initial-command m)

record poly-time-machine : Set where
inductive
field
m : machine
runtime : ℕ → ℕ
poly : is-poly runtime
is-runtime : (l : List Bool)
→ (is-inj₂ (nsteps (runtime (length l)) (initial-state m l))) ≡ true

get-inj₂ : {A B : Set} → (e : A ⊎ B) → is-inj₂ e ≡ true → B
get-inj₂ (inj₁ x) ()
get-inj₂ (inj₂ x) _ = x

run-poly-time-machine : poly-time-machine → List Bool → Bool
run-poly-time-machine m inp = get-inj₂ _ (poly-time-machine.is-runtime m inp)

np-machine : Set
np-machine = poly-time-machine

search : ℕ → poly-time-machine → List Bool → Bool
search zero    m inp = run-poly-time-machine m inp
search (suc n) m inp = search n m (false ∷ inp) ∨ search n m (true ∷ inp)

run-np-machine : np-machine → List Bool → Bool
run-np-machine m inp = search (length inp) m inp

P=NP : Set
P=NP =
(m-np : np-machine) →
Σ[ m-p ∈ poly-time-machine ]
(((inp : List Bool) → run-poly-time-machine m-p inp ≡ run-np-machine m-np inp))
$$$$


The definition is not correct. It states that a machine is polynomial time (the field poly in poly-time-machine) when its running time is below the exponential function $$n \mapsto 2^n$$ (the definition is-poly). This would allow, for example, a running time $$n \mapsto 1.5^n$$, which isn not poly-time according to the accepted definition.
• So would it suffice to fix is-poly to look like is-poly f = Σ[ m ∈ ℕ ] f ∈𝒪 (λ x → x ^ m) where f ∈𝒪 g = Σ[ c ∈ ℕ ] Σ[ x₀ ∈ ℕ ] ((x : ℕ) → x₀ ≤ x → f x ≤ c * g x)`? Would this then be a correct statement of P = NP? Nov 18 '19 at 17:47