FO(DTC): first-order logic with deterministic transitive closure

The logic that captures deterministic logarithmic space on ordered structures (Immerman 1987): first-order logic with a transitive-closure operator that may only follow a step when it is the only step available. DescriptiveComplexity.LOGSPACE is defined by it, exactly as DescriptiveComplexity.NL is defined by the Krom fragment and DescriptiveComplexity.PTIME by the Horn one.

Determinism as a formula, not as a side condition

There are two ways to say "the walk is deterministic". One is to carry a proof: a specification together with the hypothesis that its Step relation is functional on every structure. That is the wrong choice here – the hypothesis is not first-order data, and it would have to be re-established after every pullback, at which point closure under reductions stops being a syntactic argument.

The other is Immerman's own: keep an arbitrary DescriptiveComplexity.TCSpec and read its transition formula through its determinization

detStep(x̄, ȳ)  :=  step(x̄, ȳ)  ∧  ∀ z̄. step(x̄, z̄) → z̄ = ȳ

which is again first-order. Every specification then denotes a legitimate deterministic walk (DescriptiveComplexity.TCSpec.det_functional), nothing has to be preserved, and nothing is lost: on a specification whose steps are already functional the determinization is equivalent to it (DescriptiveComplexity.TCSpec.det_step_of_functional).

The one wrinkle the textbook formula does not show is modes. A node of a DescriptiveComplexity.TCSpec is a mode together with a tuple (DescriptiveComplexity.TCSpec.Node), so "the only step available" has to quantify over successor nodes, not successor tuples: the uniqueness clause is a finite conjunction over the modes, in which the mode comparison is resolved at formula-construction time (⊥ for a mode other than the intended target, so that a step into it refutes the guard). This is the same static/dynamic split as the tag comparisons of DescriptiveComplexity.lexLeF.

What is here

DescriptiveComplexity.TCSpec.det and its semantics (DescriptiveComplexity.TCSpec.det_step_iff: a determinized step is a step with no competitor), the resulting definability notion DescriptiveComplexity.DTCDefinable, and the inclusion at the level of definability, DescriptiveComplexity.DTCDefinable.tcDefinable – the future L ⊆ NL, a one-liner because a determinized specification is a specification.

Determinizing the transition formula

def DescriptiveComplexity.TCSpec.detVar {L : FirstOrder.Language} (spec : TCSpec L) : Fin spec.k ⊕ Fin spec.k → (Fin spec.k ⊕ Fin spec.k) ⊕ Fin spec.k

The renaming used by the uniqueness clause: the transition formula is re-read with its first tuple still the current one and its second tuple the freshly quantified z̄.

Equations

• spec.detVar = Sum.elim (fun (i : Fin spec.k) => Sum.inl (Sum.inl i)) Sum.inr

noncomputable def DescriptiveComplexity.TCSpec.detStep {L : FirstOrder.Language} (spec : TCSpec L) (m n : spec.Mode) : (L.sum FirstOrder.Language.order).Formula (Fin spec.k ⊕ Fin spec.k)

The determinized transition formula at a pair of modes: this step, and no other step out of the current node. The competing successors are quantified as a tuple z̄ and a mode m'; the mode is compared statically, so the uniqueness clause has one conjunct per mode, asserting z̄ = ȳ at the intended one and refuting the step at every other.

Equations

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

@[reducible]

noncomputable def DescriptiveComplexity.TCSpec.det {L : FirstOrder.Language} (spec : TCSpec L) : TCSpec L

The deterministic reading of a specification: the same modes, arity and endpoints, with the transition formula replaced by its determinization.

Marked @[reducible] so that the modes and the arity of spec.det are those of spec transparently: a node of the deterministic reading is a node, and numerals at Fin spec.det.k elaborate as they do at Fin spec.k.

Equations

• spec.det = { Mode := spec.Mode, modeFinite := ⋯, k := spec.k, step := spec.detStep, src := spec.src, tgt := spec.tgt }

