Oracle-relative Kolmogorov complexity -- definitions

The machine and Boolean oracle are both explicit parameters. As in the ordinary machine-relative layer, extended naturals distinguish a zero-length description from the absence of any description. The bounded clock charges local transitions and oracle lookups according to OracleTM.reachesIn.

def Complexity.OracleTM.producingProgramSizes {n : ℕ} (machine : OracleTM n) (oracle : BooleanOracle) (output : List Bool) : Set ℕ

Lengths of programs that eventually produce output relative to oracle.

Equations

• machine.producingProgramSizes oracle output = {size : ℕ | ∃ (program : List Bool), program.length = size ∧ machine.Produces oracle program output}

def Complexity.OracleTM.timeBoundedProducingProgramSizes {n : ℕ} (machine : OracleTM n) (oracle : BooleanOracle) (output : List Bool) (time : ℕ) : Set ℕ

Lengths of programs that produce output within time relative to oracle.

Equations

• machine.timeBoundedProducingProgramSizes oracle output time = {size : ℕ | ∃ (program : List Bool), program.length = size ∧ machine.ProducesInTime oracle program output time}

noncomputable def Complexity.OracleTM.plainKolmogorovComplexity {n : ℕ} (machine : OracleTM n) (oracle : BooleanOracle) (output : List Bool) : WithTop ℕ

Plain description complexity relative to a machine and Boolean oracle.

Equations

• machine.plainKolmogorovComplexity oracle output = sInf ((fun (size : ℕ) => ↑size) '' machine.producingProgramSizes oracle output)

noncomputable def Complexity.OracleTM.timeBoundedKolmogorovComplexity {n : ℕ} (machine : OracleTM n) (oracle : BooleanOracle) (output : List Bool) (time : ℕ) : WithTop ℕ

Whole-output time-bounded description complexity relative to a machine and Boolean oracle.

Equations

• machine.timeBoundedKolmogorovComplexity oracle output time = sInf ((fun (size : ℕ) => ↑size) '' machine.timeBoundedProducingProgramSizes oracle output time)