Documentation

CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain

Polynomial time on plain machines #

Turing.MultiTapeTM.ComputableTidilyInPolyTime asks for a tidy machine, which clears its work tapes and rewinds its heads before halting, within polynomially bounded time and space. Neither requirement changes the class. A machine that halts within t steps visits at most k t + k work-tape cells, where k is its number of work tapes (Turing.MultiTapeTM.ComputesInTimeAndSpace.space_linear), and the tidy normal form makes any machine tidy at a linear cost in time and space (Turing.MultiTapeTM.ComputableInTimeAndSpace.exists_computableTidilyInTimeAndSpace). So a function is tidily computable in polynomial time exactly when some machine computes it in the sense of upstream Turing.MultiTapeTM.ComputableInTimeAndSpace, within polynomially bounded time and space (Turing.MultiTapeTM.computableTidilyInPolyTime_iff_exists_computableInTimeAndSpaceOfLength), and a polynomial time bound alone already suffices (Turing.MultiTapeTM.ComputableInTimeAndSpace.computableTidilyInPolyTime) Arora and Barak, Chapter 1.

Passing from tidy to plain computations is lossless: a tidy machine is a machine, with the same bounds. Passing from plain to tidy computations changes the bounds by linear functions whose coefficients depend on the machine.

The plain notion, Turing.MultiTapeTM.ComputableInPolyTime, is the one for definitions and public statements; the tidy notion is a proof device. Proofs switch between them with Turing.MultiTapeTM.ComputableInPolyTime.tidy and Turing.MultiTapeTM.ComputableInPolyTime.of_tidy. The core closure rules of the plain notion use direct machine constructions and are registered with fun_prop, together with the transition from tidy to plain computability. fun_prop decomposes a plain goal with the plain closure rules and proves the remaining atoms from plain hypotheses or, through the transition, from tidy certificates. Ordinary plain rules for captured scans and list operations are supplied by PolyTime.List and PolyTime.BitString. If a routine has only a tidy construction certificate, its proof can switch explicitly with .of_tidy.

Mixing plain hypotheses with tidy certificates #

There is deliberately no fun_prop transition from plain to tidy: registering it together with the reverse transition would create a search cycle. In particular, a tidy goal such as ComputableTidilyInPolyTime (fun a => [f a]) enc (encList encIntBin) cannot use a plain certificate for f directly. This occurs when constructing singleton target lists in CslibFrontier/Computability/Complexity/Classes/WPP/Robustness.lean and CslibFrontier/Computability/Complexity/Classes/WPP/TwoSided.lean. Unbounded fun_prop can exhaust its heartbeat budget while looking for another certificate. Restate the needed hypothesis with have hf := hf.tidy before fun_prop, or use polytime from CslibFrontier.Tactic.PolyTime, which prepares plain hypotheses for tidy search. When trying composition speculatively, use fun_prop (config := { maxSteps := 32 }) to bound that attempt, then supply a certificate or switch tactics. This is a search budget, not a guarantee that every unsuccessful search is cheap.

selectVerifier, andVerifier and orVerifier have plain fun_prop rules in CslibFrontier/Computability/Complexity/Classes/SharpP/Combinators.lean, so plain verifier hypotheses need no manual .tidy conversion for a plain goal. Their tidy rules remain available for proofs using the tidy calculus.

For a tidy certificate covering a whole composite whose intermediate encoding is difficult to infer, prefer polytime, or convert the hypotheses with .tidy and use .of_tidy (by fun_prop). Two representative cases are the binary threshold fun a => 3 * (k a * 2 ^ q.eval (enc a).length) in inter_mem_SBP_of_mem_BPP (where k uses encNat, while the exponent uses encUnary), and the input-dependent sharpTest verifier in CslibFrontier/Computability/Complexity/Classes/Toda.lean. polytime proves both directly from plain hypotheses. The mixed-encoding examples and the bounded singleton failure are checked in CslibFrontierTests/PolyTimeMixes.lean.

Upstream Turing.MultiTapeTM.DecidableInTimeAndSpace decides a problem through its Boolean indicator. Turing.MultiTapeTM.decidableInTimeAndSpace_iff restates it for any Boolean function deciding membership, the form used by the classes in Cslib.Complexity.

Main results #

References #

Time bounds space #

source
theorem Turing.MultiTapeTM.indicator_eq_iff {α : Type u_1} {A : Set α} {g : α → Bool} :
indicator A = g ↔ ∀ (a : α), a ∈ A ↔ g a = true

The indicator of A is the Boolean function that is true exactly on A.

Decidability through a Boolean decider #

source
theorem Turing.MultiTapeTM.decidableInTimeAndSpace_iff {α : Type u_1} {A : Set α} {enc : α ↪ List Bool} {t s : α → ℕ} :
DecidableInTimeAndSpace A enc t s ↔ ∃ (g : α → Bool), ComputableInTimeAndSpace g enc encBool t s ∧ ∀ (a : α), a ∈ A ↔ g a = true

A problem is decidable within given bounds exactly when some Boolean function deciding membership is computable within them, with answers encoded by encBool.

Tidy and plain polynomial time #

