Dominance and dependency trees

This file defines dominance as the reflexive-transitive closure of the arc relation, the projection (yield) it induces, tree well-formedness, and the order theory of dominance on trees.

Main definitions

• Dominates is the reflexive-transitive closure of the arc relation.
• Graph.IsTree is tree well-formedness: no arc into the root, a unique head elsewhere, and acyclicity. It is decidable.
• DominanceOrder is Fin n reordered by dominance. On a tree it is a partial order with the root as bottom, the head as predecessor, and the lowest common governor as meet, bundled as mathlib's RootedTree by Graph.toRootedTree.
• Tree n is a graph bundled with its tree-hood, so the dominance-order instances hold with no side conditions.

Main results

• IsTree.root_dominates: the root of a tree dominates every position.
• Dominates.antisymm and Dominates.comparable: on trees dominance is a partial order under which the dominators of any position form a chain.

Implementation notes

Dominates is an abbrev for Relation.ReflTransGen g.Adj, so mathlib's closure API (.refl, .tail, .trans, .single, cases_tail, total_of_right_unique, …) applies to dominance facts directly; this file adds only what mentions the dependency carrier. Decidability comes from Core/Relation/ReflTransGen.lean.

References

[KN06] — Mildly non-projective dependency structures, source of the dominance and projection definitions

@[reducible, inline]

abbrev DependencyGrammar.Dominates {n : ℕ} (g : Graph n) : Fin n → Fin n → Prop

v dominates x if a (possibly empty) chain of arcs leads from v to x ([KN06] §2).

Equations

• DependencyGrammar.Dominates g = Relation.ReflTransGen g.Adj

def DependencyGrammar.Graph.dominated {n : ℕ} (g : Graph n) (v : Fin n) : Set (Fin n)

The positions v dominates, v itself included — the yield of v in the source terminology.

Equations

• g.dominated v = {x : Fin n | DependencyGrammar.Dominates g v x}

@[simp]

theorem DependencyGrammar.Graph.mem_dominated {n : ℕ} {g : Graph n} {v x : Fin n} : x ∈ g.dominated v ↔ Dominates g v x

@[instance_reducible]

instance DependencyGrammar.instDecidablePredFinMemSetDominated {n : ℕ} (g : Graph n) (v : Fin n) : DecidablePred fun (x : Fin n) => x ∈ g.dominated v

Equations

• DependencyGrammar.instDecidablePredFinMemSetDominated g v x✝ = DependencyGrammar.instDecidablePredFinMemSetDominated._aux_1 g v x✝

def DependencyGrammar.Graph.projection {n : ℕ} (g : Graph n) (v : Fin n) : List (Fin n)

The yield of v in ascending position order, the projection π(v) of [KN06] §2.

Equations

• g.projection v = List.filter (fun (x : Fin n) => decide (x ∈ g.dominated v)) (List.finRange n)

@[simp]

theorem DependencyGrammar.Graph.mem_projection {n : ℕ} {g : Graph n} {v x : Fin n} : x ∈ g.projection v ↔ Dominates g v x

Well-formedness

structure DependencyGrammar.Graph.IsTree {n : ℕ} (g : Graph n) : Prop

The graph is a dependency tree: nothing points at the root, every other position has exactly one head, and no position dominates itself. On Fin n these imply rootedness and connectivity — every non-root position's head chain terminates at the unique headless position.

• not_adj_root (v : Fin n) : ¬g.Adj v g.root
• existsUnique_adj (w : Fin n) : w ≠ g.root → ∃! v : Fin n, g.Adj v w
• acyclic (v : Fin n) : ¬Relation.TransGen g.Adj v v

theorem DependencyGrammar.Graph.isTree_iff {n : ℕ} (g : Graph n) : g.IsTree ↔ (∀ (v : Fin n), ¬g.Adj v g.root) ∧ (∀ (w : Fin n), w ≠ g.root → ∃! v : Fin n, g.Adj v w) ∧ ∀ (v : Fin n), ¬Relation.TransGen g.Adj v v

@[instance_reducible]

instance DependencyGrammar.instDecidableIsTree {n : ℕ} (g : Graph n) : Decidable g.IsTree

Equations

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

Dominance as an order on trees

theorem DependencyGrammar.Graph.IsTree.leftUnique_adj {n : ℕ} {g : Graph n} (hT : g.IsTree) : Relator.LeftUnique g.Adj

In a tree, a position has at most one head.

