Pulling SO(TC) definability back through an interpretation

SO(TC) definability is closed under (ordered) first-order reductions (DescriptiveComplexity.SOTCDefinable.of_orderedReduction). This is what makes DescriptiveComplexity.PSPACE a DescriptiveComplexity.ComplexityClass rather than a mere definability predicate.

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

A state of an SO(TC) walk is an assignment of a second-order block, so pulling a specification back is entirely a matter of pulling its block back – there are no tuples of elements and no modes to rearrange, unlike DescriptiveComplexity.TCSpec.comap. The block pullback of DescriptiveComplexity.SecondOrderPull already supplies everything:

• the pulled block is DescriptiveComplexity.SOBlock.pull, one (n·d)-ary relation variable on the base universe per n-tuple of tags;
• its assignments are in bijection with the assignments of the original block on the interpreted universe (DescriptiveComplexity.SOBlock.pullAssignEquiv, the two transfers pullAssign/mergeAssign being mutually inverse);
• the three sentences are pulled back by DescriptiveComplexity.FOInterpretation.pullSentence through the interpretation extended along the block – twice for the transition sentence, which sees two copies of the block.

The order enters as it does for the clausal fragments and for FO(TC): the sentences 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 SO(TC) definability is required for every linear order, the lexicographic one is available.

The chain of transports

Each of the three correctness lemmas is the same three-step chain, read from the interpreted side:

1. DescriptiveComplexity.FOInterpretation.realize_pullSentence – the pulled sentence on the base structure is the original on the interpreted one;
2. DescriptiveComplexity.FOInterpretation.extendSOEquiv – interpreting and then expanding by a block is expanding by the pulled block and then interpreting (once per copy of the block);
3. DescriptiveComplexity.FOInterpretation.ordExtendLEquiv – the order-extended interpretation produces the interpreted structure with the lexicographic order.

Steps 2 and 3 need the expansion of an isomorphism along a block that is interpreted by the same assignment on both sides, which is DescriptiveComplexity.SOBlock.extendEquiv at an identity map (its transport DescriptiveComplexity.SOBlock.mapAssign along Equiv.refl is the identity, by definitional eta).

The two assignment transfers are mutually inverse

theorem DescriptiveComplexity.SOBlock.mergeAssign_pullAssign {Tag : Type} [Finite Tag] {d : ℕ} {A : Type} (B : SOBlock) (ρ : B.Assignment (Tag × (Fin d → A))) : B.mergeAssign (B.pullAssign ρ) = ρ

Merging a pulled assignment gives the assignment back: the transfer DescriptiveComplexity.SOBlock.pullAssign is injective, with DescriptiveComplexity.SOBlock.mergeAssign as a retraction on the other side.

def DescriptiveComplexity.SOBlock.pullAssignEquiv (Tag : Type) [Finite Tag] (d : ℕ) (A : Type) (B : SOBlock) : B.Assignment (Tag × (Fin d → A)) ≃ (pull Tag d B).Assignment A

The states of the pulled walk are the states of the original walk on the interpreted universe: assignments of the pulled block on the base universe correspond bijectively to assignments of the block on the tagged tuples.

Equations

• DescriptiveComplexity.SOBlock.pullAssignEquiv Tag d A B = { toFun := B.pullAssign, invFun := B.mergeAssign, left_inv := ⋯, right_inv := ⋯ }

The pullback of a specification

noncomputable def DescriptiveComplexity.FOInterpretation.ordExtendSO {L L' : FirstOrder.Language} {Tag : Type} [Finite Tag] [LinearOrder Tag] {d : ℕ} (I : FOInterpretation (L.sum FirstOrder.Language.order) L' Tag d) (B : SOBlock) : FOInterpretation ((L.sum FirstOrder.Language.order).sum (SOBlock.pull Tag d B).lang) ((L'.sum FirstOrder.Language.order).sum B.lang) Tag d

The interpretation extended with the order and along one copy of a block: the layer through which the source and target sentences are pulled back.

Equations

• I.ordExtendSO B = I.ordExtend.extendSO B

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

The pullback of a specification through an interpretation: the walk of spec on the interpreted structure, written on the base structure. Its states are the assignments of the pulled block; its three sentences are pulled back through the order-extended interpretation, expanded along one copy of the block for the endpoints and along two for the transition.

Equations

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

theorem DescriptiveComplexity.SOTCSpec.comap_isSrc_iff {L L' : FirstOrder.Language} [L'.IsRelational] {Tag : Type} [Finite Tag] [LinearOrder Tag] {d : ℕ} (spec : SOTCSpec L') (I : FOInterpretation (L.sum FirstOrder.Language.order) L' Tag d) {A : Type} [L.Structure A] [LinearOrder A] (ρ : spec.B.Assignment (I.Map A)) : spec.IsSrc ρ ↔ (spec.comap I).IsSrc (spec.B.pullAssign ρ)

Starting states correspond.

theorem DescriptiveComplexity.SOTCSpec.comap_isTgt_iff {L L' : FirstOrder.Language} [L'.IsRelational] {Tag : Type} [Finite Tag] [LinearOrder Tag] {d : ℕ} (spec : SOTCSpec L') (I : FOInterpretation (L.sum FirstOrder.Language.order) L' Tag d) {A : Type} [L.Structure A] [LinearOrder A] (ρ : spec.B.Assignment (I.Map A)) : spec.IsTgt ρ ↔ (spec.comap I).IsTgt (spec.B.pullAssign ρ)

Accepting states correspond.

theorem DescriptiveComplexity.SOTCSpec.comap_step_iff {L L' : FirstOrder.Language} [L'.IsRelational] {Tag : Type} [Finite Tag] [LinearOrder Tag] {d : ℕ} (spec : SOTCSpec L') (I : FOInterpretation (L.sum FirstOrder.Language.order) L' Tag d) {A : Type} [L.Structure A] [LinearOrder A] (ρ σ : spec.B.Assignment (I.Map A)) : spec.Step ρ σ ↔ (spec.comap I).Step (spec.B.pullAssign ρ) (spec.B.pullAssign σ)

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

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

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

Closure under reductions

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

SO(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 states the assignments of the pulled block.

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

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