The successor, predecessor and zero test in binary

encNat, reexported from Encodings.Nat.Bits, encodes a natural number by its binary digits, least significant first (Nat.bits). Each of the three counter operations is computed by one streaming transducer that reads its input once and uses no work tape:

• the successor's 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 predecessor turns the borrowed 0s into 1s and the first 1 into a 0, which it holds back until a further digit shows that it is not the leading digit, and then copies the rest;
• the zero test emits whether the input was empty.

Main results

• Turing.MultiTapeTM.computableInTimeAndSpace_succ, computableInTimeAndSpace_pred, computableInTimeAndSpace_isZero: the operations are computable within 2 * (encNat n).length + 3 steps and zero work space.
• Turing.MultiTapeTM.ComputableInDegree.natSucc, .natPred, .natIsZero: their linear forms.

@[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.ComputableInDegree.natSucc : ComputableInDegree (fun (x : ℕ) => x + 1) encNat encNat 1 1

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

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

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

theorem Turing.MultiTapeTM.ComputableInDegree.natPred : ComputableInDegree (fun (x : ℕ) => x - 1) encNat encNat 1 1

Binary predecessor in linear time and work space, from computableInTimeAndSpace_pred.

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

Binary zero test in linear time and zero work space. One streaming transducer decides n = 0 from encNat n within 2 * (encNat n).length + 3 steps without work tapes.

theorem Turing.MultiTapeTM.ComputableInDegree.natIsZero : ComputableInDegree (fun (n : ℕ) => decide (n = 0)) encNat encBool 1 1

Binary zero test in linear time and work space, from computableInTimeAndSpace_isZero.