Post-processing terms

The arithmetic a counting reduction may apply to the answer of its one oracle call (DescriptiveComplexity.Counting.Reduction). Two layers, kept apart so that every number written stays of polynomially many bits:

• DescriptiveComplexity.PolyTerm: numerals, definable cardinalities – the number of tagged tuples of the instance satisfying first-order formulas over the ordered expansion – sums and products. Its values are polynomial in the size of the instance.
• DescriptiveComplexity.PostTerm: the oracle's answer, a polynomial term, a power of two whose exponent is a polynomial term, sums, products, truncated differences, quotients and remainders.

So a post-processing term is a fixed arithmetic expression over the oracle's answer and first-order definable counts: it can be evaluated in polynomial time, and it does no counting of its own beyond tuples of the instance.

Both layers are pulled back along a relativized interpretation (DescriptiveComplexity.PolyTerm.pull, DescriptiveComplexity.PostTerm.pull): a definable cardinality of the interpreted structure is a definable cardinality of the instance. A cardinality is stored as the universe of a relativized interpretation into the empty vocabulary, so the pullback is the composition of relativized interpretations and needs nothing new. With substitution for the oracle's answer (DescriptiveComplexity.PostTerm.subst), this is what makes one-call reductions compose.

Polynomial terms

inductive DescriptiveComplexity.PolyTerm (L : FirstOrder.Language) : Type 1

Terms denoting numbers polynomial in the size of the instance: numerals, definable cardinalities, sums and products.

• num {L : FirstOrder.Language} (k : ℕ) : PolyTerm L

  A numeral.

• card {L : FirstOrder.Language} {Tag : Type} [Finite Tag] {dim : ℕ} (J : RelFOInterpretation (L.sum FirstOrder.Language.order) FirstOrder.Language.empty Tag dim) : PolyTerm L

  The number of tagged tuples satisfying their tag's domain formula, i.e., the size of the universe of a relativized interpretation.

• add {L : FirstOrder.Language} (p q : PolyTerm L) : PolyTerm L

  A sum.

• mul {L : FirstOrder.Language} (p q : PolyTerm L) : PolyTerm L

  A product.

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

The value of a polynomial term at an ordered structure.

Equations

• DescriptiveComplexity.PolyTerm.eval A (DescriptiveComplexity.PolyTerm.num k) = k
• DescriptiveComplexity.PolyTerm.eval A (DescriptiveComplexity.PolyTerm.card J) = Nat.card (J.MapRel A)
• DescriptiveComplexity.PolyTerm.eval A (p.add q) = DescriptiveComplexity.PolyTerm.eval A p + DescriptiveComplexity.PolyTerm.eval A q
• DescriptiveComplexity.PolyTerm.eval A (p.mul q) = DescriptiveComplexity.PolyTerm.eval A p * DescriptiveComplexity.PolyTerm.eval A q

def DescriptiveComplexity.PolyTerm.cardInterp {L : FirstOrder.Language} {k : ℕ} (φ : (L.sum FirstOrder.Language.order).Formula (Fin k)) : RelFOInterpretation (L.sum FirstOrder.Language.order) FirstOrder.Language.empty Unit k

The relativized interpretation into the empty vocabulary whose universe is the set of tuples satisfying a formula.

Equations

• DescriptiveComplexity.PolyTerm.cardInterp φ = { relFormula := fun {n : ℕ} (R : FirstOrder.Language.empty.Relations n) => isEmptyElim R, domFormula := fun (x : Unit) => φ }

def DescriptiveComplexity.PolyTerm.count {L : FirstOrder.Language} {k : ℕ} (φ : (L.sum FirstOrder.Language.order).Formula (Fin k)) : PolyTerm L

The number of k-tuples satisfying a first-order formula over the ordered expansion.

Equations

• DescriptiveComplexity.PolyTerm.count φ = DescriptiveComplexity.PolyTerm.card (DescriptiveComplexity.PolyTerm.cardInterp φ)

