Fidgeting Symbolically with Powers of 2

I was thinking about expressions built from 0, 1+, 2* and 2^. I might throw in a variable at some point. I want to answer two questions:

• is it zero or a successor (and if the latter, of what)?
• is it even or odd (and what’s its rounded down half)?

0 is both zero and twice 0. Good.

By design, these questions directly invert one each of 1+ and 2*. Meanwhile, 2* preserves zero-versus-successor, with 2*(1+n) = 1+1+2*n. And 1+ inverts parity: 1+2*h is odd with rounded down half h; 1+(1+2*h) is even, with rounded down half 1+h.

Also by design, answering even-or-odd for 2^n amounts to answering zero-or-successor for n: 2^(1+n) = 2*2^n. Moreover, we know 2^n is a successor. But what’s its predecessor? It doesn’t especially help to know whether n is zero or successor. We don’t have general addition, only successor, and we have nothing like subtraction.

Ouch! By which I mean this little language of expression succs.

I have no easy way to get my hands on 2^n-1. Let’s fix that. Consider instead the operation 2^-n = 2^n-1. So 2^-0=0, 2^-1=1, 2^-2=3. 2^-n is the biggest n-bit unsigned number.

Is 2^-n zero-or-successor? Depends on the same for n. 2^-0 = 0 and 2^-(1+n) = 2^(1+n) – 1 = 2*2^n – 1 = 2*(1+(2^n-1)) -1 = (2+2*(2^n-1)) -1 = 1+2*(2^n-1) = 1+2*2^-n.

Is 2^-n even or odd? Depends on whether n is zero-or successor. 2^-0 = 2*0, definitely even, and 2^-(1+n) = 2^(1+n)-1 = 2*2^n-1 = 2*(1+2^n-1)-1 = 2+2*(2^n-1)-1 = 1+2*2^-n, definitely odd.

That is, the language generated by 0, 1+, 2* and 2^- allows us a compositional symbolic way to compute both zero-or-successor and even-or-odd.

Thankfully, 2^n = 1+2^-n remains obviously even if n is even. Check 2^(1+n) = 1+2^-(1+n) = 1+1+2*2^-n = 2*(1+2^-n) = 2*2^n.

Note that these operations are all unary. So if we’re going to throw in variables, we need consider at most one variable. We don’t know whether a variable is zero-or-successor or even-or-odd, so we can get stuck figuring that out. But sometimes we’ll get lucky: 1+n is definitely a successor and 2*n is definitely even. And if we get lucky, we definitely stay lucky, whatever you substitute for the variable (doing the same substitution to the predecessor or the rounded down half).

So I wonder if this is a nice language of sizes for widths of vectors allowing cons, snoc, and binary chop.

(Thinking about it, the sweetness comes from the fact that when 2^-n is a successor, it is in particular an odd successor.)