SUCCINCT-REACH as a Savitch recursion

The first half of the reduction of SUCCINCT-REACH to QSAT: rewriting the yes-instances of DescriptiveComplexity.SUCCINCTREACH – a reachability statement with an unbounded number of steps – as the bounded, recursively doubled statement DescriptiveComplexity.SavPow of DescriptiveComplexity.Savitch, whose unfolding has depth equal to the number of state variables. That is the form a quantifier prefix can express.

The vertices of the walk are not the states themselves – a state is a predicate on the whole universe – but their restrictions to the state variables (DescriptiveComplexity.stCls), since that is all the clause groups can read. There are 2 ^ m such restrictions for m state variables (DescriptiveComplexity.card_stateClass), so m levels of doubling suffice: DescriptiveComplexity.succinctReachable_iff_savPow.

@[reducible, inline]

abbrev DescriptiveComplexity.StateVar (A : Type) [FirstOrder.Language.transSys.Structure A] : Type

The state variables of an instance, as a type: the coordinates of a state that the clause groups can read.

Equations

• DescriptiveComplexity.StateVar A = { x : A // FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsStateVar ![x] }

def DescriptiveComplexity.stCls {A : Type} [FirstOrder.Language.transSys.Structure A] (S : A → Prop) : StateVar A → Prop

The class of a state: its restriction to the state variables. Two states with the same class are interchangeable everywhere in the semantics.

Equations

• DescriptiveComplexity.stCls S x = S ↑x

theorem DescriptiveComplexity.stCls_eq_iff {A : Type} [FirstOrder.Language.transSys.Structure A] {S S' : A → Prop} : stCls S = stCls S' ↔ ∀ (x : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsStateVar ![x] → (S x ↔ S' x)

noncomputable def DescriptiveComplexity.stateDepth (A : Type) [FirstOrder.Language.transSys.Structure A] : ℕ

The number of state variables: the depth of the Savitch recursion the reduction writes as a quantifier prefix.

Equations

• DescriptiveComplexity.stateDepth A = Nat.card (DescriptiveComplexity.StateVar A)

The semantics only sees a state through its class

theorem DescriptiveComplexity.readsCur_congr {A : Type} [FirstOrder.Language.transSys.Structure A] {ν S S' : A → Prop} (h : stCls S = stCls S') (hr : ReadsCur A ν S) : ReadsCur A ν S'

theorem DescriptiveComplexity.writesNext_congr {A : Type} [FirstOrder.Language.transSys.Structure A] {ν S S' : A → Prop} (h : stCls S = stCls S') (hw : WritesNext A ν S) : WritesNext A ν S'

theorem DescriptiveComplexity.isStart_congr {A : Type} [FirstOrder.Language.transSys.Structure A] {S S' : A → Prop} (h : stCls S = stCls S') (hs : IsStart A S) : IsStart A S'

theorem DescriptiveComplexity.isGoal_congr {A : Type} [FirstOrder.Language.transSys.Structure A] {S S' : A → Prop} (h : stCls S = stCls S') (hs : IsGoal A S) : IsGoal A S'

theorem DescriptiveComplexity.savInv_stepRel {A : Type} [FirstOrder.Language.transSys.Structure A] : SavInv stCls (StepRel A)

The transition relation lives on the classes: it only depends on its two endpoints through their restrictions to the state variables.

theorem DescriptiveComplexity.card_stateClass {A : Type} [FirstOrder.Language.transSys.Structure A] [Finite A] : Nat.card (StateVar A → Prop) = 2 ^ stateDepth A

There are 2 ^ m classes of states for m state variables.

theorem DescriptiveComplexity.succinctReachable_iff_savPow {A : Type} [FirstOrder.Language.transSys.Structure A] [Finite A] : SuccinctReachable A ↔ ∃ (S : A → Prop) (T : A → Prop), IsStart A S ∧ IsGoal A T ∧ SavPow stCls (StepRel A) (stateDepth A) S T

SUCCINCT-REACH as a bounded, recursively doubled reachability statement. The walk saturates after 2 ^ m moves, m the number of state variables, and DescriptiveComplexity.SavPow at depth m is exactly that bound.