Pulling a walk back through a relativized interpretation

A walk on the structure an interpretation produces is a walk on the base structure: its tuples become tuples of coordinates, and the tags of its points – being finite, static data – are carried in the mode (DescriptiveComplexity.ParamTCSpec.comapRel). This is DescriptiveComplexity.TCSpec.comap of DescriptiveComplexity.TransitiveClosurePull with the two features a reduction notion needs added: parameters, so that what is pulled back is a relation rather than a sentence, and a definable domain, so that the interpretation may be relativized.

What the domain costs

Over the whole universe the encoding of nodes is a bijection and the transfer is an isomorphism of walks. Over a definable domain it is not: a tagged tuple of the base need not be a point of the target at all. The pulled walk is therefore guarded – its step formula asks both endpoints to be in the domain (DescriptiveComplexity.ParamTCSpec.domTupleF) – so that it never leaves the image of the encoding, and the correspondence (DescriptiveComplexity.ParamTCSpec.reachAt_comapRel_iff) is stated between in-domain nodes, which is where the formulas that read it evaluate it: the guarded pullback of DescriptiveComplexity.RelComposition hands every atom its arguments already in the domain.

What it is for

Two things. It is what pulls a membership walk back through a reduction (DescriptiveComplexity.TCSpec.pullSpec), the first half of the closure of DescriptiveComplexity.NL under ≤ᵗᶜ, the second half being the flattening of the pulled walk (DescriptiveComplexity.TransitiveClosureFlatten); and it is what pulls the outer walks of a composite back to the base, the first half of transitivity of ≤ᵗᶜ (DescriptiveComplexity.TCReduction.trans), whose second half is the same flattening.

The guarded pullback at an arbitrary variable type

noncomputable def DescriptiveComplexity.RelFOInterpretation.pullRelF {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dim : ℕ} {β : Type} (I : RelFOInterpretation L₁ L₂ Tag dim) (φ : L₂.Formula β) (τ : β → Tag) : L₁.Formula (β × Fin dim)

The guarded pullback of a formula at an arbitrary variable type: the relativized sibling of DescriptiveComplexity.FOInterpretation.pullF.

Equations

• I.pullRelF φ τ = FirstOrder.Language.Formula.relabel (fun (p : (β ⊕ Fin 0) × Fin dim) => (Sum.elim id finZeroElim p.1, p.2)) (I.pullRel φ (Sum.elim τ finZeroElim))

theorem DescriptiveComplexity.RelFOInterpretation.realize_pullRelF {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dim : ℕ} {β : Type} (I : RelFOInterpretation L₁ L₂ Tag dim) {A : Type} [L₁.Structure A] (φ : L₂.Formula β) (τ : β → Tag) (v : β × Fin dim → A) (hv : ∀ (b : β), (I.domFormula (τ b)).Realize fun (j : Fin dim) => v (b, j)) : (I.pullRelF φ τ).Realize v ↔ φ.Realize fun (b : β) => ⟨(τ b, fun (j : Fin dim) => v (b, j)), ⋯⟩

Coordinates of a pulled node

def DescriptiveComplexity.ParamTCSpec.coordIx (dim : ℕ) {n : ℕ} (i : Fin n) (j : Fin dim) : Fin (n * dim)

The coordinate of a pulled tuple holding the j-th coordinate of the i-th point.

Equations

• DescriptiveComplexity.ParamTCSpec.coordIx dim i j = finProdFinEquiv (i, j)

def DescriptiveComplexity.ParamTCSpec.pointOf {Tag : Type} {dim : ℕ} {A : Type} {n : ℕ} (τ : Fin n → Tag) (w : Fin (n * dim) → A) (i : Fin n) : Tag × (Fin dim → A)

The point of the target a pulled tuple encodes at its i-th slot.

Equations

• DescriptiveComplexity.ParamTCSpec.pointOf τ w i = (τ i, fun (j : Fin dim) => w (DescriptiveComplexity.ParamTCSpec.coordIx dim i j))

The pulled walk

noncomputable def DescriptiveComplexity.ParamTCSpec.domTupleF {L₁ L₂ : FirstOrder.Language} {Tag : Type} {dim : ℕ} (I : RelFOInterpretation L₁ L₂ Tag dim) {n : ℕ} (τ : Fin n → Tag) : L₁.Formula (Fin (n * dim))

“Every point this tuple encodes is in the domain”, as a formula.

Equations

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

theorem DescriptiveComplexity.ParamTCSpec.realize_domTupleF {L₁ L₂ : FirstOrder.Language} {Tag : Type} {dim : ℕ} (I : RelFOInterpretation L₁ L₂ Tag dim) {A : Type} [L₁.Structure A] {n : ℕ} (τ : Fin n → Tag) (w : Fin (n * dim) → A) : (domTupleF I τ).Realize w ↔ ∀ (i : Fin n), (I.domFormula (τ i)).Realize fun (j : Fin dim) => w (coordIx dim i j)

