Quantitative first-order logic, and the class FP

The quantitative logic of Arenas, Muñoz, Riveros 2020, in its first-order fragment QFO: above a layer of Boolean formulas, a layer of terms denoting natural numbers,

α ::= φ | s | α + α | α · α | Σx. α | Πx. α,

a formula counting 1 when it holds and 0 when it does not, and the two quantifiers being the sum and the product over the elements of the structure (DescriptiveComplexity.QTerm, DescriptiveComplexity.QTerm.eval). The logic, its semantics and the idea of separating a Boolean level from a quantitative one are theirs; QSO, the full logic of the paper, has second-order sums and products as well, which are not formalized here.

FP, the class of the functions computable in polynomial time – here those with natural-number values, which is what a DescriptiveComplexity.CountingProblem is – is defined by this logic over a Boolean layer of least fixed points: a problem is in FP when it is the value of a QFO term over the vocabulary expanded by the relations of a least fixed point, on every ordered finite structure (DescriptiveComplexity.FPDefinable). That QFO(LFP) captures FP over ordered structures is Theorem 4.4 of the paper; it is cited, not proved, as the capture theorems behind the other logically defined classes of the library are where no machine characterization is given.

A term over the plain ordered vocabulary, with no fixed point, defines a problem of FP (DescriptiveComplexity.fpDefinable_of_qfo): this is the case of most concrete functions, the fixed point being what makes the class all of FP.

Positivity is first-order

Whether a term is positive is a formula (DescriptiveComplexity.QTerm.pos): a sum is positive when some summand is, a product when every factor is. So the support of a problem of FP is in PTIME (DescriptiveComplexity.support_mem_PTIME_of_fpDefinable), as the support of a problem of #P is in NP; and a parsimoniously #P-hard problem cannot be in FP unless NP ⊆ PTIME (DescriptiveComplexity.NP_subset_PTIME_of_parsimoniousHard_of_fpDefinable).

Terms

inductive DescriptiveComplexity.QTerm (L : FirstOrder.Language) : Type → Type 1

The terms of quantitative first-order logic over a Boolean layer of first-order formulas, with free variables in α (Arenas, Muñoz, Riveros 2020, grammar (3.1), restricted to first-order quantifiers). A quantifier binds a block of n variables at once, the variables Sum.inr i of α ⊕ Fin n; the quantifiers Σx and Πx of the paper are the case n = 1.

• ind {L : FirstOrder.Language} {α : Type} (φ : L.Formula α) : QTerm L α

  A formula: 1 when it holds, 0 when it does not.

• const {L : FirstOrder.Language} {α : Type} (s : ℕ) : QTerm L α

  A constant.

• add {L : FirstOrder.Language} {α : Type} (s t : QTerm L α) : QTerm L α

  A sum.

• mul {L : FirstOrder.Language} {α : Type} (s t : QTerm L α) : QTerm L α

  A product.

• sum {L : FirstOrder.Language} {α : Type} (n : ℕ) (t : QTerm L (α ⊕ Fin n)) : QTerm L α

  Σx̄. t: the sum over the n-tuples of elements of the structure.

• prod {L : FirstOrder.Language} {α : Type} (n : ℕ) (t : QTerm L (α ⊕ Fin n)) : QTerm L α

  Πx̄. t: the product over the n-tuples of elements of the structure.

noncomputable def DescriptiveComplexity.QTerm.eval {L : FirstOrder.Language} {A : Type} [L.Structure A] {α : Type} : QTerm L α → (α → A) → ℕ

The value of a term in a structure, under a valuation (Table 1 of the paper).

Equations

• (DescriptiveComplexity.QTerm.ind φ).eval x✝ = if φ.Realize x✝ then 1 else 0
• (DescriptiveComplexity.QTerm.const s).eval x✝ = s
• (s.add t).eval x✝ = s.eval x✝ + t.eval x✝
• (s.mul t).eval x✝ = s.eval x✝ * t.eval x✝
• (DescriptiveComplexity.QTerm.sum n t).eval x✝ = ∑ᶠ (w : Fin n → A), t.eval (Sum.elim x✝ w)
• (DescriptiveComplexity.QTerm.prod n t).eval x✝ = ∏ᶠ (w : Fin n → A), t.eval (Sum.elim x✝ w)

noncomputable def DescriptiveComplexity.QTerm.value {L : FirstOrder.Language} (t : QTerm L Empty) (A : Type) [L.Structure A] : ℕ

The value of a closed term.

Equations

• t.value A = t.eval default

def DescriptiveComplexity.QTerm.onTerm {L L' : FirstOrder.Language} (Φ : L →ᴸ L') {α : Type} : QTerm L α → QTerm L' α

Reading a term in a larger vocabulary.

Equations

