TAOCP 7.1.3 Exercise 17
An expression $E(x_1,\ldots,x_m)$ is built from integer variables and integer constants using only $+$ and $\oplus$ (and possibly also $&$ in the second part).
Section 7.1.3: Bitwise Tricks and Techniques
Exercise 17. [HM36] The results of exercise 16 make it possible to decide whether or not any two given animating functions are equal. Is there an algorithm that decides whether any given expression is identically zero, when that expression is constructed from a finite number of integer variables and constants using only the binary operations $+$ and $\oplus$? What if we also allow $&$?
Verified: no
Solve time: 1m07s
Setup
An expression $E(x_1,\ldots,x_m)$ is built from integer variables and integer constants using only $+$ and $\oplus$ (and possibly also $&$ in the second part). Two expressions are considered identical if they define the same function on all integers.
Each integer is viewed as an infinite binary string $(\ldots x_2 x_1 x_0)_2$, so operations are interpreted bitwise with carries for $+$, and coordinatewise for $\oplus$ and $&$.
The problem is to decide whether a given expression is identically zero.
Solution
The key point is that every such expression induces a digit-wise computation on binary expansions with only finitely many possible “memory states” at each bit position. This makes the induced function representable by a finite automaton acting on binary representations.
The operation $\oplus$ acts independently on each bit position by $0 \oplus 0 = 0$, $0 \oplus 1 = 1$, $1 \oplus 0 = 1$, $1 \oplus 1 = 0$, so it introduces no interaction between bit positions.
The operation $&$ also acts independently on each bit position by $0 & 0 = 0$, $0 & 1 = 0$, $1 & 0 = 0$, $1 & 1 = 1$, so it likewise introduces no interaction between bit positions.
The operation $+$ is the only source of dependence between bits. When computing $x + y$ in binary, the $k$-th output bit depends on $x_k$, $y_k$, and the carry $c_k \in {0,1}$, and produces a new carry $c_{k+1} \in {0,1}$. Thus addition is governed by a finite-state transition system with exactly two carry states.
Now consider an arbitrary expression $E$. Each subexpression $F$ induces a function of the input bits together with a finite amount of carry information arising from additions appearing inside $F$. We proceed by structural induction on the syntax tree of $E$.
For a variable or constant, no carry state is required. For $F \oplus G$ and $F & G$, the value of each output bit depends only on the corresponding bits of $F$ and $G$, so the state needed to compute $F \star G$ is the product of the states needed for $F$ and $G$, still finite.
For $F + G$, at each bit position the computation depends on the triple consisting of the current bit outputs of $F$ and $G$ together with a carry bit in ${0,1}$. If $F$ and $G$ are already computable by finite-state machines producing their bits synchronously, then adding them introduces only one additional binary state for the carry, so the combined system remains finite-state.
Thus every subexpression defines a function whose evaluation at bit position $k$ depends only on $k$ and a finite state depending on previous bits. Consequently, the entire expression defines a function computed by a finite-state transducer on binary inputs.
A finite-state transducer over binary digits induces a regular relation between input and output binary expansions. In particular, the set of inputs on which the output is nonzero is a regular set of binary sequences. Emptiness of a regular set is decidable, since it reduces to reachability of an accepting state in the underlying finite automaton.
To decide whether $E$ is identically zero, construct the finite automaton that computes the output bits of $E$ and tracks whether any output bit is nonzero. This requires augmenting the state space with a flag indicating whether a $1$ has appeared in any output position. The resulting automaton is finite because it is built from finitely many subexpressions, each contributing only finitely many states and at most one carry bit per addition.
The expression $E$ is identically zero if and only if this automaton has no accepting run producing a $1$ in any output position. This condition is decidable by standard graph reachability in a finite directed graph.
If $&$ is also allowed, the argument is unchanged because $&$ is bitwise and introduces no additional carry states. All states remain finite, and the same construction yields a finite automaton.
This completes the proof. ∎
Verification
Each operation in $\oplus$ and $&$ is purely coordinatewise, so no inter-bit dependency arises from these operations. The only propagation mechanism is the carry in addition, and that carry takes exactly two values at each step. Since any finite composition of additions introduces only finitely many simultaneous carry variables, the total state space remains finite.
The constructed automaton is therefore finite, so the induced language of binary representations is regular. Regular language emptiness is decidable by finite graph reachability, which applies directly to the constructed machine.
Notes
The argument can be rephrased as the statement that expressions built from $+$, $\oplus$, and $&$ define an automatic structure over binary representations of integers. In such structures, first-order definable properties, including equality to zero of term functions, are decidable by automata-theoretic methods.