Reachability, and the Horn fragment at work

The problem REACH – is some marked target reachable from some marked source in a directed graph? – and its complement UNREACH, over the vocabulary FirstOrder.Language.stGraph of graphs with marked sources and targets.

The point of this file is UNREACH: it is the worked instance of the SO-Horn fragment of DescriptiveComplexity.SecondOrderHorn. Its Horn program guesses a binary relation T and forces it, by two rules, to contain the transitive closure of the edge relation, then rules out with a goal clause the case of a marked target lying in T (or being itself a marked source):

             edge(x, y) → T(x, y)
  T(x, y) ∧  edge(y, z) → T(x, z)
  T(x, y) ∧ source(x) ∧ target(y) → ⊥
            source(x) ∧ target(x) → ⊥

Such a program is satisfiable exactly when its least model – here the transitive closure – already satisfies the goal clauses, which is why the existential second-order quantifier in front of a Horn kernel expresses a polynomial-time property rather than a nondeterministic guess. That is the content of DescriptiveComplexity.unreach_sigmaSOHornDefinable, and with the Horn discharge it gives DescriptiveComplexity.unreach_le_hornSat: UNREACH first-order reduces to HORN-SAT.

Note that it is the complement that the fragment defines: goal clauses can only rule models out. This is the usual state of affairs for SO-Horn, and harmless, both problems being in polynomial time.

The same file also places UNREACH one level lower, in DescriptiveComplexity.NL: the Krom fragment defines it by a two-literal program guessing the set U of vertices from which a marked target is reachable,

              target(x) → U(x)
  edge(x, y)            → ¬U(y) ∨ U(x)
              source(x) → ¬U(x)

and the same asymmetry appears one level down, for the same reason. A clausal fragment states closure and rejection, so it defines UNREACH head-on (DescriptiveComplexity.unreach_mem_NL) while REACH would need the guessed set to be contained in the true reachable set – a minimality condition no clause can impose. At the Horn level the way out was the equivalence with FO(LFP), a full logic closed under negation; at the Krom level the corresponding statement is NL = coNL, i.e. Immerman–Szelepcsényi, and it is what carries DescriptiveComplexity.unreach_mem_NL over to REACH ∈ NL (DescriptiveComplexity.reach_mem_NL, in DescriptiveComplexity.ImmermanSzelepcsenyi).

inductive FirstOrder.Language.stGraphRel : ℕ → Type

Relation symbols of the vocabulary of graphs with marked sources and targets.

• edge : stGraphRel 2

  edge a b: there is an edge from a to b.

• source : stGraphRel 1

  source a: the vertex a is a marked source.

• target : stGraphRel 1

  target a: the vertex a is a marked target.

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqStGraphRel {a✝ : ℕ} : DecidableEq (stGraphRel a✝)

Equations

• FirstOrder.Language.instDecidableEqStGraphRel = FirstOrder.Language.instDecidableEqStGraphRel.decEq

def FirstOrder.Language.instDecidableEqStGraphRel.decEq {a✝ : ℕ} (x✝ x✝¹ : stGraphRel a✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.instDecidableEqStGraphRel.decEq FirstOrder.Language.stGraphRel.edge FirstOrder.Language.stGraphRel.edge = isTrue FirstOrder.Language.instDecidableEqStGraphRel.decEq._proof_1

def FirstOrder.Language.stGraph : Language

The relational vocabulary of directed graphs with marked sources and targets.

Equations

• FirstOrder.Language.stGraph = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.stGraphRel }

instance FirstOrder.Language.instIsRelationalStGraph : Language.stGraph.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.sgEdge : Language.stGraph.Relations 2

The edge symbol.

Equations

• FirstOrder.Language.sgEdge = FirstOrder.Language.stGraphRel.edge

@[reducible, inline]

abbrev FirstOrder.Language.sgSource : Language.stGraph.Relations 1

The marked-source symbol.

Equations

