Steiner Tree: definitions

STEINER TREE (Karp 1972) in its node-weighted form with unit weights: given a graph, a set of terminals and a threshold k, is there a connected set of vertices containing every terminal and using at most k non-terminals? The vocabulary FirstOrder.Language.steinerGraph is that of graphs with two unary marks – the terminals, and the marked set carrying k in the unary representation of DescriptiveComplexity.Numbers.Unary.

Karp's original problem weights edges and bounds the total weight; on a tree the two readings differ by one (#edges = #vertices - 1), so the reduction below would carry over, but the bridge between them needs the fact that a connected graph has at least n - 1 edges. Mathlib has it only for trees on a whole vertex type (SimpleGraph.IsTree.card_edgeFinset), so the edge-weighted version waits for that glue; the node-weighted version is the standard variant and is what this file formalizes.

Connectivity, and its first-order certificate

Connectivity (DescriptiveComplexity.ConnectedOn) is stated with Relation.ReflTransGen over the symmetric restriction of adjacency to the chosen set, so it is the usual undirected notion and is not first-order. As for acyclicity in DescriptiveComplexity.Problems.Feedback, what saves the membership proof is a certificate: a root of the chosen set together with a strict partial order in which every other chosen vertex has a chosen neighbour strictly below it (DescriptiveComplexity.connectedOn_iff_exists_root_order). Walking down that order reaches the root, and the root joins any two vertices.

Producing the certificate from connectivity is the direction with content: it needs a distance, which Relation.ReflTransGen does not carry. The DescriptiveComplexity.reachIn staging below supplies it – reachability in at most n steps, with Nat.find picking the least such n – and that is the whole of the extra machinery. It is stated for an arbitrary relation, so the Hamilton problems and the edge-weighted Steiner tree can reuse it.

inductive FirstOrder.Language.steinerRel : ℕ → Type

Relation symbols of the language of graphs with terminals.

• adj : steinerRel 2

  adj a b: there is an edge between a and b.

• terminal : steinerRel 1

  terminal a: the vertex a must be spanned.

• marked : steinerRel 1

  marked a: the vertex a belongs to the marked set carrying the threshold.

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqSteinerRel {a✝ : ℕ} : DecidableEq (steinerRel a✝)

Equations

• FirstOrder.Language.instDecidableEqSteinerRel = FirstOrder.Language.instDecidableEqSteinerRel.decEq

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

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.instDecidableEqSteinerRel.decEq FirstOrder.Language.steinerRel.adj FirstOrder.Language.steinerRel.adj = isTrue FirstOrder.Language.instDecidableEqSteinerRel.decEq._proof_1

def FirstOrder.Language.steinerGraph : Language

The relational language of graphs with terminals: adjacency, a set of terminals to be spanned, and a marked set whose cardinality is the budget of non-terminals.

Equations

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

instance FirstOrder.Language.instIsRelationalSteinerGraph : Language.steinerGraph.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.stAdj : Language.steinerGraph.Relations 2

The adjacency symbol of terminal-marked graphs.

Equations

• FirstOrder.Language.stAdj = FirstOrder.Language.steinerRel.adj

@[reducible, inline]

abbrev FirstOrder.Language.stTerminal : Language.steinerGraph.Relations 1

The terminal symbol of terminal-marked graphs.

Equations

• FirstOrder.Language.stTerminal = FirstOrder.Language.steinerRel.terminal

@[reducible, inline]

abbrev FirstOrder.Language.stMarked : Language.steinerGraph.Relations 1

The mark symbol of terminal-marked graphs.

Equations

• FirstOrder.Language.stMarked = FirstOrder.Language.steinerRel.marked

Connectivity and its certificate

def DescriptiveComplexity.Link {A : Type} (Adjp : A → A → Prop) (S : A → Prop) (a b : A) : Prop

The edges available inside a chosen set: adjacency in either direction, restricted to the set.

Equations

• DescriptiveComplexity.Link Adjp S a b = (S a ∧ S b ∧ (Adjp a b ∨ Adjp b a))

theorem DescriptiveComplexity.link_symm {A : Type} {Adjp : A → A → Prop} {S : A → Prop} {a b : A} (h : Link Adjp S a b) : Link Adjp S b a

