Transitivity of FO(TC) and FO(DTC) reductions

P ≤ᵗᶜ Q and Q ≤ᵗᶜ R give P ≤ᵗᶜ R (DescriptiveComplexity.TCReduction.trans), and likewise for ≤ᵈᵗᶜ (DescriptiveComplexity.DTCReduction.trans): the reductions with a logic inside are reduction orders.

The composite

The outer reduction's interpretation reads the reachability relations of its own walks, which run on the structure the inner reduction produces. Pulled back through the inner interpretation (DescriptiveComplexity.ParamTCSpec.comapRel) they are walks over the base structure expanded by the inner walks' relations; flattened (DescriptiveComplexity.ParamTCSpec.flat) they are walks over the base structure alone, and they join the inner family (DescriptiveComplexity.TCInterpretation.flatFamily). The inner interpretation is then extended to the outer family's vocabulary (DescriptiveComplexity.TCInterpretation.CompositeBlock.extendOuter): a reachability atom of an outer walk is interpreted by “the two endpoints have encodings between which the flat walk reaches”, with the encodings pinned by DescriptiveComplexity.ParamTCSpec.encF. Composing the outer interpretation with the extended inner one (DescriptiveComplexity.RelFOInterpretation.compRel) is then the composite reduction, and no formula is ever rewritten: the guarded pullback substitutes the extended formulas for the atoms.

The extended interpretation produces exactly the outer reduction's input – the inner structure, ordered lexicographically, expanded by the outer walks' relations (DescriptiveComplexity.TCInterpretation.CompositeBlock.extendOuterLEquiv) – which is where the two halves of the normal form meet: the pullback's correspondence between in-domain nodes and the flat walk's at the encodings.

The deterministic case

The same construction with the searching flat walk, which is functional; the composite's family is read through its determinization, and the flat walks lose nothing by it. The pullback of a determinized walk is functional (DescriptiveComplexity.ParamTCSpec.comapRel_functional), which is what the searching simulation needs.

The pullback of a functional walk is functional

theorem DescriptiveComplexity.ParamTCSpec.encode_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) : encode τp (decode a ha) = a

Encoding after decoding is the identity.

theorem DescriptiveComplexity.ParamTCSpec.comapRel_functional {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} (h : ∀ (z : Fin s.par → I.MapRel A) (a b c : s.Node (I.MapRel A)), s.StepAt z a b → s.StepAt z a c → b = c) (z : Fin (s.par * dim) → A) (a b c : (s.comapRel I τp).Node A) (hb : (s.comapRel I τp).StepAt z a b) (hc : (s.comapRel I τp).StepAt z a c) : b = c

The pullback of a functional walk is functional.

The outer walks, pulled back and flattened

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.TCInterpretation.pulled {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag₁ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ : ℕ} (I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁) (s : ParamTCSpec (L₂.sum FirstOrder.Language.order)) (τp : Fin s.par → Tag₁) : ParamTCSpec ((L₁.sum FirstOrder.Language.order).sum I.fam.block.lang)

An outer walk, pulled back through the inner interpretation: a walk over the base structure expanded by the inner walks' relations.

Equations

• I.pulled s τp = s.comapRel I.ordInterp τp

