Documentation

DescriptiveComplexity.Counting.QuantitativePull

Pulling a quantitative term back through an interpretation #

A term of quantitative first-order logic (DescriptiveComplexity.QTerm) over the target vocabulary of an interpretation I becomes a term over its source vocabulary, with the same value: DescriptiveComplexity.QTerm.pull and DescriptiveComplexity.QTerm.eval_pull. A formula is pulled back as formulas are (DescriptiveComplexity.FOInterpretation.pull); a sum or a product over the n-tuples of the interpreted universe, which is Tag × A ^ d, becomes a finite sum or product over the assignments of tags to the n variables, of a sum or product over n · d elements of A.

This is what closes FP under parsimonious reductions (DescriptiveComplexity.Counting.FP), the least fixed point being pulled back as for PTIME (DescriptiveComplexity.lfpAssign_pull).

source
def DescriptiveComplexity.QTerm.bigAdd {L : FirstOrder.Language} {α : Type} :
List (QTerm L α) → QTerm L α

The sum of a list of terms.

Equations
Instances For
    Dependency graph
    source
    def DescriptiveComplexity.QTerm.bigMul {L : FirstOrder.Language} {α : Type} :
    List (QTerm L α) → QTerm L α

    The product of a list of terms.

    Equations
    Instances For
      Dependency graph
      source
      noncomputable def DescriptiveComplexity.FOInterpretation.pullFormula {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {d : ℕ} (I : FOInterpretation L₁ L₂ Tag d) {α : Type} (φ : L₂.Formula α) (τ : α → Tag) :
      L₁.Formula (α × Fin d)

      The pullback of a formula with free variables through an interpretation: each variable becomes d variables, its tag being given.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Dependency graph
        source
        theorem DescriptiveComplexity.FOInterpretation.realize_pullFormula {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {d : ℕ} (I : FOInterpretation L₁ L₂ Tag d) {A : Type} [L₁.Structure A] {α : Type} (φ : L₂.Formula α) (τ : α → Tag) (w : α × Fin d → A) :
        (I.pullFormula φ τ).Realize w ↔ φ.Realize (I.liftEnv τ w)
        Dependency graph
        source
        def DescriptiveComplexity.blockRelabel {d : ℕ} {α : Type} {n : ℕ} :
        (α ⊕ Fin n) × Fin d → α × Fin d ⊕ Fin (n * d)

        The variables of a pulled-back quantifier block: the d coordinates of each of the n bound variables, laid out as one block of n * d.

        Equations
        Instances For
          Dependency graph
          source
          noncomputable def DescriptiveComplexity.QTerm.pull {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {d : ℕ} (I : FOInterpretation L₁ L₂ Tag d) {α : Type} :
          QTerm L₂ α → (α → Tag) → QTerm L₁ (α × Fin d)

          The pullback of a term through an interpretation.

          Equations
          Instances For
            Dependency graph
            source
            def DescriptiveComplexity.blockEquiv {L₁ L₂ : FirstOrder.Language} {Tag : Type} {d : ℕ} (I : FOInterpretation L₁ L₂ Tag d) (A : Type) (n : ℕ) :
            (Fin n → Tag) × (Fin (n * d) → A) ≃ (Fin n → I.Map A)

            The tuples of points of the interpreted universe: an assignment of tags, and one block of coordinates.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Dependency graph
              source
              theorem DescriptiveComplexity.liftEnv_blockRelabel {L₁ L₂ : FirstOrder.Language} {Tag : Type} {d : ℕ} (I : FOInterpretation L₁ L₂ Tag d) {A α : Type} {n : ℕ} (τ : α → Tag) (w : α × Fin d → A) (p : (Fin n → Tag) × (Fin (n * d) → A)) :
              I.liftEnv (Sum.elim τ p.1) (Sum.elim w p.2 ∘ blockRelabel) = Sum.elim (I.liftEnv τ w) ((blockEquiv I A n) p)
              Dependency graph
              source
              theorem DescriptiveComplexity.QTerm.eval_pull {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {d : ℕ} (I : FOInterpretation L₁ L₂ Tag d) {A : Type} [L₁.Structure A] [Finite A] {α : Type} (t : QTerm L₂ α) (τ : α → Tag) (w : α × Fin d → A) :
              (pull I t τ).eval w = t.eval (I.liftEnv τ w)

              A pulled-back term has, in the source structure, the value of the term in the interpreted structure.

              Dependency graph