Notes on constant multiplication in Walnut - Walnut-Theorem-Prover/Walnut GitHub Wiki

Jeffrey Shallit

February 20 2025

When you write an expression like

$f(46*n)

in Walnut how is it carried out? "Behind the scenes" what is going on is that first an automaton of two inputs, n and x, is created, such that it accepts if and only if x = 46*n. If we call this automaton $m46 then $f(46*n) becomes

Ex $m46(n,x) & $f(x)

So the question then becomes, how is an automaton like $m46 constructed?

Method 1

simple iteration (don't use this!)

def m2 "z=n+n":
def m3 "Ex $m2(n,x) & z=x+n":
def m4 "Ex $m3(n,x) & z=x+n":
def m5 "Ex $m4(n,x) & z=x+n":
def m6 "Ex $m5(n,x) & z=x+n":
...
def m45 "Ex $m44(n,x) & z=x+n":
def m46 "Ex $m45(n,x) & z=x+n":

which is clearly not the most efficient.

Method 2

The "old" Walnut used the binary method or "Russian peasant" method as follows:

To multiply by $k$, recursively compute intermediate automata for multiplication by $\left\lfloor \frac{k}{2} \right\rfloor$ and $\left\lceil \frac{k}{2} \right\rceil$, then add the results. Thus, for multiplication by 46, it would do what amounts to

def m2 "z=n+n":
def m3 "Ex,y $m2(n,x) & z=x+n":
def m5 "Ex,y $m2(n,x) & $m3(n,y) & z=x+y":
def m6 "Ex,y $m3(n,x) & $m3(n,y) & z=x+y":
def m11 "Ex,y $m5(n,x) & $m6(n,y) & z=x+y":
def m12 "Ex,y $m6(n,x) & $m6(n,y) & z=x+y":
def m23 "Ex,y $m11(n,x) & $m12(n,y) & z=x+y":
def m46 "Ex,y $m23(n,x) & $m23(n,y) & z=x+y":

The problem with this is that it forces an "and" between two automata for multiplication by about $\left\lfloor \frac{n}{2} \right\rfloor$ in the last step, which means that we could end up possibly squaring the number of states.

Method 3

The "new" Walnut uses a variation of this that avoids two variables in the quantifier:

def m2 "z=n+n":
def m4 "Ex $m2(n,x) & $m2(x,z)":
def m5 "Ex $m4(n,x) & z=x+n":
def m10 "Ex $m5(n,x) & $m2(x,z)":
def m11 "Ex $m10(n,x) & z=x+n":
def m22 "Ex $m11(n,x) & $m2(x,z)":
def m23 "Ex $m22(n,x) & z=x+n":
def m46 "Ex $m23(n,x) & $m2(x,z)":

This can have a very big difference in computing times, particularly when the automaton for computing the addition relation is slow, as is the case in "exotic" numeration systems like Tribonacci.

Comparison

For example, here are some computing times for Tribonacci:

Method 1

def m2 "?msd_trib z=n+n":
def m3 "?msd_trib Ex $m2(n,x) & z=x+n":
def m4 "?msd_trib Ex $m3(n,x) & z=x+n":
def m5 "?msd_trib Ex $m4(n,x) & z=x+n":
def m6 "?msd_trib Ex $m5(n,x) & z=x+n":
def m7 "?msd_trib Ex $m6(n,x) & z=x+n":
def m8 "?msd_trib Ex $m7(n,x) & z=x+n":
def m9 "?msd_trib Ex $m8(n,x) & z=x+n":
def m10 "?msd_trib Ex $m9(n,x) & z=x+n":
def m11 "?msd_trib Ex $m10(n,x) & z=x+n":
def m12 "?msd_trib Ex $m11(n,x) & z=x+n":
def m13 "?msd_trib Ex $m12(n,x) & z=x+n":
def m14 "?msd_trib Ex $m13(n,x) & z=x+n":
def m15 "?msd_trib Ex $m14(n,x) & z=x+n":
def m16 "?msd_trib Ex $m15(n,x) & z=x+n":
def m17 "?msd_trib Ex $m16(n,x) & z=x+n":
def m18 "?msd_trib Ex $m17(n,x) & z=x+n":
def m19 "?msd_trib Ex $m18(n,x) & z=x+n":
def m20 "?msd_trib Ex $m19(n,x) & z=x+n":
def m21 "?msd_trib Ex $m20(n,x) & z=x+n":
def m22 "?msd_trib Ex $m21(n,x) & z=x+n":
def m23 "?msd_trib Ex $m22(n,x) & z=x+n":
def m24 "?msd_trib Ex $m23(n,x) & z=x+n":
def m25 "?msd_trib Ex $m24(n,x) & z=x+n":
def m26 "?msd_trib Ex $m25(n,x) & z=x+n":
def m27 "?msd_trib Ex $m26(n,x) & z=x+n":
def m28 "?msd_trib Ex $m27(n,x) & z=x+n":
def m29 "?msd_trib Ex $m28(n,x) & z=x+n":
def m30 "?msd_trib Ex $m29(n,x) & z=x+n":
def m31 "?msd_trib Ex $m30(n,x) & z=x+n":
def m32 "?msd_trib Ex $m31(n,x) & z=x+n":
def m33 "?msd_trib Ex $m32(n,x) & z=x+n":
def m34 "?msd_trib Ex $m33(n,x) & z=x+n":
def m35 "?msd_trib Ex $m34(n,x) & z=x+n":
def m36 "?msd_trib Ex $m35(n,x) & z=x+n":
def m37 "?msd_trib Ex $m36(n,x) & z=x+n":
def m38 "?msd_trib Ex $m37(n,x) & z=x+n":
def m39 "?msd_trib Ex $m38(n,x) & z=x+n":
def m40 "?msd_trib Ex $m39(n,x) & z=x+n":
def m41 "?msd_trib Ex $m40(n,x) & z=x+n":
def m42 "?msd_trib Ex $m41(n,x) & z=x+n":
def m43 "?msd_trib Ex $m42(n,x) & z=x+n":
def m44 "?msd_trib Ex $m43(n,x) & z=x+n":
def m45 "?msd_trib Ex $m44(n,x) & z=x+n":
def m46 "?msd_trib Ex $m45(n,x) & z=x+n":
Total time:  514522 ms

Method 2

def m2 "?msd_trib z=n+n":
def m3 "?msd_trib Ex $m2(n,x) & z=x+n":
def m5 "?msd_trib Ex,y $m2(n,x) & $m3(n,y) & z=x+y":
def m6 "?msd_trib Ex,y $m3(n,x) & $m3(n,y) & z=x+y":
def m11 "?msd_trib Ex,y $m5(n,x) & $m6(n,y) & z=x+y":
def m12 "?msd_trib Ex,y $m6(n,x) & $m6(n,y) & z=x+y":
def m23 "?msd_trib Ex,y $m11(n,x) & $m12(n,y) & z=x+y":
def m46 "?msd_trib Ex,y $m23(n,x) & $m23(n,y) & z=x+y":
Total time:   47454 ms

Method 3

def m2 "?msd_trib z=n+n":
def m4 "?msd_trib Ex $m2(n,x) & $m2(x,z)":
def m5 "?msd_trib Ex $m4(n,x) & z=x+n":
def m10 "?msd_trib Ex $m5(n,x) & $m2(x,z)":
def m11 "?msd_trib Ex $m10(n,x) & z=x+n":
def m22 "?msd_trib Ex $m11(n,x) & $m2(x,z)":
def m23 "?msd_trib Ex $m22(n,x) & z=x+n":
def m46 "?msd_trib Ex $m23(n,x) & $m2(x,z)":
Total time:   24300 ms

Conclusion

I find it difficult to estimate the savings of method 2 over method 3 precisely because we would need to know the structure of the resulting automata, and their number of states, for each numeration system, and I don't think this is even known for Fibonacci (although there is a conjecture for that numeration system).

There might be some other approaches which would speed up things even more in practice, but it's not clear they are worth doing:

For msd_k, it is possible to directly create an automaton accepting both n and k*n in parallel, with k states, in time linear in k. It might be slightly more efficient to implement this directly for base k. But it is not clear how much it is needed, since (for example) for msd_2 we can do this for k=1000 in just 24 ms, so little gain can be expected.
For other numeration systems, more states are needed. Fibonacci seems to need $\theta\left(k^2\right)$, Tribonacci $\theta\left(k^3\right)$, and so forth, but even this has not been proved. In this case it might possibly be worthwhile computing the intermediate results like $m5 and storing them in a file for future use by later runs of Walnut, so they don't need to be recomputed. You'd have to have some sort of privileged namespace used just by Walnut for this.
The choices we presented here are between doubling (going from k to 2k) or adding 1 (going from k to k+1). One could also go from k to k-1, so (for example) multiplication by 15 could be done by 4 doubling steps follows by a single subtraction, which would likely be faster. One could try to optimize the choice between these three steps.

For optimal methods for a lot of k, see the shortest additions chains article.