[HN Gopher] Problems harder than NP-Complete
___________________________________________________________________
Problems harder than NP-Complete
Author : azhenley
Score : 46 points
Date : 2023-05-11 21:14 UTC (1 hours ago)
(HTM) web link (buttondown.email)
(TXT) w3m dump (buttondown.email)
| krick wrote:
| How hard is computing Ramsey numbers, BTW? Is there a word for
| that?
| mananaysiempre wrote:
| A practical (and solvable in practical cases!) EXPTIME-complete
| problem is type inference (or even typability) in the ML type
| system (that is Hindley-Milner extended with let-polymorphism) or
| in Trevor Jim's much nicer System P2 (equivalently rank-2
| intersection types; _a fortiori_ his System P; no, I'm not going
| to stop shilling System P, it deserves to have a language built
| upon it at least once).
|
| Decidable problems with even more insane complexity include
| provability in Presburger arithmetic (where you're forbidden from
| multiplying variables together in order to avoid the
| undecidability of Peano) and over the reals (with addition and
| multiplication only).
| apatil wrote:
| That's very interesting. In which variable is type inference
| EXPTIME complete?
|
| Whichever variable it is, I suppose in practice humans can't
| create programs that are big enough in that way for type
| inference to become impractical. However, I wonder whether
| someone could comment on what this means about the utility of
| HM-like type systems in future AI generated software.
| kachnuv_ocasek wrote:
| It's the size of the term. See this paper which proves the
| result for details:
| https://link.springer.com/chapter/10.1007/3-540-52590-4_50
| klyrs wrote:
| Something is up with the succinct circuits description.
|
| > An n-node simple graph can have up to 2^n edges, meaning it
| takes exponential space to encode
|
| An n-node simple graph can only have O(n^2) edges, and only needs
| quadratic space to encode.
| perihelions wrote:
| Pretty sure "n-node" is a typo and both vertices and edges are
| 2n.
| [deleted]
| [deleted]
| sgrove wrote:
| My absolute favorite overview of this - the video goes over both
| the explanation of the spaces, but also how it relates to a sort
| of understanding of reality itself!
|
| https://youtu.be/YX40hbAHx3s
| cvoss wrote:
| > does a CS regular expression without stars have no matches?
|
| It's worth elaborating this one, because testing whether an
| ordinary star-free regular expression has no matches is super
| easy. Not sure what the author means by "CS" (maybe just
| "computer science"?), but the actual problem is "Does a
| _generalized_ regular expression without stars have no matches? "
| Here, "generalized" means that we have two new operators, beyond
| union (alternation) and concatenation: they are intersection and
| negation. [0]
|
| You may recall that constructing an intersection automaton
| involves a cross product of NFAs, and constructing the negation
| automaton involves just flipping the accepting/rejecting states
| of a DFA. However, the NFA -> DFA construction can incur an
| exponential blowup of states.
|
| So at the very least, intuition shows that the automata we're
| working with are enormous w.r.t. the expression size. But at this
| point my intuition stops, so I won't be able to explain how we
| get from here to a TOWER-complete decision procedure for whether
| the accepting set is empty.
|
| [0] https://planetmath.org/generalizedregularexpression
| raatmarien wrote:
| And then beyond these decidable problems, there is a whole
| hierarchy of harder and harder undecidable problems, which I
| think is really cool as well.
|
| https://marienraat.nl/blog/posts/hardest-computational-probl...
| cvoss wrote:
| This is always fascinating to me, that there continues to be
| interesting structure among computational problems even after
| you pass the point where they aren't computable anymore.
|
| Kind of tangentially, but similar in spirit, I've often
| wondered about the following: You know how if you can prove
| False from a system of axioms, then the whole system collapses
| because you can prove anything from False? Well, surely not all
| such inconsistent systems are created equal. Right? There's a
| smallest/first proof of False in each inconsistent system. In
| some systems it may be very easy to prove False succinctly,
| while in others it may be a herculean effort to get your first
| proof of False. So, in that sense, some inconsistent systems
| are "more consistent" than others, or perhaps "consistent w.r.t
| particular inconsistencies". I wonder what this "structure
| among inconsistent systems" looks like!
___________________________________________________________________
(page generated 2023-05-11 23:00 UTC)