theorem DescriptiveComplexity.PolyTerm.eval_count_one {L : FirstOrder.Language} (A : Type) [L.Structure A] [LinearOrder A] (φ : (L.sum FirstOrder.Language.order).Formula (Fin 1)) : eval A (count φ) = Nat.card { a : A // φ.Realize fun (x : Fin 1) => a }

The number of elements satisfying a first-order formula over the ordered expansion, as a cardinality of a set of elements.

def DescriptiveComplexity.PolyTerm.univ {L : FirstOrder.Language} : PolyTerm L

The number of elements of the instance.

Equations

• DescriptiveComplexity.PolyTerm.univ = DescriptiveComplexity.PolyTerm.count ⊤

theorem DescriptiveComplexity.PolyTerm.eval_univ {L : FirstOrder.Language} (A : Type) [L.Structure A] [LinearOrder A] : eval A univ = Nat.card A

noncomputable def DescriptiveComplexity.PolyTerm.pull {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {T : Type} [LinearOrder T] [Finite T] {d : ℕ} (I : RelFOInterpretation (L₁.sum FirstOrder.Language.order) L₂ T d) : PolyTerm L₂ → PolyTerm L₁

The pullback of a polynomial term along a relativized interpretation: a definable cardinality of the interpreted structure, ordered lexicographically, is the size of the universe of a composite interpretation.

Equations

• DescriptiveComplexity.PolyTerm.pull I (DescriptiveComplexity.PolyTerm.num k) = DescriptiveComplexity.PolyTerm.num k
• DescriptiveComplexity.PolyTerm.pull I (DescriptiveComplexity.PolyTerm.card J) = DescriptiveComplexity.PolyTerm.card (J.compRel I.ordExtendRel)
• DescriptiveComplexity.PolyTerm.pull I (p.add q) = (DescriptiveComplexity.PolyTerm.pull I p).add (DescriptiveComplexity.PolyTerm.pull I q)
• DescriptiveComplexity.PolyTerm.pull I (p.mul q) = (DescriptiveComplexity.PolyTerm.pull I p).mul (DescriptiveComplexity.PolyTerm.pull I q)

theorem DescriptiveComplexity.PolyTerm.eval_pull {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {T : Type} [LinearOrder T] [Finite T] {d : ℕ} (I : RelFOInterpretation (L₁.sum FirstOrder.Language.order) L₂ T d) (A : Type) [L₁.Structure A] [LinearOrder A] (p : PolyTerm L₂) : eval A (pull I p) = eval (I.MapRel A) p

A pulled-back polynomial term has, at the instance, the value of the original term at the interpreted structure.

Post-processing terms

inductive DescriptiveComplexity.PostTerm (L : FirstOrder.Language) : Type 1

The arithmetic applied to the answer of an oracle call: polynomial terms, powers of two with a polynomial exponent, and the operations +, *, truncated -, / and % of the natural numbers.

• oracle {L : FirstOrder.Language} : PostTerm L

  The answer of the oracle.

• poly {L : FirstOrder.Language} (p : PolyTerm L) : PostTerm L

  A polynomial term.

• pow2 {L : FirstOrder.Language} (p : PolyTerm L) : PostTerm L

  Two to the power of a polynomial term.

• add {L : FirstOrder.Language} (s t : PostTerm L) : PostTerm L

  A sum.

• mul {L : FirstOrder.Language} (s t : PostTerm L) : PostTerm L

  A product.

• sub {L : FirstOrder.Language} (s t : PostTerm L) : PostTerm L

  A truncated difference.

• div {L : FirstOrder.Language} (s t : PostTerm L) : PostTerm L

  A quotient.

• mod {L : FirstOrder.Language} (s t : PostTerm L) : PostTerm L

  A remainder.

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

The value of a post-processing term at an ordered structure, given the answer c of the oracle.

Equations

• DescriptiveComplexity.PostTerm.eval A c DescriptiveComplexity.PostTerm.oracle = c
• DescriptiveComplexity.PostTerm.eval A c (DescriptiveComplexity.PostTerm.poly p) = DescriptiveComplexity.PolyTerm.eval A p
• DescriptiveComplexity.PostTerm.eval A c (DescriptiveComplexity.PostTerm.pow2 p) = 2 ^ DescriptiveComplexity.PolyTerm.eval A p
• DescriptiveComplexity.PostTerm.eval A c (s.add t) = DescriptiveComplexity.PostTerm.eval A c s + DescriptiveComplexity.PostTerm.eval A c t
• DescriptiveComplexity.PostTerm.eval A c (s.mul t) = DescriptiveComplexity.PostTerm.eval A c s * DescriptiveComplexity.PostTerm.eval A c t
• DescriptiveComplexity.PostTerm.eval A c (s.sub t) = DescriptiveComplexity.PostTerm.eval A c s - DescriptiveComplexity.PostTerm.eval A c t
• DescriptiveComplexity.PostTerm.eval A c (s.div t) = DescriptiveComplexity.PostTerm.eval A c s / DescriptiveComplexity.PostTerm.eval A c t
• DescriptiveComplexity.PostTerm.eval A c (s.mod t) = DescriptiveComplexity.PostTerm.eval A c s % DescriptiveComplexity.PostTerm.eval A c t

def DescriptiveComplexity.PostTerm.subst {L : FirstOrder.Language} : PostTerm L → PostTerm L → PostTerm L

Substitution of a term for the answer of the oracle.

Equations

• DescriptiveComplexity.PostTerm.oracle.subst x✝ = x✝
• (DescriptiveComplexity.PostTerm.poly p).subst x✝ = DescriptiveComplexity.PostTerm.poly p
• (DescriptiveComplexity.PostTerm.pow2 p).subst x✝ = DescriptiveComplexity.PostTerm.pow2 p
• (s.add t).subst x✝ = (s.subst x✝).add (t.subst x✝)
• (s.mul t).subst x✝ = (s.subst x✝).mul (t.subst x✝)
• (s.sub t).subst x✝ = (s.subst x✝).sub (t.subst x✝)
• (s.div t).subst x✝ = (s.subst x✝).div (t.subst x✝)
• (s.mod t).subst x✝ = (s.subst x✝).mod (t.subst x✝)

theorem DescriptiveComplexity.PostTerm.eval_subst {L : FirstOrder.Language} (A : Type) [L.Structure A] [LinearOrder A] (c : ℕ) (s u : PostTerm L) : eval A c (s.subst u) = eval A (eval A c u) s

noncomputable def DescriptiveComplexity.PostTerm.pull {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {T : Type} [LinearOrder T] [Finite T] {d : ℕ} (I : RelFOInterpretation (L₁.sum FirstOrder.Language.order) L₂ T d) : PostTerm L₂ → PostTerm L₁

The pullback of a post-processing term along a relativized interpretation, its polynomial terms being pulled back.

Equations

• DescriptiveComplexity.PostTerm.pull I DescriptiveComplexity.PostTerm.oracle = DescriptiveComplexity.PostTerm.oracle
• DescriptiveComplexity.PostTerm.pull I (DescriptiveComplexity.PostTerm.poly p) = DescriptiveComplexity.PostTerm.poly (DescriptiveComplexity.PolyTerm.pull I p)
• DescriptiveComplexity.PostTerm.pull I (DescriptiveComplexity.PostTerm.pow2 p) = DescriptiveComplexity.PostTerm.pow2 (DescriptiveComplexity.PolyTerm.pull I p)
• DescriptiveComplexity.PostTerm.pull I (s.add t) = (DescriptiveComplexity.PostTerm.pull I s).add (DescriptiveComplexity.PostTerm.pull I t)
• DescriptiveComplexity.PostTerm.pull I (s.mul t) = (DescriptiveComplexity.PostTerm.pull I s).mul (DescriptiveComplexity.PostTerm.pull I t)
• DescriptiveComplexity.PostTerm.pull I (s.sub t) = (DescriptiveComplexity.PostTerm.pull I s).sub (DescriptiveComplexity.PostTerm.pull I t)
• DescriptiveComplexity.PostTerm.pull I (s.div t) = (DescriptiveComplexity.PostTerm.pull I s).div (DescriptiveComplexity.PostTerm.pull I t)
• DescriptiveComplexity.PostTerm.pull I (s.mod t) = (DescriptiveComplexity.PostTerm.pull I s).mod (DescriptiveComplexity.PostTerm.pull I t)