Conjecture about two counters automata

Question

I would like to prove (or disprove) the following conjecture:

Conjecture: a two counter automata (2CA) cannot decide the following language:

$L = \{ n \mid $ the ternary and binary representations of $n$ have both even length or odd length$\}$

A 2CA can easily check if the binary representation has even or odd length (just keep dividing by two and update an "even length" flag after each division); in the same manner it can check if the ternary representation has even or odd length (just keep dividing by three and update an "even length" flag after each division).

But in order to calculate one of them it must destroy its input, and cannot recover it to calculate the other; so it seems that there is no way to decide $L$.

Do you know a technique that can be used to prove the conjecture?
Or can you disprove the conjecture building a 2CA that decides $L$?

I tried the same approach followed by Ibarra to prove that a 2CA cannot decide $\{n^2\mid n \geq 1\}$, but it seems not the right way.

Note: for simplicity a 2CA is equivalent to a program with one variable $c$ that initially contains the input and the following instruction set:

• INC: add one to the variable;
• DEC: decrement $c$ (only if it is greater than zero);
• JZ $lab$: if $c$ is zero jump to label $lab$ otherwise continue;
• MUL $K$: multiply $c$ by the costant $K$;
• DIV $K [, lab_0, lab_1,...,lab_{K-1}]$: divide $c$ by the constant $K$ and store the quotient to $c$ ($c = \lfloor c / K \rfloor$); possibly jump to different labels according to the remainder ($c \bmod K$);
• GOTO $lab$: unconditional jump;
• HALT Accept|Reject: halt and accept or halt and reject.

For example a program to check if the binary representation of $n$ has even length is:

   loop: JZ even   // test if n = 0
         DIV 2
         JZ odd    // test if n = 0
         DIV 2
         GOTO loop
   even: HALT Accept
    odd: HALT Reject

(we can build an equivalent 2CA)

Answer 1

So people keep nagging me to post this even though it only solves a simplified version of the problem. Okay then :)

At the end of this, I will put some of what I learned from the paper of Ibarra and Trân, and why that method breaks down on our general problem, but perhaps still gives some useful information.

But first, we'll look at the simpler problem of trying to decide the set

$L = \{ 2^n \mid $ the ternary and binary representations of $2^n$ have both even length or odd length$\}$

Note how this has $2^n$ rather than $n$ as in the original problem. In particular if the input number is not a power of 2, we want to reject it rather than attempt to calculate its length in any base.

This greatly simplifies matters: If the original number is written prime factorized as $2^{v_2} 3^{v_3} 5^{v_5} 7^{v_7} ...$, then for all the $v_i$ except $v_2$ we just need to check that they are all $0$.

This allows us to solve this simplified problem by using a wrapper around the old method (by Minsky I assume) of encoding the state of a $k$-counter automaton in the exponents of the prime factorization of the single variable of a multiplication/division automaton, which as noted in the OP above is pretty much equivalent to a 2-counter automaton.

First, we need a $k$-counter automaton to wrap. We will use 3 counters, named $v_2$, $v_3$ and $v_5$.

The automaton will accept iff for the initial counter values, the ternary and binary representations of $2^{v_2}$ have both even length or odd length, and both $v_3$ and $v_5$ are zero. When it accepts it will first zero all its counters.

