Loading ...
Sorry, an error occurred while loading the content.

tm thm proving adventures

Expand Messages
  • vznuri
    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
    Message 1 of 1 , Mar 3, 2004
      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
      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

      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
      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

      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.
    Your message has been successfully submitted and would be delivered to recipients shortly.