1 min read29th May 20201 comment
This is a special post for quick takes by __nobody. Only they can create top-level comments. Comments here also appear on the Quick Takes page and All Posts page.
1 comment, sorted by Click to highlight new comments since: Today at 11:34 PM

Observation: It should generally be safe to forbid non-termination when searching for programs/algorithms.

In practice, all useful algorithms terminate: If you know that you're dealing with a semi-decidable thing and doing serious work, you'll either (a) add a hard cutoff, or (b) structure the algorithm into a bounded step function and a controller that decides whether or not to run for another step. That transformation is not adding significant overhead size-wise, so you're bound to find a terminating algorithm "near" a non-terminating one!

Sure, that slightly changes the interface – it's now allowed to abort with "don't know", but that's a transformation that you likely would have applied anyway. Even if you consider that a drawback, not having to deal with potentially non-terminating programs / being able to use a description format that cannot represent non-terminating forms should more than make up for that.

(I just noticed this while thinking about how to best write something in Coq (and deciding on termination by "fuel limit"), after AABoyles' shortform on logical causal isolation with its tragically simple bit-flip search had recently made me think about program enumeration again…)