Pulling FO(TC) and FO(DTC) definability back through an interpretation

FO(TC) and FO(DTC) definability are closed under (ordered) first-order reductions (DescriptiveComplexity.TCDefinable.of_orderedReduction, DescriptiveComplexity.DTCDefinable.of_orderedReduction). This is what makes DescriptiveComplexity.LOGSPACE a DescriptiveComplexity.ComplexityClass rather than a mere definability predicate, and it upgrades FO(TC) from the definability notion of DescriptiveComplexity.TransitiveClosure to one closed the same way.

The walk on the interpreted structure, read on the base structure

A DescriptiveComplexity.TCSpec walks on nodes: a mode together with a k-tuple. Pulling it back through a d-dimensional interpretation with tag type Tag means walking on the nodes of the interpreted structure while writing everything in terms of the base one, and the arithmetic of that is entirely in the node type:

• a k-tuple of interpreted elements is k tags together with k · d coordinates, so the pulled specification has modes spec.Mode × (Fin spec.k → Tag) – the tags of the current tuple ride along in the mode, exactly as they ride along in the clause instances of DescriptiveComplexity.SecondOrderPull – and arity spec.k * d;
• the three formulas are the ordinary formula pullback DescriptiveComplexity.FOInterpretation.pullF at those tags, re-indexed from argument-then-coordinate to a flat tuple by finProdFinEquiv;
• DescriptiveComplexity.comapNodeEquiv is the resulting bijection between the nodes of the pullback over A and the nodes of the original over the interpreted structure, and it carries steps to steps (DescriptiveComplexity.TCSpec.comap_step_iff) and endpoints to endpoints.

The order enters as it does for the clausal fragments: the specification's formulas live over the ordered expansion of the target vocabulary, so the pullback goes through DescriptiveComplexity.FOInterpretation.ordExtend, which interprets the target's order as the lexicographic order on tagged tuples, and the interpreted structure is equipped with that same order (DescriptiveComplexity.FOInterpretation.mapLinearOrder). Since FO(TC) definability is required for every linear order, the lexicographic one is available.

Determinism travels for free

Everything about determinism reduces to one observation: the node correspondence is a bijection, and "this step has no competitor" is preserved by a bijection of node sets (DescriptiveComplexity.TCSpec.det_step_congr). So the pullback of the determinization and the determinization of the pullback have the same walk, and DescriptiveComplexity.DTCDefinable is closed under reductions by the same argument as DescriptiveComplexity.TCDefinable, with no side condition to re-establish – which is the point of taking determinization to be a formula (see DescriptiveComplexity.TransitiveClosureDet).

Pulling back a formula at an arbitrary variable type

DescriptiveComplexity.guardPull pulls back a formula whose variables are Fin k; the transition formula of a DescriptiveComplexity.TCSpec has two tuples of variables, so the same pullback is needed at an arbitrary variable type.

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

The pullback of a formula at an arbitrary variable type: an L₁-formula on the coordinates of the original variables, which realizes in A exactly as the formula realizes in the interpreted structure.

Equations

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

