tm thm proving adventures
- hi all, some more notes on the subject of tm thm proving.
last msg I explained how "resolving" a theorem encoded
into a TM (via proving halting or nonhalting of particular
inputs) is equivalent to showing how to enumerate that TM's
accepting inputs in canonical order. this is a well known
result that the recursive functions are exactly those that can be
enumerated in canonical order, and the recursively enumerable
functions cannot be enumerated in canonical order. (I will
start abbreviating this c-order)
I showed a simple TM for which when doing a reverse simulation,
it is clear we can enumerate its accepting inputs in
c-order. however, I didnt really give any kind of a (formal) proof of
that. in fact that is exactly the problem I am trying to figure
out-- how to obtain & automate formal proofs of that.
so a few more ideas along those lines.
suppose a TM has only state transitions in the form
[symbol1] -> [symbol2] whe symbol1 is the input and symbol2
is the output. if all state transitions never have a blank
character as symbol2, then that TM cannot ever shrink the size
of the string written on its input tape, and therefore when
we enumerate accepting states in reverse-order (ie starting
from halting state) we also get c-order enumeration of the
so we are concerned with machines that have states with symbol2
sometimes blank. and apparently the problem is to convert
its accepting state enumeration into a TM that doesnt have
any blank symbol2's. I will just start calling symbol2
"output symbol" or out-symbol.
another way of looking at this problem is as follows. consider
a nontrivial TM with some blank out-symbols. if we simulate
in reverse order (such as I gave in the example previously) we
will get a set of IDs. now at time "T_n" we will have an
upper and lower bound on the length of those IDs. let "LB_n" be
the lower bound of lengths in this set at time n. to prove the
machine is recursive we must prove that LB_n is a
monotonically increasing function. voila!! how do we do that?
not sure. but it is clear we cannot do it in general, ie
derive LB_n consistently, otherwise we solve the halting problem.
apparently, perhaps the key problem is that LB_n can be
any kind of astronomical function whatsoever, and there is no
function that is greater than all possible LB functions.
but here's a wild thought. suppose we pick an arbitrary LB function.
in fact it is easy to speculate on a potential LB based on
empirical simulation of the TM and watching the empirically
computed LB_n over time. then suppose we simply conjecture a plausible
now the huge question. given an LB_n' that I conjecture, can I
find an algorithm that will determine whether the actual
LB_n > LB_n' for all n? is that an undecidable problem or not?
I am suspecting that this is NOT an undecidable problem, but
in fact decidable. and that is exactly the extremely powerful
algorithm that I am searching for in my quest for
"the ultimate thm prover"
that would be the breakthrough I am looking for. it reduces the
problem of converting a machine of unknown status
("may be recursive") into a simple semi-systematic conjecture on
LB_n', and then testing that conjecture.
then this would seem to convert all of the problem of arbitrary
theorem proving into conjecturing arbitrary LB_n' and testing
I am building a TM compiler in ruby
to test some of these ideas..slow going, but good progress. several
years ago I had another TM compiler written in perl which would
be sufficient right now also, but I dont feel like relearning
or using the old code & feel perl is an ugly language compared
to ruby. the old code also supported inserting
and deleting squares of the TM tape, a variation I invented which is
obviously equivalent to the classic TM but which seemed to
be much more convenient for writing the compiler & its programming
however I suspect that the above theory is not
as simple wrt a machine with insertable and deletable states.
we have to worry not merely about blank outsymbol writing but
also deleting squares. the above (no inserting or deleting,
concerned only with blank-outsymbols) seems a little more
as a 1st test of the ideas above I would like to build
the thm proving algorithm as described above and test it
on the classic problem of computing the primes.
I wrote some TM pseudocode that can detect a prime number.
the compiler now implements several instructions from the
I wonder if anyone has ever actually created complicated
TMs? it appears that this has been done for the halting problem
by penrose, in his book _emperors new mind_, but I suspect
many problems have never actually been converted to TMs because
its almost always just a theoretical tool.
more in a bit.