Dependency graphs

This file defines the dependency structure of a sentence: the vertices are the sentence positions Fin n with their linear order, and the arcs are a partial labeling of ordered position pairs by UD v2 dependency relations. A distinguished root position replaces CoNLL-U's artificial root token.

Well-formedness (Graph.IsTree) is defined in Dominance.lean, beside the dominance relation it is stated through.

Main definitions

• Graph n is a dependency graph on n words: a token at every position, an optional UD relation on every ordered pair of positions (head to dependent), and a root position.
• Graph.toDigraph and Graph.toSimpleGraph are the directed and undirected views of a graph as mathlib's graph carriers.
• Graph.enhance adds arcs to a graph, as in UD's enhanced representation; HasUnrepresentedArg says that an enhanced graph gives a position an argument relation its basic graph lacks.

Implementation notes

Positions are 0-indexed; CoNLL-U is 1-indexed with 0 as an artificial root, so wire-format conversion shifts indices.

label returns at most one relation per ordered pair, faithful to dependency trees and basic UD. If an enhanced-UD fixture ever needs parallel arcs on one pair, the field generalizes to a list. Feature-level constraints (agreement) are Syntax/Agreement/'s domain, not the carrier's.

References

[Mel88] — Dependency syntax: theory and practice, source of the arcs-among-ordered-words presentation [KN06] — Mildly non-projective dependency structures, source of the root convention [Kuh13] — Mildly non-projective dependency grammar [dMN19] — Dependency grammar, on UD's enhanced representation

Dependency graphs

structure DependencyGrammar.Graph (n : ℕ) : Type

A dependency graph on n words: the sentence's tokens as a labeling of the positions Fin n, the arcs as a partial labeling of ordered position pairs (head → dependent) by UD relations, and a distinguished root position.

• words : Fin n → Morphology.Word

  The token at each position.

• label : Fin n → Fin n → Option UD.DepRel

  The UD relation from head v to dependent w, if there is an arc.

• root : Fin n

  The root position.

theorem DependencyGrammar.Graph.ext {n : ℕ} {x y : Graph n} (words : x.words = y.words) (label : x.label = y.label) (root : x.root = y.root) : x = y

theorem DependencyGrammar.Graph.ext_iff {n : ℕ} {x y : Graph n} : x = y ↔ x.words = y.words ∧ x.label = y.label ∧ x.root = y.root

def DependencyGrammar.Graph.Adj {n : ℕ} (g : Graph n) (v w : Fin n) : Prop

Adjacency: there is an arc from head v to dependent w.

Equations

• g.Adj v w = ((g.label v w).isSome = true)

@[instance_reducible]

instance DependencyGrammar.Graph.instDecidableRelFinAdj {n : ℕ} (g : Graph n) : DecidableRel g.Adj

Equations

• g.instDecidableRelFinAdj x✝¹ x✝ = DependencyGrammar.Graph.instDecidableRelFinAdj._aux_1 g x✝¹ x✝

theorem DependencyGrammar.Graph.adj_iff_exists {n : ℕ} {g : Graph n} {v w : Fin n} : g.Adj v w ↔ ∃ (r : UD.DepRel), g.label v w = some r

def DependencyGrammar.Graph.Linked {n : ℕ} (g : Graph n) (a b : Fin n) : Prop

Positions linked by an arc in either direction — the undirected view of adjacency.

Equations

• g.Linked a b = (g.Adj a b ∨ g.Adj b a)

@[instance_reducible]

instance DependencyGrammar.Graph.instDecidableLinked {n : ℕ} (g : Graph n) (a b : Fin n) : Decidable (g.Linked a b)

Equations

• g.instDecidableLinked a b = DependencyGrammar.Graph.instDecidableLinked._aux_1 g a b

theorem DependencyGrammar.Graph.Linked.symm {n : ℕ} {g : Graph n} {a b : Fin n} (h : g.Linked a b) : g.Linked b a

Views onto mathlib's graph carriers

def DependencyGrammar.Graph.toDigraph {n : ℕ} (g : Graph n) : Digraph (Fin n)

The graph as a mathlib Digraph on positions.

Equations

• g.toDigraph = { Adj := g.Adj }

@[simp]

theorem DependencyGrammar.Graph.toDigraph_adj {n : ℕ} (g : Graph n) (v w : Fin n) : g.toDigraph.Adj v w ↔ g.Adj v w

def DependencyGrammar.Graph.toSimpleGraph {n : ℕ} (g : Graph n) : SimpleGraph (Fin n)

The graph's undirected view: mathlib's orientation-forgetting Digraph.toSimpleGraphInclusive applied to toDigraph. Planarity and catena connectivity are stated through it.

Equations

• g.toSimpleGraph = g.toDigraph.toSimpleGraphInclusive

@[simp]

theorem DependencyGrammar.Graph.toSimpleGraph_adj {n : ℕ} (g : Graph n) (v w : Fin n) : g.toSimpleGraph.Adj v w ↔ v ≠ w ∧ g.Linked v w

