FO(PFP): first-order logic with a partial fixed point

The partial fixed-point logic (Abiteboul–Vianu 1989; Ebbinghaus–Flum 1995, ch. 7): iterate the step formulas of a DescriptiveComplexity.StepDef by replacement – each stage is one application of the step formulas to the previous one – and read the output at the first stable stage, if the iteration stabilizes at all.

The divergence convention

DescriptiveComplexity.StepDef.PFPHolds requires convergence: a diverging iteration makes the definition false, whatever the output sentence. The textbook semantics instead assigns a diverging iteration the empty relations and reads the output there; the two readings are compared precisely by DescriptiveComplexity.StepDef.realize_pfpValue_iff – they agree unless the iteration diverges and the output holds at the empty assignment. The convergence-requiring convention is chosen deliberately:

• it is what makes the translation to SO(TC) direct (DescriptiveComplexity.FixedPointPartialSpace): acceptance of the walk is «some stable stage satisfying the output is reachable», with no divergence detection – on unordered structures, none is available;
• every definition in the textbook semantics whose output fails on the empty assignment means the same thing here, and conversely a definition of this file is read in the textbook semantics by guarding its output with «the state is a fixed point of the step» – the guard is first-order (DescriptiveComplexity.StepDef.isFixedPtF in DescriptiveComplexity.FixedPointPartialSpace), and it fails at the empty assignment of a diverging iteration, since a diverging iteration's empty start is not a fixed point.

As for IFP, there is an ordered notion (DescriptiveComplexity.PFPDefinable, the setting of the capture theorem FO(≤, PFP) = PSPACE) and an order-free one (DescriptiveComplexity.PFPDefinableFree, the right-hand side of the Abiteboul–Vianu theorem), and the two must not be conflated.

Inflation is a special case

DescriptiveComplexity.StepDef.inflate disjoins each variable's own atom onto its step formula, making the partial iteration of the modified definition the inflationary iteration of the original one. Since an inflationary iteration always converges on finite structures, FO(IFP) is contained in FO(PFP) (DescriptiveComplexity.IFPDefinable.pfpDefinable, DescriptiveComplexity.IFPDefinableFree.pfpDefinableFree) – the easy inclusion of Abiteboul–Vianu, in both its ordered and order-free forms.

Closure properties

Same story as for IFP: closed under (ordered) first-order reductions by the transport lemmas of DescriptiveComplexity.FixedPointStep (DescriptiveComplexity.PFPDefinable.of_orderedReduction, DescriptiveComplexity.PFPDefinableFree.of_foReduction). Closure under complement is not by negating the output – divergence makes both a definition and its output-negation false – but follows on ordered structures from the capture theorem (DescriptiveComplexity.FixedPointPartialSpace) and PSPACE = coPSPACE.

The value of a partial definition

def DescriptiveComplexity.StepDef.PFPHolds {L : FirstOrder.Language} (d : StepDef L) (A : Type) [L.Structure A] : Prop

The value of a simultaneous induction read partially: some stage is a fixed point of the step and satisfies the output sentence. All stable stages are equal (DescriptiveComplexity.StepDef.partStage_eq_of_isFixedPt), so this says exactly «the iteration converges and its limit satisfies the output» – see the module docstring for the divergence convention.

Equations

• d.PFPHolds A = ∃ (n : ℕ), Function.IsFixedPt d.next (d.partStage A n) ∧ A ⊨ d.out

def DescriptiveComplexity.StepDef.PFPConverges {L : FirstOrder.Language} (d : StepDef L) (A : Type) [L.Structure A] : Prop

The partial iteration converges: some stage is a fixed point of the step.

Equations

• d.PFPConverges A = ∃ (n : ℕ), Function.IsFixedPt d.next (d.partStage A n)

theorem DescriptiveComplexity.StepDef.PFPHolds.converges {L : FirstOrder.Language} {d : StepDef L} {A : Type} [L.Structure A] (h : d.PFPHolds A) : d.PFPConverges A

A definition whose value is read converges.

theorem DescriptiveComplexity.StepDef.exists_least_stable {L : FirstOrder.Language} (d : StepDef L) (A : Type) [L.Structure A] (h : d.PFPConverges A) : ∃ (N : ℕ), d.partStage A N = d.partStage A (N + 1) ∧ ∀ n < N, d.partStage A n ≠ d.partStage A (n + 1)

The first stage that does not move: convergence is witnessed by a least index. That is what a machine testing «this stage and the next agree» at each round stops at, and what makes its earlier rounds' tests fail.

noncomputable def DescriptiveComplexity.StepDef.pfpValue {L : FirstOrder.Language} (d : StepDef L) (A : Type) [L.Structure A] : d.B.Assignment A

The textbook value of the partial iteration: the stable stage if the iteration converges, the empty assignment otherwise. Only used to relate the two divergence conventions (DescriptiveComplexity.StepDef.realize_pfpValue_iff); the semantics of the logic is DescriptiveComplexity.StepDef.PFPHolds.

Equations

