Direct polynomial resource consequences

These rules retain a single realizing machine. Existence of cost and output degrees is obtained from its actual polynomial clocks; it does not use a higher normal-form calculus.

Main results

• ComputableInTimeAndSpace.computableInPolyTime: polynomial time suffices at arbitrary space.
• ComputableInPolyTime.exists_degree: fixed resource and independent output degrees exist.

theorem Turing.MultiTapeTM.ComputableInTimeAndSpace.computableInPolyTime {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {t : ℕ → ℕ} {s : α → ℕ} (ht : Cslib.PolynomiallyBounded t) (h : ComputableInTimeAndSpace f encIn encOut (fun (a : α) => t (encIn a).length) s) : ComputableInPolyTime f encIn encOut

A polynomial time bound alone suffices. A function computable by some machine within a time bound polynomial in the length of the encoded input, with any space bound, is computable in polynomial time: within t steps the machine visits at most c t + c work-tape cells.

theorem Turing.MultiTapeTM.ComputableInPolyTime.exists_degree {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} (h : ComputableInPolyTime f encIn encOut) : ∃ (d : ℕ) (e : ℕ), ComputableInDegree f encIn encOut d e

Every polynomial-time realization has fixed resource and output degrees. The output degree comes from its clock; it is not identified with its workspace degree.