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

halting inputs.

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

LB_n.

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

them.

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

language.

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

unified theoretically.

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

program.

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.