Towers of walks: reachability relations that may read earlier ones

A DescriptiveComplexity.TCFamily is a finite family of walks over one vocabulary. What composition of reductions produces is not that: pulling the walks of an outer reduction back through an inner one gives walks whose step formulas read the inner walks' reachability relations. A DescriptiveComplexity.TCTower is the closure of the notion under that – a list of families, each over the vocabulary expanded by the blocks of the ones before it – which is FO(TC) with nesting, the operator applied to formulas that may themselves contain it.

The point of the construction

DescriptiveComplexity.TCTower.inflLimit_toStepDef: a tower's reachability relations are the value of a single inflationary induction, namely the stratification (DescriptiveComplexity.StepDef.stratify) of the inductions of its families. Each family is an induction already (DescriptiveComplexity.TCFamily.inflLimit_toStepDef); a stratum reads the strata below it through the gate the library's stratification already provides, and the recursion is one line per constructor.

So a tower costs nothing beyond a family: it is still an FO(LFP) interpretation (DescriptiveComplexity.TransitiveClosureReduction), with the same closure properties. Composition of ≤ᵗᶜ with itself does not go through towers in the end (DescriptiveComplexity.TransitiveClosureReductionTrans flattens the outer walks instead); a tower remains the natural reading of nested walks.

What is not claimed

That a tower can be flattened into a single family. Classically it can, and the notion this file defines is therefore the classical one; here the flattening is proved one level at a time and at the encodings of nodes (DescriptiveComplexity.ParamTCSpec.flat, DescriptiveComplexity.TransitiveClosureFlatten), which is what the closure of DescriptiveComplexity.NL under ≤ᵗᶜ uses, and not as an equality of families; a tower is not flattened as such.

Towers

inductive DescriptiveComplexity.TCTower : FirstOrder.Language → Type 1

A tower of walk families: each family's walks may read the reachability relations of the families below, its vocabulary being the base expanded by their blocks.

• nil {L : FirstOrder.Language} : TCTower L

  The empty tower.

• cons {L : FirstOrder.Language} (F : TCFamily L) (rest : TCTower (L.sum F.block.lang)) : TCTower L

  A family, and above it a tower over the vocabulary its block expands.

noncomputable def DescriptiveComplexity.TCTower.emptyStepDef (L : FirstOrder.Language) : StepDef L

The induction with no relation variables: the empty tower's.

Equations

• DescriptiveComplexity.TCTower.emptyStepDef L = { B := DescriptiveComplexity.SOBlock.trivial, step := fun (i : DescriptiveComplexity.SOBlock.trivial.ι) => Empty.elim i, out := ⊤ }

noncomputable def DescriptiveComplexity.TCTower.toStepDef {L : FirstOrder.Language} : TCTower L → StepDef L

The induction that computes a tower's reachability relations: the stratification of the families' own inductions.

Equations

• DescriptiveComplexity.TCTower.nil.toStepDef = DescriptiveComplexity.TCTower.emptyStepDef x✝
• (DescriptiveComplexity.TCTower.cons F rest).toStepDef = F.toStepDef.stratify rest.toStepDef

noncomputable def DescriptiveComplexity.TCTower.block {L : FirstOrder.Language} (T : TCTower L) : SOBlock

The block of relation variables a tower's formulas may read.

Equations

• T.block = T.toStepDef.B

@[simp]

theorem DescriptiveComplexity.TCTower.block_nil {L : FirstOrder.Language} : nil.block = SOBlock.trivial

@[simp]

theorem DescriptiveComplexity.TCTower.block_cons {L : FirstOrder.Language} (F : TCFamily L) (rest : TCTower (L.sum F.block.lang)) : (cons F rest).block = stratBlock F.block rest.block

The relations a tower holds

def DescriptiveComplexity.TCTower.stratAssign {A : Type} {B₁ B₂ : SOBlock} (ρ₁ : B₁.Assignment A) (g : Prop) (ρ₂ : B₂.Assignment A) : (stratBlock B₁ B₂).Assignment A

An assignment of a stratified block, from its three parts.

Equations

• DescriptiveComplexity.TCTower.stratAssign ρ₁ g ρ₂ (Sum.inl (Sum.inl i)) = ρ₁ i
• DescriptiveComplexity.TCTower.stratAssign ρ₁ g ρ₂ (Sum.inl (Sum.inr val)) = fun (x : Fin ((DescriptiveComplexity.stratBlock B₁ B₂).arity (Sum.inl (Sum.inr val))) → A) => g
• DescriptiveComplexity.TCTower.stratAssign ρ₁ g ρ₂ (Sum.inr i) = ρ₂ i

@[simp]

theorem DescriptiveComplexity.TCTower.strat1Assign_stratAssign {A : Type} {B₁ B₂ : SOBlock} (ρ₁ : B₁.Assignment A) (g : Prop) (ρ₂ : B₂.Assignment A) : strat1Assign (stratAssign ρ₁ g ρ₂) = ρ₁

@[simp]

theorem DescriptiveComplexity.TCTower.strat2Assign_stratAssign {A : Type} {B₁ B₂ : SOBlock} (ρ₁ : B₁.Assignment A) (g : Prop) (ρ₂ : B₂.Assignment A) : strat2Assign (stratAssign ρ₁ g ρ₂) = ρ₂

theorem DescriptiveComplexity.TCTower.stratGate_stratAssign {A : Type} {B₁ B₂ : SOBlock} (ρ₁ : B₁.Assignment A) (g : Prop) (ρ₂ : B₂.Assignment A) : StratGate (stratAssign ρ₁ g ρ₂) ↔ g

noncomputable def DescriptiveComplexity.TCTower.reachAssign {L : FirstOrder.Language} (T : TCTower L) (A : Type) (_instA : L.Structure A) : T.block.Assignment A

The relations a tower holds: each family's reachability relations, read over the structure the families below it have already expanded. The gate of each stratum is set, as it is at the value of the stratified induction.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.TCTower.nil.reachAssign x✝¹ x✝ = fun (i : DescriptiveComplexity.TCTower.nil.block.ι) => Empty.elim i

@[simp]

theorem DescriptiveComplexity.TCTower.reachAssign_cons {L : FirstOrder.Language} (F : TCFamily L) (rest : TCTower (L.sum F.block.lang)) (A : Type) (instA : L.Structure A) : (cons F rest).reachAssign A instA = stratAssign (F.reachAssign A) True (rest.reachAssign A (F.block.structure₁ (F.reachAssign A)))

A tower is an induction

theorem DescriptiveComplexity.TCTower.inflLimit_toStepDef {L : FirstOrder.Language} (T : TCTower L) (A : Type) [instA : L.Structure A] [Finite A] : T.toStepDef.inflLimit A = T.reachAssign A instA

A tower's relations are the value of one inflationary induction.