Finite input and output alphabets transfer to canonical FP #
Explicit finite-alphabet codes supply a total binary interface: the machine rejects malformed codewords with empty output before running the source. Input and output alphabets can differ and may be empty. Marked input and complete decoded output add only linear encoding and parsing overhead.
theorem
Complexity.MathlibTM0.AlphabetMachine.computes_cslib
{Input Output : Type}
(M : AlphabetMachine Input Output)
(ci : FiniteAlphabetCode Input)
(co : FiniteAlphabetCode Output)
{input : List Input}
{output : List Output}
{time : ℕ}
(h : M.OutputsWithin input output time)
:
(M.machine ci co).ComputesInTimeAndSpace (ci.encode input) (co.encode output)
(2 * (ci.encode input).length + time + (co.size + 1) * output.length + 4)
(Turing.MultiTapeTM.spaceUsed (Turing.MultiTapeTM.initCfg (ci.encode input))
(2 * (ci.encode input).length + time + (co.size + 1) * output.length + 4))
Parse input codes, preserve the complete source output, and emit its exact binary encoding.
theorem
Complexity.MathlibTM0.AlphabetMachine.mem_FP
{Input Output : Type}
{M : AlphabetMachine Input Output}
(ci : FiniteAlphabetCode Input)
(co : FiniteAlphabetCode Output)
{f : List Input → List Output}
{p q : Polynomial ℕ}
(h : ∀ (xs : List Input), M.OutputsWithin xs (f xs) (Polynomial.eval xs.length p))
(hlen : ∀ (xs : List Input), (f xs).length ≤ Polynomial.eval xs.length q)
:
Polynomial-time source word computations give total binary FP functions under explicit codes.
theorem
Complexity.MathlibTM0.AlphabetMachine.mem_FP_on_dfa
{Input Output : Type}
{M : AlphabetMachine Input Output}
(ci : FiniteAlphabetCode Input)
(co : FiniteAlphabetCode Output)
{σ : Type}
[Fintype σ]
(D : DFA Bool σ)
[DecidablePred fun (x : List Bool) => x ∈ D.accepts]
{f : List Input → List Output}
{p q : Polynomial ℕ}
(h : ∀ (xs : List Input), ci.encode xs ∈ D.accepts → M.OutputsWithin xs (f xs) (Polynomial.eval xs.length p))
(hlen : ∀ (xs : List Input), ci.encode xs ∈ D.accepts → (f xs).length ≤ Polynomial.eval xs.length q)
:
Source bounds restricted to a regular binary input domain suffice after DFA validation.