• FirstOrder.Language.sgSource = FirstOrder.Language.stGraphRel.source

@[reducible, inline]

abbrev FirstOrder.Language.sgTarget : Language.stGraph.Relations 1

The marked-target symbol.

Equations

• FirstOrder.Language.sgTarget = FirstOrder.Language.stGraphRel.target

@[reducible, inline]

abbrev FirstOrder.Language.sgEdgeO : (Language.stGraph.sum Language.order).Relations 2

The edge symbol in the ordered expansion.

Equations

• FirstOrder.Language.sgEdgeO = Sum.inl FirstOrder.Language.sgEdge

@[reducible, inline]

abbrev FirstOrder.Language.sgSourceO : (Language.stGraph.sum Language.order).Relations 1

The marked-source symbol in the ordered expansion.

Equations

• FirstOrder.Language.sgSourceO = Sum.inl FirstOrder.Language.sgSource

@[reducible, inline]

abbrev FirstOrder.Language.sgTargetO : (Language.stGraph.sum Language.order).Relations 1

The marked-target symbol in the ordered expansion.

Equations

• FirstOrder.Language.sgTargetO = Sum.inl FirstOrder.Language.sgTarget

The problem

def DescriptiveComplexity.SGEdge {A : Type} [FirstOrder.Language.stGraph.Structure A] (a b : A) : Prop

The edge relation of a marked graph.

Equations

• DescriptiveComplexity.SGEdge a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.sgEdge ![a, b]

def DescriptiveComplexity.SGSource {A : Type} [FirstOrder.Language.stGraph.Structure A] (a : A) : Prop

Being a marked source.

Equations

• DescriptiveComplexity.SGSource a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.sgSource ![a]

def DescriptiveComplexity.SGTarget {A : Type} [FirstOrder.Language.stGraph.Structure A] (a : A) : Prop

Being a marked target.

Equations

• DescriptiveComplexity.SGTarget a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.sgTarget ![a]

def DescriptiveComplexity.Reachable (A : Type) [FirstOrder.Language.stGraph.Structure A] : Prop

Some marked target is reachable from some marked source, along a (possibly empty) directed path.

Equations

• DescriptiveComplexity.Reachable A = ∃ (s : A) (t : A), DescriptiveComplexity.SGSource s ∧ DescriptiveComplexity.SGTarget t ∧ Relation.ReflTransGen DescriptiveComplexity.SGEdge s t

theorem DescriptiveComplexity.reachable_iso {A B : Type} [FirstOrder.Language.stGraph.Structure A] [FirstOrder.Language.stGraph.Structure B] (e : FirstOrder.Language.stGraph.Equiv A B) : Reachable A ↔ Reachable B

Reachability is isomorphism-invariant.

def DescriptiveComplexity.REACH : DecisionProblem FirstOrder.Language.stGraph

REACH, as a problem on graphs with marked sources and targets.

Equations

• DescriptiveComplexity.REACH = { Holds := fun (A : Type) (inst : FirstOrder.Language.stGraph.Structure A) => DescriptiveComplexity.Reachable A, iso_invariant := ⋯ }

def DescriptiveComplexity.UNREACH : DecisionProblem FirstOrder.Language.stGraph

UNREACH, the complement of REACH: no marked target is reachable from a marked source.

Equations

• DescriptiveComplexity.UNREACH = DescriptiveComplexity.REACHᶜ

The Horn program

def DescriptiveComplexity.reachBlock : SOBlock

The block of the SO-Horn definition of UNREACH: one binary relation variable, forced to contain the transitive closure of the edge relation.

Equations

• DescriptiveComplexity.reachBlock = { ι := Unit, ιFinite := ⋯, arity := fun (x : Unit) => 2 }

def DescriptiveComplexity.tAtom (i j : Fin 3) : SOAtom reachBlock 3

The atom T (xᵢ, xⱼ) of the guessed relation.

Equations

