Short descriptions

The time hierarchy theorems diagonalize only over inputs whose framed description is short: 2 ^ |unframe x| ≤ |x| (Cslib.Complexity.Diagonal.shortDesc). Decoding a description of L bits then takes time polynomial in L, of a degree fixed by the decoder, hence O(2 ^ L), which is O(|x|). Padded descriptions are short. The space hierarchy theorem asks for tiny descriptions instead (CslibFrontier.Computability.Complexity.Classes.Hierarchy.TinyDesc), so that decoding takes logarithmic space.

Main definitions

• Cslib.Complexity.Diagonal.shortDesc: whether the framed description at the start of a word is short.

Main results

• Cslib.Complexity.Diagonal.shortDesc_eq_decide: shortness compares the length of the description with the number of binary digits of the length of the word.
• Cslib.Complexity.Diagonal.computableInO_shortDesc: shortness is decided within linear time and space, by halving the length of the word once per bit of the description.

References

• M. Sipser, Introduction to the Theory of Computation, Theorems 9.3 and 9.10: the padded descriptions in the proofs of the hierarchy theorems.

def Cslib.Complexity.Diagonal.shortDesc (x : List Bool) : Bool

The description framed at the start of x is short: 2 ^ |unframe x| ≤ |x|.

theorem Cslib.Complexity.Diagonal.shortDesc_eq_decide (x : List Bool) : shortDesc x = decide ((Turing.MultiTapeTM.unframe x).length + 1 ≤ (Turing.MultiTapeTM.encNat x.length).length)

Shortness compares the length of the description with the number of binary digits of the length of the word.

Shortness in linear time

theorem Cslib.Complexity.Diagonal.computableInO_shortDesc : Turing.MultiTapeTM.ComputableInO shortDesc Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool (fun (x : List Bool) => x.length) fun (x : List Bool) => x.length

Shortness is decided within linear time and space. The length of the word and of the framed description are written in unary, and the first is halved once per bit of the second.