Computational depth -- definitions

The two-clock computational depth of output relative to a machine is the gap C_M^first(output) - C_M^later(output), where first ≤ later. Taking the second clock to infinity gives the usual one-clock gap C_M^time(output) - C_M(output).

Because this library allows a complexity to be ⊤, descriptionDifference returns ⊤ if either operand is infinite and otherwise embeds the natural-number difference. The proof layer establishes the required complexity order before using natural subtraction.

def Complexity.descriptionDifference (upper lower : WithTop ℕ) : WithTop ℕ

Difference of two finite extended-natural description lengths. If either length is infinite, the difference is infinite rather than silently defaulting to zero.

Equations

• Complexity.descriptionDifference upper lower = WithTop.recTopCoe ⊤ (fun (upperValue : ℕ) => WithTop.recTopCoe ⊤ (fun (lowerValue : ℕ) => ↑(upperValue - lowerValue)) lower) upper

noncomputable def Complexity.TM.computationalDepthBetween {n : ℕ} (machine : TM n) (output : List Bool) (firstTime laterTime : ℕ) : WithTop ℕ

Machine-relative two-clock computational depth: C_M^firstTime(output) - C_M^laterTime(output). Its exact laws require firstTime ≤ laterTime.

Equations

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

noncomputable def Complexity.TM.computationalDepth {n : ℕ} (machine : TM n) (output : List Bool) (time : ℕ) : WithTop ℕ

Machine-relative time-bounded computational depth: C_M^time(output) - C_M(output).

Equations

• machine.computationalDepth output time = Complexity.descriptionDifference (machine.timeBoundedKolmogorovComplexity output time) (machine.plainKolmogorovComplexity output)