• DescriptiveComplexity.tAtom i j = { idx := (), args := ![i, j] }

noncomputable def DescriptiveComplexity.edgeG (i j : Fin 3) : (FirstOrder.Language.stGraph.sum FirstOrder.Language.order).Formula (Fin 3)

The guard edge (xᵢ, xⱼ). Guards live over the ordered expansion of the vocabulary, as DescriptiveComplexity.SigmaSOHornDefinable requires; this program happens not to need the order.

Equations

• DescriptiveComplexity.edgeG i j = FirstOrder.Language.sgEdgeO.formula₂ (FirstOrder.Language.var i) (FirstOrder.Language.var j)

noncomputable def DescriptiveComplexity.sourceG (i : Fin 3) : (FirstOrder.Language.stGraph.sum FirstOrder.Language.order).Formula (Fin 3)

The guard source xᵢ.

Equations

• DescriptiveComplexity.sourceG i = FirstOrder.Language.sgSourceO.formula₁ (FirstOrder.Language.var i)

noncomputable def DescriptiveComplexity.targetG (i : Fin 3) : (FirstOrder.Language.stGraph.sum FirstOrder.Language.order).Formula (Fin 3)

The guard target xᵢ.

Equations

• DescriptiveComplexity.targetG i = FirstOrder.Language.sgTargetO.formula₁ (FirstOrder.Language.var i)

noncomputable def DescriptiveComplexity.reachC1 : HornClause (FirstOrder.Language.stGraph.sum FirstOrder.Language.order) reachBlock 3

Base rule: an edge is in T.

Equations

• DescriptiveComplexity.reachC1 = { guard := DescriptiveComplexity.edgeG 0 1, body := [], head := some (DescriptiveComplexity.tAtom 0 1) }

noncomputable def DescriptiveComplexity.reachC2 : HornClause (FirstOrder.Language.stGraph.sum FirstOrder.Language.order) reachBlock 3

Inductive rule: T is closed under appending an edge.

Equations

• DescriptiveComplexity.reachC2 = { guard := DescriptiveComplexity.edgeG 1 2, body := [DescriptiveComplexity.tAtom 0 1], head := some (DescriptiveComplexity.tAtom 0 2) }

noncomputable def DescriptiveComplexity.reachC3 : HornClause (FirstOrder.Language.stGraph.sum FirstOrder.Language.order) reachBlock 3

Goal clause: no marked target is in T from a marked source.

Equations

• DescriptiveComplexity.reachC3 = { guard := DescriptiveComplexity.sourceG 0 ⊓ DescriptiveComplexity.targetG 1, body := [DescriptiveComplexity.tAtom 0 1], head := none }

noncomputable def DescriptiveComplexity.reachC4 : HornClause (FirstOrder.Language.stGraph.sum FirstOrder.Language.order) reachBlock 3

Goal clause: no vertex is both a marked source and a marked target (the empty path).

Equations

• DescriptiveComplexity.reachC4 = { guard := DescriptiveComplexity.sourceG 0 ⊓ DescriptiveComplexity.targetG 0, body := [], head := none }

noncomputable def DescriptiveComplexity.reachProgram : HornProgram (FirstOrder.Language.stGraph.sum FirstOrder.Language.order) reachBlock 3

The Horn program defining UNREACH: two rules generating the transitive closure of the edge relation into T, and two goal clauses forbidding a marked target to be reached from a marked source.

Equations

• DescriptiveComplexity.reachProgram = [DescriptiveComplexity.reachC1, DescriptiveComplexity.reachC2, DescriptiveComplexity.reachC3, DescriptiveComplexity.reachC4]

Correctness of the program

def DescriptiveComplexity.TRel {A : Type} (ρ : reachBlock.Assignment A) (x y : A) : Prop

The relation guessed by an assignment of the block.

Equations

• DescriptiveComplexity.TRel ρ x y = ρ () ![x, y]