theorem DependencyGrammar.not_adj_dominates {n : ℕ} {g : Graph n} {v w : Fin n} (hacyc : ∀ (v : Fin n), ¬Relation.TransGen g.Adj v v) (hadj : g.Adj v w) (hdom : Dominates g w v) : False

No arc closes a dominance cycle, on acyclic graphs.

theorem DependencyGrammar.Dominates.antisymm {n : ℕ} {g : Graph n} {v w : Fin n} (hacyc : ∀ (v : Fin n), ¬Relation.TransGen g.Adj v v) (hvw : Dominates g v w) (hwv : Dominates g w v) : v = w

Dominance is antisymmetric on acyclic graphs.

theorem DependencyGrammar.Dominates.to_head {n : ℕ} {g : Graph n} {v w u : Fin n} (hT : g.IsTree) (hvw : Dominates g v w) (hne : v ≠ w) (hu : g.Adj u w) : Dominates g v u

A strict dominator of w dominates w's head.

theorem DependencyGrammar.Dominates.comparable {n : ℕ} {g : Graph n} {v w x : Fin n} (hT : g.IsTree) (hv : Dominates g v x) (hw : Dominates g w x) : Dominates g v w ∨ Dominates g w v

On a tree, positions dominating a common position are comparable: the dominators of any position form a chain.

theorem DependencyGrammar.Graph.IsTree.root_dominates {n : ℕ} {g : Graph n} (hT : g.IsTree) (v : Fin n) : Dominates g g.root v

The root dominates every position: head chains ascend, without repetition, to the unique headless position.

theorem DependencyGrammar.Graph.IsTree.projection_root {n : ℕ} {g : Graph n} (hT : g.IsTree) : g.projection g.root = List.finRange n

The root's projection is the whole sentence.

Paths across a boundary

theorem DependencyGrammar.disjoint_dominated {n : ℕ} {g : Graph n} {v w : Fin n} (hT : g.IsTree) (hvw : ¬Dominates g v w) (hwv : ¬Dominates g w v) : Disjoint (g.dominated v) (g.dominated w)

Incomparable positions of a tree dominate disjoint sets.

theorem DependencyGrammar.exists_link_across {n : ℕ} {g : Graph n} {v : Fin n} {S : Set (Fin n)} {x y : Fin n} (hx : Dominates g v x) (hy : Dominates g v y) (hxS : x ∈ S) (hyS : y ∉ S) : ∃ (p : Fin n) (q : Fin n), g.Linked p q ∧ Dominates g v p ∧ Dominates g v q ∧ p ∈ S ∧ q ∉ S

If v dominates a position inside S and one outside it, some link below v crosses the boundary of S.

The head function

def DependencyGrammar.Graph.headOf {n : ℕ} (g : Graph n) (v : Fin n) : Fin n

The least head of v, defaulting to v when headless — under IsTree, the unique head of a non-root position and the root at the root.

Equations

• g.headOf v = WithTop.untopD v (g.parents v).min

theorem DependencyGrammar.Graph.IsTree.adj_headOf {n : ℕ} {g : Graph n} (hT : g.IsTree) {v : Fin n} (hv : v ≠ g.root) : g.Adj (g.headOf v) v

theorem DependencyGrammar.Graph.IsTree.headOf_eq {n : ℕ} {g : Graph n} (hT : g.IsTree) {u v : Fin n} (h : g.Adj u v) : g.headOf v = u

theorem DependencyGrammar.Graph.IsTree.headOf_root {n : ℕ} {g : Graph n} (hT : g.IsTree) : g.headOf g.root = g.root

The dominance order

def DependencyGrammar.DominanceOrder {n : ℕ} (_g : Graph n) : Type