• DescriptiveComplexity.QTerm.onTerm Φ (DescriptiveComplexity.QTerm.ind φ) = DescriptiveComplexity.QTerm.ind (Φ.onFormula φ)
• DescriptiveComplexity.QTerm.onTerm Φ (DescriptiveComplexity.QTerm.const s) = DescriptiveComplexity.QTerm.const s
• DescriptiveComplexity.QTerm.onTerm Φ (s.add t) = (DescriptiveComplexity.QTerm.onTerm Φ s).add (DescriptiveComplexity.QTerm.onTerm Φ t)
• DescriptiveComplexity.QTerm.onTerm Φ (s.mul t) = (DescriptiveComplexity.QTerm.onTerm Φ s).mul (DescriptiveComplexity.QTerm.onTerm Φ t)
• DescriptiveComplexity.QTerm.onTerm Φ (DescriptiveComplexity.QTerm.sum n t) = DescriptiveComplexity.QTerm.sum n (DescriptiveComplexity.QTerm.onTerm Φ t)
• DescriptiveComplexity.QTerm.onTerm Φ (DescriptiveComplexity.QTerm.prod n t) = DescriptiveComplexity.QTerm.prod n (DescriptiveComplexity.QTerm.onTerm Φ t)

def DescriptiveComplexity.QTerm.relabel {L : FirstOrder.Language} {α : Type} : QTerm L α → {β : Type} → (α → β) → QTerm L β

Renaming the free variables of a term.

Equations

• (DescriptiveComplexity.QTerm.ind φ).relabel x✝ = DescriptiveComplexity.QTerm.ind (FirstOrder.Language.Formula.relabel x✝ φ)
• (DescriptiveComplexity.QTerm.const s).relabel x✝ = DescriptiveComplexity.QTerm.const s
• (s.add t).relabel x✝ = (s.relabel x✝).add (t.relabel x✝)
• (s.mul t).relabel x✝ = (s.relabel x✝).mul (t.relabel x✝)
• (DescriptiveComplexity.QTerm.sum n t).relabel x✝ = DescriptiveComplexity.QTerm.sum n (t.relabel (Sum.map x✝ id))
• (DescriptiveComplexity.QTerm.prod n t).relabel x✝ = DescriptiveComplexity.QTerm.prod n (t.relabel (Sum.map x✝ id))

Positivity

noncomputable def DescriptiveComplexity.QTerm.pos {L : FirstOrder.Language} {α : Type} : QTerm L α → L.Formula α

“The term is positive”, as a formula: a formula is positive when it holds, a sum when some summand is, a product when every factor is.

Equations

• (DescriptiveComplexity.QTerm.ind φ).pos = φ
• (DescriptiveComplexity.QTerm.const s).pos = if s = 0 then ⊥ else ⊤
• (s.add t).pos = s.pos ⊔ t.pos
• (s.mul t).pos = s.pos ⊓ t.pos
• (DescriptiveComplexity.QTerm.sum n t).pos = FirstOrder.Language.Formula.iExs (Fin n) t.pos
• (DescriptiveComplexity.QTerm.prod n t).pos = FirstOrder.Language.Formula.iAlls (Fin n) t.pos

FP

structure DescriptiveComplexity.QLFPDef (L : FirstOrder.Language) : Type 1

A definition in QFO(LFP): a least fixed point, as for DescriptiveComplexity.LFPDef, and a quantitative term over the vocabulary expanded by its relations, read at the fixed point.

• B : SOBlock

  The relation variables computed by the fixed point.

• k : ℕ

  The number of first-order variables shared by the rules.

• rules : List (HornClause (L.sum FirstOrder.Language.order) self.B self.k)

  The rules defining the variables.

• out : QTerm ((L.sum FirstOrder.Language.order).sum self.B.lang) Empty

  The quantitative output.

noncomputable def DescriptiveComplexity.QLFPDef.value {L : FirstOrder.Language} (d : QLFPDef L) (A : Type) [L.Structure A] [LinearOrder A] : ℕ

The value of a definition on an ordered structure: the output, read at the least fixed point of the rules.

Equations

• d.value A = d.out.value A

def DescriptiveComplexity.FPDefinable {L : FirstOrder.Language} [L.IsRelational] (C : CountingProblem L) : Prop

A counting problem is in FP when, on nonempty finite structures, it is the value of a definition in QFO(LFP), whatever the linear order (Arenas, Muñoz, Riveros 2020, Theorem 4.4).

Equations

• DescriptiveComplexity.FPDefinable C = ∃ (d : DescriptiveComplexity.QLFPDef L), ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A], C.Count A = d.value A

theorem DescriptiveComplexity.fpDefinable_congr {L : FirstOrder.Language} [L.IsRelational] {C C' : CountingProblem L} (h : ∀ (A : Type) [inst : L.Structure A] [Finite A], C.Count A = C'.Count A) (hC : FPDefinable C) : FPDefinable C'

theorem DescriptiveComplexity.fpDefinable_of_qfo {L : FirstOrder.Language} [L.IsRelational] {C : CountingProblem L} (t : QTerm (L.sum FirstOrder.Language.order) Empty) (h : ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A], C.Count A = t.value A) : FPDefinable C

A term with no fixed point defines a problem of FP: a counting problem that is the value of a QFO term over the ordered vocabulary is in FP. Registered in the Lax archive as Lax366625.FPByDigits.fpDefinable_of_qfo.

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

The support of a problem of FP is in PTIME: positivity of the output term is a first-order formula over the fixed point.

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

A problem of FP is not parsimoniously #P-hard, unless NP ⊆ PTIME.