Dominance, dependency forests and dependency trees

A position of a dependency graph dominates another when a chain of arcs leads from the first to the second. The graph is a forest when no position dominates its own head and no position has two heads, and a tree when in addition its root dominates every position. On a forest dominance is a partial order in which the dominators of a position form a chain, so positions neither of which dominates the other have disjoint yields.

Main definitions

• Dominates: the reflexive-transitive closure of the arc relation. Graph.yield is the set of positions a position dominates, and Graph.projection lists it in ascending order.
• Graph.IsForest: no position dominates its own head, and no position has two heads.
• Graph.IsTree: a forest whose root dominates every position.
• DominanceOrder: the positions ordered by dominance, on a forest a partial order with the head as predecessor and on a tree one with the root as bottom.
• Tree: a graph bundled with a proof that it is a tree.

Main statements

• Graph.isTree_iff_forall_not_adj_iff: a tree is a forest whose only headless position is its root.
• Graph.isTree_iff_leftUnique_adj: a graph is a tree when no position has two heads, the root has none, and the root dominates every position, so that acyclicity need not be assumed.
• Graph.IsForest.disjoint_yield: on a forest, positions neither of which dominates the other have disjoint yields.
• exists_adj_adj_of_not_dominates: positions under a common dominator, neither dominating the other, lie under distinct dependents of one position.

Implementation notes

• Dominates is an abbrev for Relation.ReflTransGen g.Adj, so mathlib's closure API applies to dominance directly and decidability comes from Core/Relation/ReflTransGen.lean. Dot notation on a dominance hypothesis therefore resolves in Relation.ReflTransGen.
• Decidable g.IsTree goes through Graph.isTree_iff_leftUnique_adj, which searches from the root alone instead of looking for a cycle from every position.
• DominanceOrder g carries the instances that mathlib's Order/SuccPred/Tree.lean and the command relations of Syntax/Command.lean are stated over. Its archimedean property is inferred from finiteness.

References

• [KN06]

Dominance

@[reducible, inline]

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

v dominates x when a possibly empty chain of arcs leads from v to x.

Equations

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

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

The yield of v is the set of positions v dominates, v itself included.

Equations

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

@[simp]

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

@[instance_reducible]

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

Equations

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

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

The projection of v is its yield in ascending order of position.

Equations