def DescriptiveComplexity.ConnectedOn {A : Type} (Adjp : A → A → Prop) (S : A → Prop) : Prop

A set of vertices is connected if any two of its members are joined by a path inside it.

Equations

• DescriptiveComplexity.ConnectedOn Adjp S = ∀ (x y : A), S x → S y → Relation.ReflTransGen (DescriptiveComplexity.Link Adjp S) x y

Reachability in a bounded number of steps

Relation.ReflTransGen carries no length, and the certificate needs one: the order it guesses is “distance to the root”.

def DescriptiveComplexity.reachIn {A : Type} (R : A → A → Prop) : ℕ → A → A → Prop

Reachability in at most n steps.

Equations

• DescriptiveComplexity.reachIn R 0 x✝¹ x✝ = (x✝¹ = x✝)
• DescriptiveComplexity.reachIn R n.succ x✝¹ x✝ = (DescriptiveComplexity.reachIn R n x✝¹ x✝ ∨ ∃ (z : A), DescriptiveComplexity.reachIn R n x✝¹ z ∧ R z x✝)

theorem DescriptiveComplexity.reflTransGen_iff_exists_reachIn {A : Type} (R : A → A → Prop) (x y : A) : Relation.ReflTransGen R x y ↔ ∃ (n : ℕ), reachIn R n x y

Reachability is reachability in some bounded number of steps.

theorem DescriptiveComplexity.reflTransGen_symm {A : Type} {R : A → A → Prop} (hsymm : ∀ (a b : A), R a b → R b a) {x y : A} (h : Relation.ReflTransGen R x y) : Relation.ReflTransGen R y x

The reflexive-transitive closure of a symmetric relation is symmetric.

The certificate

theorem DescriptiveComplexity.connectedOn_iff_exists_root_order {A : Type} [Finite A] (Adjp : A → A → Prop) (S : A → Prop) : ConnectedOn Adjp S ↔ ∀ (r : A), S r → ∃ (Lt : A → A → Prop), (∀ (x y z : A), Lt x y → Lt y z → Lt x z) ∧ (∀ (x : A), ¬Lt x x) ∧ ∀ (x : A), S x → x ≠ r → ∃ (y : A), Link Adjp S x y ∧ Lt y x

Connectivity is first-order certifiable: a set is connected exactly when, from any of its members chosen as root, some strict partial order makes every other member have a neighbour strictly below it. Walking down the order reaches the root, and the root joins any two members.

theorem DescriptiveComplexity.connectedOn_iff_exists_root {A : Type} [Finite A] (Adjp : A → A → Prop) (S : A → Prop) : ConnectedOn Adjp S ↔ ∃ (Rt : A → Prop), (∀ (x : A), Rt x → S x) ∧ (∀ (x y : A), Rt x → Rt y → x = y) ∧ ∃ (Lt : A → A → Prop), (∀ (x y z : A), Lt x y → Lt y z → Lt x z) ∧ (∀ (x : A), ¬Lt x x) ∧ ∀ (x : A), S x → ¬Rt x → ∃ (y : A), Link Adjp S x y ∧ Lt y x

The existential form of the certificate, the one a Σ₁ definition guesses: a root relation (constrained to hold of at most one element of the set) together with the order. The empty set is connected and has no root, which is why the root is guessed as a relation rather than an element.

