PSPACE is closed under FO(LFP) reductions #
DescriptiveComplexity.mem_PSPACE_of_lfpReduction: a problem reducing to a
polynomial-space problem by a polynomial-time reduction is in polynomial space.
With it, every class of this library from PTIME to PSPACE – and every level of
the polynomial hierarchy in between – is closed under ≤ˡᶠᵖ, hence under
≤ᵗᶜ and ≤ᵈᵗᶜ.
The route, and why it is the fixed-point one #
DescriptiveComplexity.PSPACE is defined by SO(TC), so the natural attempt is
to absorb the reduction's induction into the walk: give the walk's state a
copy of the induction's variables, iterate the induction in it, freeze, then
run the original walk. That works, and it is the same construction as the one
carried out here – but on the fixed-point side of the capture theorem it costs
one construction instead of two, because the pullback half is already built:
DescriptiveComplexity.StepDef.pullRel pulls a simultaneous iteration through
a relativized interpretation, where SO(TC) would need that written afresh.
So the proof goes: FO(≤, PFP) is PSPACE (DescriptiveComplexity.PSPACE through
DescriptiveComplexity.pfpDefinable_iff_mem_PSPACE); the membership witness of
Q is pulled back through the reduction's interpretation
(DescriptiveComplexity.StepDef.pfpHolds_pullRel); and the reduction's own
induction is absorbed by
DescriptiveComplexity.StepDef.pfpHolds_stratifyPFP – an inflationary stratum
gating a partial one, which is the walk-with-a-preliminary-phase written as an
iteration.
That last step is where the earlier pessimism about FO(PFP) was wrong: what a
partial iteration cannot do is gate itself, and it does not have to – the
gate is an arity-0 variable of the state, set by the inflationary stratum,
and the partial stratum is merely conjoined with it.
PSPACE is closed under FO(LFP) reductions.