Deciding reachability in a deterministic walk: a step budget

The atom case of the normal form for FO(DTC): the reachability relation of a walk read through its determinization (DescriptiveComplexity.ParamTCSpec.det) has a functional DescriptiveComplexity.Decider (DescriptiveComplexity.ParamTCSpec.detReachDecider). No inductive counting is involved: the decider follows the one run of the walk from the first endpoint, exits yes on standing at the second, and exits no when the run is stuck – either because the walk has no step to take, or because a step budget is exhausted.

The budget is the walk's own set of nodes: a second node, carried beside the current one and advanced by one at every step in the mode-major lexicographic order of nodes (DescriptiveComplexity.ParamTCSpec.cntSuccF), so that the run may take exactly as many steps as there are nodes. A node reachable along a functional relation is reached in fewer steps than that (DescriptiveComplexity.exists_iterate_lt_card), so a run that has not arrived when the budget runs out never will. This is the argument of DescriptiveComplexity.LOGSPACE_eq_coLOGSPACE, with parameters.

theorem DescriptiveComplexity.covBy_right_unique {α : Type} [LinearOrder α] {a b c : α} (hb : a ⋖ b) (hc : a ⋖ c) : b = c

In a linear order, an element covers at most one element.

The counter

@[instance_reducible]

noncomputable def DescriptiveComplexity.ParamTCSpec.modeOrder {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) : LinearOrder W.Mode

An arbitrary linear order on the modes, for the counter.

Equations

• W.modeOrder = DescriptiveComplexity.finiteLinearOrder W.Mode

@[reducible, inline]

abbrev DescriptiveComplexity.ParamTCSpec.Counter {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) (A : Type) : Type

The counter's values: the nodes of the walk, mode-major then lexicographically on tuples.

Equations

• W.Counter A = Lex (W.Mode × Lex (Fin W.k → A))

@[reducible, inline]

