Quadratic schoolbook binary addition

The existing NatAdd.addStep fold consumes the first input's bits and the remaining bits of the second input, emitting one sum digit per round. A second consuming fold adds the carry to the remaining second input. Both folds have linear-sized states and linear-cost rounds, so addition takes quadratic time and independent linear output-charged workspace in the encoded input length. No iteration by the numeric operands or normalization of the result is needed.

Main results

• ComputableInO.natAdd: binary addition in quadratic time and linear charged workspace.

theorem Turing.MultiTapeTM.ComputableInO.natAdd : ComputableInO (fun (p : ℕ × ℕ) => p.1 + p.2) (encPair encNat encNat) encNat (fun (p : ℕ × ℕ) => (((encPair encNat encNat) p).length + 1) ^ 2) fun (p : ℕ × ℕ) => ((encPair encNat encNat) p).length + 1

Binary addition, using the existing consuming carry folds. Time is quadratic and charged workspace linear in the framed input length, independently of the numeric operands.