Complexity : Time Computable functions

Stream: Is there code for X?

[Shreyas Srinivas]

I notice that we have all the pieces we need to define Time computable functions, but I can't find them in mathlib. Do we have those? If not, I can make a quick PR

[Shreyas Srinivas]

Basically they are

1. Functions in the linear and superlinear range which are likely to appear naturally in complexity
2. Important for time and space hierarchy theorems

[Bolton Bailey]

Turing.TM2ComputableInTime?

[Shreyas Srinivas]

Not not that. I might have made a terminology error. I’m talking about time constructible functions

[Bolton Bailey]

Or perhaps you are talking about what wikipedia calls "Time-Constructible functions"? I haven't seen those.

[Shreyas Srinivas]

Something like this :

import Mathlib

open Computability Turing


abbrev TimeConstructible (T : ℕ → ℕ) : Prop :=
  ∃ M : @TM2ComputableInTime ℕ ℕ unaryFinEncodingNat unaryFinEncodingNat T,
    ∃ c d, ∀ n : ℕ, M.time n ≤ c * (T n) + d

[Shreyas Srinivas]

Naturally this defintion is only useful when we prove that for common classes of super linear functions, this property holds

[Shreyas Srinivas]

The purpose of this definition is to be able to stop a turing machine after O(T(n)) steps for a specified T(n). In the context of relevant theorems, this is only possible for time constructible functions