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))
```