Here is some code for that, in an assembly format similar to the OP (I've just added variables to the instructions). I haven't actually tested it, since I have nothing to run it with, but I consider this a formality: 3-counter automata are well known to be Turing-complete, and to be able to construct any computable function of one of their initial values.

// Check that v3 and v5 are both zero.
                JZ v3, check5
                GOTO reject
check5:         JZ v5, init3
                GOTO reject
// Decrement v2 until it is zero, constructing 2^n in the process.  If 2^n
// was even, we will then pass to even2 with 2^n in v3; If 2^n was odd, we
// will pass to odd2 with 2^n in v5.
init3:          INC v3          // Set v3 to 1 = 2^0 to start with.
even1:          // We have decremented v2 an even number of times so far.
                // 2^decremented amount is in v3.
                JZ v2, odd2
                DEC v2
dup3to5:        JZ v3, odd1
                DEC v3
                INC v5
                INC v5
                GOTO dup3to5
odd1:           // We have decremented v2 an odd number of times so far.
                // 2^decremented amount is in v5.
                JZ v2, even2
                DEC v2
dup5to3:        JZ v5, even1
                DEC v5
                INC v3
                INC v3
                GOTO dup5to3
// The second part checks the ternary length of 2^n, which starts out in v3
// or v5 according to whether the *binary* length of 2^n (i.e. n+1) was odd
// or even.
odd2:           // v3 needs to have odd ternary length to accept.
                // It is simplest to consider 0 to have even length in both
                // binary and ternary.  This works out as long as we're
                // consistent.
                JZ v3, reject
trisect3to5:    DEC v3
                DEC v3
                JZ v3, even2
                DEC v3
                INC v5
                GOTO trisect3to5
even2:          // v5 needs to have even ternary length to accept
                JZ v5, accept
trisect5to3:    DEC v5
                DEC v5
                JZ v5, odd2
                DEC v5
                INC v3
                GOTO trisect5to3
accept:         HALT Accept
reject:         HALT Reject

The next step is then to re-encode the above in the exponents of a single variable automaton. As the result is pretty long, I'll just describe the general method, but a full version (slightly "optimized" in spots) is on my website.

                JZ vp, label
                DEC vp
next:           ...

becomes (basically divide by p, and then do cleanup to undo if the division wasn't even):

                DIV p, next, ..., newlabel.fp-1
newlabel.f1:    MUL p
                GOTO newlabel.i1
...
newlabel.fp-1:  MUL p
                INC
newlabel.ip-2:  INC
...
newlabel.i1:    INC
                GOTO label
next:           ...

INC vp becomes MUL p. Individual JZ and DEC can first be changed into the combined form. GOTO label and HALT Reject are unchanged.

HALT Accept would be unchanged, except that in our case we still have one final check to do: we need to ensure that there are no prime factors in the number other than 2,3 and 5. Since our particular 3-counter automaton zeros the counters it uses when it accepts, this is simple: just test that the final variable is 1, which can be done by jumping to the code

                DEC     // BTW it cannot be zero before this.
                JZ accept
                HALT Reject
accept:         HALT Accept

The code on my website also has an initial check that the number isn't zero, which I've just realized is redundant with the v3, v5 zero checks, oh well.

As I mentioned, the above method works for the simplified problem, but it really has no chance of working for the general one, because: In the general problem the precise value of every prime's exponent counts for deciding its general size and thus which lengths it has in various bases. This means that:

• We have no "free" primes to use for counters.
• Even if we did have free primes for counters, we don't really have a way to extract all the necessary information from the infinitely many other primes whose exponent values do matter.

So let's end with an explanation of the gist of the general method from the above linked paper by Ibarra and Trân (freely downloadable version) for how to prove that certain problems aren't solvable by a 2CA, and how it annoyingly breaks down in our case.

First, they modify every 2CA into a "normal form", in which the two counters switch in "phases" between one only increasing and the other only decreasing until it reaches zero. The number of states $s$ of this normalized automaton plays an important role in the estimates.

Then, they analyze this automaton to conclude that they can construct certain arithmetic sequences of numbers whose behavior are linked. To be precise (Some of this is not stated as theorems, but is implicit in the proof of both of their two main examples):

1. If a number x is accepted by the automaton, without the size $v^x_i$ of the nonzero counter at the beginning of a phase $i$ ever going $\leq s$, then there exists an integer $D>0$ such that all the numbers $x + n D$, $n\geq 0$ are accepted.

2. If a set $X$ contains at least $s^2+1$ accepted numbers such that for each number $x\in X$ there is a phase $i$ such that $v^x_i\leq s$, then we can find $p, r\in X$, and integers $K_1,K_2$ such that

   • For every integer $n\geq 0$, either $p + n K_1$ and $r + n K_2$ are both accepted by the automaton, or both are rejected.

(Thoughts:

• They require $x>s$ for $x\in X$ but I think this is actually unnecessary. Actually so is that they are accepted.
• Most of this should also hold for rejected numbers, as long as the rejection is by explicit halting rather than nontermination.)

For their own examples they also frequently use the fact that $D,K_1,K_2$ have no prime factors $>s$. To prove impossibility, they then derive contradictions by showing that such arithmetical sequences cannot exist.

In our problem, getting a contradiction from this breaks down with the second case. If we have $K_1 = K_2 = 6^k$, where $k$ is large enough that no number between $p$ and $r$ is divisible by either $2^k$ or $3^k$, then there will also be no powers of 2 or 3 between $p + 6^k n$ and $q + 6^k n$, so they are either both accepted or both rejected.

Point 1 can still be shown to be impossible, because powers of 2 and 3 mostly grow further and further apart. And I believe I can show the second case impossible if $K_1\neq K_2$ (I've emailed @MarzioDeBiasi the argument). So perhaps someone could use this information to restrict the form of the automaton further, and finally derive a contradiction from that.