• g.projection v = List.filter (fun (x : Fin n) => decide (x ∈ g.yield 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

theorem DependencyGrammar.Graph.exists_adj_mem_yield {n : ℕ} {g : Graph n} {v x : Fin n} (hx : x ∈ g.yield v) (hne : x ≠ v) : ∃ (u : Fin n), g.Adj v u ∧ x ∈ g.yield u

A position in the yield of v other than v is in the yield of a dependent of v.

theorem DependencyGrammar.exists_link_across {n : ℕ} {g : Graph n} {v x y : Fin n} {S : Set (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.

theorem DependencyGrammar.exists_adj_adj_of_not_dominates {n : ℕ} {g : Graph n} {u v x : Fin n} (hu : Dominates g x u) (hv : Dominates g x v) (huv : ¬Dominates g u v) (hvu : ¬Dominates g v u) : ∃ (p : Fin n) (u' : Fin n) (v' : Fin n), g.Adj p u' ∧ g.Adj p v' ∧ u' ≠ v' ∧ Dominates g u' u ∧ Dominates g v' v

Positions under a common dominator, neither of which dominates the other, lie under distinct dependents of one position, their lowest common governor.

Forests and trees

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

A dependency graph is a forest when no position dominates its own head and no position has two heads ([KN06], Definition 2).

• not_dominates_of_adj ⦃v w : Fin n⦄ : g.Adj v w → ¬Dominates g w v

  The graph is acyclic: a dependent does not dominate its head.

• leftUnique_adj : Relator.LeftUnique g.Adj

  A position has at most one head.

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

A dependency graph is a tree when it is a forest whose root dominates every position.

• not_dominates_of_adj ⦃v w : Fin n⦄ : g.Adj v w → ¬Dominates g w v
• leftUnique_adj : Relator.LeftUnique g.Adj
• root_dominates (v : Fin n) : Dominates g g.root v

  The root dominates every position.

@[instance_reducible]

instance DependencyGrammar.instDecidableIsForest {n : ℕ} (g : Graph n) : Decidable g.IsForest

Equations

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

theorem DependencyGrammar.Graph.IsForest.not_adj_self {n : ℕ} {g : Graph n} {v : Fin n} (hF : g.IsForest) : ¬g.Adj v v

theorem DependencyGrammar.Graph.IsForest.acyclic {n : ℕ} {g : Graph n} (hF : g.IsForest) (v : Fin n) : ¬Relation.TransGen g.Adj v v

No position of a forest lies on a cycle.

theorem DependencyGrammar.Graph.IsForest.dominates_antisymm {n : ℕ} {g : Graph n} {v w : Fin n} (hF : g.IsForest) (hvw : Dominates g v w) (hwv : Dominates g w v) : v = w

theorem DependencyGrammar.Graph.IsForest.dominates_head {n : ℕ} {g : Graph n} {u v w : Fin n} (hF : g.IsForest) (hvw : Dominates g v w) (hne : v ≠ w) (hu : g.Adj u w) : Dominates g v u

A position dominating w and distinct from it dominates the head of w.

theorem DependencyGrammar.Graph.IsForest.dominates_total {n : ℕ} {g : Graph n} {v w x : Fin n} (hF : g.IsForest) (hv : Dominates g v x) (hw : Dominates g w x) : Dominates g v w ∨ Dominates g w v

The dominators of a position of a forest form a chain.

theorem DependencyGrammar.Graph.IsForest.disjoint_yield {n : ℕ} {g : Graph n} {v w : Fin n} (hF : g.IsForest) (hvw : ¬Dominates g v w) (hwv : ¬Dominates g w v) : Disjoint (g.yield v) (g.yield w)

Positions of a forest neither of which dominates the other have disjoint yields.

theorem DependencyGrammar.Graph.IsForest.disjoint_yield_of_adj {n : ℕ} {g : Graph n} {u v w : Fin n} (hF : g.IsForest) (hw : g.Adj v w) (hu : g.Adj v u) (hne : w ≠ u) : Disjoint (g.yield w) (g.yield u)

Two dependents of one head in a forest have disjoint yields.

theorem DependencyGrammar.Graph.not_isForest_enhance {n : ℕ} {g : Graph n} {v w x : Fin n} (hv : g.Adj v w) (hx : x ≠ v) (r : UD.DepRel) (extra : List (Fin n × Fin n × UD.DepRel)) (hmem : (x, w, r) ∈ extra) : ¬(g.enhance extra).IsForest

A graph in which enhancement gives a position a second head is not a forest, as when the embedded verb of a control or raising structure gains the matrix subject.

theorem DependencyGrammar.Graph.IsTree.not_adj_root {n : ℕ} {g : Graph n} (hT : g.IsTree) (v : Fin n) : ¬g.Adj v g.root

theorem DependencyGrammar.Graph.IsTree.exists_adj {n : ℕ} {g : Graph n} {w : Fin n} (hT : g.IsTree) (hw : w ≠ g.root) : ∃ (v : Fin n), g.Adj v w

theorem DependencyGrammar.Graph.isTree_iff_forall_not_adj_iff {n : ℕ} {g : Graph n} : g.IsTree ↔ g.IsForest ∧ ∀ (w : Fin n), (∀ (v : Fin n), ¬g.Adj v w) ↔ w = g.root

A tree is a forest whose only headless position is its root, a forest with exactly one root ([KN06], Definition 2).

theorem DependencyGrammar.Graph.isTree_iff_leftUnique_adj {n : ℕ} {g : Graph n} : g.IsTree ↔ Relator.LeftUnique g.Adj ∧ (∀ (v : Fin n), ¬g.Adj v g.root) ∧ ∀ (v : Fin n), Dominates g g.root v

A graph is a tree when no position has two heads, the root has none, and the root dominates every position: a cycle would have to be entered from the root's side through a second head.

@[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.

The head function

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

The least head of v, and v itself when it has none. In a forest it is the head of every position that has one.

Equations

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

theorem DependencyGrammar.Graph.headOf_of_forall_not_adj {n : ℕ} {g : Graph n} {v : Fin n} (h : ∀ (u : Fin n), ¬g.Adj u v) : g.headOf v = v

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

The dominance order

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

The positions of g ordered by dominance instead of by position.

Equations

• DependencyGrammar.DominanceOrder _g = Fin n

instance DependencyGrammar.instFactIsForestOfIsTree {n : ℕ} {g : Graph n} [hT : Fact g.IsTree] : Fact g.IsForest

@[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.instPartialOrder {n : ℕ} {g : Graph n} [hF : Fact g.IsForest] : PartialOrder (DominanceOrder g)

Equations

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

@[instance_reducible]

instance DependencyGrammar.DominanceOrder.instDecidableLE {n : ℕ} {g : Graph n} [hF : Fact g.IsForest] : DecidableLE (DominanceOrder g)

Equations

• v.instDecidableLE w = Relation.ReflTransGen.instDecidableRel_linglib v w

@[instance_reducible]

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

The predecessor of a position is its head, and a headless position is its own.

Equations

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

@[instance_reducible]

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

Equations

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

Bundled trees

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

A dependency tree is a graph bundled with a proof that it is a tree.

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

  The underlying graph is a tree.

@[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 its tree-hood, decided by default.

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, which makes the instances of its dominance order available.