def DescriptiveComplexity.ParamTCSpec.comapVar {L₂ : FirstOrder.Language} {dim : ℕ} (s : ParamTCSpec L₂) : ((Fin s.k ⊕ Fin s.k) ⊕ Fin s.par) × Fin dim → (Fin (s.k * dim) ⊕ Fin (s.k * dim)) ⊕ Fin (s.par * dim)

The variables of a pulled step formula: the two tuples and the parameters, each spread over its coordinates.

Equations

• s.comapVar (Sum.inl (Sum.inl i), j) = Sum.inl (Sum.inl (DescriptiveComplexity.ParamTCSpec.coordIx dim i j))
• s.comapVar (Sum.inl (Sum.inr i), j) = Sum.inl (Sum.inr (DescriptiveComplexity.ParamTCSpec.coordIx dim i j))
• s.comapVar (Sum.inr i, j) = Sum.inr (DescriptiveComplexity.ParamTCSpec.coordIx dim i j)

def DescriptiveComplexity.ParamTCSpec.comapSrcVar {L₂ : FirstOrder.Language} {dim : ℕ} (s : ParamTCSpec L₂) : Fin (s.k * dim) → (Fin (s.k * dim) ⊕ Fin (s.k * dim)) ⊕ Fin (s.par * dim)

The relabeling of a guard on one tuple into the step formula's variables.

Equations

• s.comapSrcVar m = Sum.inl (Sum.inl m)

def DescriptiveComplexity.ParamTCSpec.comapTgtVar {L₂ : FirstOrder.Language} {dim : ℕ} (s : ParamTCSpec L₂) : Fin (s.k * dim) → (Fin (s.k * dim) ⊕ Fin (s.k * dim)) ⊕ Fin (s.par * dim)

The relabeling of a guard on one tuple into the step formula's variables.

Equations

• s.comapTgtVar m = Sum.inl (Sum.inr m)

def DescriptiveComplexity.ParamTCSpec.comapParVar {L₂ : FirstOrder.Language} {dim : ℕ} (s : ParamTCSpec L₂) : Fin (s.par * dim) → (Fin (s.k * dim) ⊕ Fin (s.k * dim)) ⊕ Fin (s.par * dim)

The relabeling of a guard on one tuple into the step formula's variables.

Equations

• s.comapParVar = Sum.inr

noncomputable def DescriptiveComplexity.ParamTCSpec.comapRel {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dim : ℕ} (s : ParamTCSpec L₂) (I : RelFOInterpretation L₁ L₂ Tag dim) (τp : Fin s.par → Tag) : ParamTCSpec L₁

The pullback of a walk through a relativized interpretation, at a static assignment of tags to its parameters: the tuples become tuples of coordinates, the tags of the two endpoints are carried in the mode, and the step is guarded by the domain formulas of everything it mentions.

Equations

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

The nodes of the pulled walk

def DescriptiveComplexity.ParamTCSpec.InDom {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dim : ℕ} {s : ParamTCSpec L₂} {I : RelFOInterpretation L₁ L₂ Tag dim} {A : Type} [L₁.Structure A] {τp : Fin s.par → Tag} (a : (s.comapRel I τp).Node A) : Prop

A node of the pulled walk is in domain when every point it encodes is a point of the target.

Equations

• DescriptiveComplexity.ParamTCSpec.InDom a = ∀ (i : Fin s.k), (I.domFormula (a.1.2 i)).Realize fun (j : Fin dim) => a.2 (DescriptiveComplexity.ParamTCSpec.coordIx dim i j)

def DescriptiveComplexity.ParamTCSpec.ParInDom {L₁ L₂ : FirstOrder.Language} {Tag : Type} {dim : ℕ} {s : ParamTCSpec L₂} {A : Type} [L₁.Structure A] (I : RelFOInterpretation L₁ L₂ Tag dim) (τp : Fin s.par → Tag) (z : Fin (s.par * dim) → A) : Prop

A valuation of the pulled parameters is in domain when every point it encodes is.

Equations

• DescriptiveComplexity.ParamTCSpec.ParInDom I τp z = ∀ (i : Fin s.par), (I.domFormula (τp i)).Realize fun (j : Fin dim) => z (DescriptiveComplexity.ParamTCSpec.coordIx dim i j)

def DescriptiveComplexity.ParamTCSpec.decode {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dim : ℕ} {s : ParamTCSpec L₂} {I : RelFOInterpretation L₁ L₂ Tag dim} {A : Type} [L₁.Structure A] {τp : Fin s.par → Tag} (a : (s.comapRel I τp).Node A) (ha : InDom a) : s.Node (I.MapRel A)

The node of the target that an in-domain node encodes.

Equations

• DescriptiveComplexity.ParamTCSpec.decode a ha = (a.1.1, fun (i : Fin s.k) => ⟨(a.1.2 i, fun (j : Fin dim) => a.2 (DescriptiveComplexity.ParamTCSpec.coordIx dim i j)), ⋯⟩)

def DescriptiveComplexity.ParamTCSpec.decodePar {L₁ L₂ : FirstOrder.Language} {Tag : Type} {dim : ℕ} {s : ParamTCSpec L₂} {I : RelFOInterpretation L₁ L₂ Tag dim} {A : Type} [L₁.Structure A] {τp : Fin s.par → Tag} {z : Fin (s.par * dim) → A} (hz : ParInDom I τp z) : Fin s.par → I.MapRel A

