0
$\begingroup$

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))
```
$\endgroup$
4
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – helianthus Nov 18 '19 at 17:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.