Qyriad

A myriad of Qyriad

@Qyriad

Mikaela, Lily, Violet, and Ciri — a plural collective of nerdy, quoiromantic, poly, lesbian computer engineers and leftists.

Current media obsessions: Persona 5, RWBY, Cosmere

log in
Qyriad
@Qyriad
lunasorcery
@lunasorcery
lexyeevee
@lexyeevee

the halting problem problem

the halting problem is, of course, the question of how to make a computer program that can determine whether any other computer program eventually stops, or runs forever. this is well known to be undecidable

the halting problem problem is that i have seen multiple tech people insist that this means you cannot ever tell whether any computer program halts. this is nonsense. consider the following python program:

i assert that this program halts. i mean, obviously.

the trick, of course, is that "undecidable" is a mathematician word that really means we have at least one, incredibly annoying, counterexample. and the conflict completely evaporates if we are willing to receive "i don't know" as an answer, because the counterexample depends on having an oracle that gives a correct yes/no answer in the first place.

maybe this is the difference between "computer science" and "software development"? computer science is about explaining why this cannot be done in the general case because there is a contrived case where it is logically impossible; software development is about shrugging and saying "we'll throw an exception for that then"

nex3
@nex3

the halting problem problem problem

is determining when any given tech person will stop insisting that you can't tell whether any computer program halts

@Qyriad shared with:
You must log in to comment.

in reply to @lexyeevee's post:

ebu
@ebu

Sometimes I think of language design and type systems and while I know the level of analysis to determine whether, for example, a given function halts or not, or is total on its inputs, in the general case is impossible. But I think that there is some level of analysis that tries to determine those things that is useful. I think of Typescript's never type -- sure, that's not solveable in the general sense but it can still be determined often enough that it makes for a useful part of a type system. (some of Java's annotations fall in this category, too, but the programmer is responsible for determining them in cases where it's trivial for static analysis to figure out)

login to reply
hierarchon
@hierarchon

more seriously i think the difference is that you can't really formalize the notion of 'good enough', yeah. can you build a halting problem solver that will work for 90% of programs out there in the world? yeah, probably, but it's also really easy to accidentally build something turing-complete

login to reply
manishearth
@manishearth

I see this often with a lot of NP-hard stuff. Folks go "this is NP-hard so we shouldn't do it" but often you can still do it and if you hit a complex case just say "no i don't want to anymore please give me different input"

like, proper dependency resolution? NP-hard. but cargo still does it. it just approximates at times and might complain in cases where there is a valid answer but it can't find one.

see also: trait resolution. really anything in PL where someone uses the word "resolution".

login to reply
lunasorcery
@lunasorcery

This post (and this comment) reminded me of the Picross stuff I've been playing with recently. In the general case it's an NP-complete problem to solve a Picross puzzle, but in practical terms a significant number of the possible puzzles can be solved in polynomial time using pretty straightforward strategies, so the majority of commercial Picross implementations only feature those polynomially-solvable puzzles.

login to reply
tomforsyth
@tomforsyth

As usual people are again getting mixed up between "computer science" and "science involving actual computers". Not only do they not have much to do with each other, they're frequently glaring at each other refusing to speak and waiting for the other one to apologise first.

login to reply