theorem DescriptiveComplexity.ConnectedOn.of_equiv {A B : Type} (u : B ≃ A) {AdjB : B → B → Prop} {SB : B → Prop} {AdjA : A → A → Prop} {SA : A → Prop} (hadj : ∀ (b b' : B), AdjB b b' ↔ AdjA (u b) (u b')) (hS : ∀ (b : B), SB b ↔ SA (u b)) (h : ConnectedOn AdjB SB) : ConnectedOn AdjA SA

ConnectedOn transports along an equivalence commuting with the adjacency relations and the chosen sets.

Connectivity costs edges

The certificate gives each non-root member of a connected set a parent edge, and that assignment is injective: two members sharing an edge would have to be each other's parent, hence strictly below each other. This is the n - 1 edge bound for connected graphs, in the form the edge-weighted Steiner tree needs, and it is proved from the certificate rather than from a spanning tree.

theorem DescriptiveComplexity.ncard_le_ncard_of_connected {A : Type} [Finite A] {T : A → A → Prop} {S : A → Prop} {r : A} (hr : S r) (hconn : ConnectedOn T S) : {x : A | S x ∧ x ≠ r}.ncard ≤ {p : A × A | T p.1 p.2}.ncard

A connected set costs edges: a set connected through T has at most one more element than T has pairs.

The problem

def DescriptiveComplexity.SteinerOn {A : Type} (Adjp : A → A → Prop) (Term Kp : A → Prop) : Prop

Some connected set contains every terminal and uses at most as many non-terminals as the number encoded by the marked set.

Equations

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

theorem DescriptiveComplexity.steinerOn_iff_certificate {A : Type} [Finite A] (Adjp : A → A → Prop) (Term Kp : A → Prop) : SteinerOn Adjp Term Kp ↔ ∃ (S : A → Prop), (∀ (x : A), Term x → S x) ∧ (∃ (Rt : A → Prop), (∀ (x : A), Rt x → S x) ∧ (∀ (x y : A), Rt x → Rt y → x = y) ∧ ∃ (Lt : A → A → Prop), (∀ (x y z : A), Lt x y → Lt y z → Lt x z) ∧ (∀ (x : A), ¬Lt x x) ∧ ∀ (x : A), S x → ¬Rt x → ∃ (y : A), Link Adjp S x y ∧ Lt y x) ∧ Nonempty ({ x : A // S x ∧ ¬Term x } ↪ { x : A // Kp x })

The certified form, with connectivity witnessed by a root and an order and the threshold by an injection: the shape the second-order definition guesses.

def DescriptiveComplexity.SteinerEdgeOn {A : Type} (Adjp : A → A → Prop) (Term Kp : A → Prop) : Prop

Some set of edges of the graph, connecting a set that contains every terminal, is at most as large as the number encoded by the marked set: the edge-weighted Steiner tree with unit weights, Karp's original reading.

The chosen edges are given as a set of ordered pairs, one per edge, and connectivity reads them symmetrically (DescriptiveComplexity.ConnectedOn); a witness listing both orientations of an edge merely pays for it twice, so the yes-instances are unaffected. The threshold compares a count of pairs with a count of elements, which is meaningful because a threshold is just a number – and necessary here, since an edge set can be quadratically larger than the universe.

Equations

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

theorem DescriptiveComplexity.steinerEdgeOn_iff_certificate {A : Type} [Finite A] (Adjp : A → A → Prop) (Term Kp : A → Prop) : SteinerEdgeOn Adjp Term Kp ↔ ∃ (T : A → A → Prop) (S : A → Prop), (∀ (a b : A), T a b → Adjp a b) ∧ (∀ (x : A), Term x → S x) ∧ (∃ (Rt : A → Prop), (∀ (x : A), Rt x → S x) ∧ (∀ (x y : A), Rt x → Rt y → x = y) ∧ ∃ (Lt : A → A → Prop), (∀ (x y z : A), Lt x y → Lt y z → Lt x z) ∧ (∀ (x : A), ¬Lt x x) ∧ ∀ (x : A), S x → ¬Rt x → ∃ (y : A), Link T S x y ∧ Lt y x) ∧ Nonempty ({ p : A × A // T p.1 p.2 } ↪ { x : A // Kp x })

The certified form of the edge-weighted problem.

theorem DescriptiveComplexity.SteinerOn.of_equiv {A B : Type} (u : B ≃ A) {AdjB : B → B → Prop} {TermB KB : B → Prop} {AdjA : A → A → Prop} {TermA KA : A → Prop} (hadj : ∀ (b b' : B), AdjB b b' ↔ AdjA (u b) (u b')) (hterm : ∀ (b : B), TermB b ↔ TermA (u b)) (hK : ∀ (b : B), KB b ↔ KA (u b)) (h : SteinerOn AdjB TermB KB) : SteinerOn AdjA TermA KA

SteinerOn transports along an equivalence commuting with the three predicates.

theorem DescriptiveComplexity.SteinerOn.equiv_iff {A B : Type} (u : B ≃ A) {AdjB : B → B → Prop} {TermB KB : B → Prop} {AdjA : A → A → Prop} {TermA KA : A → Prop} (hadj : ∀ (b b' : B), AdjB b b' ↔ AdjA (u b) (u b')) (hterm : ∀ (b : B), TermB b ↔ TermA (u b)) (hK : ∀ (b : B), KB b ↔ KA (u b)) : SteinerOn AdjB TermB KB ↔ SteinerOn AdjA TermA KA

SteinerOn transports along an equivalence, iff version.

theorem DescriptiveComplexity.SteinerEdgeOn.of_equiv {B A : Type} (u : B ≃ A) {AdjB : B → B → Prop} {TermB KB : B → Prop} {AdjA : A → A → Prop} {TermA KA : A → Prop} (hadj : ∀ (b b' : B), AdjB b b' ↔ AdjA (u b) (u b')) (hterm : ∀ (b : B), TermB b ↔ TermA (u b)) (hK : ∀ (b : B), KB b ↔ KA (u b)) (h : SteinerEdgeOn AdjB TermB KB) : SteinerEdgeOn AdjA TermA KA

SteinerEdgeOn transports along an equivalence commuting with the three predicates.

theorem DescriptiveComplexity.SteinerEdgeOn.equiv_iff {B A : Type} (u : B ≃ A) {AdjB : B → B → Prop} {TermB KB : B → Prop} {AdjA : A → A → Prop} {TermA KA : A → Prop} (hadj : ∀ (b b' : B), AdjB b b' ↔ AdjA (u b) (u b')) (hterm : ∀ (b : B), TermB b ↔ TermA (u b)) (hK : ∀ (b : B), KB b ↔ KA (u b)) : SteinerEdgeOn AdjB TermB KB ↔ SteinerEdgeOn AdjA TermA KA

SteinerEdgeOn transports along an equivalence, iff version.

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

Adjacency in a graph with terminals.

Equations

• DescriptiveComplexity.STAdj a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.stAdj ![a, b]

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

Being a terminal.

Equations

• DescriptiveComplexity.STTerminal a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.stTerminal ![a]

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

Belonging to the marked set carrying the threshold.

Equations

• DescriptiveComplexity.STMarked a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.stMarked ![a]

def DescriptiveComplexity.HasSmallSteinerTree (A : Type) [FirstOrder.Language.steinerGraph.Structure A] : Prop

A graph with terminals admits a connected set spanning the terminals and using at most as many non-terminals as its marked set has elements. (Finiteness of the universe is part of the property: cardinality thresholds are only meaningful on finite structures.)

Equations

• DescriptiveComplexity.HasSmallSteinerTree A = (Finite A ∧ DescriptiveComplexity.SteinerOn DescriptiveComplexity.STAdj DescriptiveComplexity.STTerminal DescriptiveComplexity.STMarked)

theorem DescriptiveComplexity.hasSmallSteinerTree_iso {A B : Type} [FirstOrder.Language.steinerGraph.Structure A] [FirstOrder.Language.steinerGraph.Structure B] (e : FirstOrder.Language.steinerGraph.Equiv A B) : HasSmallSteinerTree A ↔ HasSmallSteinerTree B

The Steiner-tree property is isomorphism-invariant.

def DescriptiveComplexity.HasSmallEdgeSteinerTree (A : Type) [FirstOrder.Language.steinerGraph.Structure A] : Prop

A graph with terminals admits a set of edges connecting its terminals, of size at most the number encoded by the marked set.

Equations

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

theorem DescriptiveComplexity.hasSmallEdgeSteinerTree_iso {A B : Type} [FirstOrder.Language.steinerGraph.Structure A] [FirstOrder.Language.steinerGraph.Structure B] (e : FirstOrder.Language.steinerGraph.Equiv A B) : HasSmallEdgeSteinerTree A ↔ HasSmallEdgeSteinerTree B

The edge-weighted Steiner-tree property is isomorphism-invariant.

def DescriptiveComplexity.EdgeSteinerTree : DecisionProblem FirstOrder.Language.steinerGraph

STEINER TREE (edge-weighted, unit weights) – Karp's original reading – as a problem on graphs with terminals: is there a set of at most k edges connecting all the terminals?

Equations

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

def DescriptiveComplexity.SteinerTree : DecisionProblem FirstOrder.Language.steinerGraph

STEINER TREE (node-weighted, unit weights), as a problem on graphs with terminals: is there a connected set of vertices containing every terminal and using at most as many non-terminals as the marked set has elements?

Equations

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