feat(Classes): prove finitely-supported functions belong to FP - #16
Conversation
Any function of the form `fun s => if s ∈ S then g s else []` with `S` a finite set is polynomial-time computable: a work-tape-free lookup machine hard-wires the finite table into its states, tracking viable prefixes of `S` while scanning the input and then emitting the fixed output, all in linear time. This gives the base case for assembling FP functions from finitely many exceptional values. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
LGTM, except can you move some of the generic names in TM under a bit more specific of a namespace?
|
Ok, I have changed the namespace to TM.FinsetDomain. It also started to seem to me like some of the |
|
Once CI passes we can merge! This was a nice PR: would you like to become a collaborator on the library? Happy to add you if you are interested. |
|
Thanks, sure, happy to collaborate! I will try to clean up my (Fable's) work on PH and add that next. I'm interested in getting to the Sipser–Lautemann theorem |
|
Perfect! I'll add you. This seems reasonable, we should already have some of the infrastructure, for instance for amplification, from BPP subseteq P/poly. |
|
It takes so long to build, I imagine there are likely things we can do to improve that. I wonder if potentially making a cache and split it into multiple packages would be sensible given how massive this thing is getting... |
2 participants
This PR adds the theorem that functions from List Bool to List Bool which return a nonempty value only on fintely many inputs are in FP.
🤖 Generated with Claude Code