• API
• FAQ
• Tools
• Archive
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.
Top