Universal input coding and polynomial-time simulation

The universal function Turing.MultiTapeTM.Universal.universal runs a described machine on an input for a given number of steps. Its time and space are polynomial in the length of the description, of the input and of the number of steps written in unary (Turing.MultiTapeTM.Universal.universal_bounds_unary), so it is tidily computable in polynomial time when the number of steps is written in unary (Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_universal). Written in binary, the number of steps would be exponential in its length.

The input-coding API translates bits to unary symbols (false ↦ 0, true ↦ 1) in linear time and output size. It also certifies polynomial-time decoding of descriptions and coding of a single bit, independently of hierarchy theorems and Ladner's language.

Main definitions

• Turing.MultiTapeTM.Universal.encTrueDoubled: a bit-list encoding doubling every true.
• Turing.MultiTapeTM.Universal.trueDoubleT, Turing.MultiTapeTM.Universal.symbolsT: transducers implementing the conversion from bit words to framed unary symbols.

Main results

• Turing.MultiTapeTM.Universal.computableTidilyInDegree_map_eBit: input symbols in linear time and output size.

• Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_decodeDesc, Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_map_eBit, Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_eBit: polynomial-time description decoding and bit coding.

• Turing.MultiTapeTM.Universal.universal_bounds_unary: the time and space of the universal function, polynomially in the length of its input with the number of steps in unary.

• Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_universal: the universal function, with its number of steps in unary, is polynomial-time.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach

The symbols of the input

def Turing.MultiTapeTM.Universal.trueDoubled (b : Bool) : List Bool

The code of a bit list with every true doubled: false ↦ [false], true ↦ [true, true].

def Turing.MultiTapeTM.Universal.encTrueDoubled : List Bool ↪ List Bool

Bit lists with every true doubled.

def Turing.MultiTapeTM.Universal.trueDoubleT : Transducer Bool Unit

Doubles every true.

def Turing.MultiTapeTM.Universal.symbolsT : Transducer Bool Bool

Reads a doubled word as the framed unary symbols 0 for false and 1 for true.

theorem Turing.MultiTapeTM.Universal.trueDoubleT_run (x : List Bool) : trueDoubleT.run () x = encTrueDoubled x

theorem Turing.MultiTapeTM.Universal.symbolsT_run (x : List Bool) : symbolsT.run false (encTrueDoubled x) = (encList encUnary) (List.map (⇑eBit) x)

theorem Turing.MultiTapeTM.Universal.computableTidilyInDegree_map_eBit : ComputableTidilyInDegree (fun (x : List Bool) => List.map (⇑eBit) x) encBits (encList encUnary) 1 1

The input as symbols, in linear time and space.

theorem Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_decodeDesc : ComputableTidilyInPolyTime decodeDesc encBits eDesc

Decoding a machine description is polynomial-time in the input word.

theorem Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_map_eBit : ComputableTidilyInPolyTime (fun (w : List Bool) => List.map (⇑eBit) w) encBits (encList encUnary)

The input of a machine as symbols is linear.

theorem Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_eBit : ComputableTidilyInPolyTime (fun (b : Bool) => eBit b) encBool encUnary

The coding of bits as symbols is a finite computation.

Simulation with a unary clock

theorem Turing.MultiTapeTM.Universal.universal_bounds_unary (i : Desc × List ℕ × ℕ) : (i.2.2 + 1) * (stepBound (descLen i.1) ((encList encUnary) i.2.1).length i.2.2 + runBound (descLen i.1) ((encList encUnary) i.2.1).length i.2.2 + ((encNat i.2.2).length + 1) ^ 2) + ((eIn i).length + 1) ^ 2 ≤ 100025 * (((encPair eDesc (encPair (encList encUnary) encUnary)) i).length + 1) ^ 8 ∧ runBound (descLen i.1) ((encList encUnary) i.2.1).length i.2.2 + (eIn i).length ≤ 205 * (((encPair eDesc (encPair (encList encUnary) encUnary)) i).length + 1) ^ 3

The time and space of the universal function, polynomially in the length of its input with the number of steps in unary.

theorem Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_universal : ComputableTidilyInPolyTime universal (encPair eDesc (encPair (encList encUnary) encUnary)) eOut

The universal function with a unary clock is polynomial-time: written in unary, the number of steps counts towards the length of the input.