Documentation

Complexity.Computability.GenericRAM.Native.BooleanSearch

Streaming first-match search on Boolean words #

The width is a runtime unary natural. The test receives the retained context and one Boolean word, and the search retains at most one matching word. The implementation uses BooleanFold; the list of all words occurs only in the correctness specification.

This supplies the unrestricted representative scan of [OAI26c], Lemma 3.2, printed p. 23. In that application the test checks measurements, without the fixed-bit restriction used in the second scan. This module does not implement that second scan or the counting algorithm.

Main definitions #

Cslib.GenericRAM.BooleanSearch.run: first matching word, or none.
Cslib.GenericRAM.BooleanSearch.runPrefix: the complete state after a prefix of the traversal.
Cslib.GenericRAM.BooleanSearch.certificate: native search from a supplied native test.

Main results #

Cslib.GenericRAM.BooleanSearch.run_eq_find?: equality with the existing enumeration's search.
Cslib.GenericRAM.BooleanSearch.run_eq_none_iff, Cslib.GenericRAM.BooleanSearch.run_some: completeness and soundness.
Cslib.GenericRAM.BooleanSearch.length_prefix_le: complete live-state bound at every prefix.
Cslib.GenericRAM.BooleanSearch.exists_computableInO: traversal-proportional time and polynomial workspace when the test has polynomial resource bounds.

References #

OpenAI, The Exponential Time Hypothesis is False, Lemma 3.2, pp. 22–23.

def Cslib.GenericRAM.BooleanSearch.step {C : Type} (test : C × List Bool → Bool) (p : (ℕ × List Bool) × C × Option (List Bool)) :

C × Option (List Bool)

Retain the context and the first match, using the existing list-search step.

Instances For

def Cslib.GenericRAM.BooleanSearch.runPrefix {C : Type} (test : C × List Bool → Bool) (p : C × ℕ) (j : ℕ) :

ℕ × ℕ × C × Option (List Bool)

Prefix state: binary index, unary width, context and at most one matching word.

Instances For

def Cslib.GenericRAM.BooleanSearch.run {C : Type} (test : C × List Bool → Bool) (p : C × ℕ) :

Option (List Bool)

Stream all words of the runtime width and return the first match in enumeration order. After finding a match the traversal retains it and makes no further calls to the test.

Instances For

theorem Cslib.GenericRAM.BooleanSearch.prefix_accumulator {C : Type} (test : C × List Bool → Bool) (p : C × ℕ) (j : ℕ) :

(runPrefix test p j).2.2 = (p.1, List.find? (fun (w : List Bool) => test (p.1, w)) (List.map (BitString.lowBits p.2) (List.range j)))

Every prefix retains the original context and the first match among the visited words. The list on the right is specification-only, not a stored traversal history.

theorem Cslib.GenericRAM.BooleanSearch.run_eq_find? {C : Type} (test : C × List Bool → Bool) (p : C × ℕ) :

run test p = List.find? (fun (w : List Bool) => test (p.1, w)) (BitString.enumList p.2)

The streaming result has exactly the first-match semantics of the existing enumeration.

theorem Cslib.GenericRAM.BooleanSearch.run_eq_some_iff {C : Type} (test : C × List Bool → Bool) (p : C × ℕ) (word : List Bool) :

run test p = some word ↔ test (p.1, word) = true ∧ ∃ (before : List (List Bool)) (after : List (List Bool)), BitString.enumList p.2 = before ++ word :: after ∧ ∀ w ∈ before, test (p.1, w) = false

A returned word passes the test and every earlier word in enumeration order fails it.

theorem Cslib.GenericRAM.BooleanSearch.prefix_some {C : Type} (test : C × List Bool → Bool) (p : C × ℕ) (j : ℕ) {word : List Bool} (h : (runPrefix test p j).2.2.2 = some word) :

word.length = p.2 ∧ test (p.1, word) = true

A match retained at any prefix has the requested width and passes the test.

theorem Cslib.GenericRAM.BooleanSearch.run_some {C : Type} (test : C × List Bool → Bool) (p : C × ℕ) {word : List Bool} (h : run test p = some word) :

word.length = p.2 ∧ test (p.1, word) = true

Every returned word has the requested width and passes the test.

theorem Cslib.GenericRAM.BooleanSearch.run_eq_none_iff {C : Type} (test : C × List Bool → Bool) (p : C × ℕ) :

