Documentation

Complexity.Logics.FirstOrder.Ordered.DomainInterpretation.Composition

Composition of certified ordered interpretations #

An outer ordered interpretation J is composed with an inner interpretation I carrying a numeric certificate. The composite has dimension l * k, flattening the outer coordinate before the inner one. Its domain says that every block is a domain tuple of I and that the ranks of the blocks satisfy the pullback of the domain formula of J; its relation formulas are pullbacks of those of J. The inner certificate is what makes these pullbacks possible: the formulas of J mention the numeric symbols of the image of I.

Flattened lexicographic order on the composite domain is lexicographic order on the ranks of the blocks, so the composite ranks are exactly the ranks of J in the image of I. Hence the image of the composite is the image of J in the image of I. Pulling back an outer certificate through the inner one certifies the composite. This is the substitution proof of [Immerman1999, Proposition 1.28 and Exercise 2.15(1)].

Main definitions #

Main results #

References #

source
noncomputable def Cslib.Logic.FO.Ordered.DomainInterpretation.Certificate.pullback {L : FirstOrder.Language} {L' : FirstOrder.Language} {k l : ℕ} [L'.IsRelational] {I : DomainInterpretation L L' k} (C : I.Certificate) {β : Type u_1} (φ : (language L').Formula (β × Fin l)) :
(language L).Formula (β × Fin (l * k))

Pull back a formula on blocks of l target variables along a certified interpretation, and flatten each block of blocks to l * k source variables.

Instances For
    source
    noncomputable def Cslib.Logic.FO.Ordered.DomainInterpretation.comp {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {k l : ℕ} [L'.IsRelational] (J : DomainInterpretation L' L'' l) {I : DomainInterpretation L L' k} (C : I.Certificate) :
    DomainInterpretation L L'' (l * k)

    Compose an outer interpretation with a certified inner interpretation, flattening (j, i) to j * k + i.

    Instances For
      source
      theorem Cslib.Logic.FO.Ordered.DomainInterpretation.realize_comp_domain {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {k l : ℕ} [L'.IsRelational] (J : DomainInterpretation L' L'' l) {I : DomainInterpretation L L' k} (C : I.Certificate) {M : Structure L} (x : Fin (l * k) → Fin M.size) :
      (J.comp C).domain.Realize x ↔ (∀ (j : Fin l), I.domain.Realize fun (i : Fin k) => x (finProdFinEquiv (j, i))) ∧ (C.onFormula J.domain).Realize fun (p : Fin l × Fin k) => x (finProdFinEquiv p)
      source
      theorem Cslib.Logic.FO.Ordered.DomainInterpretation.card_comp {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {k l : ℕ} [L'.IsRelational] (J : DomainInterpretation L' L'' l) {I : DomainInterpretation L L' k} (C : I.Certificate) (hI : I.Admissible) (M : Structure L) :
      (J.comp C).card M = J.card (I.map hI M)

      The composite image has one element per domain tuple of J in the image of I.

      source
      theorem Cslib.Logic.FO.Ordered.DomainInterpretation.unrank_comp {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {k l : ℕ} [L'.IsRelational] (J : DomainInterpretation L' L'' l) {I : DomainInterpretation L L' k} (C : I.Certificate) {M : Structure L} (hI : I.Admissible) (i : Fin ((J.comp C).card M)) :
      (J.comp C).unrank M i = flattenTuple fun (j : Fin l) => I.unrank M (J.unrank (I.map hI M) (Fin.cast ⋯ i) j)

      The composite ranks flatten the blocks of the ranks of J in the image of I.

      source
      theorem Cslib.Logic.FO.Ordered.DomainInterpretation.admissible_comp {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {k l : ℕ} [L'.IsRelational] (J : DomainInterpretation L' L'' l) {I : DomainInterpretation L L' k} (C : I.Certificate) (hI : I.Admissible) (hJ : J.Admissible) :
      (J.comp C).Admissible

      The composite of admissible interpretations is admissible.

      source
      theorem Cslib.Logic.FO.Ordered.DomainInterpretation.realize_pullback_comp {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {k l : ℕ} [L'.IsRelational] (J : DomainInterpretation L' L'' l) {I : DomainInterpretation L L' k} (C : I.Certificate) {M : Structure L} (hI : I.Admissible) {β : Type u_1} (φ : (language L').Formula (β × Fin l)) (v : β → Fin ((J.comp C).card M)) :
      ((C.pullback φ).Realize fun (p : β × Fin (l * k)) => (J.comp C).unrank M (v p.1) p.2) ↔ φ.Realize fun (p : β × Fin l) => J.unrank (I.map hI M) (Fin.cast ⋯ (v p.1)) p.2

      A pulled-back formula holds of composite ranks when it holds of the corresponding ranks of J in the image of I.

      source
      theorem Cslib.Logic.FO.Ordered.DomainInterpretation.map_comp {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {k l : ℕ} [L'.IsRelational] (J : DomainInterpretation L' L'' l) {I : DomainInterpretation L L' k} (C : I.Certificate) [L''.IsRelational] (hI : I.Admissible) (hJ : J.Admissible) (M : Structure L) :
      (J.comp C).map ⋯ M = J.map hJ (I.map hI M)

      The composite image is the iterated image.

      source
      noncomputable def Cslib.Logic.FO.Ordered.DomainInterpretation.Certificate.comp {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {k l : ℕ} [L'.IsRelational] {J : DomainInterpretation L' L'' l} (C' : J.Certificate) {I : DomainInterpretation L L' k} (C : I.Certificate) (hI : I.Admissible) :
      (J.comp C).Certificate

      Pull back the outer numeric definitions through the inner certificate.

      Instances For