Min-max duality for required paths in in-forests

An in-forest is a finite type with a partial successor map σ : α → Option α and no cycles (Acyclic). A directed path (FPath) is determined by its starting vertex and its number of vertices: its vertices are the successive partial iterates of σ (iter). Given requirements r : α → ℕ, a path is required (FPath.Required) when it is nonempty and its length is at least r v at its final vertex v.

We prove that inside any finite vertex set S : Finset α, there exist a vertex set H ⊆ S meeting every required path in S (Covers) and a family P of pairwise vertex-disjoint required paths in S (Packing) of the same cardinality (exists_cover_packing), while every packing has cardinality at most that of every cover (packing_card_le_cover). Consequently the minimum hitting set and the maximum disjoint packing have equal size (forest_duality).

Main definitions

• Cslib.FunctionalGraph.ForestDuality.iter: partial iteration of σ : α → Option α.
• Cslib.FunctionalGraph.ForestDuality.FPath: a directed path given by start vertex and length.
• Cslib.FunctionalGraph.ForestDuality.FPath.Mem: a vertex lies on a path.
• Cslib.FunctionalGraph.ForestDuality.FPath.End: a path is nonempty and ends at a vertex.
• Cslib.FunctionalGraph.ForestDuality.FPath.Within: every vertex of a path lies in S.
• Cslib.FunctionalGraph.ForestDuality.Covers: a vertex set hitting all required paths in S.
• Cslib.FunctionalGraph.ForestDuality.Packing: a pairwise vertex-disjoint family of required paths in S.
• Cslib.FunctionalGraph.ForestDuality.Acyclic: absence of directed cycles under σ.

Main results

• Cslib.FunctionalGraph.ForestDuality.packing_card_le_cover: weak duality.
• Cslib.FunctionalGraph.ForestDuality.exists_cover_packing: strong duality on any finite vertex subset S.
• Cslib.FunctionalGraph.ForestDuality.forest_duality: combined min-max duality.

References

• Adapted from lean/Proofs/ForestDuality.lean at revision c4cfa198 of [S. Schlesinger, Square-root circuit bounds for iterated functions] [Sch26f].

def Cslib.FunctionalGraph.ForestDuality.iter {α : Type u} (σ : α → Option α) : ℕ → α → Option α

Partial iteration of the successor map: iter σ k u is the k-th successor of u.

theorem Cslib.FunctionalGraph.ForestDuality.iter_add {α : Type u} (σ : α → Option α) (a c : ℕ) (u : α) : iter σ (a + c) u = (iter σ a u).bind (iter σ c)

Iterating a + c times is iterating a times and then, if defined, c more times.

structure Cslib.FunctionalGraph.ForestDuality.FPath (α : Type u) : Type u

A directed path in an in-forest, specified by its starting vertex and its number of vertices.

• start : α

  The first vertex of the path.

• len : ℕ

  The number of vertices on the path.

@[instance_reducible]

instance Cslib.FunctionalGraph.ForestDuality.instDecidableEqFPath {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (FPath α✝)

def Cslib.FunctionalGraph.ForestDuality.instDecidableEqFPath.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : FPath α✝) : Decidable (x✝ = x✝¹)

def Cslib.FunctionalGraph.ForestDuality.FPath.Mem {α : Type u} {σ : α → Option α} (p : FPath α) (v : α) : Prop

Vertex membership: v is one of the first len partial iterates from start.

def Cslib.FunctionalGraph.ForestDuality.FPath.End {α : Type u} {σ : α → Option α} (p : FPath α) (v : α) : Prop

The path is nonempty and ends at v.

def Cslib.FunctionalGraph.ForestDuality.FPath.Required {α : Type u} {σ : α → Option α} (r : α → ℕ) (p : FPath α) : Prop

The path is nonempty and its length is at least the requirement r v of its last vertex v.

def Cslib.FunctionalGraph.ForestDuality.FPath.Within {α : Type u} {σ : α → Option α} (S : Finset α) (p : FPath α) : Prop

Every vertex of the path lies in S.

def Cslib.FunctionalGraph.ForestDuality.Covers {α : Type u} (σ : α → Option α) (r : α → ℕ) (S H : Finset α) : Prop

H meets every required path contained in S.

def Cslib.FunctionalGraph.ForestDuality.Packing {α : Type u} (σ : α → Option α) (r : α → ℕ) (S : Finset α) (P : Finset (FPath α)) : Prop

P is a family of pairwise vertex-disjoint required paths contained in S.

def Cslib.FunctionalGraph.ForestDuality.Acyclic {α : Type u} (σ : α → Option α) : Prop

Acyclicity: no vertex is its own k-th successor for k > 0.

theorem Cslib.FunctionalGraph.ForestDuality.packing_card_le_cover {α : Type u} (σ : α → Option α) {r : α → ℕ} {S H : Finset α} {P : Finset (FPath α)} (hP : Packing σ r S P) (hH : Covers σ r S H) : P.card ≤ H.card

Weak duality. Any family of pairwise disjoint required paths in S has cardinality at most that of any hitting set for required paths in S.

theorem Cslib.FunctionalGraph.ForestDuality.exists_cover_packing {α : Type u} (σ : α → Option α) [Finite α] (hac : Acyclic σ) (r : α → ℕ) (S : Finset α) : ∃ H ⊆ S, ∃ (P : Finset (FPath α)), Covers σ r S H ∧ Packing σ r S P ∧ P.card = H.card

Strong duality. On every finite vertex subset S, there exist a hitting set H ⊆ S and a disjoint packing P of required paths in S with equal cardinality.

theorem Cslib.FunctionalGraph.ForestDuality.forest_duality {α : Type u} (σ : α → Option α) [Finite α] (hac : Acyclic σ) (r : α → ℕ) (S : Finset α) : ∃ (H : Finset α) (P : Finset (FPath α)), Covers σ r S H ∧ Packing σ r S P ∧ P.card = H.card ∧ (∀ (H' : Finset α), Covers σ r S H' → H.card ≤ H'.card) ∧ ∀ (P' : Finset (FPath α)), Packing σ r S P' → P'.card ≤ P.card

Min-max duality for required paths in an in-forest. There exist a hitting set H and a disjoint packing P of required paths in S with equal cardinality, every hitting set is at least that large, and every disjoint packing is at most that large.