@[instance_reducible]

instance DependencyGrammar.Graph.instDecidableRelFinAdjToSimpleGraph {n : ℕ} (g : Graph n) : DecidableRel g.toSimpleGraph.Adj

Equations

• g.instDecidableRelFinAdjToSimpleGraph v w = decidable_of_iff (v ≠ w ∧ g.Linked v w) ⋯

theorem DependencyGrammar.Graph.toSimpleGraph_adj_of_ne {n : ℕ} {g : Graph n} {v w : Fin n} (h : v ≠ w) : g.toSimpleGraph.Adj v w ↔ g.Linked v w

Off the diagonal the two undirected views agree; they can differ only on self-arcs, which toSimpleGraph drops and Linked keeps.

Heads and dependents

def DependencyGrammar.Graph.parents {n : ℕ} (g : Graph n) (w : Fin n) : Finset (Fin n)

The head positions of w.

Equations

• g.parents w = {v : Fin n | g.Adj v w}

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

The dependent positions of v.

Equations

• g.children v = {w : Fin n | g.Adj v w}

@[simp]

theorem DependencyGrammar.Graph.mem_parents {n : ℕ} {g : Graph n} {v w : Fin n} : v ∈ g.parents w ↔ g.Adj v w

@[simp]

theorem DependencyGrammar.Graph.mem_children {n : ℕ} {g : Graph n} {v w : Fin n} : w ∈ g.children v ↔ g.Adj v w

Constructors

def DependencyGrammar.Graph.arcsLabel {n : ℕ} (arcs : List (Fin n × Fin n × UD.DepRel)) (v w : Fin n) : Option UD.DepRel

The partial label function induced by a CoNLL-U-style arc list of (head, dependent, relation) triples. First match wins.

Equations

• DependencyGrammar.Graph.arcsLabel arcs v w = Option.map (fun (x : Fin n × Fin n × UD.DepRel) => x.2.2) (List.find? (fun (a : Fin n × Fin n × UD.DepRel) => a.1 == v && a.2.1 == w) arcs)

theorem DependencyGrammar.Graph.arcsLabel_isSome_iff {n : ℕ} {arcs : List (Fin n × Fin n × UD.DepRel)} {v w : Fin n} : (arcsLabel arcs v w).isSome = true ↔ ∃ (r : UD.DepRel), (v, w, r) ∈ arcs

An arc list labels a pair exactly when some triple mentions it; which relation wins on duplicates is arcsLabel's business, not whether.

def DependencyGrammar.Graph.ofArcs (words : List Morphology.Word) (root : Fin words.length) (arcs : List (Fin words.length × Fin words.length × UD.DepRel)) : Graph words.length

Build a graph from CoNLL-U-style data: the token list (whose length fixes n), the root position, and the arcs as (head, dependent, relation) triples. Later arcs for the same pair are ignored.

Equations

• DependencyGrammar.Graph.ofArcs words root arcs = { words := words.get, label := DependencyGrammar.Graph.arcsLabel arcs, root := root }

@[simp]

theorem DependencyGrammar.Graph.ofArcs_adj {words : List Morphology.Word} {root : Fin words.length} {arcs : List (Fin words.length × Fin words.length × UD.DepRel)} {v w : Fin words.length} : (ofArcs words root arcs).Adj v w ↔ ∃ (r : UD.DepRel), (v, w, r) ∈ arcs

def DependencyGrammar.Graph.enhance {n : ℕ} (g : Graph n) (extra : List (Fin n × Fin n × UD.DepRel)) : Graph n

Add arcs to a graph (existing labels win), as in UD's enhanced representation: semantic relations the single-headed tree cannot encode — shared dependents in coordination, controlled subjects, relative-clause gaps — become explicit arcs.

Equations

• g.enhance extra = { words := g.words, label := fun (v w : Fin n) => g.label v w <|> DependencyGrammar.Graph.arcsLabel extra v w, root := g.root }

@[simp]

theorem DependencyGrammar.Graph.enhance_adj {n : ℕ} {g : Graph n} {extra : List (Fin n × Fin n × UD.DepRel)} {v w : Fin n} : (g.enhance extra).Adj v w ↔ g.Adj v w ∨ ∃ (r : UD.DepRel), (v, w, r) ∈ extra

def DependencyGrammar.HasUnrepresentedArg {n : ℕ} (basic enhanced : Graph n) (w : Fin n) : Prop

Position w has an argument relation in the enhanced graph that the basic graph fails to encode.

Equations

• DependencyGrammar.HasUnrepresentedArg basic enhanced w = ∃ (v : Fin n), enhanced.Adj v w ∧ ¬basic.Adj v w

@[instance_reducible]

instance DependencyGrammar.instDecidableHasUnrepresentedArg {n : ℕ} (b e : Graph n) (w : Fin n) : Decidable (HasUnrepresentedArg b e w)

Equations

• DependencyGrammar.instDecidableHasUnrepresentedArg b e w = DependencyGrammar.instDecidableHasUnrepresentedArg._aux_1 b e w