Tiny descriptions

The space hierarchy below linear space diagonalizes only over inputs whose framed description is tiny: 2 ^ |unframe x| ≤ Nat.size |x|, that is, at most log₂ |x| + 1 (Cslib.Complexity.Diagonal.tinyDesc). Decoding a description of L bits takes space polynomial in L, of a degree fixed by the decoder, hence O(2 ^ L), which is O(log |x|). So a diagonal reading its input in place decodes its description in logarithmic space (Cslib.Complexity.Diagonal.computableInLogSpace_decodeDesc_tinyCut). Padded descriptions are tiny once the padding is doubly exponential in the description.

Main definitions

• Cslib.Complexity.Diagonal.tinyDesc: whether the framed description at the start of a word is tiny.
• Cslib.Complexity.Diagonal.tinyCut: the framed description at the start of a word when it is tiny, and the empty word otherwise.

Main results

• Cslib.Complexity.Diagonal.tinyDesc_frame_append: a description padded to doubly exponential length is tiny.
• Cslib.Complexity.Diagonal.computableInLogSpace_tinyDesc, Cslib.Complexity.Diagonal.computableInLogSpace_tinyCut: tininess is decided, and tiny descriptions are cut out, in logarithmic space.
• Cslib.Complexity.Diagonal.computableInLogSpace_decodeDesc_tinyCut: tiny descriptions are decoded in logarithmic space.
• Cslib.Complexity.Diagonal.exists_length_eDesc_decodeDesc_tinyCut_le: the decoded tiny description has O(log |x|) bits.

References

• M. Sipser, Introduction to the Theory of Computation, Theorem 9.3: the padded descriptions in the proof of the space hierarchy theorem.

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

The description framed at the start of x is tiny: 2 ^ |unframe x| ≤ Nat.size |x|, the number of binary digits of the length of x.

theorem Cslib.Complexity.Diagonal.tinyDesc_eq_decide (x : List Bool) : tinyDesc x = decide ((Turing.MultiTapeTM.unframe x).length < x.length.size.size)

Tininess compares the length of the description with the binary length of the binary length of the word.

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

The description framed at the start of x when it is tiny, and the empty word otherwise.

theorem Cslib.Complexity.Diagonal.tinyCut_of_tinyDesc {x : List Bool} (h : tinyDesc x = true) : tinyCut x = Turing.MultiTapeTM.unframe x

theorem Cslib.Complexity.Diagonal.two_pow_length_tinyCut_le (x : List Bool) : 2 ^ (tinyCut x).length ≤ x.length.log2 + 1

A cut description is tiny: 2 ^ |tinyCut x| ≤ log₂ |x| + 1.

theorem Cslib.Complexity.Diagonal.tinyDesc_frame_append {w pad : List Bool} (h : 2 ^ 2 ^ w.length ≤ pad.length) : tinyDesc (Turing.MultiTapeTM.frame w ++ pad) = true

A description padded to doubly exponential length is tiny.

Tiny descriptions in logarithmic space

theorem Cslib.Complexity.Diagonal.computableInLogSpace_tinyDesc : Turing.MultiTapeTM.ComputableInLogSpace tinyDesc Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool

Tininess is decided in logarithmic space, by comparing unary numbers.

theorem Cslib.Complexity.Diagonal.computableInLogSpace_tinyCut : Turing.MultiTapeTM.ComputableInLogSpace tinyCut Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits

Tiny descriptions are cut out in logarithmic space.

theorem Cslib.Complexity.Diagonal.computableInLogSpace_decodeDesc_tinyCut : Turing.MultiTapeTM.ComputableInLogSpace (fun (x : List Bool) => Turing.MultiTapeTM.Universal.decodeDesc (tinyCut x)) Turing.MultiTapeTM.encBits Turing.MultiTapeTM.Universal.eDesc

Tiny descriptions are decoded in logarithmic space. Decoding takes space polynomial in the length L of the description, which is O(2 ^ L) = O(log n) on a tiny description, and the cut description is recomputed whenever the decoder reads it (Turing.MultiTapeTM.ComputableInTimeAndSpace.comp_space).

theorem Cslib.Complexity.Diagonal.exists_length_eDesc_decodeDesc_tinyCut_le : ∃ (c : ℕ), ∀ (x : List Bool), (Turing.MultiTapeTM.Universal.eDesc (Turing.MultiTapeTM.Universal.decodeDesc (tinyCut x))).length ≤ c * (x.length.log2 + 1)

Tiny descriptions decode to short descriptions: the decoded cut description has encoded length O(log n), since decoding L bits gives a description of length polynomial in L.