Documentation

Complexity.Computability.Machines.Turing.MultiTape.PolyTime

Polynomial time on multi-tape machines #

Turing.MultiTapeTM.ComputableInPolyTime f encIn encOut: some machine with a binary alphabet and finitely many states computes f in the sense of Turing.MultiTapeTM.ComputableInTimeAndSpace, within time and space bounded by polynomially bounded functions of the length of the encoded input Arora and Barak, Chapter 1. Time and space are independent bounds, as in Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength; that a polynomial time bound already bounds the space is a lemma about machines, not part of the definition.

The predicate is registered with fun_prop. This file proves the closure rules that need no machine construction beyond upstream's: the identity, constants, functions on finite types and changes of representation.

Main definitions #

Main results #

References #

source
def Turing.MultiTapeTM.ComputableInPolyTime {α : Type u_1} {β : Type u_2} (f : α → β) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) :
Prop

f is computable in polynomial time: some machine with a binary alphabet and finitely many states computes f, relative to the encodings encIn and encOut, within time and space bounded by polynomially bounded functions of the length of the encoded input.

Instances For
    source
    theorem Turing.MultiTapeTM.ComputableInPolyTime.of_eq {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encOut (f a) = encIn a) :
    ComputableInPolyTime f encIn encOut

    A function whose encoded values are its encoded arguments is computable in polynomial time: the machine copies its input.

    source
    theorem Turing.MultiTapeTM.ComputableInPolyTime.of_finite {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} [Finite α] (f : α → β) :
    ComputableInPolyTime f encIn encOut

    Every function on a finite type is computable in polynomial time, by a lookup machine.

    Automation #

    source
    theorem Turing.MultiTapeTM.ComputableInPolyTime.id' {α : Type u_1} {encIn : α ↪ List Bool} :
    ComputableInPolyTime (fun (a : α) => a) encIn encIn
    source
    theorem Turing.MultiTapeTM.ComputableInPolyTime.const {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} (b : β) :
    ComputableInPolyTime (fun (x : α) => b) encIn encOut