Polynomial-time functions with a regular input format #
A finite Mathlib machine need only satisfy its time and output bounds on the
inputs accepted by a DFA. Checking that format and returning the empty string
on rejection yields a total function in canonical FP.
theorem
Complexity.MathlibTM0.BinaryMachine.guarded_outputsWithin
(M : BinaryMachine)
{σ : Type}
[Fintype σ]
(D : DFA Bool σ)
{w output : List Bool}
{time : ℕ}
(hw : w ∈ D.accepts)
(h : M.OutputsWithin w output time)
:
A DFA guard runs the source on valid inputs with linear overhead.
theorem
Complexity.MathlibTM0.BinaryMachine.guarded_outputsWithin_empty
(M : BinaryMachine)
{σ : Type}
[Fintype σ]
(D : DFA Bool σ)
{w : List Bool}
(hw : w ∉ D.accepts)
:
(M.guarded D).OutputsWithin w [] w.length
A DFA guard rejects malformed inputs with empty output in one scan.
theorem
Complexity.MathlibTM0.BinaryMachine.mem_FP_on_dfa
{M : BinaryMachine}
{σ : Type}
[Fintype σ]
(D : DFA Bool σ)
[DecidablePred fun (x : List Bool) => x ∈ D.accepts]
{f : List Bool → List Bool}
{p q : Polynomial ℕ}
(h : ∀ w ∈ D.accepts, M.OutputsWithin w (f w) (Polynomial.eval w.length p))
(hlen : ∀ w ∈ D.accepts, (f w).length ≤ Polynomial.eval w.length q)
:
Polynomial bounds on a regular domain give a total FP function, empty elsewhere.