An induction, then a partial iteration: one partial iteration

DescriptiveComplexity.StepDef.stratify composes two inflationary inductions. This file composes an inflationary induction with a partial one (DescriptiveComplexity.StepDef.stratifyPFP): the value of the second iteration, run over the structure expanded by the first one's limit, is the value of a single partial iteration (DescriptiveComplexity.StepDef.pfpHolds_stratifyPFP).

That is what closes DescriptiveComplexity.PSPACE under FO(LFP) reductions (DescriptiveComplexity.FixedPointReductionSpace): a reduction's induction has to be absorbed into the membership witness, and PSPACE's witness is a partial iteration.

Why a partial second stratum still works

The received reason to expect trouble is that a partial iteration is not monotone, so “run the second stratum once the first has converged” cannot be arranged by inflation, as DescriptiveComplexity.StepDef.stratify arranges it. What makes it work anyway is that only the gating needs monotonicity, and the gate is a bit of the state, not of the second stratum:

• the first stratum's variables accumulate – its step formula is written with the accumulation spelled out, since the composite iteration replaces rather than accumulates;
• the gate is an arity-0 variable, set once the first stratum's step formulas add nothing (DescriptiveComplexity.stratGateF) and never unset;
• the second stratum's step is conjoined with the gate, so its variables stay empty until the gate fires and then iterate partially, from the empty assignment, over the frozen first stratum.

The stage count then shifts by the gate's index and nothing else: the composite is at stage G + 1 + m exactly what the second stratum is at stage m (DescriptiveComplexity.StepDef.strat2Assign_partStage_add). Fixed points can only occur after the gate has fired – before it, either the first stratum still moves or the gate itself does – so the composite converges exactly when the second stratum does, and reads the same output there.

The atom of a first-stratum variable

noncomputable def DescriptiveComplexity.strat1AtomF (L : FirstOrder.Language) (B₁ B₂ : SOBlock) (i : B₁.ι) : (L.sum (stratBlock B₁ B₂).lang).Formula (Fin (B₁.arity i))

A first-stratum variable, as a formula over the combined block: the composite iteration replaces rather than accumulates, so the accumulation has to be written out.

Equations

• DescriptiveComplexity.strat1AtomF L B₁ B₂ i = (DescriptiveComplexity.strat1Sym L B₁ B₂ i).formula fun (j : Fin (B₁.arity i)) => FirstOrder.Language.var j

The composite

@[reducible]

noncomputable def DescriptiveComplexity.StepDef.stratifyPFP {L : FirstOrder.Language} (d₁ : StepDef L) (d₂ : StepDef (L.sum d₁.B.lang)) : StepDef L

An inflationary stratum followed by a partial one: the first stratum's variables accumulate, the gate fires when they stop moving, and the second stratum's variables iterate partially behind the gate, over the frozen first stratum.

Reducible, so that the block of the composite is the combined block: the stage lemmas below rewrite with assignment-level equalities, which instance search must see through.

Equations

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

The three parts of one step

The stages of the composite

theorem DescriptiveComplexity.StepDef.strat2Assign_partStage_add {L : FirstOrder.Language} (d₁ : StepDef L) (d₂ : StepDef (L.sum d₁.B.lang)) {A : Type} [L.Structure A] {G : ℕ} {ρ₁ : d₁.B.Assignment A} (hG : StratGate ((d₁.stratifyPFP d₂).partStage A G)) (hbot : strat2Assign ((d₁.stratifyPFP d₂).partStage A G) = d₂.B.botAssign A) (hfr : ∀ (n : ℕ), G ≤ n → strat1Assign ((d₁.stratifyPFP d₂).partStage A n) = ρ₁) (m : ℕ) : strat2Assign ((d₁.stratifyPFP d₂).partStage A (G + m)) = d₂.partStage A m

Once the gate is on and the first stratum frozen, the second stratum replays its own partial stages.

The value of the composite

theorem DescriptiveComplexity.StepDef.pfpHolds_stratifyPFP {L : FirstOrder.Language} (d₁ : StepDef L) (d₂ : StepDef (L.sum d₁.B.lang)) {A : Type} [L.Structure A] [Finite A] : (d₁.stratifyPFP d₂).PFPHolds A ↔ d₂.PFPHolds A

The composite computes the second iteration over the first one's limit. An inflationary induction followed by a partial iteration is one partial iteration: the composite converges exactly when the second stratum does, over the structure expanded by the first stratum's limit, and reads the same output there.