Zulip Chat Archive

Stream: new members

Topic: Computability, P (and NP)


view this post on Zulip 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 with tt being the only yes-instance 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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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.]

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Aug 28 2020 at 18:33):

I would have suggested a PR by about the second item on the list

view this post on Zulip Mario Carneiro (Aug 28 2020 at 18:33):

it sounds like you have 5 or 6 PR's here

view this post on Zulip 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

view this post on Zulip Pim Spelier (Aug 29 2020 at 11:11):

Thanks for all the advice! I didn't mention this, but we work with self-defined 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?

view this post on Zulip 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?

view this post on Zulip Bryan Gin-ge Chen (Aug 29 2020 at 11:14):

You can start here. Feel free to ask for clarification or help if anything is unclear!

view this post on Zulip Pim Spelier (Aug 29 2020 at 12:54):

Thanks, that's really useful! I see we do need write access to non-master branches of the mathlib repository, can we get that? Our usernames are MadPidgeon and pimsp

view this post on Zulip Bryan Gin-ge Chen (Aug 29 2020 at 13:05):

Invites sent! https://github.com/leanprover-community/mathlib/invitations

view this post on Zulip 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.

view this post on Zulip 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 encodables to encodings and vice versa.

view this post on Zulip 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