feat: add implementation of P vs NP problem

[BoltonBailey]

This PR implements #676: The P vs NP problem.

I have tried to keep the definitions as simple as possible to avoid misstatements. This PR defines:

• Decision problems as functions from Lists of Bools to Bool
• Complexity classes as sets of decision problems
• P as the class of decision problems computable with TM2ComputableInPolyTime using a generic encoding for List Bool
• NP using an adaptation of the definition in Arora-Barak.

As a bonus, this includes a definition of co-NP and the NP vs co-NP conjecture.

[BoltonBailey]

Also, be advised, I took some of the code around the encodings of lists from an old Zulip thread discussing this problem, I am not sure if the person who wrote that has gone through the CLA process - should I try to get permission from them or rewrite that part of the code?

[mo271]

Also, be advised, I took some of the code around the encodings of lists from an old Zulip thread discussing this problem, I am not sure if the person who wrote that has gone through the CLA process - should I try to get permission from them or rewrite that part of the code?

If you think they contributed substantially, perhaps it would be good to add them as co-author by amending one of the commits with something like Co-authored-by: Foo Bar <[email protected]>. This will make the CLA bot pick it up, I suppose. But of course this is a question of your judgment on how substantial their contribution was.

Definitely nice that you link the zulip discussion in the code!

[BoltonBailey]

I was able to replace Daniel Weber's encodings with a more compact implementation, perhaps we can revisit it if we want a more general implementation in the future, but for now it should be fine.