abbrev DescriptiveComplexity.ParamTCSpec.cntOf {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [LinearOrder A] (c : W.Mode) (r : Fin W.k → A) : W.Counter A

The counter holding a mode and a tuple.

Equations

• W.cntOf c r = toLex (c, toLex r)

@[reducible, inline]

abbrev DescriptiveComplexity.ParamTCSpec.DCoord {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) : Type

The coordinates of the decider: the current tuple, then the counter's.

Equations

• W.DCoord = (Fin W.k ⊕ Fin W.k)

The formulas

def DescriptiveComplexity.ParamTCSpec.runVar {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) : (Fin W.k ⊕ Fin W.k) ⊕ Fin W.par → (W.DCoord ⊕ W.DCoord) ⊕ W.AtomPar

The variables of the determinized step, in the decider's step.

Equations

• W.runVar (Sum.inl (Sum.inl i)) = Sum.inl (Sum.inl (Sum.inl i))
• W.runVar (Sum.inl (Sum.inr i)) = Sum.inl (Sum.inr (Sum.inl i))
• W.runVar (Sum.inr j) = Sum.inr (W.parIx j)

noncomputable def DescriptiveComplexity.ParamTCSpec.atTgtF {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) (mb m : W.Mode) : (L.sum FirstOrder.Language.order).Formula (W.DCoord ⊕ W.AtomPar)

“The current tuple is the second endpoint, and the mode is its mode.”

Equations

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

noncomputable def DescriptiveComplexity.ParamTCSpec.cntSuccF {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) (c c' : W.Mode) : (L.sum FirstOrder.Language.order).Formula ((W.DCoord ⊕ W.DCoord) ⊕ W.AtomPar)

The counter advances by one: same mode and the successor tuple, or the next mode with the tuple going from the maximum to the minimum.

Equations

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

noncomputable def DescriptiveComplexity.ParamTCSpec.runStepF {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) (mb m c m' c' : W.Mode) : (L.sum FirstOrder.Language.order).Formula ((W.DCoord ⊕ W.DCoord) ⊕ W.AtomPar)

The run step: the determinized step of the walk, off the target, the counter advancing.

Equations

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

def DescriptiveComplexity.ParamTCSpec.exVar {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) : (W.DCoord ⊕ W.DCoord) ⊕ W.AtomPar → (W.DCoord ⊕ W.AtomPar) ⊕ W.DCoord

The variables of a step, with the next tuple quantified.

Equations

• W.exVar (Sum.inl (Sum.inl c)) = Sum.inl (Sum.inl c)
• W.exVar (Sum.inl (Sum.inr c)) = Sum.inr c
• W.exVar (Sum.inr g) = Sum.inl (Sum.inr g)

noncomputable def DescriptiveComplexity.ParamTCSpec.hasStepF {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) (mb m c : W.Mode) : (L.sum FirstOrder.Language.order).Formula (W.DCoord ⊕ W.AtomPar)

“Some run step is available.”

Equations

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

@[reducible]

noncomputable def DescriptiveComplexity.ParamTCSpec.detReachDecider {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) (ma mb : W.Mode) : Decider L W.AtomPar

The decider of reachability in the deterministic reading between two modes, at the two endpoints and the parameters: it enters the walk at the first endpoint with the counter at its least value, follows the one run, exits yes on standing at the second endpoint and no when no run step is available.

Equations

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

Semantics of the formulas

theorem DescriptiveComplexity.ParamTCSpec.realize_atTgtF {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (mb : W.Mode) (w : W.AtomPar → A) (m : W.Mode) (t : W.DCoord → A) : (W.atTgtF mb m).Realize (Sum.elim t w) ↔ m = mb ∧ t ∘ Sum.inl = w ∘ W.rightIx

theorem DescriptiveComplexity.ParamTCSpec.realize_cntSuccF {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (w : W.AtomPar → A) [Nonempty A] (c c' : W.Mode) (t t' : W.DCoord → A) : (W.cntSuccF c c').Realize (Sum.elim (Sum.elim t t') w) ↔ W.cntOf c (t ∘ Sum.inr) ⋖ W.cntOf c' (t' ∘ Sum.inr)

theorem DescriptiveComplexity.ParamTCSpec.realize_runStepF {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (mb : W.Mode) (w : W.AtomPar → A) [Nonempty A] (m c m' c' : W.Mode) (t t' : W.DCoord → A) : (W.runStepF mb m c m' c').Realize (Sum.elim (Sum.elim t t') w) ↔ W.det.StepAt (w ∘ W.parIx) (m, t ∘ Sum.inl) (m', t' ∘ Sum.inl) ∧ ¬(m = mb ∧ t ∘ Sum.inl = w ∘ W.rightIx) ∧ W.cntOf c (t ∘ Sum.inr) ⋖ W.cntOf c' (t' ∘ Sum.inr)

Steps and exits of the decider

theorem DescriptiveComplexity.ParamTCSpec.detReachDecider_stepAt_none_some {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (ma mb : W.Mode) (w : W.AtomPar → A) (m c : W.Mode) (t t' : W.DCoord → A) : (W.detReachDecider ma mb).StepAt w (none, t) (some (m, c), t') ↔ m = ma ∧ (∀ (c' : W.Mode), c ≤ c') ∧ t' ∘ Sum.inl = w ∘ W.leftIx ∧ ∀ (i : Fin W.k) (a : A), t' (Sum.inr i) ≤ a

theorem DescriptiveComplexity.ParamTCSpec.detReachDecider_stepAt_some_some {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (ma mb : W.Mode) (w : W.AtomPar → A) [Nonempty A] (m c m' c' : W.Mode) (t t' : W.DCoord → A) : (W.detReachDecider ma mb).StepAt w (some (m, c), t) (some (m', c'), t') ↔ W.det.StepAt (w ∘ W.parIx) (m, t ∘ Sum.inl) (m', t' ∘ Sum.inl) ∧ ¬(m = mb ∧ t ∘ Sum.inl = w ∘ W.rightIx) ∧ W.cntOf c (t ∘ Sum.inr) ⋖ W.cntOf c' (t' ∘ Sum.inr)

theorem DescriptiveComplexity.ParamTCSpec.detReachDecider_not_stepAt_none {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (ma mb : W.Mode) (w : W.AtomPar → A) (a : (W.detReachDecider ma mb).Node A) (t' : W.DCoord → A) : ¬(W.detReachDecider ma mb).StepAt w a (none, t')

theorem DescriptiveComplexity.ParamTCSpec.detReachDecider_exitAt_some_true {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (ma mb : W.Mode) (w : W.AtomPar → A) (m c : W.Mode) (t : W.DCoord → A) : (W.detReachDecider ma mb).ExitAt w (some (m, c), t) true ↔ m = mb ∧ t ∘ Sum.inl = w ∘ W.rightIx

theorem DescriptiveComplexity.ParamTCSpec.detReachDecider_exitAt_some_false {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (ma mb : W.Mode) (w : W.AtomPar → A) (m c : W.Mode) (t : W.DCoord → A) : (W.detReachDecider ma mb).ExitAt w (some (m, c), t) false ↔ ¬(m = mb ∧ t ∘ Sum.inl = w ∘ W.rightIx) ∧ ¬∃ (b : (W.detReachDecider ma mb).Node A), (W.detReachDecider ma mb).StepAt w (some (m, c), t) b

theorem DescriptiveComplexity.ParamTCSpec.detReachDecider_not_exitAt_none {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (ma mb : W.Mode) (w : W.AtomPar → A) (t : W.DCoord → A) (o : Bool) : ¬(W.detReachDecider ma mb).ExitAt w (none, t) o

The run

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.ParamTCSpec.detNext {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (w : W.AtomPar → A) : W.Node A → W.Node A

The one step of the determinized walk, as a function.

Equations

• W.detNext w = DescriptiveComplexity.stepNext (W.det.StepAt (w ∘ W.parIx))

theorem DescriptiveComplexity.ParamTCSpec.detNext_functional {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (w : W.AtomPar → A) (u v v' : W.Node A) (hv : W.det.StepAt (w ∘ W.parIx) u v) (hv' : W.det.StepAt (w ∘ W.parIx) u v') : v = v'

def DescriptiveComplexity.ParamTCSpec.DetInv {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (ma mb : W.Mode) (w : W.AtomPar → A) (i : ℕ) (m c : W.Mode) (t : W.DCoord → A) : Prop

What a node of the decider records: the current node is the i-th of the run from the first endpoint, the counter has rank i, and no earlier node of the run was the second endpoint.

Equations

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

theorem DescriptiveComplexity.ParamTCSpec.det_reachAt_iff {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (ma mb : W.Mode) (w : W.AtomPar → A) : W.det.ReachAt (w ∘ W.parIx) (ma, w ∘ W.leftIx) (mb, w ∘ W.rightIx) ↔ ∃ (n : ℕ), (W.detNext w)^[n] (ma, w ∘ W.leftIx) = (mb, w ∘ W.rightIx)

Reachability in the determinized walk is iteration of its step.

theorem DescriptiveComplexity.ParamTCSpec.card_counter {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} : Nat.card (W.Counter A) = Nat.card (W.Node A)

theorem DescriptiveComplexity.ParamTCSpec.not_reach_of_stuck {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (ma mb : W.Mode) (w : W.AtomPar → A) [Nonempty A] [Finite A] {i : ℕ} {m c : W.Mode} {t : W.DCoord → A} (hinv : W.DetInv ma mb w i m c t) (htgt : ¬(m = mb ∧ t ∘ Sum.inl = w ∘ W.rightIx)) (hstuck : ¬∃ (b : (W.detReachDecider ma mb).Node A), (W.detReachDecider ma mb).StepAt w (some (m, c), t) b) : ¬W.det.ReachAt (w ∘ W.parIx) (ma, w ∘ W.leftIx) (mb, w ∘ W.rightIx)

A stuck run does not reach the target.

theorem DescriptiveComplexity.ParamTCSpec.detReachDecider_run {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (ma mb : W.Mode) (w : W.AtomPar → A) [Nonempty A] [Finite A] (κ : W.Counter A) (m c : W.Mode) (t : W.DCoord → A) (i : ℕ) : W.cntOf c (t ∘ Sum.inr) = κ → W.DetInv ma mb w i m c t → (W.det.ReachAt (w ∘ W.parIx) (ma, w ∘ W.leftIx) (mb, w ∘ W.rightIx) → ∃ (b : (W.detReachDecider ma mb).Node A), (W.detReachDecider ma mb).ReachAt w (some (m, c), t) b ∧ (W.detReachDecider ma mb).ExitAt w b true) ∧ (¬W.det.ReachAt (w ∘ W.parIx) (ma, w ∘ W.leftIx) (mb, w ∘ W.rightIx) → ∃ (b : (W.detReachDecider ma mb).Node A), (W.detReachDecider ma mb).ReachAt w (some (m, c), t) b ∧ (W.detReachDecider ma mb).ExitAt w b false)

The run decides, from any node the invariant admits: it exits yes if the target is reachable, no if not. Proved downwards along the counter.

theorem DescriptiveComplexity.ParamTCSpec.detReachDecider_inv {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (ma mb : W.Mode) (w : W.AtomPar → A) [Nonempty A] [Finite A] (t : W.DCoord → A) {b : (W.detReachDecider ma mb).Node A} (h : (W.detReachDecider ma mb).ReachAt w (none, t) b) : b = (none, t) ∨ ∃ (m : W.Mode) (c : W.Mode) (t' : W.DCoord → A) (i : ℕ), b = (some (m, c), t') ∧ W.DetInv ma mb w i m c t'

What the decider may have reached from its start: its start, or a node the invariant admits.

theorem DescriptiveComplexity.ParamTCSpec.decides_detReachDecider {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (ma mb : W.Mode) (w : W.AtomPar → A) [Nonempty A] [Finite A] : (W.detReachDecider ma mb).Decides w (W.det.ReachAt (w ∘ W.parIx) (ma, w ∘ W.leftIx) (mb, w ∘ W.rightIx))

The decider decides reachability in the deterministic reading between its two modes, at the two endpoints and the parameters.

theorem DescriptiveComplexity.ParamTCSpec.functional_detReachDecider {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (ma mb : W.Mode) [Nonempty A] : (W.detReachDecider ma mb).Functional A

The decider is functional.

The deciders of a family, read deterministically

noncomputable def DescriptiveComplexity.TCFamily.detReachDeciders {L : FirstOrder.Language} (F : TCFamily (L.sum FirstOrder.Language.order)) (q : F.block.ι) : Decider L (Fin (F.block.arity q))

The deterministic reachability deciders of a family: one per relation variable of its block, deciding the reachability relations of the family's deterministic reading.

Equations

• F.detReachDeciders q = (F.spec q.fst).detReachDecider q.snd.1 q.snd.2

theorem DescriptiveComplexity.TCFamily.decides_detReachDeciders {L : FirstOrder.Language} (F : TCFamily (L.sum FirstOrder.Language.order)) (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (q : F.block.ι) (w : Fin (F.block.arity q) → A) : (F.detReachDeciders q).Decides w (F.det.reachAssign A q w)

The deciders decide the deterministic reading's reachability relations.

theorem DescriptiveComplexity.TCFamily.functional_detReachDeciders {L : FirstOrder.Language} (F : TCFamily (L.sum FirstOrder.Language.order)) (A : Type) [L.Structure A] [LinearOrder A] [Nonempty A] (q : F.block.ι) : (F.detReachDeciders q).Functional A

The deciders are functional.