Binary addition in logarithmic space (source code)

= Binary addition in logarithmic space

For canonical positive <binary numeral system> inputs, a <logspace transducer> can emit the canonical representation of their <sum> most significant digit first. Count the operand lengths, compute the final <arithmetic carry> to determine output length, and then compute each requested result digit by restarting the least-significant-first column recurrence. Each pass uses only a fixed number of $O(\log n)$-<bit> indices and one <arithmetic carry>. The <binary-addition carry invariant> proves correctness. <Logspace composition by recomputation> consequently permits any <L> property of the resulting digit <string>, including being a <binary palindrome>, to be tested without storing the sum.