Note: the following is synthesized from
a conversation between Tommy Bidne, Morgan Thomas, and I. #
onwards
(Also see
this pretty-good write-up I did on cohost)
Say you have a conjecture that some predicate
P holds on every natural number. And say you have a
turing machine tP which searches for counter-examples and halts when it finds one; that is,
tP halts
iff the conjecture
∀n P(n) is false. Also say you have a
function S:N→N such that
tP has not halted after n steps ⟺∀k<S(n):P(k)
That is,
S tells us the “speed” of
tP; after running
tP for
n steps we will have verified
P(n) for
0≤n<S(n).
Okay, that’s the setup.
Now assume that a counter-example
c to
P exists. Then we know
tP halts on some
n. Further, it must halt after at most
BB(tP) steps
rk (because otherwise it would run forever). In turn, the counterexample
c must be less than
S(BB(tP)).
where
BB(t) denotes
BB(n,m) where
n is the number of states in
t and
m the number of symbols
This means that the existence of the
function BB bounding runtime on halting machines
tP indirectly establishes a bound on counter-examples to conjectures
P.
So we have for a counter-example searching TM
(tP,S) that any counterexamples must be less than
S(BB(tP)). If we are interested in finding whether or not the conjecture
P actually is true, we can do so by explicitely running
tP on all numbers
0≤n<S(BB(tP)); as such, to make this search as fast as possible, it behooves us to try and minimize
S(BB(tP)).
Finding a counter-example searching TM
(tP,S) with small
S(BB(tP)) can essentially be done in 3 ways:
Try to minimize
n—the number of states in
tP—which lowers
BB(tP)
Try to minimize
m—the number of symbols in
tP—which lowers
BB(tP)
Try to make
S slow-growing; that is, try to make
tP slow-running.
In other words, if we want to do an exhaustive search with
tP, it is useful to construct
tP to be the smallest TM which runs as
slowly as possible. This results in a tighter bound on possible counter-examples to
P; these potential counterexamples can then be tested with a fast-running
turing machine.