Binary digit access in linear work space

A bit of a binary natural is obtained by iterating the tail of its binary encoding and reading its head, with a missing bit read as false. Every intermediate word is a suffix of the input word. The iteration count is binary; its value is not charged as work space.

This proof was extracted unchanged from Christian Reitwiessner's tree-evaluation reader so that numeric algorithms can reuse it without depending on tree evaluation.

Main results

• Turing.MultiTapeTM.ComputableInSpace.natTestBit: binary digit access in work space linear in the binary encodings of both the value and the index.

References

• N. Immerman, Descriptive Complexity, proof of Theorem 3.1.

theorem Turing.MultiTapeTM.ComputableInSpace.natTestBit : ComputableInSpace (fun (q : ℕ × ℕ) => q.1.testBit q.2) (encPair encNat encNat) encBool fun (q : ℕ × ℕ) => 32 * (((encPair encNat encNat) q).length + 1)

A bit of a binary natural, k.testBit j from (k, j).

theorem Turing.MultiTapeTM.ComputableTidilyInSpace.natTestBit : ComputableTidilyInSpace (fun (q : ℕ × ℕ) => q.1.testBit q.2) (encPair encNat encNat) encBool fun (q : ℕ × ℕ) => 32 * (((encPair encNat encNat) q).length + 1)

A bit of a binary natural, k.testBit j from (k, j).