Binary subtraction and comparison

The existing borrow algorithm runs through consuming input-word cursors, so every round costs only a linear amount and there are at most as many rounds as input digits. The plain machine certificate retains quadratic time and linear output-charged workspace, independently of the numeric operands.

Comparison is computed by one zip transducer (Turing.MultiTapeTM.ZipTransducer) that reads both operands in lockstep, least significant digit first, and remembers whether the digits read so far compare as less than. It runs in linear time and in work space linear in the first operand.

Main results

• ComputableInO.natSub: truncated subtraction in quadratic time and linear charged space.
• Turing.MultiTapeTM.computableInTimeAndSpace_natLt: strict comparison within 3 * (encPair encNat encNat p).length + 1 steps and (encNat p.1).length + 2 work-tape cells.
• Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.natLt: its linear form.
• ComputableInO.natLt: strict comparison with the bounds of ComputableInO.natSub.

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

Binary comparison in linear time. One zip transducer decides 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.ComputableInLinearTimeAndSpace.natLt : ComputableInLinearTimeAndSpace (fun (p : ℕ × ℕ) => decide (p.1 < p.2)) (encPair encNat encNat) encBool

Binary comparison in linear time and work space, from computableInTimeAndSpace_natLt.

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

Truncated subtraction in binary, b - a from (a, b).

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

The strict order in binary, from the linear zip-transducer certificate Turing.MultiTapeTM.computableInTimeAndSpace_natLt.