theorem DescriptiveComplexity.reachProgram_holds_iff {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] (ρ : reachBlock.Assignment A) : reachProgram.Holds ρ ↔ ((∀ (x y : A), SGEdge x y → TRel ρ x y) ∧ ∀ (x y z : A), TRel ρ x y → SGEdge y z → TRel ρ x z) ∧ (∀ (x y : A), TRel ρ x y → SGSource x → SGTarget y → False) ∧ ∀ (x : A), SGSource x → SGTarget x → False

What it means for an assignment to satisfy the program: the guessed relation contains the transitive closure of the edge relation, and meets no source-target pair.

def DescriptiveComplexity.transClosureAssign {A : Type} [FirstOrder.Language.stGraph.Structure A] : reachBlock.Assignment A

The transitive closure of the edge relation, as an assignment of the block: the least model of the two rules of the program.

Equations

• DescriptiveComplexity.transClosureAssign x✝ w = Relation.TransGen DescriptiveComplexity.SGEdge (w ⟨0, Nat.zero_lt_two⟩) (w ⟨1, Nat.one_lt_two⟩)

@[simp]

theorem DescriptiveComplexity.tRel_transClosureAssign {A : Type} [FirstOrder.Language.stGraph.Structure A] (x y : A) : TRel transClosureAssign x y ↔ Relation.TransGen SGEdge x y

theorem DescriptiveComplexity.transGen_tRel {A : Type} [FirstOrder.Language.stGraph.Structure A] {ρ : reachBlock.Assignment A} (h1 : ∀ (x y : A), SGEdge x y → TRel ρ x y) (h2 : ∀ (x y z : A), TRel ρ x y → SGEdge y z → TRel ρ x z) {a b : A} (h : Relation.TransGen SGEdge a b) : TRel ρ a b

Any model of the two rules of the program contains the transitive closure of the edge relation.

UNREACH is SO-Horn definable

theorem DescriptiveComplexity.unreach_sigmaSOHornDefinable : SigmaSOHornDefinable UNREACH

UNREACH is SO-Horn definable: the guessed relation is forced to contain the transitive closure of the edge relation, and the goal clauses forbid it to link a marked source to a marked target. The witness in the nontrivial direction is the transitive closure – the least model of the two rules.

theorem DescriptiveComplexity.unreach_mem_PTIME : PTIME.Mem UNREACH

UNREACH is in PTIME, by definition of the class as SO-Horn definability.

theorem DescriptiveComplexity.unreach_le_hornSat : Nonempty (OrderedFOReduction UNREACH HORNSAT)

UNREACH first-order reduces to HORN-SAT, by the Horn discharge.

theorem DescriptiveComplexity.unreach_lfpDefinable : LFPDefinable UNREACH

UNREACH is FO(LFP) definable, being SO-Horn definable.

theorem DescriptiveComplexity.reach_lfpDefinable : LFPDefinable REACH

REACH is FO(LFP) definable – and this is a statement the Horn fragment cannot make head-on. Reachability is the complement of the SO-Horn definable UNREACH, and complementing is free in the logic (DescriptiveComplexity.LFPDefinable.compl), while a goal clause can only reject.

theorem DescriptiveComplexity.reach_mem_PTIME : PTIME.Mem REACH

REACH is in PTIME after all: what the fragment cannot say head-on it can say through the equivalence with FO(LFP) (DescriptiveComplexity.SigmaSOHornDefinable.compl).

UNREACH is SO-Krom definable, hence in NL

The Krom fragment needs no transitive closure: it guesses the set of vertices from which a marked target is reachable, closes it under predecessors – a two-literal implication – and forbids a marked source to belong to it.

def DescriptiveComplexity.uBlock : SOBlock

The block of the SO-Krom definition of UNREACH: one unary relation variable, the set of vertices from which a marked target is reachable.

Equations

• DescriptiveComplexity.uBlock = { ι := Unit, ιFinite := ⋯, arity := fun (x : Unit) => 1 }

