ΣQSO(FO): quantitative second-order logic with second-order sums #
The fragment ΣQSO(FO) of the quantitative second-order logic of Arenas, Muñoz, Riveros 2020: above a Boolean layer of first-order formulas, terms denoting natural numbers,
α ::= φ | s | α + α | α · α | Σx. α | Πx. α | ΣX. α,
the first-order quantitative terms of DescriptiveComplexity.QTerm together
with the second-order sum ΣX. α, the sum over the relations X of the
value of α in the structure expanded by X
(DescriptiveComplexity.SQTerm, DescriptiveComplexity.SQTerm.eval). The
second-order product ΠX of the full logic QSO is left out: ΣQSO(FO) is the
fragment that captures #P over ordered structures, which is
DescriptiveComplexity.mem_sharpP_iff_sqDefinable.
The terms of ΣQSO(FO) over the vocabulary L, with free first-order
variables in α. A first-order quantifier binds a block of n variables at
once, the variables Sum.inr i of α ⊕ Fin n; a second-order sum binds the
relation variables of a block, the term under it being over the vocabulary
expanded by the block.
- ind
{L : FirstOrder.Language}
{α : Type}
(φ : L.Formula α)
: SQTerm L α
A formula:
1when it holds,0when it does not. - const
{L : FirstOrder.Language}
{α : Type}
(s : ℕ)
: SQTerm L α
A constant.
- add
{L : FirstOrder.Language}
{α : Type}
(s t : SQTerm L α)
: SQTerm L α
A sum.
- mul
{L : FirstOrder.Language}
{α : Type}
(s t : SQTerm L α)
: SQTerm L α
A product.
- sum
{L : FirstOrder.Language}
{α : Type}
(n : ℕ)
(t : SQTerm L (α ⊕ Fin n))
: SQTerm L α
Σx̄. t: the sum over then-tuples of elements. - prod
{L : FirstOrder.Language}
{α : Type}
(n : ℕ)
(t : SQTerm L (α ⊕ Fin n))
: SQTerm L α
Πx̄. t: the product over then-tuples of elements. - sosum
{L : FirstOrder.Language}
{α : Type}
(B : SOBlock)
(t : SQTerm (L.sum B.lang) α)
: SQTerm L α
ΣX̄. t: the sum over the assignments of a block of relation variables.
Instances For
Dependency graph
The value of a term in a structure, under a valuation.
Equations
- (DescriptiveComplexity.SQTerm.ind φ).eval x✝² x✝ = if φ.Realize x✝ then 1 else 0
- (DescriptiveComplexity.SQTerm.const s).eval x✝² x✝ = s
- (s.add t).eval x✝² x✝ = s.eval x✝² x✝ + t.eval x✝² x✝
- (s.mul t).eval x✝² x✝ = s.eval x✝² x✝ * t.eval x✝² x✝
- (DescriptiveComplexity.SQTerm.sum n t).eval x✝² x✝ = ∑ᶠ (w : Fin n → x✝²), t.eval x✝² (Sum.elim x✝ w)
- (DescriptiveComplexity.SQTerm.prod n t).eval x✝² x✝ = ∏ᶠ (w : Fin n → x✝²), t.eval x✝² (Sum.elim x✝ w)
- (DescriptiveComplexity.SQTerm.sosum B t).eval x✝² x✝ = ∑ᶠ (ρ : B.Assignment x✝²), t.eval x✝² x✝