The class FP

FP is the class of the functions computable in polynomial time. It is a class of computations more than of counting: nothing in a function of FP has to count anything. The library sees its natural-number-valued part, a function from structures to numbers being what DescriptiveComplexity.CountingProblem is, whether or not the number counts solutions. This is the convention of the paper cited below, which defines FP as the class of the functions f : Σ* → ℕ computable in polynomial time (its Section 2.2), lists it among the “counting complexity classes”, and notes that the value of a counting problem need not be a number of solutions. Functions with other outputs (strings, structures, witnesses of a search problem) are outside this formalization.

As a class of the library (DescriptiveComplexity.FP): the problems definable in QFO(LFP), the first-order fragment of the quantitative logic of Arenas, Muñoz, Riveros 2020 over a Boolean layer of least fixed points. That this logic captures FP over ordered structures is their Theorem 4.4.

The class is closed under ordered parsimonious reductions (DescriptiveComplexity.FPDefinable.of_orderedParsimonious): the least fixed point pulls back through the interpretation as it does for PTIME (DescriptiveComplexity.lfpAssign_pull), and the quantitative output as DescriptiveComplexity.QTerm.pull.

theorem DescriptiveComplexity.FPDefinable.of_orderedParsimonious {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {C : CountingProblem L₁} {D : CountingProblem L₂} (f : OrderedParsimoniousReduction C D) (h : FPDefinable D) : FPDefinable C

FP is closed under ordered parsimonious reductions. Registered in the Lax archive as Lax366625.FPClosure.FP_mem_of_orderedParsimonious.

theorem DescriptiveComplexity.FPDefinable.of_parsimonious {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {C : CountingProblem L₁} {D : CountingProblem L₂} (f : ParsimoniousReduction C D) (h : FPDefinable D) : FPDefinable C

FP is closed under parsimonious reductions.

noncomputable def DescriptiveComplexity.FP : CountingClass

The class FP, in its natural-number-valued part: the functions from structures to numbers definable in QFO(LFP), i.e., computable in polynomial time (Arenas, Muñoz, Riveros 2020, Theorem 4.4). It is closed under parsimonious reductions.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.support_mem_PTIME_of_mem_FP {L : FirstOrder.Language} [L.IsRelational] {C : CountingProblem L} (h : FP.Mem C) : PTIME.Mem C.support

The support of a problem of FP is in PTIME. Registered in the Lax archive as Lax366625.FPAndPTIME.support_mem_PTIME_of_mem_FP.

theorem DescriptiveComplexity.NP_subset_PTIME_of_mem_FP_of_parsimoniousHard {L : FirstOrder.Language} [L.IsRelational] {C : CountingProblem L} (h : FP.Mem C) (hard : SharpP.ParsimoniousHard C) : NP ⊆ PTIME

No problem of FP is parsimoniously #P-hard, unless NP ⊆ PTIME. Registered in the Lax archive as Lax366625.FPAndPTIME.NP_subset_PTIME_of_mem_FP_of_parsimoniousHard.