SUCCINCT-REACH is in PSPACE

The membership half: reachability in a propositionally described transition system is SO(TC) definable, hence in DescriptiveComplexity.PSPACE.

This is the cheapest membership proof in the library, and the reason is structural: SUCCINCT-REACH is the syntactic image of SO(TC), so the specification is a transcription rather than a construction. The walk carries four monadic relation variables:

• X, the state being walked – the only component that matters;
• V, the valuation witnessing the transition that entered the current state (a transition needs an existential over all variables, auxiliary ones included, and a walk has no existential of its own, so the witness is stored in the state it leads to);
• W₁ and W₂, the valuations witnessing the source and the target conditions. Two are needed rather than one because a walk of length zero must satisfy both conditions at the same state, with possibly different witnesses.

V, W₁ and W₂ are unconstrained wherever they are not used, so the walk on the four variables projects onto the walk on states, which is what DescriptiveComplexity.succinctReachable_iff_accepts says.

Building the sentences

The three sentences share three generic shapes, stated over an arbitrary vocabulary so that the same builder and the same realization lemma serve the current copy of the block and the next one:

• DescriptiveComplexity.clausesHoldS – “every clause of this group contains a true literal”, the kernel of DescriptiveComplexity.satKernel with its symbols abstracted;
• DescriptiveComplexity.agreeOnS – “on every marked element these two unary relations agree”;
• DescriptiveComplexity.writesS – “on the next-state copy of every marked element, this unary relation holds the value the other gives to the element itself”.

Three generic sentence shapes

noncomputable def DescriptiveComplexity.clausesHoldS {L : FirstOrder.Language} (grp : L.Relations 1) (pos neg : L.Relations 2) (nu : L.Relations 1) : L.Sentence

“Every clause of the group grp contains a literal that nu makes true.”

Equations

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

noncomputable def DescriptiveComplexity.agreeOnS {L : FirstOrder.Language} (mark nu st : L.Relations 1) : L.Sentence

“On every element marked by mark, the unary relations nu and st agree.”

Equations

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

noncomputable def DescriptiveComplexity.writesS {L : FirstOrder.Language} (mark : L.Relations 1) (nxt : L.Relations 2) (nu st : L.Relations 1) : L.Sentence

“Whenever y is the nxt-successor of an element x marked by mark, nu holds of y exactly when st holds of x.”

Equations

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

theorem DescriptiveComplexity.realize_clausesHoldS {L : FirstOrder.Language} {M : Type} [L.Structure M] (grp : L.Relations 1) (pos neg : L.Relations 2) (nu : L.Relations 1) : M ⊨ clausesHoldS grp pos neg nu ↔ ∀ (c : M), FirstOrder.Language.Structure.RelMap grp ![c] → ∃ (x : M), FirstOrder.Language.Structure.RelMap pos ![c, x] ∧ FirstOrder.Language.Structure.RelMap nu ![x] ∨ FirstOrder.Language.Structure.RelMap neg ![c, x] ∧ ¬FirstOrder.Language.Structure.RelMap nu ![x]

theorem DescriptiveComplexity.realize_agreeOnS {L : FirstOrder.Language} {M : Type} [L.Structure M] (mark nu st : L.Relations 1) : M ⊨ agreeOnS mark nu st ↔ ∀ (x : M), FirstOrder.Language.Structure.RelMap mark ![x] → (FirstOrder.Language.Structure.RelMap nu ![x] ↔ FirstOrder.Language.Structure.RelMap st ![x])

theorem DescriptiveComplexity.realize_writesS {L : FirstOrder.Language} {M : Type} [L.Structure M] (mark : L.Relations 1) (nxt : L.Relations 2) (nu st : L.Relations 1) : M ⊨ writesS mark nxt nu st ↔ ∀ (x y : M), FirstOrder.Language.Structure.RelMap mark ![x] → FirstOrder.Language.Structure.RelMap nxt ![x, y] → (FirstOrder.Language.Structure.RelMap nu ![y] ↔ FirstOrder.Language.Structure.RelMap st ![x])

The block and the vocabularies

def DescriptiveComplexity.srBlock : SOBlock

The block of the SO(TC) specification of SUCCINCT-REACH: four unary relation variables – the state, the transition witness, and the two endpoint witnesses.

Equations

• DescriptiveComplexity.srBlock = { ι := Bool × Bool, ιFinite := ⋯, arity := fun (x : Bool × Bool) => 1 }

@[reducible, inline]

