Finite statistical tests as Boolean oracles -- definitions

A fixed-length finite test is extended to all binary query strings by rejecting malformed lengths. This supplies the canonical oracle used by reconstruction decoders without placing the test's exponentially long truth table inside the program description.

def Complexity.decodeFixedWidthBoolean? (length : ℕ) (bits : List Bool) : Option (Fin length → Bool)

Decode a list only when it has exactly the advertised fixed length.

Equations

• Complexity.decodeFixedWidthBoolean? length bits = if hlength : bits.length = length then some fun (index : Fin length) => bits.get ⟨↑index, ⋯⟩ else none

def Complexity.finiteTestOracle {outputLength : ℕ} (test : Finset (Fin outputLength → Bool)) : BooleanOracle

Canonical total Boolean oracle associated to a finite fixed-length test. Queries of the wrong length are rejected.

Equations

• Complexity.finiteTestOracle test query = match Complexity.decodeFixedWidthBoolean? outputLength query with | some output => decide (output ∈ test) | none => false