def DescriptiveComplexity.uAtom (i : Fin 3) : SOAtom uBlock 3

The atom U xᵢ of the guessed set.

Equations

• DescriptiveComplexity.uAtom i = { idx := (), args := ![i] }

def DescriptiveComplexity.uLit (i : Fin 3) (pos : Bool) : KromLit uBlock 3

The literal U xᵢ, positive or negated.

Equations

• DescriptiveComplexity.uLit i pos = { atom := DescriptiveComplexity.uAtom i, positive := pos }

noncomputable def DescriptiveComplexity.unreachK1 : KromClause (FirstOrder.Language.stGraph.sum FirstOrder.Language.order) uBlock 3

A marked target belongs to U.

Equations

• DescriptiveComplexity.unreachK1 = { guard := DescriptiveComplexity.targetG 0, lit₁ := some (DescriptiveComplexity.uLit 0 true), lit₂ := none }

noncomputable def DescriptiveComplexity.unreachK2 : KromClause (FirstOrder.Language.stGraph.sum FirstOrder.Language.order) uBlock 3

U is closed under predecessors: an edge into U starts in U.

Equations

• DescriptiveComplexity.unreachK2 = { guard := DescriptiveComplexity.edgeG 0 1, lit₁ := some (DescriptiveComplexity.uLit 1 false), lit₂ := some (DescriptiveComplexity.uLit 0 true) }

noncomputable def DescriptiveComplexity.unreachK3 : KromClause (FirstOrder.Language.stGraph.sum FirstOrder.Language.order) uBlock 3

No marked source belongs to U.

Equations

• DescriptiveComplexity.unreachK3 = { guard := DescriptiveComplexity.sourceG 0, lit₁ := some (DescriptiveComplexity.uLit 0 false), lit₂ := none }

noncomputable def DescriptiveComplexity.unreachKromProgram : KromProgram (FirstOrder.Language.stGraph.sum FirstOrder.Language.order) uBlock 3

The Krom program defining UNREACH.

Equations

• DescriptiveComplexity.unreachKromProgram = [DescriptiveComplexity.unreachK1, DescriptiveComplexity.unreachK2, DescriptiveComplexity.unreachK3]

def DescriptiveComplexity.URel {A : Type} (ρ : uBlock.Assignment A) (x : A) : Prop

The set guessed by an assignment of the block.

Equations

• DescriptiveComplexity.URel ρ x = ρ () ![x]

theorem DescriptiveComplexity.unreachKromProgram_holds_iff {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] (ρ : uBlock.Assignment A) : unreachKromProgram.Holds ρ ↔ (∀ (x : A), SGTarget x → URel ρ x) ∧ (∀ (x y : A), SGEdge x y → URel ρ y → URel ρ x) ∧ ∀ (x : A), SGSource x → ¬URel ρ x

What it means for an assignment to satisfy the Krom program: the guessed set contains the marked targets, is closed under predecessors, and avoids the marked sources.

def DescriptiveComplexity.coReachAssign {A : Type} [FirstOrder.Language.stGraph.Structure A] : uBlock.Assignment A

The set of vertices from which a marked target is reachable: the witness of the nontrivial direction.

Equations

• DescriptiveComplexity.coReachAssign x✝ w = ∃ (t : A), DescriptiveComplexity.SGTarget t ∧ Relation.ReflTransGen DescriptiveComplexity.SGEdge (w ⟨0, Nat.zero_lt_one⟩) t

@[simp]

theorem DescriptiveComplexity.uRel_coReachAssign {A : Type} [FirstOrder.Language.stGraph.Structure A] (x : A) : URel coReachAssign x ↔ ∃ (t : A), SGTarget t ∧ Relation.ReflTransGen SGEdge x t