abbrev DescriptiveComplexity.srX : Bool × Bool

The relation variable holding the current state.

Equations

• DescriptiveComplexity.srX = (false, false)

@[reducible, inline]

abbrev DescriptiveComplexity.srV : Bool × Bool

The relation variable holding the valuation witnessing the transition that entered the current state.

Equations

• DescriptiveComplexity.srV = (false, true)

@[reducible, inline]

abbrev DescriptiveComplexity.srW₁ : Bool × Bool

The relation variable holding the valuation witnessing the source condition.

Equations

• DescriptiveComplexity.srW₁ = (true, false)

@[reducible, inline]

abbrev DescriptiveComplexity.srW₂ : Bool × Bool

The relation variable holding the valuation witnessing the target condition.

Equations

• DescriptiveComplexity.srW₂ = (true, true)

def DescriptiveComplexity.srSym (i : Bool × Bool) : srBlock.lang.Relations 1

The symbol of the relation variable i of the block.

Equations

• DescriptiveComplexity.srSym i = ⟨i, ⋯⟩

@[reducible, inline]

abbrev DescriptiveComplexity.srBase : FirstOrder.Language

The input vocabulary together with the order, over which the sentences of an SO(TC) specification live.

Equations

• DescriptiveComplexity.srBase = FirstOrder.Language.transSys.sum FirstOrder.Language.order

@[reducible, inline]

abbrev DescriptiveComplexity.srLang₁ : FirstOrder.Language

The vocabulary of the endpoint sentences: one copy of the block.

Equations

• DescriptiveComplexity.srLang₁ = DescriptiveComplexity.srBase.sum DescriptiveComplexity.srBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.srLang₂ : FirstOrder.Language

The vocabulary of the transition sentence: two copies of the block.

Equations

• DescriptiveComplexity.srLang₂ = DescriptiveComplexity.srLang₁.sum DescriptiveComplexity.srBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.srIn₁ {n : ℕ} (r : FirstOrder.Language.transSys.Relations n) : srLang₁.Relations n

An input symbol, in the endpoint vocabulary.

Equations

• DescriptiveComplexity.srIn₁ r = Sum.inl (Sum.inl r)

@[reducible, inline]

abbrev DescriptiveComplexity.srVar₁ (i : Bool × Bool) : srLang₁.Relations 1

A relation variable of the block, in the endpoint vocabulary.

Equations

• DescriptiveComplexity.srVar₁ i = Sum.inr (DescriptiveComplexity.srSym i)

@[reducible, inline]

abbrev DescriptiveComplexity.srIn₂ {n : ℕ} (r : FirstOrder.Language.transSys.Relations n) : srLang₂.Relations n

An input symbol, in the transition vocabulary.

Equations

• DescriptiveComplexity.srIn₂ r = Sum.inl (Sum.inl (Sum.inl r))

@[reducible, inline]

abbrev DescriptiveComplexity.srCur₂ (i : Bool × Bool) : srLang₂.Relations 1

A relation variable of the current copy of the block, in the transition vocabulary.

Equations

• DescriptiveComplexity.srCur₂ i = Sum.inl (Sum.inr (DescriptiveComplexity.srSym i))

@[reducible, inline]

abbrev DescriptiveComplexity.srNext₂ (i : Bool × Bool) : srLang₂.Relations 1

A relation variable of the next copy of the block, in the transition vocabulary.

Equations

• DescriptiveComplexity.srNext₂ i = Sum.inr (DescriptiveComplexity.srSym i)

noncomputable def DescriptiveComplexity.srSpec : SOTCSpec FirstOrder.Language.transSys

The SO(TC) specification of SUCCINCT-REACH. A transition holds when the next state's transition witness satisfies every transition clause, reads the current state on the state variables and writes the next state on their next-state copies; the endpoint conditions are the two clause groups checked against their own witnesses.

Equations

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

Reading the specification back

def DescriptiveComplexity.srPred {A : Type} (ρ : srBlock.Assignment A) (i : Bool × Bool) : A → Prop

The predicate held by the relation variable i in the assignment ρ.

Equations

• DescriptiveComplexity.srPred ρ i a = ρ i fun (x : Fin (DescriptiveComplexity.srBlock.arity i)) => a

def DescriptiveComplexity.srAssign {A : Type} (f : Bool × Bool → A → Prop) : srBlock.Assignment A

The assignment holding the given four predicates.

Equations

