Binary addition, bitwise disjunction and multiplication

Addition and bitwise disjunction are computed by zip transducers (Turing.MultiTapeTM.ZipTransducer) that read both operands in lockstep, least significant digit first. The addition transducer keeps the carry as its state, emits one digit of the word adder NatAdd.addBits per pair of digits and the final carry at the end. The disjunction transducer emits the disjunction of each pair of digits; the longer operand ends in a one, so the output has no trailing zero. Both run in linear time and in work space linear in the first operand.

Multiplication folds the shift-and-add round NatMul.mulStep over the digits of the first factor. Its states have linear length and each round is one addition, so it takes cubic time and linear charged workspace. This is the only machine certificate for binary multiplication; the degree, space and polynomial-time forms are weakenings of it.

Main results

• Turing.MultiTapeTM.computableInTimeAndSpace_natAdd: binary addition within 3 * (encPair encNat encNat p).length + 1 steps and (encNat p.1).length + 2 work-tape cells.
• Turing.MultiTapeTM.computableInTimeAndSpace_natOr: bitwise disjunction within the same bounds.
• Turing.MultiTapeTM.ComputableInDegree.natAdd, .natOr: their linear forms.
• Turing.MultiTapeTM.ComputableInO.natAdd: binary addition in quadratic time and linear charged workspace.
• Turing.MultiTapeTM.ComputableInO.natMul: binary multiplication in cubic time and linear charged workspace.

theorem Turing.MultiTapeTM.computableInTimeAndSpace_natAdd : ComputableInTimeAndSpace (fun (p : ℕ × ℕ) => p.1 + p.2) (encPair encNat encNat) encNat (fun (p : ℕ × ℕ) => 3 * ((encPair encNat encNat) p).length + 1) fun (p : ℕ × ℕ) => (encNat p.1).length + 2

Binary addition in linear time. One zip transducer computes a + b from encPair encNat encNat (a, b) within 3 * (encPair encNat encNat p).length + 1 steps and (encNat p.1).length + 2 work-tape cells.

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

Binary addition in linear time and work space, from computableInTimeAndSpace_natAdd.

theorem Turing.MultiTapeTM.computableInTimeAndSpace_natOr : ComputableInTimeAndSpace (fun (p : ℕ × ℕ) => p.1 ||| p.2) (encPair encNat encNat) encNat (fun (p : ℕ × ℕ) => 3 * ((encPair encNat encNat) p).length + 1) fun (p : ℕ × ℕ) => (encNat p.1).length + 2

Bitwise disjunction in linear time. One zip transducer computes a ||| b from encPair encNat encNat (a, b) within 3 * (encPair encNat encNat p).length + 1 steps and (encNat p.1).length + 2 work-tape cells.

theorem Turing.MultiTapeTM.ComputableInDegree.natOr : ComputableInDegree (fun (p : ℕ × ℕ) => p.1 ||| p.2) (encPair encNat encNat) encNat 1 1

Bitwise disjunction in linear time and work space, from computableInTimeAndSpace_natOr.

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 within the quadratic clock and linear charged workspace used by its clients, from the linear zip-transducer certificate computableInTimeAndSpace_natAdd.

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

Binary multiplication by the shift-and-add fold NatMul.mulStep over the digits of the first factor. Each of the linearly many rounds adds numbers of linear length, so time is cubic and charged workspace linear in the framed input length, independently of the numeric operands.