Normalization of expansions in more exotic numeration systems - Walnut-Theorem-Prover/Walnut GitHub Wiki

Here are some notes about how to "normalize" expansions in more exotic numeration systems, such as Fibonacci, Tribonacci, or a custom numeration system you can design and use with Walnut.

Start with the Fibonacci (or "Zeckendorf") numeration system as an example. In this numeration system, digits have the values 1,2,3,5,8,13,..., the Fibonacci numbers. A binary string represents a natural number in exactly the same way as in base 2, except we use the Fibonacci numbers (largest first) as values of digits, instead of (say) the powers of 2. However, this can result in numbers having two different representations. The number 3, for example, could be written either as 100 or 11. To guarantee unique representations, we impose a rule: a binary string in this system must not contain any occurrence of the block 11.

Now, sometimes it is useful to allow representations that violate this rule. In this case, since Walnut expects numbers to be represented obeying the rule, we need a "normalizer". This is an automaton that takes two inputs, v and n, in parallel. Here v is an arbitrary binary string, and n is a number in Fibonacci representation. The normalizer should accept the input (v,n) if v, evaluated in the numeration system, gives the same result as n. For example, an input [0,1][1,0][1,0] should be accepted because v=011 which evaluates to 3 and n=100 which also evaluates to 3.

Here is a way to "automatically" get a normalizer. The idea is to take v and split it into two pieces x and y, each of which obeys the rule of the numeration system (here, no occurrence of 11), and then assert that n=x+y.

Here is one way to split x into two pieces appropriately: make one automaton that takes every 2nd 1 appearing in v, starting with the first, and the other that takes every 2nd 1, starting with the second. We can do this as follows:

reg mod1 msd_2 msd_fib "[0,0]*([1,1][0,0]*[1,0][0,0]*)*(()|[1,1][0,0]*|[1,1][0,0]*[1,0][0,0]*)":

(retain 1st1, 3rd 1, 5th 1, etc.)

reg mod2 msd_2 msd_fib "[0,0]*([1,0][0,0]*[1,1][0,0]*)*(()|[1,0][0,0]*|[1,0][0,0]*[1,1][0,0]*)":

(retain 2nd 1, 4th 1, 6th 1, etc.)

def normalize "?msd_fib Ex,y $mod1((?msd_2 v),x) & $mod2((?msd_2 v),y) & z=x+y":

Here we treat v as if it were a number in base 2. If needed, we can use the alphabet command of Walnut to change the declared alphabet to {0,1}.

For Tribonacci we would need to break up v into three pieces.