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 (or as less than or equal); equality by one that remembers whether they agree. Both run 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.computableInTimeAndSpace_natLe, Turing.MultiTapeTM.computableInTimeAndSpace_natEq: non-strict comparison and equality within the same bounds.
• Turing.MultiTapeTM.ComputableInDegree.natLt, .natLe, .natEq: their linear forms.
• 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.ComputableInDegree.natLt : ComputableInDegree (fun (p : ℕ × ℕ) => decide (p.1 < p.2)) (encPair encNat encNat) encBool 1 1

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

theorem Turing.MultiTapeTM.computableInTimeAndSpace_natLe : 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

Non-strict 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.ComputableInDegree.natLe : ComputableInDegree (fun (p : ℕ × ℕ) => decide (p.1 ≤ p.2)) (encPair encNat encNat) encBool 1 1

Non-strict binary comparison in linear time and work space, from computableInTimeAndSpace_natLe.

theorem Turing.MultiTapeTM.computableInTimeAndSpace_natEq : 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 equality 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.ComputableInDegree.natEq : ComputableInDegree (fun (p : ℕ × ℕ) => decide (p.1 = p.2)) (encPair encNat encNat) encBool 1 1

Binary equality in linear time and work space, from computableInTimeAndSpace_natEq.

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.