FO(≤, PFP) is contained in SO(TC)

The easy half of the capture theorem FO(≤, PFP) = PSPACE (Abiteboul–Vianu 1989; Ebbinghaus–Flum 1995, ch. 7): a partial fixed-point iteration is a deterministic walk on the state space SO(TC) walks on – the assignments of the block – so a DescriptiveComplexity.StepDef read partially translates into a DescriptiveComplexity.SOTCSpec verbatim (DescriptiveComplexity.StepDef.toSOTCSpec):

• the walk's states are the assignments of the same block;
• its transition sentence says «the second copy is one application of the step formulas to the first» (DescriptiveComplexity.StepDef.nextSentence);
• its source is the empty assignment (DescriptiveComplexity.StepDef.botSentence);
• its target says «the state is a fixed point of the step, and the output holds» (DescriptiveComplexity.StepDef.isFixedPtF, conjoined with the output).

The states reachable from the source along the deterministic transition are exactly the partial stages, so acceptance is DescriptiveComplexity.StepDef.PFPHolds (DescriptiveComplexity.StepDef.accepts_toSOTCSpec) – with no divergence detection: under the convergence-requiring semantics of DescriptiveComplexity.FixedPointPartial, a diverging iteration simply reaches no target state. This is what the divergence convention buys; the textbook convention would need a step counter to make divergence positively detectable, and a counter is the one thing this translation would otherwise need the order for.

Whence FO(≤, PFP) ⊆ PSPACE: DescriptiveComplexity.PFPDefinable.sotcDefinable and DescriptiveComplexity.mem_PSPACE_of_pfpDefinable. The converse inclusion – PSPACE ⊆ FO(≤, PFP), completing the capture – iterates the PSPACE-complete deterministic machine problem and is built in DescriptiveComplexity.FixedPointPartialMachine.

DescriptiveComplexity.StepDef.isFixedPtF is also the guard that reads a definition of this library in the textbook divergence convention – see the divergence discussion in DescriptiveComplexity.FixedPointPartial.

Enumerating the variables of a block

noncomputable def DescriptiveComplexity.SOBlock.idxList (B : SOBlock) : List B.ι

The relation variables of a block, as a list: the sentences below conjoin one clause per variable.

Equations

• B.idxList = Finset.univ.toList

theorem DescriptiveComplexity.SOBlock.mem_idxList (B : SOBlock) (i : B.ι) : i ∈ B.idxList

The three sentences of the walk

@[reducible, inline]

abbrev DescriptiveComplexity.StepDef.newVarSym (L : FirstOrder.Language) (B : SOBlock) (i : B.ι) : ((L.sum B.lang).sum B.lang).Relations (B.arity i)

The atom of a block variable in the second copy of the block, over two copies.

Equations

• DescriptiveComplexity.StepDef.newVarSym L B i = Sum.inr (DescriptiveComplexity.varSym B i)

noncomputable def DescriptiveComplexity.StepDef.nextSentence {L : FirstOrder.Language} (d : StepDef L) : ((L.sum d.B.lang).sum d.B.lang).Sentence

«The second copy of the block is one application of the step formulas to the first»: the transition sentence of the walk.

Equations

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

noncomputable def DescriptiveComplexity.StepDef.botSentence {L : FirstOrder.Language} (d : StepDef L) : (L.sum d.B.lang).Sentence

«Every relation of the block is empty»: the source sentence of the walk.

Equations

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

noncomputable def DescriptiveComplexity.StepDef.isFixedPtF {L : FirstOrder.Language} (d : StepDef L) : (L.sum d.B.lang).Sentence

«The state is a fixed point of the step formulas», as a sentence over one copy of the block. Also the guard that transfers a definition between the two divergence conventions – see DescriptiveComplexity.FixedPointPartial.

Equations

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

Their semantics

theorem DescriptiveComplexity.StepDef.realize_nextSentence {L : FirstOrder.Language} (d : StepDef L) {A : Type} [L.Structure A] (ρ σ : d.B.Assignment A) : A ⊨ d.nextSentence ↔ σ = d.next ρ

theorem DescriptiveComplexity.StepDef.realize_botSentence {L : FirstOrder.Language} (d : StepDef L) {A : Type} [L.Structure A] (ρ : d.B.Assignment A) : A ⊨ d.botSentence ↔ ρ = d.B.botAssign A

theorem DescriptiveComplexity.StepDef.realize_isFixedPtF {L : FirstOrder.Language} (d : StepDef L) {A : Type} [L.Structure A] (ρ : d.B.Assignment A) : A ⊨ d.isFixedPtF ↔ Function.IsFixedPt d.next ρ

The walk of a partial iteration

noncomputable def DescriptiveComplexity.StepDef.toSOTCSpec {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) : SOTCSpec L

The SO(TC) specification of a partial fixed-point definition: walk the deterministic iteration of the step formulas from the empty assignment, and accept at a stable stage satisfying the output.

Equations

• d.toSOTCSpec = { B := d.B, step := d.nextSentence, src := d.botSentence, tgt := d.isFixedPtF ⊓ d.out }

theorem DescriptiveComplexity.StepDef.toSOTCSpec_step_iff {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (ρ σ : d.B.Assignment A) : d.toSOTCSpec.Step ρ σ ↔ σ = d.next ρ

theorem DescriptiveComplexity.StepDef.toSOTCSpec_isSrc_iff {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (ρ : d.B.Assignment A) : d.toSOTCSpec.IsSrc ρ ↔ ρ = d.B.botAssign A

theorem DescriptiveComplexity.StepDef.toSOTCSpec_isTgt_iff {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (ρ : d.B.Assignment A) : d.toSOTCSpec.IsTgt ρ ↔ Function.IsFixedPt d.next ρ ∧ A ⊨ d.out

theorem DescriptiveComplexity.StepDef.reach_toSOTCSpec {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (σ : d.B.Assignment A) : d.toSOTCSpec.Reach (d.B.botAssign A) σ ↔ ∃ (n : ℕ), σ = d.partStage A n

The states reachable from the empty assignment are exactly the partial stages.

theorem DescriptiveComplexity.StepDef.accepts_toSOTCSpec {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] : d.toSOTCSpec.Accepts A ↔ d.PFPHolds A

Acceptance of the walk is the value of the partial definition: a stable stage satisfying the output is reachable from the empty assignment exactly when the iteration converges to a limit satisfying the output.

FO(≤, PFP) is contained in PSPACE

theorem DescriptiveComplexity.PFPDefinable.sotcDefinable {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : PFPDefinable P) : SOTCDefinable P

Every FO(≤, PFP) definable problem is SO(TC) definable: the partial iteration is a deterministic walk on the assignments of its own block.

theorem DescriptiveComplexity.mem_PSPACE_of_pfpDefinable {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : PFPDefinable P) : PSPACE.Mem P

FO(≤, PFP) is contained in PSPACE.