The Stack Overflow podcast is back! Listen to an interview with our new CEO.

New answers tagged

0

You can't determine the running time of a generic program automatically, this is an undecidable problem similar to the Halting problem. Maybe you can try to enumerate a very well defined subset of the possible codes up to certain size. But in order to be useful for an search/optimization algorithm (other than random search), this subset needs to be ...


4

In these sorts of cases, one idiomatic way is to run it with gas, and to create one non-total gas value to let you finish the program. Yes, perhaps Idris should offer a combinator for IO that allows full streams to be run, but this is sufficient, and doesn't affect the validity of anything else. Seeing this, I'd agree that the IO monad should be coinductive,...


0

accepts if $M$ doesn't halt on $x$ That's not something a Turing machine can do in general: informally, keep in mind that accepting has to happen at some finite stage while we can't in general tell that a program isn't going to halt in finite time (which is why HP is undecidable). Your $M'$ is implicitly treating a co-r.e. event (non-halting) as r.e. (so ...


Top 50 recent answers are included