• DescriptiveComplexity.srAssign f i v = f i (v ⟨0, Nat.zero_lt_one⟩)

@[simp]

theorem DescriptiveComplexity.srPred_srAssign {A : Type} (f : Bool × Bool → A → Prop) (i : Bool × Bool) : srPred (srAssign f) i = f i

theorem DescriptiveComplexity.srRealize_inf₁ {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (ρ : srBlock.Assignment A) (φ ψ : srLang₁.Sentence) : A ⊨ φ ⊓ ψ ↔ A ⊨ φ ∧ A ⊨ ψ

Splitting a conjunction of endpoint sentences, with the block expansion supplied explicitly: instance search does not see through the specification's block field.

theorem DescriptiveComplexity.srRealize_inf₂ {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (ρ σ : srBlock.Assignment A) (φ ψ : srLang₂.Sentence) : A ⊨ φ ⊓ ψ ↔ A ⊨ φ ∧ A ⊨ ψ

The same splitting for the transition sentence.

theorem DescriptiveComplexity.relMap_srVar₁ {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (ρ : srBlock.Assignment A) (i : Bool × Bool) (w : Fin 1 → A) : FirstOrder.Language.Structure.RelMap (srVar₁ i) w ↔ srPred ρ i (w 0)

theorem DescriptiveComplexity.relMap_srIn₁ {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {n : ℕ} (ρ : srBlock.Assignment A) (r : FirstOrder.Language.transSys.Relations n) (w : Fin n → A) : FirstOrder.Language.Structure.RelMap (srIn₁ r) w ↔ FirstOrder.Language.Structure.RelMap r w

theorem DescriptiveComplexity.relMap_srCur₂ {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (ρ σ : srBlock.Assignment A) (i : Bool × Bool) (w : Fin 1 → A) : FirstOrder.Language.Structure.RelMap (srCur₂ i) w ↔ srPred ρ i (w 0)

theorem DescriptiveComplexity.relMap_srNext₂ {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (ρ σ : srBlock.Assignment A) (i : Bool × Bool) (w : Fin 1 → A) : FirstOrder.Language.Structure.RelMap (srNext₂ i) w ↔ srPred σ i (w 0)

theorem DescriptiveComplexity.relMap_srIn₂ {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {n : ℕ} (ρ σ : srBlock.Assignment A) (r : FirstOrder.Language.transSys.Relations n) (w : Fin n → A) : FirstOrder.Language.Structure.RelMap (srIn₂ r) w ↔ FirstOrder.Language.Structure.RelMap r w

theorem DescriptiveComplexity.srSpec_isSrc_iff {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (ρ : srBlock.Assignment A) : srSpec.IsSrc ρ ↔ ClausesHold A (srPred ρ srW₁) FirstOrder.Language.tsSrcCl ∧ ReadsCur A (srPred ρ srW₁) (srPred ρ srX)

A starting state of the specification is a state whose W₁ component witnesses the source condition.

theorem DescriptiveComplexity.srSpec_isTgt_iff {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (ρ : srBlock.Assignment A) : srSpec.IsTgt ρ ↔ ClausesHold A (srPred ρ srW₂) FirstOrder.Language.tsTgtCl ∧ ReadsCur A (srPred ρ srW₂) (srPred ρ srX)

An accepting state of the specification is a state whose W₂ component witnesses the target condition.

theorem DescriptiveComplexity.srSpec_step_iff {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (ρ σ : srBlock.Assignment A) : srSpec.Step ρ σ ↔ ClausesHold A (srPred σ srV) FirstOrder.Language.tsStepCl ∧ ReadsCur A (srPred σ srV) (srPred ρ srX) ∧ WritesNext A (srPred σ srV) (srPred σ srX)

A transition of the specification is a transition of the system, witnessed by the V component of the state it enters.

Correctness of the specification

theorem DescriptiveComplexity.succinctReachable_iff_accepts {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] : SuccinctReachable A ↔ srSpec.Accepts A

The specification is correct: it accepts a transition system exactly when some target state is reachable from some source state.

theorem DescriptiveComplexity.succinctReach_sotcDefinable : SOTCDefinable SUCCINCTREACH

SUCCINCT-REACH is SO(TC) definable: the walk on states is the walk of the specification, its extra components carrying the existential witnesses a transitive closure cannot quantify on its own.

theorem DescriptiveComplexity.succinctReach_mem_PSPACE : PSPACE.Mem SUCCINCTREACH

SUCCINCT-REACH is in PSPACE.