@[simp]

theorem DescriptiveComplexity.TCSpec.det_mode {L : FirstOrder.Language} (spec : TCSpec L) : spec.det.Mode = spec.Mode

@[simp]

theorem DescriptiveComplexity.TCSpec.det_k {L : FirstOrder.Language} (spec : TCSpec L) : spec.det.k = spec.k

Semantics of the determinization

theorem DescriptiveComplexity.TCSpec.realize_detStep {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (m n : spec.Mode) (x y : Fin spec.k → A) : (spec.detStep m n).Realize (Sum.elim x y) ↔ (spec.step m n).Realize (Sum.elim x y) ∧ ∀ (m' : spec.Mode) (z : Fin spec.k → A), (spec.step m m').Realize (Sum.elim x z) → m' = n ∧ z = y

theorem DescriptiveComplexity.TCSpec.det_step_iff {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (a b : spec.Node A) : spec.det.Step a b ↔ spec.Step a b ∧ ∀ (c : spec.Node A), spec.Step a c → c = b

A determinized step is a step with no competitor: the node b is reached from a in the deterministic walk exactly when it is reached in the original one and is the only node so reached.

@[simp]

theorem DescriptiveComplexity.TCSpec.det_isSrc {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (a : spec.Node A) : spec.det.IsSrc a ↔ spec.IsSrc a

The source nodes of the deterministic reading are those of the original.

@[simp]

theorem DescriptiveComplexity.TCSpec.det_isTgt {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (a : spec.Node A) : spec.det.IsTgt a ↔ spec.IsTgt a

The accepting nodes of the deterministic reading are those of the original.

Functional specifications

def DescriptiveComplexity.TCSpec.Functional {L : FirstOrder.Language} (spec : TCSpec L) (A : Type) [L.Structure A] [LinearOrder A] : Prop

A specification is functional on a structure when every node has at most one successor: the walk it describes is deterministic on the nose.

Equations

• spec.Functional A = ∀ (a b c : spec.Node A), spec.Step a b → spec.Step a c → b = c

theorem DescriptiveComplexity.TCSpec.det_functional {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] : spec.det.Functional A

The deterministic reading is functional, whatever the specification it comes from: this is what makes determinization the right packaging, there being nothing left to assume.

theorem DescriptiveComplexity.TCSpec.det_step_of_functional {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] (h : spec.Functional A) (a b : spec.Node A) : spec.det.Step a b ↔ spec.Step a b

Determinizing a functional specification changes nothing: no step had a competitor to begin with.

FO(DTC) definability

def DescriptiveComplexity.DTCDefinable {L : FirstOrder.Language} (P : DecisionProblem L) : Prop

A decision problem is FO(DTC) definable if, on nonempty finite ordered structures, it is defined by a single deterministic transitive closure: there is a DescriptiveComplexity.TCSpec whose accepting nodes are reachable from its starting nodes along its determinization exactly on the yes-instances.

As for DescriptiveComplexity.TCDefinable, the equivalence is required for every linear order on the universe, so this is order-invariant FO(DTC) definability: the problem itself does not see the order, while the transition and endpoint formulas may.

Equations

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

theorem DescriptiveComplexity.dtcDefinable_congr {L : FirstOrder.Language} {P Q : DecisionProblem L} (h : ∀ (A : Type) [inst : L.Structure A] [Finite A], P.Holds A ↔ Q.Holds A) : DTCDefinable P ↔ DTCDefinable Q

FO(DTC) definability only depends on the finite instances of a problem.

theorem DescriptiveComplexity.DTCDefinable.tcDefinable {L : FirstOrder.Language} {P : DecisionProblem L} (h : DTCDefinable P) : TCDefinable P

FO(DTC) ⊆ FO(TC), the definability-level L ⊆ NL: a determinized specification is a specification like any other.