PVersusNP.agda

module PVersusNP where

P-equals-NP : Set

data sum {A : Set} (B : A -> Set) : Set where
    _,_ : (a : A) -> B a -> sum B

pi0 : {A : Set} {B : A -> Set} -> sum B -> A
pi0 (a , b) = a

data either (A : Set) (B : Set) : Set where
    left : A -> either A B
    right : B -> either A B

data N : Set where
    Z : N
    S : N -> N

iterate : {A : Set} -> N -> A -> (A -> A) -> A
iterate Z z s = z
iterate (S n) z s = s (iterate n z s)

_+_ : N -> N -> N
Z + m = m
S n + m = S (n + m)

_*_ : N -> N -> N
Z * m = Z
S n * m = m + (n * m)

exp : N -> N -> N
exp n Z = S Z
exp n (S m) = n * exp n m

data bool : Set where
    false : bool
    true : bool

if_then_else_ : {A : Set} -> bool -> A -> A -> A
if true then x else _ = x
if false then _ else x = x

_or_ : bool -> bool -> bool
a or b = if a then true else b

data assert : bool -> Set where
    taut : assert true

_<=_ : N -> N -> bool
Z <= n = true
S n <= Z = false
S n <= S m = n <= m

is-poly : (N -> N) -> Set
is-poly f = sum (\(m : N) -> ((n : N) -> assert (f n <= exp (S (S n)) m)))

is-right : {A B : Set} -> either A B -> bool
is-right (left _) = false
is-right (right _) = true

data fn : N -> Set where
    fz : {n : N} -> fn (S n)
    fs : {n : N} -> fn n -> fn (S n)

data vec (A : Set) : N -> Set where
    end : vec A Z
    _,_ : {n : N} -> A -> vec A n -> vec A (S n)

ref : {A : Set} {n : N} -> fn n -> vec A n -> A
ref fz (a , _) = a
ref (fs m) (_ , rest) = ref m rest

subs : {A : Set} {n : 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 : N) -> A -> vec A n
replicate Z a = end
replicate (S n) a = a , replicate n a

data list (A : Set) : Set where
    end : list A
    _,_ : A -> list A -> list A

len : {A : Set} -> list A -> N
len end = Z
len (_ , rest) = S (len rest)

data command (stacks : N) (states : N) : 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 : N
        states : N
        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 -> either (state m) bool
exec : {m : machine} -> command-mach m -> state m -> either (state m) bool
step m s = exec (ref (state.current s) (machine.commands m)) s
exec (return b) _ = right b
exec (push i b c) s = let
    prev-stack : list bool
    prev-stack = ref i (state.stacks s)
        in left (mkState
            (subs i (b , prev-stack) (state.stacks s))
            c)

exec (pop i ct cf ce) s with ref i (state.stacks s)
... | end = left (mkState
    (state.stacks s)
    ce)
... | true , rest = left (mkState
    (subs i rest (state.stacks s))
    ct)
... | false , rest = left (mkState
    (subs i rest (state.stacks s))
    cf)

step-or-halted : (m : machine) -> either (state m) bool -> either (state m) bool
step-or-halted m (right b) = right b
step-or-halted m (left s) = step m s

nsteps : {m : machine} -> N -> state m -> either (state m) bool
nsteps {m} n s = iterate n (left 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
    field
        polytime-machine : machine
        runtime : N -> N
        poly : is-poly runtime
        is-runtime : (l : list bool) -> assert (is-right
            (nsteps (runtime (len l)) (initial-state polytime-machine l)))

get-right : {A B : Set} -> (e : either A B) -> assert (is-right e) -> B
get-right (left x) ()
get-right (right x) _ = x

run-poly-time-machine : poly-time-machine -> list bool -> bool
run-poly-time-machine m inp = get-right _ (poly-time-machine.is-runtime m inp)

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

search : N -> poly-time-machine -> list bool -> bool
search Z m inp = run-poly-time-machine m inp
search (S n) m inp = search n m (false , inp) or search n m (true , inp)

run-np-machine : np-machine -> list bool -> bool
run-np-machine m inp = search (len inp) m inp

data _==_ {A : Set} (a : A) : A -> Set where
    refl : a == a

P-equals-NP = (m-np : np-machine) -> sum (\(m-p : poly-time-machine) -> ((inp :
    list bool) -> run-poly-time-machine m-p inp == run-np-machine m-np inp))