run test p = none ↔ ∀ (word : List Bool), word.length = p.2 → test (p.1, word) = false

Failure means that no word of the requested width passes the test.

theorem Cslib.GenericRAM.BooleanSearch.run_ne_none_iff {C : Type} (test : C × List Bool → Bool) (p : C × ℕ) :

run test p ≠ none ↔ ∃ (word : List Bool), word.length = p.2 ∧ test (p.1, word) = true

A word satisfying the test exists exactly when the streaming search returns a word.

theorem Cslib.GenericRAM.BooleanSearch.length_prefix_result_le {C : Type} (test : C × List Bool → Bool) (p : C × ℕ) (j : ℕ) :

((Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool)) (runPrefix test p j).2.2.2).length ≤ 3 * p.2 + 1

A prefix stores at most one width-sized result, including the option tag and list framing.

theorem Cslib.GenericRAM.BooleanSearch.length_prefix_accumulator_le {C : Type} {encC : C ↪ List Bool} (test : C × List Bool → Bool) (p : C × ℕ) (j : ℕ) :

((Turing.MultiTapeTM.encPair encC (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool))) (runPrefix test p j).2.2).length ≤ 2 * (encC p.1).length + 3 * p.2 + 2

The complete captured accumulator has polynomial size at every prefix, independently of the number of visited assignments.

theorem Cslib.GenericRAM.BooleanSearch.length_prefix_le {C : Type} {encC : C ↪ List Bool} (test : C × List Bool → Bool) (p : C × ℕ) (j : ℕ) (hj : j ≤ 2 ^ p.2) :

((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair encC (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool))))) (runPrefix test p j)).length ≤ 2 * (encC p.1).length + 7 * p.2 + 6

The full index/width/context/result state stays polynomial even at the terminal prefix.

Certify the captured search step with an arbitrary native test. The outer branch skips the test when a word has already been found; the decoder's bit word is converted to the agreed list encoding before invoking the test.

Instances For

theorem Cslib.GenericRAM.BooleanSearch.stepCertificate_isPolynomial {C : Type} {encC : C ↪ List Bool} {test : C × List Bool → Bool} (ct : NativeCertificate test (Turing.MultiTapeTM.encPair encC (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool)) Turing.MultiTapeTM.encBool) (hct : ct.IsPolynomial) :

(stepCertificate ct).IsPolynomial

A polynomial native test gives a polynomial step in the complete captured input encoding. This does not assert polynomial time for the exponential traversal.

noncomputable def Cslib.GenericRAM.BooleanSearch.certificate {C : Type} {encC : C ↪ List Bool} {test : C × List Bool → Bool} (ct : NativeCertificate test (Turing.MultiTapeTM.encPair encC (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool)) Turing.MultiTapeTM.encBool) :

NativeCertificate (run test) (Turing.MultiTapeTM.encPair encC Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool))

One fixed native machine searches all runtime widths and contexts. Its independently charged time and space bounds are those of the binary streaming iterator, including count preparation, initialization, decoding, the selected test calls and output projection.

Instances For

theorem Cslib.GenericRAM.BooleanSearch.exists_computableInO {C : Type} {encC : C ↪ List Bool} {test : C × List Bool → Bool} (ct : NativeCertificate test (Turing.MultiTapeTM.encPair encC (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool)) Turing.MultiTapeTM.encBool) (hct : ct.IsPolynomial) :

∃ (overhead : C × ℕ → ℕ) (workspace : C × ℕ → ℕ), Turing.MultiTapeTM.PolyBounded (fun (p : C × ℕ) => ((Turing.MultiTapeTM.encPair encC Turing.MultiTapeTM.encUnary) p).length) overhead ∧ Turing.MultiTapeTM.PolyBounded (fun (p : C × ℕ) => ((Turing.MultiTapeTM.encPair encC Turing.MultiTapeTM.encUnary) p).length) workspace ∧ Turing.MultiTapeTM.ComputableInO (run test) (Turing.MultiTapeTM.encPair encC Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool)) (fun (p : C × ℕ) => (2 ^ p.2 + 1) * overhead p) workspace

With a polynomial test, search takes the traversal count times polynomial overhead and only polynomial charged workspace. The two polynomials and the realizing machine are fixed before the runtime context and width. In particular, the traversal count does not enter space.