Zulip Chat Archive
Stream: new members
Topic: Computability, P (and NP)
Pim Spelier (Aug 28 2020 at 10:40):
Hi all,
Me and @Daan van Gent have been working on trying to define problems, P and hopefully even NP. We were wondering how exactly this process of development should go, as we feel this subject is something that eventually should be in mathlib.
Right now, our questions are: when is a first version ready to be pushed to mathlib? There are already some definitions and theorems that we believe to be of interest, could they already be PR'ed? Is there stuff that we need to do before it's ready to be PR'ed? Basically, this is something we're having fun with and want to continue, but we don't know how the process works exactly.
For the interested reader, the state of the project right now: we have forked mathlib to this repository, and while this is very much a work in progress (we're doing a partial refactoring now), we currently have
 A definition of problem
 A definition of reduction
 A definition of computable (in polytime) (using Turing machines)

A definition of P
and the lemma's 
A proof that the identity is (polytime) computable
 A proof that the problem on
bool
withtt
being the only yesinstance is in P
Also, on the TM front we're working on increasing the functional power of a Turing machine, for example by making a call stack and formalising libraries (both still very much a work in progress).
Our goals (in order of short term to long term):
 Prove that the composition of (polytime) computable functions is (polytime) computable (this will give that a problem reducing to a problem in P is itself in P)
 Prove that all four problems on
bool
are in P  Prove that is_even is in P
 Prove that is_odd is in P by giving a reduction to is_even
 Define NP (this should be very doable already)
 Show that P is a subset of NP
 Define NPC
 Enhance the functional power of Turing machines further
 Prove that SAT is in NPC
Johan Commelin (Aug 28 2020 at 10:55):
Wow! That's a huge list. You make it seem like the LftCM workshop was ages ago!
Johan Commelin (Aug 28 2020 at 10:56):
@Mario Carneiro Is probably the maintainer who knows best how and what and where this should go in mathlib. He wrote most of the compu/TM stuff that is in mathlib
Johan Commelin (Aug 28 2020 at 10:57):
Concerning PR's, just to get a feeling for the process, I would start with a very small PR (say 30 lines).
In general we encourage PRs to be at most (say, roughly) 300 lines. [Of course there are exceptions.]
Scott Morrison (Aug 28 2020 at 11:31):
"early and often" is the advice for PRs, I think. As soon as something feels a bit stable (e.g. you've already been through one cycle of throwing it out in disgust and starting over, but this time the next few steps seem to work as well), try to split off that chunk of your work into a PR.
Mario Carneiro (Aug 28 2020 at 18:33):
I would have suggested a PR by about the second item on the list
Mario Carneiro (Aug 28 2020 at 18:33):
it sounds like you have 5 or 6 PR's here
Mario Carneiro (Aug 28 2020 at 18:36):
oops, I missed that the second half is only goals and not completed stuff. I would suggest 2 PR's, one for the definition of P and one for work on the TM library
Pim Spelier (Aug 29 2020 at 11:11):
Thanks for all the advice! I didn't mention this, but we work with selfdefined encodings instead of encodables (the encodable seems to be better suited for partial recursive functions than Turing machines). This has already been refactored and used, so could that be the first PR? And for the second PR, we can probably do the definitions of (polytime) computable by a Turing machine and the definition of P. Does that make sense?
Pim Spelier (Aug 29 2020 at 11:12):
By the way, how do I PR something? Is there a link somewhere where it's explained?
Bryan Ginge Chen (Aug 29 2020 at 11:14):
You can start here. Feel free to ask for clarification or help if anything is unclear!
Pim Spelier (Aug 29 2020 at 12:54):
Thanks, that's really useful! I see we do need write access to nonmaster branches of the mathlib repository, can we get that? Our usernames are MadPidgeon and pimsp
Bryan Ginge Chen (Aug 29 2020 at 13:05):
Invites sent! https://github.com/leanprovercommunity/mathlib/invitations
Mario Carneiro (Aug 29 2020 at 19:35):
@Pim Spelier While I understand the reason you need a different encodable interface, I would like to only have one, so you should keep in mind how the existing encodable definitions can be retrofitted on a more TM friendly definition.
Pim Spelier (Aug 30 2020 at 09:38):
What exactly do you mean with retrofitting the existing definitions? The difference between encodable
and encoding
is something we've been thinking about, and our plan was to eventually show that there are two functions f: \N \to list \Gamma\0\1
and g: list \Gamma\0\1 \to \N
such that $g\circ f$ is primitive recursive and $f \circ g$ is computable by a Turing machine. That should give a way to go from encodable
s to encoding
s and vice versa.
Pim Spelier (Aug 30 2020 at 09:38):
Does that sound like a good solution, or do you have other suggestions/comments?
Last updated: May 13 2021 at 05:21 UTC