SHARE
TWEET

PVersusNP.agda

itaibn Jul 27th, 2015 533 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. module PVersusNP where
  2.  
  3. P-equals-NP : Set
  4.  
  5. data sum {A : Set} (B : A -> Set) : Set where
  6.     _,_ : (a : A) -> B a -> sum B
  7.  
  8. pi0 : {A : Set} {B : A -> Set} -> sum B -> A
  9. pi0 (a , b) = a
  10.  
  11. data either (A : Set) (B : Set) : Set where
  12.     left : A -> either A B
  13.     right : B -> either A B
  14.  
  15. data N : Set where
  16.     Z : N
  17.     S : N -> N
  18.  
  19. iterate : {A : Set} -> N -> A -> (A -> A) -> A
  20. iterate Z z s = z
  21. iterate (S n) z s = s (iterate n z s)
  22.  
  23. _+_ : N -> N -> N
  24. Z + m = m
  25. S n + m = S (n + m)
  26.  
  27. _*_ : N -> N -> N
  28. Z * m = Z
  29. S n * m = m + (n * m)
  30.  
  31. exp : N -> N -> N
  32. exp n Z = S Z
  33. exp n (S m) = n * exp n m
  34.  
  35. data bool : Set where
  36.     false : bool
  37.     true : bool
  38.  
  39. if_then_else_ : {A : Set} -> bool -> A -> A -> A
  40. if true then x else _ = x
  41. if false then _ else x = x
  42.  
  43. _or_ : bool -> bool -> bool
  44. a or b = if a then true else b
  45.  
  46. data assert : bool -> Set where
  47.     taut : assert true
  48.  
  49. _<=_ : N -> N -> bool
  50. Z <= n = true
  51. S n <= Z = false
  52. S n <= S m = n <= m
  53.  
  54. is-poly : (N -> N) -> Set
  55. is-poly f = sum (\(m : N) -> ((n : N) -> assert (f n <= exp (S (S n)) m)))
  56.  
  57. is-right : {A B : Set} -> either A B -> bool
  58. is-right (left _) = false
  59. is-right (right _) = true
  60.  
  61. data fn : N -> Set where
  62.     fz : {n : N} -> fn (S n)
  63.     fs : {n : N} -> fn n -> fn (S n)
  64.  
  65. data vec (A : Set) : N -> Set where
  66.     end : vec A Z
  67.     _,_ : {n : N} -> A -> vec A n -> vec A (S n)
  68.  
  69. ref : {A : Set} {n : N} -> fn n -> vec A n -> A
  70. ref fz (a , _) = a
  71. ref (fs m) (_ , rest) = ref m rest
  72.  
  73. subs : {A : Set} {n : N} -> fn n -> A -> vec A n -> vec A n
  74. subs fz a (_ , rest) = a , rest
  75. subs (fs m) a (b , rest) = b , subs m a rest
  76.  
  77. replicate : {A : Set} -> (n : N) -> A -> vec A n
  78. replicate Z a = end
  79. replicate (S n) a = a , replicate n a
  80.  
  81. data list (A : Set) : Set where
  82.     end : list A
  83.     _,_ : A -> list A -> list A
  84.  
  85. len : {A : Set} -> list A -> N
  86. len end = Z
  87. len (_ , rest) = S (len rest)
  88.  
  89. data command (stacks : N) (states : N) : Set where
  90.     push : fn stacks -> bool -> fn states -> command stacks states
  91.     pop : fn stacks -> fn states -> fn states -> fn states -> command stacks
  92.         states
  93.     return : bool -> command stacks states
  94.  
  95. record machine : Set where
  96.     field
  97.         stacks : N
  98.         states : N
  99.         commands : vec (command stacks states) states
  100.         initial-command : fn states
  101.  
  102. command-mach : machine -> Set
  103. command-mach m = command (machine.stacks m) (machine.states m)
  104.  
  105. record state (m : machine) : Set where
  106.     constructor mkState
  107.     field
  108.         stacks : vec (list bool) (machine.stacks m)
  109.         current : fn (machine.states m)
  110.  
  111. step : (m : machine) -> state m -> either (state m) bool
  112. exec : {m : machine} -> command-mach m -> state m -> either (state m) bool
  113. step m s = exec (ref (state.current s) (machine.commands m)) s
  114. exec (return b) _ = right b
  115. exec (push i b c) s = let
  116.     prev-stack : list bool
  117.     prev-stack = ref i (state.stacks s)
  118.         in left (mkState
  119.             (subs i (b , prev-stack) (state.stacks s))
  120.             c)
  121.  
  122. exec (pop i ct cf ce) s with ref i (state.stacks s)
  123. ... | end = left (mkState
  124.     (state.stacks s)
  125.     ce)
  126. ... | true , rest = left (mkState
  127.     (subs i rest (state.stacks s))
  128.     ct)
  129. ... | false , rest = left (mkState
  130.     (subs i rest (state.stacks s))
  131.     cf)
  132.  
  133. step-or-halted : (m : machine) -> either (state m) bool -> either (state m) bool
  134. step-or-halted m (right b) = right b
  135. step-or-halted m (left s) = step m s
  136.  
  137. nsteps : {m : machine} -> N -> state m -> either (state m) bool
  138. nsteps {m} n s = iterate n (left s) (step-or-halted m)
  139.  
  140. initial-state : (m : machine) -> list bool -> state m
  141. initial-state m l = mkState (replicate (machine.stacks m) l)
  142.     (machine.initial-command m)
  143.  
  144. record poly-time-machine : Set where
  145.     field
  146.         polytime-machine : machine
  147.         runtime : N -> N
  148.         poly : is-poly runtime
  149.         is-runtime : (l : list bool) -> assert (is-right
  150.             (nsteps (runtime (len l)) (initial-state polytime-machine l)))
  151.  
  152. get-right : {A B : Set} -> (e : either A B) -> assert (is-right e) -> B
  153. get-right (left x) ()
  154. get-right (right x) _ = x
  155.  
  156. run-poly-time-machine : poly-time-machine -> list bool -> bool
  157. run-poly-time-machine m inp = get-right _ (poly-time-machine.is-runtime m inp)
  158.  
  159. np-machine : Set
  160. np-machine = poly-time-machine
  161.  
  162. search : N -> poly-time-machine -> list bool -> bool
  163. search Z m inp = run-poly-time-machine m inp
  164. search (S n) m inp = search n m (false , inp) or search n m (true , inp)
  165.  
  166. run-np-machine : np-machine -> list bool -> bool
  167. run-np-machine m inp = search (len inp) m inp
  168.  
  169. data _==_ {A : Set} (a : A) : A -> Set where
  170.     refl : a == a
  171.  
  172. P-equals-NP = (m-np : np-machine) -> sum (\(m-p : poly-time-machine) -> ((inp :
  173.     list bool) -> run-poly-time-machine m-p inp == run-np-machine m-np inp))
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
Top