The successor in binary

encNat, reexported from Encodings.Nat.Bits, encodes a natural number by its binary digits, least significant first (Nat.bits). The successor is computed by one streaming transducer whose state is the carry: on each digit b in carry c it emits c ^^ b and keeps the carry c && b, and at the end it emits a final 1 exactly when a carry remains. The machine reads its input once and uses no work tape.

Main results

• Turing.MultiTapeTM.computableInTimeAndSpace_succ: the successor is computable within 2 * (encNat n).length + 3 steps and zero work space.
• Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.natSucc: its linear form.

@[reducible, inline]

abbrev Turing.MultiTapeTM.encNat3 : ℕ × ℕ × ℕ ↪ List Bool

The framed binary encoding of triples of natural numbers.

theorem Turing.MultiTapeTM.computableInTimeAndSpace_succ : ComputableInTimeAndSpace (fun (x : ℕ) => x + 1) encNat encNat (fun (n : ℕ) => 2 * (encNat n).length + 3) fun (x : ℕ) => 0

Binary successor in linear time and zero work space. One streaming transducer computes n + 1 from encNat n within 2 * (encNat n).length + 3 steps without work tapes.

theorem Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.natSucc : ComputableInLinearTimeAndSpace (fun (x : ℕ) => x + 1) encNat encNat

Binary successor in linear time and work space, from computableInTimeAndSpace_succ.