Polynomial advice — definitions

Advice is a length-indexed binary string. An advised machine receives the self-delimiting encoding pair (advice n) x on its read-only input tape, while time remains charged against the original input length n.

This file also defines the nonuniform circuit family obtained by fixing both the deterministic choice prefix and the length-dependent advice prefix of a bounded acceptance circuit.

@[reducible, inline]

abbrev Complexity.Advice : Type

A binary advice string for every original input length.

Equations

• Complexity.Advice = (ℕ → List Bool)

def Complexity.advisedInput (a : Advice) (x : List Bool) : List Bool

Put the length-dependent advice before the ordinary input using the self-delimiting pairing encoding.

Equations

• Complexity.advisedInput a x = Complexity.pair (a x.length) x

def Complexity.PolynomialAdvice (a : Advice) : Prop

Advice has polynomial length when one natural-coefficient polynomial bounds every advice string.

Equations

• Complexity.PolynomialAdvice a = ∃ (p : Polynomial ℕ), ∀ (n : ℕ), (a n).length ≤ Polynomial.eval n p

def Complexity.Advice.fixedPrefix (a : Advice) (n : ℕ) : List Bool

The fixed prefix preceding an ordinary n-bit input.

Equations

• a.fixedPrefix n = Complexity.pair (a n) []

def Complexity.Advice.inputBits (a : Advice) {n : ℕ} (x : BitString n) : BitString ((a.fixedPrefix n).length + n)

The full advised input as a fixed-length bit string, factored into its fixed prefix followed by the live ordinary input.

Equations

• a.inputBits x = Fin.append (a.fixedPrefix n).get x

def Complexity.TM.DecidesWithAdviceInTime {k : ℕ} (tm : TM k) (a : Advice) (L : Language) (T : ℕ → ℕ) : Prop

A DTM decides L with advice a in time T when it starts on pair (a |x|) x, halts within T |x|, and writes the ordinary language verdict. The resource bound is indexed by the original input length, not the paired input length.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.TM.advisedBoundedAcceptanceBit {k : ℕ} (tm : TM k) (a : Advice) (T : ℕ → ℕ) {n : ℕ} (x : BitString n) : Bool

Exact fixed-horizon advised acceptance predicate on a fixed-length live input.

Equations

• tm.advisedBoundedAcceptanceBit a T x = Complexity.CircuitUnrolling.boundedAcceptanceBit tm.toNTM (T n) (a.inputBits x) fun (x : Fin (T n)) => false

noncomputable def Complexity.TM.adviceCircuitFamily {k : ℕ} (tm : TM k) (a : Advice) (T : ℕ → ℕ) : CircuitFamily Basis.andOr2

The nonuniform family obtained by hardwiring the advice for each length into the bounded deterministic acceptance circuit.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.PAdvice : Set Language

Languages decided in polynomial time with polynomial-length advice.

Equations

• One or more equations did not get rendered due to their size.