__nobody's Shortform

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 [LW(p) · GW(p)] with its tragically simple bit-flip search had recently made me think about program enumeration again…)