theorem DescriptiveComplexity.TCInterpretation.exists_pulledStepDecider {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {Tag₁ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ : ℕ} (I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁) (Dq : (q : I.fam.block.ι) → Decider L₁ (Fin (I.fam.block.arity q))) (hD : ∀ (A : Type) [inst : L₁.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (q : I.fam.block.ι) (w : Fin (I.fam.block.arity q) → A), (Dq q).Decides w (I.fam.reachAssign A q w)) (s : ParamTCSpec (L₂.sum FirstOrder.Language.order)) (τp : Fin s.par → Tag₁) (m n : (I.pulled s τp).Mode) : ∃ (D : Decider L₁ ((Fin (I.pulled s τp).k ⊕ Fin (I.pulled s τp).k) ⊕ Fin (I.pulled s τp).par)), (∀ (A : Type) [inst : L₁.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (v : (Fin (I.pulled s τp).k ⊕ Fin (I.pulled s τp).k) ⊕ Fin (I.pulled s τp).par → A), D.Decides v (((I.pulled s τp).step m n).Realize v)) ∧ ∀ (A : Type) [inst : L₁.Structure A] [inst_1 : LinearOrder A], (∀ (q : I.fam.block.ι), (Dq q).Functional A) → D.Functional A

noncomputable def DescriptiveComplexity.TCInterpretation.pulledStepDecider {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {Tag₁ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ : ℕ} (I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁) (Dq : (q : I.fam.block.ι) → Decider L₁ (Fin (I.fam.block.arity q))) (hD : ∀ (A : Type) [inst : L₁.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (q : I.fam.block.ι) (w : Fin (I.fam.block.arity q) → A), (Dq q).Decides w (I.fam.reachAssign A q w)) (s : ParamTCSpec (L₂.sum FirstOrder.Language.order)) (τp : Fin s.par → Tag₁) (m n : (I.pulled s τp).Mode) : Decider L₁ ((Fin (I.pulled s τp).k ⊕ Fin (I.pulled s τp).k) ⊕ Fin (I.pulled s τp).par)

The deciders of the pulled walk's steps.

Equations

• I.pulledStepDecider Dq hD s τp m n = Classical.choose ⋯

theorem DescriptiveComplexity.TCInterpretation.pulledStepDecider_decides {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {Tag₁ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ : ℕ} (I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁) (Dq : (q : I.fam.block.ι) → Decider L₁ (Fin (I.fam.block.arity q))) (hD : ∀ (A : Type) [inst : L₁.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (q : I.fam.block.ι) (w : Fin (I.fam.block.arity q) → A), (Dq q).Decides w (I.fam.reachAssign A q w)) (s : ParamTCSpec (L₂.sum FirstOrder.Language.order)) (τp : Fin s.par → Tag₁) (A : Type) [L₁.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (m n : (I.pulled s τp).Mode) (v : (Fin (I.pulled s τp).k ⊕ Fin (I.pulled s τp).k) ⊕ Fin (I.pulled s τp).par → A) : (I.pulledStepDecider Dq hD s τp m n).Decides v (((I.pulled s τp).step m n).Realize v)

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.TCInterpretation.flatWalk {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {Tag₁ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ : ℕ} (I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁) (Dq : (q : I.fam.block.ι) → Decider L₁ (Fin (I.fam.block.arity q))) (hD : ∀ (A : Type) [inst : L₁.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (q : I.fam.block.ι) (w : Fin (I.fam.block.arity q) → A), (Dq q).Decides w (I.fam.reachAssign A q w)) (s : ParamTCSpec (L₂.sum FirstOrder.Language.order)) (τp : Fin s.par → Tag₁) (det : Bool) : ParamTCSpec (L₁.sum FirstOrder.Language.order)

An outer walk, pulled back and flattened: a walk over the base structure alone.

Equations

• I.flatWalk Dq hD s τp det = ((I.pulled s τp).flat (I.pulledStepDecider Dq hD s τp) det).toParam

theorem DescriptiveComplexity.TCInterpretation.flatWalk_functional {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {Tag₁ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ : ℕ} (I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁) (Dq : (q : I.fam.block.ι) → Decider L₁ (Fin (I.fam.block.arity q))) (hD : ∀ (A : Type) [inst : L₁.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (q : I.fam.block.ι) (w : Fin (I.fam.block.arity q) → A), (Dq q).Decides w (I.fam.reachAssign A q w)) (s : ParamTCSpec (L₂.sum FirstOrder.Language.order)) (τp : Fin s.par → Tag₁) {A : Type} [L₁.Structure A] [LinearOrder A] [Nonempty A] (h : ∀ (q : I.fam.block.ι), (Dq q).Functional A) : (I.flatWalk Dq hD s τp true).Functional A

The searching flat walk is functional when the inner deciders are.

The flat family

noncomputable def DescriptiveComplexity.TCInterpretation.flatFamily {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {Tag₁ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ : ℕ} (I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁) (Dq : (q : I.fam.block.ι) → Decider L₁ (Fin (I.fam.block.arity q))) (hD : ∀ (A : Type) [inst : L₁.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (q : I.fam.block.ι) (w : Fin (I.fam.block.arity q) → A), (Dq q).Decides w (I.fam.reachAssign A q w)) (F : TCFamily (L₂.sum FirstOrder.Language.order)) (det : Bool) : TCFamily (L₁.sum FirstOrder.Language.order)

The outer family, pulled back and flattened: one walk per outer walk and tag assignment of its parameters.

Equations

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

Extending the inner interpretation to the outer family's vocabulary

structure DescriptiveComplexity.TCInterpretation.CompositeBlock {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {Tag₁ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ : ℕ} (I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁) (Dq : (q : I.fam.block.ι) → Decider L₁ (Fin (I.fam.block.arity q))) (hD : ∀ (A : Type) [inst : L₁.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (q : I.fam.block.ι) (w : Fin (I.fam.block.arity q) → A), (Dq q).Decides w (I.fam.reachAssign A q w)) (F : TCFamily (L₂.sum FirstOrder.Language.order)) (det : Bool) : Type 1

The composite family, abstractly: a block with an assignment, into which the inner family's relation variables and the flat walks' embed, with their assignments. Abstract so that the composite family may be read as it is (≤ᵗᶜ) or through its determinization (≤ᵈᵗᶜ).

• B : SOBlock

  The block.

• ρ (A : Type) [L₁.Structure A] [LinearOrder A] : self.B.Assignment A

  Its assignment on each structure.

• ι₁ : I.fam.block.ι → self.B.ι

  The inner family's relation variables.

• arity₁ (q : I.fam.block.ι) : self.B.arity (self.ι₁ q) = I.fam.block.arity q

  Their arities.

• ρ₁ (A : Type) [L₁.Structure A] [LinearOrder A] (q : I.fam.block.ι) (w : Fin (I.fam.block.arity q) → A) : self.ρ A (self.ι₁ q) (w ∘ Fin.cast ⋯) ↔ I.fam.reachAssign A q w

  Their assignments.

• ι₂ (p : (I.flatFamily Dq hD F det).Ix) : ((I.flatFamily Dq hD F det).spec p).Mode → ((I.flatFamily Dq hD F det).spec p).Mode → self.B.ι

  The flat walks' relation variables, per pair of modes.

• arity₂ (p : (I.flatFamily Dq hD F det).Ix) (m n : ((I.flatFamily Dq hD F det).spec p).Mode) : self.B.arity (self.ι₂ p m n) = (I.flatFamily Dq hD F det).block.arity ⟨p, (m, n)⟩

  Their arities.

• ρ₂ (A : Type) [L₁.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (p : (I.flatFamily Dq hD F det).Ix) (m n : ((I.flatFamily Dq hD F det).spec p).Mode) (w : Fin ((I.flatFamily Dq hD F det).block.arity ⟨p, (m, n)⟩) → A) : self.ρ A (self.ι₂ p m n) (w ∘ Fin.cast ⋯) ↔ ((I.flatFamily Dq hD F det).spec p).ReachAt (w ∘ ((I.flatFamily Dq hD F det).spec p).parIx) (m, w ∘ ((I.flatFamily Dq hD F det).spec p).leftIx) (n, w ∘ ((I.flatFamily Dq hD F det).spec p).rightIx)

  Their assignments: the flat walks' reachability relations.

noncomputable def DescriptiveComplexity.TCInterpretation.CompositeBlock.lhom {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {Tag₁ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ : ℕ} {I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁} {Dq : (q : I.fam.block.ι) → Decider L₁ (Fin (I.fam.block.arity q))} {hD : ∀ (A : Type) [inst : L₁.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (q : I.fam.block.ι) (w : Fin (I.fam.block.arity q) → A), (Dq q).Decides w (I.fam.reachAssign A q w)} {F : TCFamily (L₂.sum FirstOrder.Language.order)} {det : Bool} (C : I.CompositeBlock Dq hD F det) : (L₁.sum FirstOrder.Language.order).sum I.fam.block.lang →ᴸ (L₁.sum FirstOrder.Language.order).sum C.B.lang

The vocabulary map from the inner family's expansion to the composite's.

Equations

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

@[instance_reducible]

noncomputable def DescriptiveComplexity.TCInterpretation.CompositeBlock.structure {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {Tag₁ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ : ℕ} {I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁} {Dq : (q : I.fam.block.ι) → Decider L₁ (Fin (I.fam.block.arity q))} {hD : ∀ (A : Type) [inst : L₁.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (q : I.fam.block.ι) (w : Fin (I.fam.block.arity q) → A), (Dq q).Decides w (I.fam.reachAssign A q w)} {F : TCFamily (L₂.sum FirstOrder.Language.order)} {det : Bool} (C : I.CompositeBlock Dq hD F det) (A : Type) [L₁.Structure A] [LinearOrder A] : ((L₁.sum FirstOrder.Language.order).sum C.B.lang).Structure A

The composite structure: the base expanded by the composite block.

Equations

• C.structure A = C.B.structure₁ (C.ρ A)

theorem DescriptiveComplexity.TCInterpretation.CompositeBlock.isExpansionOn {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {Tag₁ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ : ℕ} {I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁} {Dq : (q : I.fam.block.ι) → Decider L₁ (Fin (I.fam.block.arity q))} {hD : ∀ (A : Type) [inst : L₁.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (q : I.fam.block.ι) (w : Fin (I.fam.block.arity q) → A), (Dq q).Decides w (I.fam.reachAssign A q w)} {F : TCFamily (L₂.sum FirstOrder.Language.order)} {det : Bool} (C : I.CompositeBlock Dq hD F det) {A : Type} [L₁.Structure A] [LinearOrder A] : C.lhom.IsExpansionOn A

The vocabulary map is an expansion.

theorem DescriptiveComplexity.TCInterpretation.CompositeBlock.realize_lhom {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {Tag₁ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ : ℕ} {I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁} {Dq : (q : I.fam.block.ι) → Decider L₁ (Fin (I.fam.block.arity q))} {hD : ∀ (A : Type) [inst : L₁.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (q : I.fam.block.ι) (w : Fin (I.fam.block.arity q) → A), (Dq q).Decides w (I.fam.reachAssign A q w)} {F : TCFamily (L₂.sum FirstOrder.Language.order)} {det : Bool} (C : I.CompositeBlock Dq hD F det) {A : Type} [L₁.Structure A] [LinearOrder A] {α : Type} (φ : ((L₁.sum FirstOrder.Language.order).sum I.fam.block.lang).Formula α) (v : α → A) : (C.lhom.onFormula φ).Realize v ↔ φ.Realize v

The outer atoms

def DescriptiveComplexity.outerTags {L₂ : FirstOrder.Language} {Tag₁ : Type} {F : TCFamily (L₂.sum FirstOrder.Language.order)} {n : ℕ} (q : F.block.lang.Relations n) (τ : Fin n → Tag₁) : Fin ((F.spec (↑q).fst).k + (F.spec (↑q).fst).k + (F.spec (↑q).fst).par) → Tag₁

The tags of an outer symbol's arguments, in its walk's packing.

Equations

• DescriptiveComplexity.outerTags q τ p = τ (Fin.cast ⋯ p)

def DescriptiveComplexity.outerTp {L₂ : FirstOrder.Language} {Tag₁ : Type} {F : TCFamily (L₂.sum FirstOrder.Language.order)} {n : ℕ} (q : F.block.lang.Relations n) (τ : Fin n → Tag₁) : Fin (F.spec (↑q).fst).par → Tag₁

The tags of the walk's parameters.

Equations

• DescriptiveComplexity.outerTp q τ j = DescriptiveComplexity.outerTags q τ ((F.spec (↑q).fst).parIx j)

def DescriptiveComplexity.outerXsel {L₂ : FirstOrder.Language} {d₁ : ℕ} {F : TCFamily (L₂.sum FirstOrder.Language.order)} {n : ℕ} (q : F.block.lang.Relations n) : Fin ((F.spec (↑q).fst).k * d₁) → Fin n × Fin d₁

The coordinates of the first endpoint, among the symbol's variables.

Equations

• DescriptiveComplexity.outerXsel q c = (Fin.cast ⋯ ((F.spec (↑q).fst).leftIx (finProdFinEquiv.symm c).1), (finProdFinEquiv.symm c).2)

def DescriptiveComplexity.outerYsel {L₂ : FirstOrder.Language} {d₁ : ℕ} {F : TCFamily (L₂.sum FirstOrder.Language.order)} {n : ℕ} (q : F.block.lang.Relations n) : Fin ((F.spec (↑q).fst).k * d₁) → Fin n × Fin d₁

The coordinates of the second endpoint.

Equations

• DescriptiveComplexity.outerYsel q c = (Fin.cast ⋯ ((F.spec (↑q).fst).rightIx (finProdFinEquiv.symm c).1), (finProdFinEquiv.symm c).2)

def DescriptiveComplexity.outerZsel {L₂ : FirstOrder.Language} {d₁ : ℕ} {F : TCFamily (L₂.sum FirstOrder.Language.order)} {n : ℕ} (q : F.block.lang.Relations n) : Fin ((F.spec (↑q).fst).par * d₁) → Fin n × Fin d₁

The coordinates of the parameters.

Equations

• DescriptiveComplexity.outerZsel q c = (Fin.cast ⋯ ((F.spec (↑q).fst).parIx (finProdFinEquiv.symm c).1), (finProdFinEquiv.symm c).2)

@[reducible, inline]

abbrev DescriptiveComplexity.outerIx {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {Tag₁ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ : ℕ} {I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁} {Dq : (q : I.fam.block.ι) → Decider L₁ (Fin (I.fam.block.arity q))} {hD : ∀ (A : Type) [inst : L₁.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (q : I.fam.block.ι) (w : Fin (I.fam.block.arity q) → A), (Dq q).Decides w (I.fam.reachAssign A q w)} {F : TCFamily (L₂.sum FirstOrder.Language.order)} {det : Bool} {n : ℕ} (q : F.block.lang.Relations n) (τ : Fin n → Tag₁) : (I.flatFamily Dq hD F det).Ix

The index of the flat walk interpreting the symbol.

Equations

• DescriptiveComplexity.outerIx q τ = ⟨(↑q).fst, DescriptiveComplexity.outerTp q τ⟩

@[reducible, inline]

abbrev DescriptiveComplexity.outerMode₁ {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {Tag₁ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ : ℕ} {I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁} {Dq : (q : I.fam.block.ι) → Decider L₁ (Fin (I.fam.block.arity q))} {hD : ∀ (A : Type) [inst : L₁.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (q : I.fam.block.ι) (w : Fin (I.fam.block.arity q) → A), (Dq q).Decides w (I.fam.reachAssign A q w)} {F : TCFamily (L₂.sum FirstOrder.Language.order)} {det : Bool} {n : ℕ} (q : F.block.lang.Relations n) (τ : Fin n → Tag₁) : ((I.flatFamily Dq hD F det).spec (outerIx q τ)).Mode

The two modes of the flat walk between which reachability is asked.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.outerMode₂ {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {Tag₁ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ : ℕ} {I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁} {Dq : (q : I.fam.block.ι) → Decider L₁ (Fin (I.fam.block.arity q))} {hD : ∀ (A : Type) [inst : L₁.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (q : I.fam.block.ι) (w : Fin (I.fam.block.arity q) → A), (Dq q).Decides w (I.fam.reachAssign A q w)} {F : TCFamily (L₂.sum FirstOrder.Language.order)} {det : Bool} {n : ℕ} (q : F.block.lang.Relations n) (τ : Fin n → Tag₁) : ((I.flatFamily Dq hD F det).spec (outerIx q τ)).Mode

The two modes of the flat walk between which reachability is asked.

Equations

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

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.outerK {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {Tag₁ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ : ℕ} {I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁} {Dq : (q : I.fam.block.ι) → Decider L₁ (Fin (I.fam.block.arity q))} {hD : ∀ (A : Type) [inst : L₁.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (q : I.fam.block.ι) (w : Fin (I.fam.block.arity q) → A), (Dq q).Decides w (I.fam.reachAssign A q w)} {F : TCFamily (L₂.sum FirstOrder.Language.order)} {det : Bool} {n : ℕ} (q : F.block.lang.Relations n) (τ : Fin n → Tag₁) : ℕ

The number of coordinates of the flat walk interpreting the symbol.

Equations

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

noncomputable def DescriptiveComplexity.TCInterpretation.CompositeBlock.outerAtomF {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {Tag₁ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ : ℕ} {I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁} {Dq : (q : I.fam.block.ι) → Decider L₁ (Fin (I.fam.block.arity q))} {hD : ∀ (A : Type) [inst : L₁.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (q : I.fam.block.ι) (w : Fin (I.fam.block.arity q) → A), (Dq q).Decides w (I.fam.reachAssign A q w)} {F : TCFamily (L₂.sum FirstOrder.Language.order)} {det : Bool} (C : I.CompositeBlock Dq hD F det) {n : ℕ} (q : F.block.lang.Relations n) (τ : Fin n → Tag₁) : ((L₁.sum FirstOrder.Language.order).sum C.B.lang).Formula (Fin n × Fin d₁)

The interpretation of an outer reachability atom: the two endpoints have encodings between which the flat walk reaches.

Equations

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

def DescriptiveComplexity.outerPt {L₁ L₂ : FirstOrder.Language} {Tag₁ : Type} [LinearOrder Tag₁] {d₁ : ℕ} {I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁} {F : TCFamily (L₂.sum FirstOrder.Language.order)} {A : Type} [L₁.Structure A] [LinearOrder A] {n : ℕ} (q : F.block.lang.Relations n) (τ : Fin n → Tag₁) (v : Fin n × Fin d₁ → A) (hv : ∀ (i : Fin n), (I.toRel.domFormula (τ i)).Realize fun (j : Fin d₁) => v (i, j)) (p : Fin ((F.spec (↑q).fst).k + (F.spec (↑q).fst).k + (F.spec (↑q).fst).par)) : I.ordInterp.MapRel A

The point of the inner structure held at a position of the symbol.

Equations

• DescriptiveComplexity.outerPt q τ v hv p = ⟨(DescriptiveComplexity.outerTags q τ p, fun (c : Fin d₁) => v (Fin.cast ⋯ p, c)), ⋯⟩

theorem DescriptiveComplexity.outer_inDom_left {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag₁ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ : ℕ} {I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁} {F : TCFamily (L₂.sum FirstOrder.Language.order)} {A : Type} [L₁.Structure A] [LinearOrder A] {n : ℕ} (q : F.block.lang.Relations n) (τ : Fin n → Tag₁) (v : Fin n × Fin d₁ → A) (hv : ∀ (i : Fin n), (I.toRel.domFormula (τ i)).Realize fun (j : Fin d₁) => v (i, j)) : ParamTCSpec.InDom (((↑q).snd.1, fun (j : Fin (F.spec (↑q).fst).k) => outerTags q τ ((F.spec (↑q).fst).leftIx j)), v ∘ outerXsel q)

theorem DescriptiveComplexity.outer_inDom_right {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag₁ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ : ℕ} {I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁} {F : TCFamily (L₂.sum FirstOrder.Language.order)} {A : Type} [L₁.Structure A] [LinearOrder A] {n : ℕ} (q : F.block.lang.Relations n) (τ : Fin n → Tag₁) (v : Fin n × Fin d₁ → A) (hv : ∀ (i : Fin n), (I.toRel.domFormula (τ i)).Realize fun (j : Fin d₁) => v (i, j)) : ParamTCSpec.InDom (((↑q).snd.2, fun (j : Fin (F.spec (↑q).fst).k) => outerTags q τ ((F.spec (↑q).fst).rightIx j)), v ∘ outerYsel q)

theorem DescriptiveComplexity.outer_parInDom {L₁ L₂ : FirstOrder.Language} {Tag₁ : Type} [LinearOrder Tag₁] {d₁ : ℕ} {I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁} {F : TCFamily (L₂.sum FirstOrder.Language.order)} {A : Type} [L₁.Structure A] [LinearOrder A] {n : ℕ} (q : F.block.lang.Relations n) (τ : Fin n → Tag₁) (v : Fin n × Fin d₁ → A) (hv : ∀ (i : Fin n), (I.toRel.domFormula (τ i)).Realize fun (j : Fin d₁) => v (i, j)) : ParamTCSpec.ParInDom I.ordInterp (outerTp q τ) (v ∘ outerZsel q)

theorem DescriptiveComplexity.outer_decode_left {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag₁ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ : ℕ} {I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁} {F : TCFamily (L₂.sum FirstOrder.Language.order)} {A : Type} [L₁.Structure A] [LinearOrder A] {n : ℕ} (q : F.block.lang.Relations n) (τ : Fin n → Tag₁) (v : Fin n × Fin d₁ → A) (hv : ∀ (i : Fin n), (I.toRel.domFormula (τ i)).Realize fun (j : Fin d₁) => v (i, j)) : ParamTCSpec.decode (((↑q).snd.1, fun (j : Fin (F.spec (↑q).fst).k) => outerTags q τ ((F.spec (↑q).fst).leftIx j)), v ∘ outerXsel q) ⋯ = ((↑q).snd.1, fun (j : Fin (F.spec (↑q).fst).k) => outerPt q τ v hv ((F.spec (↑q).fst).leftIx j))

theorem DescriptiveComplexity.outer_decode_right {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag₁ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ : ℕ} {I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁} {F : TCFamily (L₂.sum FirstOrder.Language.order)} {A : Type} [L₁.Structure A] [LinearOrder A] {n : ℕ} (q : F.block.lang.Relations n) (τ : Fin n → Tag₁) (v : Fin n × Fin d₁ → A) (hv : ∀ (i : Fin n), (I.toRel.domFormula (τ i)).Realize fun (j : Fin d₁) => v (i, j)) : ParamTCSpec.decode (((↑q).snd.2, fun (j : Fin (F.spec (↑q).fst).k) => outerTags q τ ((F.spec (↑q).fst).rightIx j)), v ∘ outerYsel q) ⋯ = ((↑q).snd.2, fun (j : Fin (F.spec (↑q).fst).k) => outerPt q τ v hv ((F.spec (↑q).fst).rightIx j))

theorem DescriptiveComplexity.outer_decodePar {L₁ L₂ : FirstOrder.Language} {Tag₁ : Type} [LinearOrder Tag₁] {d₁ : ℕ} {I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁} {F : TCFamily (L₂.sum FirstOrder.Language.order)} {A : Type} [L₁.Structure A] [LinearOrder A] {n : ℕ} (q : F.block.lang.Relations n) (τ : Fin n → Tag₁) (v : Fin n × Fin d₁ → A) (hv : ∀ (i : Fin n), (I.toRel.domFormula (τ i)).Realize fun (j : Fin d₁) => v (i, j)) : ParamTCSpec.decodePar ⋯ = fun (j : Fin (F.spec (↑q).fst).par) => outerPt q τ v hv ((F.spec (↑q).fst).parIx j)

theorem DescriptiveComplexity.TCInterpretation.CompositeBlock.realize_outerAtomF {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {Tag₁ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ : ℕ} {I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁} {Dq : (q : I.fam.block.ι) → Decider L₁ (Fin (I.fam.block.arity q))} {hD : ∀ (A : Type) [inst : L₁.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (q : I.fam.block.ι) (w : Fin (I.fam.block.arity q) → A), (Dq q).Decides w (I.fam.reachAssign A q w)} {F : TCFamily (L₂.sum FirstOrder.Language.order)} {det : Bool} (C : I.CompositeBlock Dq hD F det) {A : Type} [L₁.Structure A] [LinearOrder A] {n : ℕ} (q : F.block.lang.Relations n) (τ : Fin n → Tag₁) [Finite A] [Nonempty A] (v : Fin n × Fin d₁ → A) (hv : ∀ (i : Fin n), (I.toRel.domFormula (τ i)).Realize fun (j : Fin d₁) => v (i, j)) {a₀ : A} (hbot : ∀ (a : A), a₀ ≤ a) (hdet : det = true → ∀ (z : Fin (F.spec (↑q).fst).par → I.ordInterp.MapRel A) (a b c : (F.spec (↑q).fst).Node (I.ordInterp.MapRel A)), (F.spec (↑q).fst).StepAt z a b → (F.spec (↑q).fst).StepAt z a c → b = c) : (C.outerAtomF q τ).Realize v ↔ (F.spec (↑q).fst).ReachAt (fun (j : Fin (F.spec (↑q).fst).par) => outerPt q τ v hv ((F.spec (↑q).fst).parIx j)) ((↑q).snd.1, fun (j : Fin (F.spec (↑q).fst).k) => outerPt q τ v hv ((F.spec (↑q).fst).leftIx j)) ((↑q).snd.2, fun (j : Fin (F.spec (↑q).fst).k) => outerPt q τ v hv ((F.spec (↑q).fst).rightIx j))

The outer atom's interpretation says reachability in the outer walk, between the points the symbol's arguments encode.

The extended interpretation

noncomputable def DescriptiveComplexity.TCInterpretation.CompositeBlock.extendOuter {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {Tag₁ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ : ℕ} {I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁} {Dq : (q : I.fam.block.ι) → Decider L₁ (Fin (I.fam.block.arity q))} {hD : ∀ (A : Type) [inst : L₁.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (q : I.fam.block.ι) (w : Fin (I.fam.block.arity q) → A), (Dq q).Decides w (I.fam.reachAssign A q w)} (F : TCFamily (L₂.sum FirstOrder.Language.order)) {det : Bool} (C : I.CompositeBlock Dq hD F det) : RelFOInterpretation ((L₁.sum FirstOrder.Language.order).sum C.B.lang) ((L₂.sum FirstOrder.Language.order).sum F.block.lang) Tag₁ d₁

The inner interpretation, extended to the outer family's vocabulary: the base symbols and the order as before, an outer reachability atom by DescriptiveComplexity.TCInterpretation.CompositeBlock.outerAtomF.

Equations

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

noncomputable def DescriptiveComplexity.TCInterpretation.CompositeBlock.extendOuterLEquiv {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {Tag₁ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ : ℕ} {I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁} {Dq : (q : I.fam.block.ι) → Decider L₁ (Fin (I.fam.block.arity q))} {hD : ∀ (A : Type) [inst : L₁.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (q : I.fam.block.ι) (w : Fin (I.fam.block.arity q) → A), (Dq q).Decides w (I.fam.reachAssign A q w)} {F : TCFamily (L₂.sum FirstOrder.Language.order)} {det : Bool} (C : I.CompositeBlock Dq hD F det) {A : Type} [L₁.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {a₀ : A} (hbot : ∀ (a : A), a₀ ≤ a) (hdet : det = true → ∀ (i : F.Ix) (z : Fin (F.spec i).par → I.ordInterp.MapRel A) (a b c : (F.spec i).Node (I.ordInterp.MapRel A)), (F.spec i).StepAt z a b → (F.spec i).StepAt z a c → b = c) : ((L₂.sum FirstOrder.Language.order).sum F.block.lang).Equiv ((extendOuter F C).MapRel A) (I.Map A)

The extended interpretation produces the outer reduction's input: the inner structure, ordered lexicographically, expanded by the outer walks' reachability relations.

Equations

• C.extendOuterLEquiv hbot hdet = { toEquiv := Equiv.subtypeEquivRight ⋯, map_fun' := ⋯, map_rel' := ⋯ }

The composite interpretation

def DescriptiveComplexity.TCFamily.sum {L : FirstOrder.Language} (G H : TCFamily L) : TCFamily L

The sum of two families.

Equations

• G.sum H = { Ix := G.Ix ⊕ H.Ix, ixFinite := ⋯, spec := Sum.elim G.spec H.spec }

noncomputable def DescriptiveComplexity.TCInterpretation.CompositeBlock.compInterp {L₁ L₂ L₃ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {Tag₁ Tag₂ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ d₂ : ℕ} {I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁} {Dq : (q : I.fam.block.ι) → Decider L₁ (Fin (I.fam.block.arity q))} {hD : ∀ (A : Type) [inst : L₁.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (q : I.fam.block.ι) (w : Fin (I.fam.block.arity q) → A), (Dq q).Decides w (I.fam.reachAssign A q w)} {det : Bool} (If : TCInterpretation (L₂.sum FirstOrder.Language.order) L₃ Tag₂ d₂) (C : I.CompositeBlock Dq hD If.fam det) : RelFOInterpretation ((L₁.sum FirstOrder.Language.order).sum C.B.lang) L₃ (Tag₂ × (Fin d₂ → Tag₁)) (d₂ * d₁)

The composite interpretation: the outer interpretation composed with the extended inner one.

Equations

• DescriptiveComplexity.TCInterpretation.CompositeBlock.compInterp If C = If.toRel.compRel (DescriptiveComplexity.TCInterpretation.CompositeBlock.extendOuter If.fam C)

noncomputable def DescriptiveComplexity.TCInterpretation.CompositeBlock.compLEquiv {L₁ L₂ L₃ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] [L₃.IsRelational] {Tag₁ Tag₂ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ d₂ : ℕ} {I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁} {Dq : (q : I.fam.block.ι) → Decider L₁ (Fin (I.fam.block.arity q))} {hD : ∀ (A : Type) [inst : L₁.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (q : I.fam.block.ι) (w : Fin (I.fam.block.arity q) → A), (Dq q).Decides w (I.fam.reachAssign A q w)} {det : Bool} (If : TCInterpretation (L₂.sum FirstOrder.Language.order) L₃ Tag₂ d₂) (C : I.CompositeBlock Dq hD If.fam det) {A : Type} [L₁.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {a₀ : A} (hbot : ∀ (a : A), a₀ ≤ a) (hdet : det = true → ∀ (i : If.fam.Ix) (z : Fin (If.fam.spec i).par → I.ordInterp.MapRel A) (a b c : (If.fam.spec i).Node (I.ordInterp.MapRel A)), (If.fam.spec i).StepAt z a b → (If.fam.spec i).StepAt z a c → b = c) : L₃.Equiv ((compInterp If C).MapRel A) (If.Map (I.Map A))

The composite produces the twice-interpreted structure.

Equations

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

Transitivity

noncomputable def DescriptiveComplexity.TCReduction.trans {L₁ L₂ L₃ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] [L₃.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} {R : DecisionProblem L₃} (g : TCReduction P Q) (f : TCReduction Q R) : TCReduction P R

Transitivity of FO(TC) reductions. The composite's family is the inner family together with the outer family's walks pulled back and flattened; its interpretation is the outer one composed with the inner one extended to the outer walks' vocabulary.

Equations

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

noncomputable def DescriptiveComplexity.DTCReduction.trans {L₁ L₂ L₃ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] [L₃.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} {R : DecisionProblem L₃} (g : DTCReduction P Q) (f : DTCReduction Q R) : DTCReduction P R

Transitivity of FO(DTC) reductions. The same composite with the searching flat walks, read through its determinization: the inner walks are read deterministically as before, and the flat walks, being functional, are unchanged by it.

Equations

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

@[instance_reducible]

noncomputable instance DescriptiveComplexity.instTransDecisionProblemTCReduction {L₁ L₂ L₃ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] [L₃.IsRelational] : Trans TCReduction TCReduction TCReduction

Trans instance: FO(TC) reductions compose.

Equations

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

@[instance_reducible]

noncomputable instance DescriptiveComplexity.instTransDecisionProblemDTCReduction {L₁ L₂ L₃ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] [L₃.IsRelational] : Trans DTCReduction DTCReduction DTCReduction

Trans instance: FO(DTC) reductions compose.

Equations

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