Writing quantitative terms

Helpers for writing a term of quantitative first-order logic (DescriptiveComplexity.QTerm) the way it is read, and for evaluating it.

A quantifier of DescriptiveComplexity.QTerm binds a block of variables, named by position in a sum type. DescriptiveComplexity.QTerm.sumOver and DescriptiveComplexity.QTerm.prodOver bind one variable and hand it to the body by name: the body is a function of the bound variable, and of the way the variables already in scope are read under the binder. So sumOver fun up x => f (up y) x is Σx. f(y, x), and its value is a sum over the elements (DescriptiveComplexity.QTerm.eval_sumOver).

DescriptiveComplexity.QTerm.cond is the choice between two terms by a formula.

def DescriptiveComplexity.QTerm.sumOver {L : FirstOrder.Language} {γ : Type} (f : {δ : Type} → (γ → δ) → δ → QTerm L δ) : QTerm L γ

Σx. t: the body is given the reading of the variables in scope, and the bound variable.

Equations

• DescriptiveComplexity.QTerm.sumOver f = DescriptiveComplexity.QTerm.sum 1 (f Sum.inl (Sum.inr 0))

def DescriptiveComplexity.QTerm.prodOver {L : FirstOrder.Language} {γ : Type} (f : {δ : Type} → (γ → δ) → δ → QTerm L δ) : QTerm L γ

Πx. t: the body is given the reading of the variables in scope, and the bound variable.

Equations

• DescriptiveComplexity.QTerm.prodOver f = DescriptiveComplexity.QTerm.prod 1 (f Sum.inl (Sum.inr 0))

def DescriptiveComplexity.QTerm.cond {L : FirstOrder.Language} {γ : Type} (φ : L.Formula γ) (s t : QTerm L γ) : QTerm L γ

The choice between two terms: s where the formula holds, t where it does not.

Equations

• DescriptiveComplexity.QTerm.cond φ s t = ((DescriptiveComplexity.QTerm.ind φ).mul s).add ((DescriptiveComplexity.QTerm.ind (FirstOrder.Language.BoundedFormula.not φ)).mul t)

theorem DescriptiveComplexity.QTerm.eval_sumOver {L : FirstOrder.Language} {γ A : Type} [L.Structure A] (f : {δ : Type} → (γ → δ) → δ → QTerm L δ) (v : γ → A) : (sumOver fun {δ : Type} => f).eval v = ∑ᶠ (a : A), (f Sum.inl (Sum.inr 0)).eval (Sum.elim v fun (x : Fin 1) => a)