theorem DescriptiveComplexity.uRel_of_reflTransGen {A : Type} [FirstOrder.Language.stGraph.Structure A] {ρ : uBlock.Assignment A} (h2 : ∀ (x y : A), SGEdge x y → URel ρ y → URel ρ x) {x y : A} (h : Relation.ReflTransGen SGEdge x y) : URel ρ y → URel ρ x

A set closed under predecessors and containing the marked targets contains every vertex from which a marked target is reachable.

theorem DescriptiveComplexity.unreach_sigmaSOKromDefinable : SigmaSOKromDefinable UNREACH

UNREACH is SO-Krom definable: guess the set of vertices from which a marked target is reachable. The clauses are two-literal – the closure rule is ¬U(y) ∨ U(x) – so no transitive closure has to be built, unlike in the Horn program above.

theorem DescriptiveComplexity.unreach_mem_NL : NL.Mem UNREACH

UNREACH is in NL, by definition of the class as SO-Krom definability.

REACH is FO(TC) definable

The canonical example of DescriptiveComplexity.TCDefinable, and the one the logic is shaped after: REACH is a transitive closure, at arity one, of the edge relation between the marked sources and the marked targets. Note the contrast with the two clausal fragments above, which define the complement head-on: here it is reachability itself that is stated, which is why closing FO(TC) under complement (Immerman–Szelepcsényi) is what REACH ∈ NL waits on.

noncomputable def DescriptiveComplexity.tcEdgeF : (FirstOrder.Language.stGraph.sum FirstOrder.Language.order).Formula (Fin 1 ⊕ Fin 1)

The transition formula of the walk: an edge from the current vertex to the next one.

Equations

• DescriptiveComplexity.tcEdgeF = FirstOrder.Language.sgEdgeO.formula₂ (FirstOrder.Language.var (Sum.inl 0)) (FirstOrder.Language.var (Sum.inr 0))

noncomputable def DescriptiveComplexity.tcSourceF : (FirstOrder.Language.stGraph.sum FirstOrder.Language.order).Formula (Fin 1)

The starting tuples of the walk: the marked sources.

Equations

• DescriptiveComplexity.tcSourceF = FirstOrder.Language.sgSourceO.formula₁ (FirstOrder.Language.var 0)

noncomputable def DescriptiveComplexity.tcTargetF : (FirstOrder.Language.stGraph.sum FirstOrder.Language.order).Formula (Fin 1)

The accepting tuples of the walk: the marked targets.

Equations

• DescriptiveComplexity.tcTargetF = FirstOrder.Language.sgTargetO.formula₁ (FirstOrder.Language.var 0)

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.reachSpec : TCSpec FirstOrder.Language.stGraph

REACH as a single transitive closure: a walk along edges, from a marked source to a marked target.

Equations

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

@[simp]

theorem DescriptiveComplexity.step_reachSpec {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] (a b : reachSpec.Node A) : reachSpec.Step a b ↔ SGEdge (a.2 0) (b.2 0)

@[simp]

theorem DescriptiveComplexity.realize_tcSourceF {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] (v : Fin 1 → A) : tcSourceF.Realize v ↔ SGSource (v 0)

@[simp]

theorem DescriptiveComplexity.realize_tcTargetF {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] (v : Fin 1 → A) : tcTargetF.Realize v ↔ SGTarget (v 0)

theorem DescriptiveComplexity.reach_of_reflTransGen {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] {x y : A} (h : Relation.ReflTransGen SGEdge x y) : reachSpec.Reach ((), fun (x_1 : Fin reachSpec.k) => x) ((), fun (x : Fin reachSpec.k) => y)

A path in the graph is a walk of the specification.

theorem DescriptiveComplexity.reflTransGen_of_reach {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] {u v : reachSpec.Node A} (h : reachSpec.Reach u v) : Relation.ReflTransGen SGEdge (u.2 0) (v.2 0)

A walk of the specification is a path in the graph.

theorem DescriptiveComplexity.reach_tcDefinable : TCDefinable REACH

REACH is FO(TC) definable: it is a single transitive closure of the edge relation, at arity one.