The weights of a weighted instance, as quantitative terms

A weight of a fact of a weighted instance (DescriptiveComplexity.Counting.WeightedWorlds) is written in binary in the instance. It is the value of a term of quantitative first-order logic:

• DescriptiveComplexity.wNum: the number written by the bits of a fact, Σi. [bit i] · Πj. ([j below i] + 1);
• DescriptiveComplexity.fullPresT, DescriptiveComplexity.fullAbsT: the weight of presence and the weight of absence of a fact, whatever its status (DescriptiveComplexity.fullPresWeight, DescriptiveComplexity.fullAbsWeight);
• DescriptiveComplexity.linGuardT: 1 when the positions are linearly ordered, 0 otherwise.

These are the leaves of a term computing the weighted count of a safe query: see DescriptiveComplexity.Examples.ProbabilisticQueries.

@[reducible, inline]

abbrev DescriptiveComplexity.wOrd (L : FirstOrder.Language) : FirstOrder.Language

The vocabulary of weighted instances, with the order of the definitions.

Equations

• DescriptiveComplexity.wOrd L = (DescriptiveComplexity.weightedLang L).sum FirstOrder.Language.order

noncomputable def DescriptiveComplexity.posLtF {L : FirstOrder.Language} {δ : Type} (j i : δ) : (wOrd L).Formula δ

“j is a position strictly below i”, in the order of the instance.

Equations

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

noncomputable def DescriptiveComplexity.wNum {L : FirstOrder.Language} {δ : Type} {n : ℕ} (S : WeightedRel L (n + 1)) (e : Fin n → δ) : QTerm (wOrd L) δ

The number written by the bits of a fact: S(x̄, ·) read in binary.

Equations

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

def DescriptiveComplexity.certA {L : FirstOrder.Language} {δ : Type} {n : ℕ} (R : L.Relations n) (e : Fin n → δ) : (wOrd L).Formula δ

“The fact is certain.”

Equations

• DescriptiveComplexity.certA R e = DescriptiveComplexity.factAtom (Sum.inl (DescriptiveComplexity.WeightedRel.cert R)) e

def DescriptiveComplexity.uncA {L : FirstOrder.Language} {δ : Type} {n : ℕ} (R : L.Relations n) (e : Fin n → δ) : (wOrd L).Formula δ

“The fact is uncertain.”

Equations

• DescriptiveComplexity.uncA R e = DescriptiveComplexity.factAtom (Sum.inl (DescriptiveComplexity.WeightedRel.unc R)) e

noncomputable def DescriptiveComplexity.fullPresT {L : FirstOrder.Language} {δ : Type} {n : ℕ} (R : L.Relations n) (e : Fin n → δ) : QTerm (wOrd L) δ

The weight of presence of a fact, as a term.

Equations

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

noncomputable def DescriptiveComplexity.fullAbsT {L : FirstOrder.Language} {δ : Type} {n : ℕ} (R : L.Relations n) (e : Fin n → δ) : QTerm (wOrd L) δ

The weight of absence of a fact, as a term.

Equations

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

noncomputable def DescriptiveComplexity.linGuardT {L : FirstOrder.Language} {δ : Type} : QTerm (wOrd L) δ

1 when the positions of the instance are linearly ordered, 0 otherwise.

Equations

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