Bounded existential search with independent resources

A test is run on the words of a runtime unary width, retaining the context and one candidate. The search reuses the test's workspace. Its time is the number of candidates times the test-time bound and polynomial bookkeeping; its space is the test-space bound plus polynomial bookkeeping. Neither test bound has to be polynomial or monotone. The list of all candidates is used only in the specification, not stored by the native machine.

Main results

• Turing.MultiTapeTM.ComputableInO.exists_bits: streamed existential search with independent test-time and test-space bounds, plus polynomial bookkeeping.
• Turing.MultiTapeTM.IsComputable.exists_bits, Turing.MultiTapeTM.IsComputable.forall_bits: bounded existential and universal search over words of exact unary length preserve IsComputable.

theorem Turing.MultiTapeTM.ComputableInO.exists_bits {C : Type} {encC : C ↪ List Bool} {test : C × List Bool → Bool} {Tf Sf : C × List Bool → ℕ} (hf : ComputableInO test (encPair encC encBits) encBool Tf Sf) {T S : C × ℕ → ℕ} (hT : ∀ (p : C × ℕ) (w : List Bool), w.length = p.2 → Tf (p.1, w) ≤ T p) (hS : ∀ (p : C × ℕ) (w : List Bool), w.length = p.2 → Sf (p.1, w) ≤ S p) : ∃ (overhead : C × ℕ → ℕ), PolyBounded (fun (p : C × ℕ) => ((encPair encC encUnary) p).length) overhead ∧ ComputableInO (fun (p : C × ℕ) => (Cslib.BitString.enumList p.2).any fun (w : List Bool) => test (p.1, w)) (encPair encC encUnary) encBool (fun (p : C × ℕ) => (2 ^ p.2 + 1) * (overhead p + T p)) fun (p : C × ℕ) => overhead p + S p

Bounded existential search. Uniform bounds on the tests of words of width n give a single search machine for all contexts and widths. The polynomial overhead includes encoding conversion, binary counters, preparation and the retained input. Encoded outputs are charged to space, as in ComputableInO; this is not a sublinear transducer-space theorem.

theorem Turing.MultiTapeTM.IsComputable.exists_bits {C : Type} {encC : C ↪ List Bool} {test : C × List Bool → Bool} (htest : IsComputable test (encPair encC encBits) encBool) : IsComputable (fun (p : C × ℕ) => (Cslib.BitString.enumList p.2).any fun (w : List Bool) => test (p.1, w)) (encPair encC encUnary) encBool

Bounded existential search over words of exact unary length preserves IsComputable.

theorem Turing.MultiTapeTM.IsComputable.forall_bits {C : Type} {encC : C ↪ List Bool} {test : C × List Bool → Bool} (htest : IsComputable test (encPair encC encBits) encBool) : IsComputable (fun (p : C × ℕ) => (Cslib.BitString.enumList p.2).all fun (w : List Bool) => test (p.1, w)) (encPair encC encUnary) encBool

Bounded universal search over words of exact unary length preserves IsComputable.