The parameters of the target that an in-domain valuation encodes.

Equations

• DescriptiveComplexity.ParamTCSpec.decodePar hz i = ⟨(τp i, fun (j : Fin dim) => z (DescriptiveComplexity.ParamTCSpec.coordIx dim i j)), ⋯⟩

def DescriptiveComplexity.ParamTCSpec.encode {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dim : ℕ} {s : ParamTCSpec L₂} {I : RelFOInterpretation L₁ L₂ Tag dim} {A : Type} [L₁.Structure A] (τp : Fin s.par → Tag) (c : s.Node (I.MapRel A)) : (s.comapRel I τp).Node A

A node of the target, read as a node of the pulled walk.

Equations

• DescriptiveComplexity.ParamTCSpec.encode τp c = ((c.1, fun (i : Fin s.k) => (↑(c.2 i)).1), fun (m : Fin (s.comapRel I τp).k) => (↑(c.2 (finProdFinEquiv.symm m).1)).2 (finProdFinEquiv.symm m).2)

theorem DescriptiveComplexity.ParamTCSpec.coord_encode {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dim : ℕ} {s : ParamTCSpec L₂} {I : RelFOInterpretation L₁ L₂ Tag dim} {A : Type} [L₁.Structure A] (τp : Fin s.par → Tag) (c : s.Node (I.MapRel A)) (i : Fin s.k) (j : Fin dim) : (encode τp c).2 (coordIx dim i j) = (↑(c.2 i)).2 j

theorem DescriptiveComplexity.ParamTCSpec.inDom_encode {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dim : ℕ} {s : ParamTCSpec L₂} {I : RelFOInterpretation L₁ L₂ Tag dim} {A : Type} [L₁.Structure A] (τp : Fin s.par → Tag) (c : s.Node (I.MapRel A)) : InDom (encode τp c)

The encoding of a node of the target is in domain.

theorem DescriptiveComplexity.ParamTCSpec.decode_encode {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dim : ℕ} {s : ParamTCSpec L₂} {I : RelFOInterpretation L₁ L₂ Tag dim} {A : Type} [L₁.Structure A] (τp : Fin s.par → Tag) (c : s.Node (I.MapRel A)) : decode (encode τp c) ⋯ = c

Encoding and decoding are inverse on nodes of the target.

Steps and reachability correspond

theorem DescriptiveComplexity.ParamTCSpec.stepAt_comapRel_iff {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dim : ℕ} {s : ParamTCSpec L₂} {I : RelFOInterpretation L₁ L₂ Tag dim} {A : Type} [L₁.Structure A] {τp : Fin s.par → Tag} {z : Fin (s.par * dim) → A} (a b : (s.comapRel I τp).Node A) : (s.comapRel I τp).StepAt z a b ↔ ∃ (ha : InDom a) (hb : InDom b) (hz : ParInDom I τp z), s.StepAt (decodePar hz) (decode a ha) (decode b hb)

A step of the pulled walk is a step of the original one, both endpoints and the parameters being in the domain.

theorem DescriptiveComplexity.ParamTCSpec.reachAt_comapRel_forward {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dim : ℕ} {s : ParamTCSpec L₂} {I : RelFOInterpretation L₁ L₂ Tag dim} {A : Type} [L₁.Structure A] {τp : Fin s.par → Tag} {z : Fin (s.par * dim) → A} {a b : (s.comapRel I τp).Node A} (h : (s.comapRel I τp).ReachAt z a b) (ha : InDom a) (hz : ParInDom I τp z) : ∃ (hb : InDom b), s.ReachAt (decodePar hz) (decode a ha) (decode b hb)

The pulled walk reaches what the original one reaches, from an in-domain node. The target's membership in the domain is part of the conclusion: a walk cannot leave the domain, its steps being guarded.

theorem DescriptiveComplexity.ParamTCSpec.reachAt_comapRel_backward {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dim : ℕ} {s : ParamTCSpec L₂} {I : RelFOInterpretation L₁ L₂ Tag dim} {A : Type} [L₁.Structure A] {τp : Fin s.par → Tag} {z : Fin (s.par * dim) → A} (hz : ParInDom I τp z) {c d : s.Node (I.MapRel A)} (h : s.ReachAt (decodePar hz) c d) : (s.comapRel I τp).ReachAt z (encode τp c) (encode τp d)

And conversely: what the original walk reaches, the pulled one reaches.

theorem DescriptiveComplexity.ParamTCSpec.reachAt_comapRel_iff {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dim : ℕ} {s : ParamTCSpec L₂} {I : RelFOInterpretation L₁ L₂ Tag dim} {A : Type} [L₁.Structure A] {τp : Fin s.par → Tag} {z : Fin (s.par * dim) → A} {a b : (s.comapRel I τp).Node A} (ha : InDom a) (hb : InDom b) (hz : ParInDom I τp z) : (s.comapRel I τp).ReachAt z a b ↔ s.ReachAt (decodePar hz) (decode a ha) (decode b hb)

Reachability corresponds, between nodes of the domain.