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.

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

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_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'

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)

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.