• d.pfpValue A = if h : d.PFPConverges A then d.partStage A (Exists.choose h) else d.B.botAssign A

theorem DescriptiveComplexity.StepDef.realize_pfpValue_iff {L : FirstOrder.Language} (d : StepDef L) (A : Type) [L.Structure A] : A ⊨ d.out ↔ d.PFPHolds A ∨ ¬d.PFPConverges A ∧ A ⊨ d.out

The two divergence conventions, compared: the textbook reading – the output at DescriptiveComplexity.StepDef.pfpValue – differs from DescriptiveComplexity.StepDef.PFPHolds exactly on a diverging iteration whose output holds at the empty assignment.

theorem DescriptiveComplexity.StepDef.pfpHolds_equiv {L : FirstOrder.Language} (d : StepDef L) {M N : Type} [L.Structure M] [L.Structure N] (e : L.Equiv M N) : d.PFPHolds M ↔ d.PFPHolds N

The value of a partial definition is isomorphism-invariant.

Definability, ordered and order-free

def DescriptiveComplexity.PFPDefinableFree {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : Prop

A decision problem is order-free FO(PFP) definable if, on nonempty finite structures, it is the value of a simultaneous induction over its own vocabulary, read partially. This is the unordered notion on the fixed-point side of the Abiteboul–Vianu theorem.

Equations

• DescriptiveComplexity.PFPDefinableFree P = ∃ (d : DescriptiveComplexity.StepDef L), ∀ (A : Type) [inst : L.Structure A] [Finite A] [Nonempty A], P.Holds A ↔ d.PFPHolds A

def DescriptiveComplexity.PFPDefinable {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : Prop

A decision problem is FO(≤, PFP) definable if, on nonempty finite ordered structures, it is the value of a simultaneous induction over the ordered expansion of its vocabulary, read partially – for every linear order, the problem itself never seeing it. This is the setting of the capture theorem FO(≤, PFP) = PSPACE (DescriptiveComplexity.FixedPointPartialSpace).

Equations

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

theorem DescriptiveComplexity.pfpDefinableFree_congr {L : FirstOrder.Language} [L.IsRelational] {P Q : DecisionProblem L} (h : ∀ (A : Type) [inst : L.Structure A] [Finite A], P.Holds A ↔ Q.Holds A) : PFPDefinableFree P ↔ PFPDefinableFree Q

Order-free FO(PFP) definability only depends on the finite instances of a problem.

theorem DescriptiveComplexity.pfpDefinable_congr {L : FirstOrder.Language} [L.IsRelational] {P Q : DecisionProblem L} (h : ∀ (A : Type) [inst : L.Structure A] [Finite A], P.Holds A ↔ Q.Holds A) : PFPDefinable P ↔ PFPDefinable Q

FO(≤, PFP) definability only depends on the finite instances of a problem.

Closure under reductions

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

Order-free FO(PFP) definability is closed under first-order reductions: the partial stages commute with the pullback of the block (DescriptiveComplexity.StepDef.partStage_pull), being a fixed point is insensitive to the pullback (DescriptiveComplexity.StepDef.isFixedPt_next_pull_iff), and the output sentence pulls back through the extended interpretation.

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

FO(≤, PFP) definability is closed under ordered first-order reductions, by the same route as for IFP (DescriptiveComplexity.IFPDefinable.of_orderedReduction), stage by stage.

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

FO(≤, PFP) definability is closed under plain first-order reductions, which are in particular ordered ones.

FO(IFP) is contained in FO(PFP)

noncomputable def DescriptiveComplexity.StepDef.inflate {L : FirstOrder.Language} (d : StepDef L) : StepDef L

The inflationary reading of a simultaneous induction, as a partial one: disjoin each variable's own atom onto its step formula, so that one partial step of the result is one inflationary step of the original.

Equations

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

theorem DescriptiveComplexity.StepDef.next_inflate {L : FirstOrder.Language} (d : StepDef L) {A : Type} [L.Structure A] (ρ : d.B.Assignment A) : d.inflate.next ρ = d.inflStep ρ

One partial step of the inflated induction is one inflationary step of the original.

theorem DescriptiveComplexity.StepDef.partStage_inflate {L : FirstOrder.Language} (d : StepDef L) (A : Type) [L.Structure A] (n : ℕ) : d.inflate.partStage A n = d.inflStage A n

The partial stages of the inflated induction are the inflationary stages of the original.

theorem DescriptiveComplexity.StepDef.pfpHolds_inflate {L : FirstOrder.Language} (d : StepDef L) (A : Type) [L.Structure A] [Finite A] : d.inflate.PFPHolds A ↔ d.IFPHolds A

On a finite structure the inflated induction converges to the inflationary limit, so its partial value is the inflationary value.

theorem DescriptiveComplexity.IFPDefinableFree.pfpDefinableFree {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : IFPDefinableFree P) : PFPDefinableFree P

Order-free FO(IFP) is contained in order-free FO(PFP): inflate the induction. The easy inclusion of the Abiteboul–Vianu theorem.

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

FO(≤, IFP) is contained in FO(≤, PFP): inflate the induction.