FO(TC): first-order logic with transitive closure

The logic that captures nondeterministic logarithmic space on ordered structures (Immerman 1987): first-order logic extended with a transitive-closure operator. If φ(x̄, ȳ) defines a binary relation on k-tuples, then TC[x̄, ȳ. φ](ū, v̄) says that v̄ is reachable from ū in the φ-graph.

The operator as data

As everywhere in this library, the operator is not added to Mathlib's FirstOrder.Language.BoundedFormula as a new constructor – that would mean redoing relabelling, substitution and realization for an extended syntax, and losing every existing lemma. It is kept at the Lean level instead: a DescriptiveComplexity.TCSpec bundles the arity k, a first-order transition formula over the ordered expansion with two k-tuples of free variables, and the two endpoint formulas; reachability itself is Relation.ReflTransGen, whose induction principles then do the work in proofs. This is the same move as DescriptiveComplexity.HornProgram for SO-Horn and DescriptiveComplexity.KromProgram for SO-Krom.

A single application of TC in front of a first-order matrix is not a restriction on ordered structures: Immerman's normal form makes every FO(posTC) formula equivalent to one, just as a single existential block suffices for DescriptiveComplexity.SigmaSODefinable. The library takes that normal form as the definition (DescriptiveComplexity.TCDefinable), exactly as it takes Σ₁-definability as the definition of NP rather than proving Fagin's theorem against a machine.

What this is for

DescriptiveComplexity.NL is already defined, by the Krom fragment (DescriptiveComplexity.LogSpace), and the two coincide (DescriptiveComplexity.tcDefinable_iff_mem_NL), so FO(TC) is not set up as a second complexity class; the modes are what would make that possible, should it become useful. A walk whose state were only a tuple of elements could not be pulled back through an interpretation, whose tags vary from node to node, and could not carry the finite data a translation needs (the atom index and sign of a literal, say); carrying it in coordinates would fail on a one-element universe. FO(TC) is here as the logic in which two things are naturally stated:

• the translation to the Krom fragment, which goes through the complement – a clausal fragment states closure and rejection, so it defines non-reachability head-on, exactly as DescriptiveComplexity.unreach_mem_NL does for the concrete case;
• Immerman–Szelepcsényi, closure of FO(TC) under complement (DescriptiveComplexity.TCDefinable.compl in DescriptiveComplexity.TransitiveClosureCompl), whose inductive-counting proof is a walk on configurations – a phase, a flag and eight registers, each a node or a count – and so lives inside a single TC. That theorem turns the above translation into an equivalence and gives REACH ∈ NL.

The canonical example is DescriptiveComplexity.reach_tcDefinable – REACH is a TC, at arity one and with a single mode, over the edge relation between the marked sources and the marked targets.

Specifications

structure DescriptiveComplexity.TCSpec (L : FirstOrder.Language) : Type 1

A single-TC definition: the transition formula of a graph on k-tuples, together with formulas for the admissible start and end tuples. All three are first-order over the ordered expansion of the vocabulary, so that they may mention the linear order, as the ordered setting of the capture theorem allows.

• Mode : Type

  The modes: a finite amount of state the walk carries besides its tuple of elements. Tuples of elements cannot hold finite data of their own – a one-element universe has only one tuple – so, exactly as tags replace the order-encoded sorts of a textbook interpretation in DescriptiveComplexity.FOInterpretation, a mode carries what the tuple cannot.

• modeFinite : Finite self.Mode

  Modes are finite.

• k : ℕ

  The arity: the walk runs on k-tuples of elements.

• step : self.Mode → self.Mode → (L.sum FirstOrder.Language.order).Formula (Fin self.k ⊕ Fin self.k)

  The transition formula, one per pair of modes, with two k-tuples of free variables: the current tuple on the left, the next one on the right.

• src : self.Mode → (L.sum FirstOrder.Language.order).Formula (Fin self.k)

  The formula defining the admissible starting tuples, per mode.

• tgt : self.Mode → (L.sum FirstOrder.Language.order).Formula (Fin self.k)

  The formula defining the accepting tuples, per mode.

@[reducible, inline]

abbrev DescriptiveComplexity.TCSpec.Node {L : FirstOrder.Language} (spec : TCSpec L) (A : Type) : Type

A node of the walk: a mode together with a k-tuple of elements.

Equations

• spec.Node A = (spec.Mode × (Fin spec.k → A))

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

One step of the walk: the transition formula of the two modes, read with the current tuple on the left and the next one on the right.

Equations

• spec.Step a b = (spec.step a.1 b.1).Realize (Sum.elim a.2 b.2)

@[reducible, inline]

abbrev DescriptiveComplexity.TCSpec.Reach {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] : spec.Node A → spec.Node A → Prop

Reachability in the walk: the reflexive-transitive closure of DescriptiveComplexity.TCSpec.Step.

Equations

• spec.Reach = Relation.ReflTransGen spec.Step

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

A node is a starting node when its tuple satisfies the source formula of its mode.

Equations

• spec.IsSrc a = (spec.src a.1).Realize a.2

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

A node is accepting when its tuple satisfies the target formula of its mode.

Equations

• spec.IsTgt a = (spec.tgt a.1).Realize a.2

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

The structure is accepted: some accepting node is reachable from some starting node.

Equations

• spec.Accepts A = ∃ (u : spec.Node A) (v : spec.Node A), spec.IsSrc u ∧ spec.IsTgt v ∧ spec.Reach u v

Isomorphism-invariance

def DescriptiveComplexity.TCSpec.mapNode {L : FirstOrder.Language} (spec : TCSpec L) {A B : Type} [L.Structure A] [LinearOrder A] [L.Structure B] [LinearOrder B] (e : (L.sum FirstOrder.Language.order).Equiv A B) (a : spec.Node A) : spec.Node B

The image of a node under an isomorphism: same mode, transported tuple.

Equations

• spec.mapNode e a = (a.1, fun (i : Fin spec.k) => e (a.2 i))

theorem DescriptiveComplexity.TCSpec.step_equiv {L : FirstOrder.Language} (spec : TCSpec L) {A B : Type} [L.Structure A] [LinearOrder A] [L.Structure B] [LinearOrder B] (e : (L.sum FirstOrder.Language.order).Equiv A B) (a b : spec.Node A) : spec.Step (spec.mapNode e a) (spec.mapNode e b) ↔ spec.Step a b

One step is preserved by an isomorphism of the ordered expansions.

theorem DescriptiveComplexity.TCSpec.reach_equiv {L : FirstOrder.Language} (spec : TCSpec L) {A B : Type} [L.Structure A] [LinearOrder A] [L.Structure B] [LinearOrder B] (e : (L.sum FirstOrder.Language.order).Equiv A B) {a b : spec.Node A} (h : spec.Reach a b) : spec.Reach (spec.mapNode e a) (spec.mapNode e b)

Reachability is preserved by an isomorphism of the ordered expansions.

theorem DescriptiveComplexity.TCSpec.accepts_equiv {L : FirstOrder.Language} (spec : TCSpec L) {A B : Type} [L.Structure A] [LinearOrder A] [L.Structure B] [LinearOrder B] (e : (L.sum FirstOrder.Language.order).Equiv A B) : spec.Accepts A ↔ spec.Accepts B

Acceptance is isomorphism-invariant (for isomorphisms of the ordered expansions, the order being visible to the formulas).

FO(TC) definability

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

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

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

Equations

• DescriptiveComplexity.TCDefinable P = ∃ (spec : DescriptiveComplexity.TCSpec L), ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A], P.Holds A ↔ spec.Accepts A

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

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