Analysis of Taus's puzzle

gistfile1.txt

Original puzzle: https://twitter.com/tausbn/status/251686364788170752

First observation: 

If G ->* {0} implies G =>* {0}, it must be the case that if 
G -> G' and G' =>* {0} then G =>* {0}.

Proof: Given G -> G' and G' =>* {0}, we have G' ->* {0}
immediately (->* contains =>*) and G ->* {0} by direct
composition (G -> G' ->* {0}). Then we have G =>* {0} by the
assumed property.

Conversely, if G -> G' and G' =>* {0} imply G =>* {0}, then
G ->* {0} implies G =>* {0}. 

Proof. By induction on the number of steps in G ->* {0}. 

Given G ->* {0}, either G = {0} (in which case {0} =>* {0}
trivially) or G -> G' ->* {0}. By the induction hypothesis, we
have G' =>* {0}, and therefore by the assumed property  and the
fact that G -> G', we have G =>* {0}.

So, we have an equivalent statement: does G -> G', and G' => {0}
imply G => {0}?

Second observation:

It is easy to create a system in CLF such that [[G']] ~> [[G]] if
and only if G -> G' (note the change in direction).

SIGDYN ---
  step: item N * !plus N M P -o {item M * item P}.

Now, we need to characterize the *set* of states S such that
fat-arrow reduce to {0}. Then, the question becomes, is
membership in state S invariant under transitions in SIGDYN?

For this, we introduce the "nonterminals" max and gen, and the
following signature:

SIGGEN ---
  gen/done: max N -o {1}.
  gen/item: gen N -o {item N}.
  gen/step: gen N * max X * !plus N M P * !leq X M * !leq X P
             -o {gen M * gen P * max P}.

S can be characterized as a generative world, the set of
nonterminal-free states G such that (max z * gen z) ~>* G under
SIGGEN.