[FOM] Is Wolfram and Cook's (2, 5) Turing machine really universal?

[Dominic Hughes]

Dear Matthew,

I'm looking for a rigorous *proof* of weak universality.  By *proof* I
mean something a young undergraduate could work through centuries from
now, long after we're all dead and gone, and be 100% convinced of the
result.  Neary and Woods are refreshingly honest about the lack of a
rigorous proof in their 2009 paper:

  ... our example is sufficiently general to prove that our machines
  simulate Turing machines via Rule 110 and we do not give a full (and
  possibly tedious) proof of correctness.

All I was asking FOM is: Is it worth my while to (attempt to) construct
such a proof?

I come from a mathematical tradition in which a proof is a pyramid of
lemmas and proposition, capped by a theorem.  Each stone of the pyramid is
self-contained enough and small enough to be verifiable by the reader.
I'd point to the proof of Fermat's Last Theorem as exemplary.  By writing
everything down in detail by 1993, a critical bug was caught, and repaired
by the time of the final Annals of Mathematics publication(s) in 1995.

While I, like you, am 100% convinced that these machines are indeed weakly
universal, our personal opinions (and examples) don't amount to a rigorous
proof.

To clarify the style of proof I'd be working towards if I continued with
this project, see (for example) page 4 of this Annals of Mathematics
paper, which shows a dependency diagram of twelve lemmas, propositions and
theorems:

  http://arxiv.org/pdf/math/0408282v3

Addressing weak universality in a similarly rigorous fashion will be a lot
of work.  Based on comments I've received so far (privately and on FOM), I
sense that the return-on-investment ratio

      credit for a rigorous proof
     -----------------------------
      effort for a rigorous proof

is rather low, so I doubt I'll resuscitate this old project.

Thanks for your feedback,

Dominic

PS Your version of the wrap construction seems as intricate as mine ---
from the point of view of a rigorous correctness proof.

On Tue, 18 Sep 2012, Matthew Cook wrote:

> > (a) The authors only provide an example run of a simulation on the
> >    so-called "ether" of Rule 110.
> >
> > (b) One must provide a construction which simulates Rule 110 on initial
> >    states with periodic words induced by the underlying cyclic tag
> >    system.
> >
> > There is a vast gap between (a) and (b).
>
> Actually there is no gap, because an initial state of (b) consists of gliders traveling in the ether of (a).  That is, the initial states needed for the proof contain plenty of ether, and the TM can bounce (change direction) in these ether regions exactly as in the "pure ether" examples.
>
> Doing this in practice is very easy.  For example, you can take the repeating word for the left hand side in Rule 110, and replace an occurrence of 10011011111000 with 100²0100²0100²0, and the result is a fine left hand word for the TM.  Hardly an intricate construction.  The right hand side is similar.
>
> I think you are right that the simple description in Wolfram's book of how to do emulations with 0s on the right and 0²s on the left may at first appear to be insufficient for emulation with arbitrary patterns.  Wolfram probably chose this example emulation for its simplicity.  However, it turns out to be easy to extend this example to arbitrary patterns.  As I put it in one paper, "Encoding the Rule 110 initial state into an initial tape for these Turing machines is fairly direct and we will not discuss the details of these transformations."
>
> > Hopefully the wrap construction can be tweaked to provide proofs of (weak)
> > universality for the three beautiful machines conjectured to be (weakly)
> > universal by Neary and Woods (2007).
>
> I think the paper of Neary and Woods is extremely clear in demonstrating how their machines work in the weak setting and why they are universal.  I would definitely refer to their universality as proven, not conjectured.
>
> Matthew
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>

http://boole.stanford.edu/~dominic