Fin n carrying the dominance order of g instead of the positional order. With [Fact g.IsTree] this is a partial order with the root as bottom, the head as predecessor, and finite descent — the order-theoretic reading of a rooted dependency tree (cf. mathlib's RootedTree).

Equations

• DependencyGrammar.DominanceOrder _g = Fin n

@[instance_reducible]

instance DependencyGrammar.DominanceOrder.instFintype {n : ℕ} {g : Graph n} : Fintype (DominanceOrder g)

Equations

• DependencyGrammar.DominanceOrder.instFintype = { elems := DependencyGrammar.DominanceOrder.instFintype._aux_1, complete := ⋯ }

@[instance_reducible]

instance DependencyGrammar.DominanceOrder.instDecidableEq {n : ℕ} {g : Graph n} : DecidableEq (DominanceOrder g)

Equations

• DependencyGrammar.DominanceOrder.instDecidableEq = DependencyGrammar.DominanceOrder.instDecidableEq._aux_1

@[instance_reducible]

instance DependencyGrammar.DominanceOrder.instOfNatOfFin {n : ℕ} {g : Graph n} {i : ℕ} [OfNat (Fin n) i] : OfNat (DominanceOrder g) i

Equations

• DependencyGrammar.DominanceOrder.instOfNatOfFin = DependencyGrammar.DominanceOrder.instOfNatOfFin._aux_1

@[instance_reducible]

instance DependencyGrammar.DominanceOrder.instPartialOrderOfFactIsTree {n : ℕ} {g : Graph n} [Fact g.IsTree] : PartialOrder (DominanceOrder g)

Equations

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

@[instance_reducible]

instance DependencyGrammar.DominanceOrder.instOrderBot {n : ℕ} {g : Graph n} [Fact g.IsTree] : OrderBot (DominanceOrder g)

Equations

• DependencyGrammar.DominanceOrder.instOrderBot = { bot := g.root, bot_le := ⋯ }

@[instance_reducible]

instance DependencyGrammar.DominanceOrder.instPredOrder {n : ℕ} {g : Graph n} [Fact g.IsTree] : PredOrder (DominanceOrder g)

Equations

• DependencyGrammar.DominanceOrder.instPredOrder = { pred := g.headOf, pred_le := ⋯, min_of_le_pred := ⋯, le_pred_of_lt := ⋯ }

@[instance_reducible]

instance DependencyGrammar.DominanceOrder.instDecidableRelLe {n : ℕ} {g : Graph n} [Fact g.IsTree] : DecidableRel fun (x1 x2 : DominanceOrder g) => x1 ≤ x2

Equations

• v.instDecidableRelLe w = Relation.ReflTransGen.instDecidableRelOfFintypeOfDecidableEq_linglib v w

instance DependencyGrammar.DominanceOrder.instIsPredArchimedean {n : ℕ} {g : Graph n} [Fact g.IsTree] : IsPredArchimedean (DominanceOrder g)

@[instance_reducible]

instance DependencyGrammar.DominanceOrder.instSemilatticeInfOfFactIsTree {n : ℕ} {g : Graph n} [Fact g.IsTree] : SemilatticeInf (DominanceOrder g)

Lowest common governor as the meet: the first head-iterate of one argument that dominates the other.

Equations

• DependencyGrammar.DominanceOrder.instSemilatticeInfOfFactIsTree = IsPredArchimedean.semilatticeInf

def DependencyGrammar.Graph.toRootedTree {n : ℕ} (g : Graph n) [Fact g.IsTree] : RootedTree

A well-formed dependency graph, as mathlib's rooted tree: positions ordered by dominance, the root as ⊥, the head as Order.pred, and the lowest common governor as ⊓.

Equations

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

Bundled trees

structure DependencyGrammar.Tree (n : ℕ) extends DependencyGrammar.Graph n : Type

A dependency tree: a graph bundled with its tree-hood, so that the dominance-order structure holds with no side conditions. Parent projections give direct access to the graph API (t.root, t.label, t.gapDegree, …).

• words : Fin n → Morphology.Word
• label : Fin n → Fin n → Option UD.DepRel
• root : Fin n
• isTree : self.IsTree

  Well-formedness of the underlying graph.

@[instance_reducible]

instance DependencyGrammar.Tree.instCoeGraph {n : ℕ} : Coe (Tree n) (Graph n)

Equations

• DependencyGrammar.Tree.instCoeGraph = { coe := DependencyGrammar.Tree.toGraph }

def DependencyGrammar.Tree.mk' {n : ℕ} (g : Graph n) (h : g.IsTree := by decide) : Tree n

Bundle a graph with decide-checked tree-hood.

Equations

• DependencyGrammar.Tree.mk' g h = { toGraph := g, isTree := h }

instance DependencyGrammar.Tree.instFact {n : ℕ} (t : Tree n) : Fact t.IsTree

A bundled tree's tree-hood, available to instance search: the Fact-gated dominance-order instances fire unconditionally.

def DependencyGrammar.Tree.toRootedTree {n : ℕ} (t : Tree n) : RootedTree

A dependency tree is a mathlib rooted tree.

Equations

• t.toRootedTree = t.toRootedTree