theorem DescriptiveComplexity.realize_pullF {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {d : ℕ} {β A : Type} [L₁.Structure A] (I : FOInterpretation L₁ L₂ Tag d) (φ : L₂.Formula β) (τ : β → Tag) (v : β × Fin d → A) : (I.pullF φ τ).Realize v ↔ φ.Realize fun (b : β) => (τ b, fun (j : Fin d) => v (b, j))

Transfer along a bijection of nodes

Acceptance only depends on the walk up to a bijection of its nodes. Stated for two specifications over two vocabularies, since the pullback relates a specification over the base structure to one over the interpreted structure.

theorem DescriptiveComplexity.TCSpec.reach_map {L L' : FirstOrder.Language} {spec₁ : TCSpec L} {spec₂ : TCSpec L'} {A B : Type} [L.Structure A] [LinearOrder A] [L'.Structure B] [LinearOrder B] (e : spec₁.Node A ≃ spec₂.Node B) (hstep : ∀ (a b : spec₁.Node A), spec₁.Step a b ↔ spec₂.Step (e a) (e b)) {a b : spec₁.Node A} (h : spec₁.Reach a b) : spec₂.Reach (e a) (e b)

theorem DescriptiveComplexity.TCSpec.accepts_congr {L L' : FirstOrder.Language} {spec₁ : TCSpec L} {spec₂ : TCSpec L'} {A B : Type} [L.Structure A] [LinearOrder A] [L'.Structure B] [LinearOrder B] (e : spec₁.Node A ≃ spec₂.Node B) (hstep : ∀ (a b : spec₁.Node A), spec₁.Step a b ↔ spec₂.Step (e a) (e b)) (hsrc : ∀ (a : spec₁.Node A), spec₁.IsSrc a ↔ spec₂.IsSrc (e a)) (htgt : ∀ (a : spec₁.Node A), spec₁.IsTgt a ↔ spec₂.IsTgt (e a)) : spec₁.Accepts A ↔ spec₂.Accepts B

Acceptance transfers along a bijection of nodes carrying steps to steps and endpoints to endpoints.

theorem DescriptiveComplexity.TCSpec.det_step_congr {L L' : FirstOrder.Language} {spec₁ : TCSpec L} {spec₂ : TCSpec L'} {A B : Type} [L.Structure A] [LinearOrder A] [L'.Structure B] [LinearOrder B] (e : spec₁.Node A ≃ spec₂.Node B) (hstep : ∀ (a b : spec₁.Node A), spec₁.Step a b ↔ spec₂.Step (e a) (e b)) (a b : spec₁.Node A) : spec₁.det.Step a b ↔ spec₂.det.Step (e a) (e b)

Determinization transfers along a bijection of nodes: having no competing successor is a property of the walk, not of its presentation.

theorem DescriptiveComplexity.TCSpec.det_accepts_iff {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (h : spec.Functional A) : spec.det.Accepts A ↔ spec.Accepts A

On a functional specification the deterministic reading changes nothing, acceptance included.

The pullback of a specification

def DescriptiveComplexity.comapStepIx (k d : ℕ) : (Fin k ⊕ Fin k) × Fin d → Fin (k * d) ⊕ Fin (k * d)

The renaming of the pulled transition formula's variables: a coordinate of an argument becomes a coordinate of the corresponding flat tuple, the two tuples staying apart.

Equations

• DescriptiveComplexity.comapStepIx k d p = Sum.elim (fun (i : Fin k) => Sum.inl (finProdFinEquiv (i, p.2))) (fun (i : Fin k) => Sum.inr (finProdFinEquiv (i, p.2))) p.1

def DescriptiveComplexity.comapEndIx (k d : ℕ) : Fin k × Fin d → Fin (k * d)

The renaming of a pulled endpoint formula's variables: argument and coordinate become a position of the flat tuple.

Equations

• DescriptiveComplexity.comapEndIx k d p = finProdFinEquiv p

noncomputable def DescriptiveComplexity.TCSpec.comap {L L' : FirstOrder.Language} [L'.IsRelational] {Tag : Type} [Finite Tag] [LinearOrder Tag] {d : ℕ} (spec : TCSpec L') (I : FOInterpretation (L.sum FirstOrder.Language.order) L' Tag d) : TCSpec L

The pullback of a specification through an interpretation: the walk of spec on the interpreted structure, written on the base structure. The tags of the current tuple ride along in the mode; its coordinates become the flat tuple of length k · d; the three formulas are pulled back at those tags, through the order-extended interpretation, the specification's formulas being allowed to mention the target's order.

Equations

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

def DescriptiveComplexity.comapNodeEquiv {L L' : FirstOrder.Language} [L'.IsRelational] {Tag : Type} [Finite Tag] [LinearOrder Tag] {d : ℕ} (spec : TCSpec L') (I : FOInterpretation (L.sum FirstOrder.Language.order) L' Tag d) {A : Type} : (spec.comap I).Node A ≃ spec.Node (I.Map A)

The bijection between the nodes of the pullback over the base structure and the nodes of the specification over the interpreted structure: a mode is a mode with a tuple of tags, and a flat tuple of coordinates is a tuple of tagged tuples.

Equations

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

Correctness of the pullback

Realizing a pulled formula on the base structure is realizing the original on the interpreted structure – once the latter is read with the lexicographic order, which is what the order-extended interpretation produces. The two structures live on the same type and differ only in how the order symbol is read, so the transport below is spelled with explicit instances.

theorem DescriptiveComplexity.realize_ordExtend_iff {L L' : FirstOrder.Language} [L'.IsRelational] {Tag : Type} [LinearOrder Tag] {d : ℕ} (I : FOInterpretation (L.sum FirstOrder.Language.order) L' Tag d) {A : Type} [L.Structure A] [LinearOrder A] {β : Type} (φ : (L'.sum FirstOrder.Language.order).Formula β) (v : β → I.Map A) : φ.Realize v ↔ φ.Realize v

Reading a formula of the ordered expansion of the target on the structure produced by the order-extended interpretation is reading it on the interpreted structure equipped with the lexicographic order.

theorem DescriptiveComplexity.TCSpec.comap_step_iff {L L' : FirstOrder.Language} [L'.IsRelational] {Tag : Type} [Finite Tag] [LinearOrder Tag] {d : ℕ} (spec : TCSpec L') (I : FOInterpretation (L.sum FirstOrder.Language.order) L' Tag d) {A : Type} [L.Structure A] [LinearOrder A] (a b : (spec.comap I).Node A) : (spec.comap I).Step a b ↔ spec.Step ((comapNodeEquiv spec I) a) ((comapNodeEquiv spec I) b)

Steps correspond: a step of the pullback on the base structure is a step of the specification on the interpreted structure.

theorem DescriptiveComplexity.TCSpec.comap_isSrc_iff {L L' : FirstOrder.Language} [L'.IsRelational] {Tag : Type} [Finite Tag] [LinearOrder Tag] {d : ℕ} (spec : TCSpec L') (I : FOInterpretation (L.sum FirstOrder.Language.order) L' Tag d) {A : Type} [L.Structure A] [LinearOrder A] (a : (spec.comap I).Node A) : (spec.comap I).IsSrc a ↔ spec.IsSrc ((comapNodeEquiv spec I) a)

Starting nodes correspond.

theorem DescriptiveComplexity.TCSpec.comap_isTgt_iff {L L' : FirstOrder.Language} [L'.IsRelational] {Tag : Type} [Finite Tag] [LinearOrder Tag] {d : ℕ} (spec : TCSpec L') (I : FOInterpretation (L.sum FirstOrder.Language.order) L' Tag d) {A : Type} [L.Structure A] [LinearOrder A] (a : (spec.comap I).Node A) : (spec.comap I).IsTgt a ↔ spec.IsTgt ((comapNodeEquiv spec I) a)

Accepting nodes correspond.

theorem DescriptiveComplexity.TCSpec.comap_accepts_iff {L L' : FirstOrder.Language} [L'.IsRelational] {Tag : Type} [Finite Tag] [LinearOrder Tag] {d : ℕ} (spec : TCSpec L') (I : FOInterpretation (L.sum FirstOrder.Language.order) L' Tag d) {A : Type} [L.Structure A] [LinearOrder A] : (spec.comap I).Accepts A ↔ spec.Accepts (I.Map A)

The pullback is correct: it accepts the base structure exactly when the specification accepts the interpreted one.

theorem DescriptiveComplexity.TCSpec.comap_det_accepts_iff {L L' : FirstOrder.Language} [L'.IsRelational] {Tag : Type} [Finite Tag] [LinearOrder Tag] {d : ℕ} (spec : TCSpec L') (I : FOInterpretation (L.sum FirstOrder.Language.order) L' Tag d) {A : Type} [L.Structure A] [LinearOrder A] : (spec.comap I).det.Accepts A ↔ spec.det.Accepts (I.Map A)

The pullback is correct for the deterministic reading too, by the same node bijection: determinism is a property of the walk.

Closure under reductions

theorem DescriptiveComplexity.TCDefinable.of_orderedReduction {L L' : FirstOrder.Language} [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (f : OrderedFOReduction P Q) (h : TCDefinable Q) : TCDefinable P

FO(TC) definability is closed under ordered first-order reductions. The walk of the specification on the interpreted structure is a walk on the base structure, its tags carried in the mode and its coordinates flattened.

theorem DescriptiveComplexity.TCDefinable.of_foReduction {L L' : FirstOrder.Language} [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (f : FOReduction P Q) (h : TCDefinable Q) : TCDefinable P

FO(TC) definability is closed under first-order reductions.

theorem DescriptiveComplexity.DTCDefinable.of_orderedReduction {L L' : FirstOrder.Language} [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (f : OrderedFOReduction P Q) (h : DTCDefinable Q) : DTCDefinable P

FO(DTC) definability is closed under ordered first-order reductions, by the same pullback: the node bijection carries the determinized walk to the determinized walk.

theorem DescriptiveComplexity.DTCDefinable.of_foReduction {L L' : FirstOrder.Language} [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (f : FOReduction P Q) (h : DTCDefinable Q) : DTCDefinable P

FO(DTC) definability is closed under first-order reductions.