source
theorem Turing.MultiTapeTM.ComputableInTimeAndSpace.computableTidilyInPolyTime {α : 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) :
ComputableTidilyInPolyTime f encIn encOut

Plain polynomial time is tidy polynomial time. A function computable by some machine within a time bound polynomial in the length of the encoded input, with any space bound, is tidily computable in polynomial time.

source
theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.exists_computableInTimeAndSpaceOfLength {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} (h : ComputableTidilyInPolyTime f encIn encOut) :
∃ (t : ℕ → ℕ) (s : ℕ → ℕ), Cslib.PolynomiallyBounded t ∧ Cslib.PolynomiallyBounded s ∧ ComputableInTimeAndSpaceOfLength f encIn encOut t s

Tidy polynomial time gives a machine computing the function within polynomially bounded time and space. The machine and its bounds are those of the tidy computation.

source
theorem Turing.MultiTapeTM.computableTidilyInPolyTime_iff_exists_computableInTimeAndSpaceOfLength {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} :
ComputableTidilyInPolyTime f encIn encOut ↔ ∃ (t : ℕ → ℕ) (s : ℕ → ℕ), Cslib.PolynomiallyBounded t ∧ Cslib.PolynomiallyBounded s ∧ ComputableInTimeAndSpaceOfLength f encIn encOut t s

Tidy polynomial time is plain polynomial time: f is tidily computable in polynomial time exactly when some machine with a binary alphabet and finitely many states computes it within time and space bounded by polynomially bounded functions of the length of the encoded input.

Bridges to ComputableInPolyTime #

source
theorem Turing.MultiTapeTM.computableInPolyTime_iff_computableTidilyInPolyTime {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} :
ComputableInPolyTime f encIn encOut ↔ ComputableTidilyInPolyTime f encIn encOut

Plain and tidy polynomial time agree. Turing.MultiTapeTM.ComputableInPolyTime unfolds to the right-hand side of Turing.MultiTapeTM.computableTidilyInPolyTime_iff_exists_computableInTimeAndSpaceOfLength.

source
theorem Turing.MultiTapeTM.ComputableInPolyTime.tidy {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} (h : ComputableInPolyTime f encIn encOut) :
ComputableTidilyInPolyTime f encIn encOut

A function computable in polynomial time is tidily computable in polynomial time. The tidy machine runs within time and space linear in the plain time bound.

source
theorem Turing.MultiTapeTM.ComputableInPolyTime.of_tidy {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} (h : ComputableTidilyInPolyTime f encIn encOut) :
ComputableInPolyTime f encIn encOut

A function tidily computable in polynomial time is computable in polynomial time, by the same machine within the same bounds.

source
theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.computableInPolyTime {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} (h : ComputableTidilyInPolyTime f encIn encOut) :
ComputableInPolyTime f encIn encOut

Turing.MultiTapeTM.ComputableInPolyTime.of_tidy for dot notation on a tidy hypothesis. As a fun_prop transition rule, it proves the atoms of a plain goal from tidy certificates.

Closure of ComputableInPolyTime #

The direct core supplies both composition directions (comp and trans) and ordinary pair projections. This facade retains legacy-client projection registrations and additional captured closure rules during migration. Proof-local tidy bridges remain available explicitly; their presence here does not make the direct core depend on a higher tidy calculus.

source
theorem Turing.MultiTapeTM.ComputableInPolyTime.fstWithEncoding {α β γ : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {output : α ↪ List Bool} {f : γ → α × β} (hf : ComputableInPolyTime f encC (encPair encA encB)) (h : ComputableInPolyTime (fun (a : α) => a) encA output) :
ComputableInPolyTime (fun (p : γ) => (f p).1) encC output

Project a first component and convert its encoding. Certifying the pair-valued function first determines the source encoding before automation searches for the conversion certificate.

source
theorem Turing.MultiTapeTM.ComputableInPolyTime.sndWithEncoding {α β γ : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {output : β ↪ List Bool} {f : γ → α × β} (hf : ComputableInPolyTime f encC (encPair encA encB)) (h : ComputableInPolyTime (fun (a : β) => a) encB output) :
ComputableInPolyTime (fun (p : γ) => (f p).2) encC output

Project a second component and convert its encoding. The pair certificate fixes the source encoding; the conversion certificate supplies the efficient change of representation.

source
theorem Turing.MultiTapeTM.ComputableInPolyTime.ite' {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encC : Bool ↪ List Bool} {c : α → Bool} {f g : α → β} (hc : ComputableInPolyTime c encIn encC) (hf : ComputableInPolyTime f encIn encMid) (hg : ComputableInPolyTime g encIn encMid) :
ComputableInPolyTime (fun (x : α) => if c x = true then f x else g x) encIn encMid

A case distinction between functions computable in polynomial time on all inputs.

source
theorem Turing.MultiTapeTM.ComputableInPolyTime.encoding_comp {δ : Type u_4} {ε : Type u_5} {input : δ ↪ List Bool} {output : ε ↪ List Bool} {f : δ → ε} (hf : ComputableInPolyTime f input output) :
ComputableInPolyTime (fun (a : δ) => output (f a)) input encBits

Return the encoded word of an already computed value. The source and result encodings of that value remain fixed; this reads the representation already produced by its certificate.