Enhanced Dependencies

@cite{de-marneffe-nivre-2019}

Basic dependency trees enforce a unique-heads constraint: every word (except root) has exactly one head. This means certain predicate-argument relations that hold semantically cannot be represented as edges in the tree:

• Shared dependents in coordination: "John sees and hears Mary" — Mary is obj of both verbs, but the tree can only attach her to one
• Controlled subjects: "Students forgot to come" — "students" is the semantic subject of "come" but has no edge to it
• Relative clause gaps: "the book that John read" — "book" is the semantic object of "read" but has no edge to it

Enhanced dependencies solve this by relaxing the tree to a directed graph where words can have multiple heads, making implicit predicate-argument relations explicit.

Key Result

For each phenomenon (coordination, control, relative clauses), we prove:

1. The basic tree has an unrepresented argument (basic_tree_loses_*)
2. The enhanced graph recovers it (enhanced_recovers_*)
3. The enhanced graph is a strict superset of the basic tree (enhancement_preserves_basic)
4. The enhanced graph violates unique-heads — confirming it's a graph, not a tree

Bridges

• → Coordination.lean: enhanceSharedDeps converts implicit shared deps to graph edges
• → LongDistance.lean: fillGap converts gap → explicit argument edge
• → DependencyLength.lean: enhanced graphs have ≥ total dep length (more edges)
• → NonProjective.lean: enhanced graphs can be non-projective

inductive DepGrammar.EnhancedDependencies.EnhancementType : Type

Enhancement type: what kind of implicit relation is being made explicit. Each variant corresponds to a phenomenon where DepTree loses information.

• coordSharedDep : EnhancementType
• controlSubject : EnhancementType
• relClauseGap : EnhancementType

instance DepGrammar.EnhancedDependencies.instReprEnhancementType : Repr EnhancementType

Equations

• DepGrammar.EnhancedDependencies.instReprEnhancementType = { reprPrec := DepGrammar.EnhancedDependencies.instReprEnhancementType.repr }

def DepGrammar.EnhancedDependencies.instReprEnhancementType.repr : EnhancementType → ℕ → Std.Format

Equations

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

instance DepGrammar.EnhancedDependencies.instDecidableEqEnhancementType : DecidableEq EnhancementType

Equations

• DepGrammar.EnhancedDependencies.instDecidableEqEnhancementType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DepGrammar.EnhancedDependencies.instBEqEnhancementType : BEq EnhancementType

Equations

• DepGrammar.EnhancedDependencies.instBEqEnhancementType = { beq := DepGrammar.EnhancedDependencies.instBEqEnhancementType.beq }

def DepGrammar.EnhancedDependencies.instBEqEnhancementType.beq : EnhancementType → EnhancementType → Bool

Equations

• DepGrammar.EnhancedDependencies.instBEqEnhancementType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def DepGrammar.DepGraph.basicDeps (g : DepGraph) : List Dependency

Extract the basic tree edges from a graph: for each word, keep only the first incoming edge (deterministic selection preserving unique-heads).

Equations

• g.basicDeps = List.filterMap (fun (i : ℕ) => List.find? (fun (x : DepGrammar.Dependency) => x.depIdx == i) g.deps) (List.range g.words.length)

def DepGrammar.DepGraph.toBasicTree (g : DepGraph) : DepTree

Extract the basic tree from a graph (filter to unique heads).

Equations

• g.toBasicTree = { words := g.words, deps := g.basicDeps, rootIdx := g.rootIdx }

def DepGrammar.EnhancedDependencies.enhancedEdges (basic : DepTree) (enhanced : DepGraph) : List Dependency

The enhanced edges: those in the graph but not in the basic tree. These are the edges that the unique-heads constraint forces us to drop.

Equations

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

def DepGrammar.EnhancedDependencies.hasUnrepresentedArg (basic : DepTree) (enhanced : DepGraph) (wordIdx : ℕ) : Bool

A word has an "unrepresented argument" in a basic tree if it's semantically an argument of some head (per the enhanced graph) but has no edge to that head in the basic tree. This is the core problem enhanced deps solve.

Equations

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

def DepGrammar.DepGraph.isWellFormed (g : DepGraph) : Bool

Enhanced graph well-formedness: acyclic, but NO unique-heads check. This is the relaxation that distinguishes DepGraph from DepTree.

Equations

• g.isWellFormed = DepGrammar.isAcyclic { words := g.words, deps := g.deps, rootIdx := g.rootIdx }

def DepGrammar.EnhancedDependencies.controlBasicTree : DepTree

Basic tree for "Students forgot to come". Students (0) attaches as nsubj of forgot (1) only.

Equations

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

def DepGrammar.EnhancedDependencies.controlEnhancedGraph : DepGraph

Enhanced graph: adds students as nsubj of come.

Equations

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

theorem DepGrammar.EnhancedDependencies.basic_tree_loses_coord_args : hasUnrepresentedArg DepGrammar.EnhancedDependencies.coordBasicTree✝ DepGrammar.EnhancedDependencies.coordEnhancedGraph✝ 4 = true

Coordination: Mary (idx 4) has an unrepresented argument in the basic tree. She is semantically obj of hears (3), but the tree only attaches her to sees (1).

theorem DepGrammar.EnhancedDependencies.basic_tree_loses_control_subject : hasUnrepresentedArg controlBasicTree controlEnhancedGraph 0 = true

Control: Students (idx 0) has an unrepresented argument in the basic tree. They are semantically nsubj of come (3), but the tree only attaches them to forgot (1).

theorem DepGrammar.EnhancedDependencies.basic_tree_loses_relclause_gap : hasUnrepresentedArg DepGrammar.EnhancedDependencies.relClauseBasicTree✝ DepGrammar.EnhancedDependencies.relClauseEnhancedGraph✝ 1 = true

Relative clause: Book (idx 1) has an unrepresented argument in the basic tree. It is semantically obj of read (4), but the tree only has acl from read.

theorem DepGrammar.EnhancedDependencies.enhanced_recovers_coord_args : DepGrammar.EnhancedDependencies.coordEnhancedGraph✝.deps.length > DepGrammar.EnhancedDependencies.coordBasicTree✝.deps.length

The enhanced graph for coordination has strictly more edges than the basic tree.

theorem DepGrammar.EnhancedDependencies.enhanced_recovers_control_subject : controlEnhancedGraph.deps.length > controlBasicTree.deps.length

The enhanced graph for control has strictly more edges than the basic tree.

theorem DepGrammar.EnhancedDependencies.enhanced_recovers_relclause_gap : DepGrammar.EnhancedDependencies.relClauseEnhancedGraph✝.deps.length > DepGrammar.EnhancedDependencies.relClauseBasicTree✝.deps.length

The enhanced graph for relative clauses has strictly more edges than the basic tree.

theorem DepGrammar.EnhancedDependencies.enhancement_preserves_basic_coord : (DepGrammar.EnhancedDependencies.coordBasicTree✝.deps.all fun (d : Dependency) => DepGrammar.EnhancedDependencies.coordEnhancedGraph✝.deps.any fun (ed : Dependency) => ed.headIdx == d.headIdx && ed.depIdx == d.depIdx && ed.depType == d.depType) = true

Enhancement preserves basic edges: every edge in the basic tree for coordination is also in the enhanced graph. The enhanced graph is a superset.

theorem DepGrammar.EnhancedDependencies.enhancement_preserves_basic_control : (controlBasicTree.deps.all fun (d : Dependency) => controlEnhancedGraph.deps.any fun (ed : Dependency) => ed.headIdx == d.headIdx && ed.depIdx == d.depIdx && ed.depType == d.depType) = true

Enhancement preserves basic edges for control.

theorem DepGrammar.EnhancedDependencies.enhancement_preserves_basic_relclause : (DepGrammar.EnhancedDependencies.relClauseBasicTree✝.deps.all fun (d : Dependency) => DepGrammar.EnhancedDependencies.relClauseEnhancedGraph✝.deps.any fun (ed : Dependency) => ed.headIdx == d.headIdx && ed.depIdx == d.depIdx && ed.depType == d.depType) = true

Enhancement preserves basic edges for relative clauses.

theorem DepGrammar.EnhancedDependencies.enhanced_not_tree_coord : hasUniqueHeads { words := DepGrammar.EnhancedDependencies.coordEnhancedGraph✝.words, deps := DepGrammar.EnhancedDependencies.coordEnhancedGraph✝¹.deps, rootIdx := DepGrammar.EnhancedDependencies.coordEnhancedGraph✝².rootIdx } = false

The coordination enhanced graph violates unique-heads — it's genuinely a graph. Mary (idx 4) has two incoming edges (obj from both sees and hears).

theorem DepGrammar.EnhancedDependencies.enhanced_not_tree_control : hasUniqueHeads { words := controlEnhancedGraph.words, deps := controlEnhancedGraph.deps, rootIdx := controlEnhancedGraph.rootIdx } = false

The control enhanced graph violates unique-heads. Students (idx 0) has two incoming edges (nsubj from both forgot and come).

theorem DepGrammar.EnhancedDependencies.enhanced_not_tree_relclause : hasUniqueHeads { words := DepGrammar.EnhancedDependencies.relClauseEnhancedGraph✝.words, deps := DepGrammar.EnhancedDependencies.relClauseEnhancedGraph✝¹.deps, rootIdx := DepGrammar.EnhancedDependencies.relClauseEnhancedGraph✝².rootIdx } = false

The relative clause enhanced graph violates unique-heads. Book (idx 1) has two incoming edges (det from the, obj from read).

theorem DepGrammar.EnhancedDependencies.basic_is_tree_coord : hasUniqueHeads DepGrammar.EnhancedDependencies.coordBasicTree✝ = true

The basic trees DO satisfy unique-heads (they are trees).

theorem DepGrammar.EnhancedDependencies.basic_is_tree_control : hasUniqueHeads controlBasicTree = true

theorem DepGrammar.EnhancedDependencies.basic_is_tree_relclause : hasUniqueHeads DepGrammar.EnhancedDependencies.relClauseBasicTree✝ = true

theorem DepGrammar.EnhancedDependencies.enhanced_wf_coord : DepGrammar.EnhancedDependencies.coordEnhancedGraph✝.isWellFormed = true

Enhanced graphs are well-formed (acyclic).

theorem DepGrammar.EnhancedDependencies.enhanced_wf_control : controlEnhancedGraph.isWellFormed = true

def DepGrammar.EnhancedDependencies.enhancedTotalDepLength (g : DepGraph) : ℕ

Total dep length on an enhanced graph (computed over all edges including enhanced ones). Since the graph has strictly more edges than the basic tree, the total dep length is ≥.

Equations

• DepGrammar.EnhancedDependencies.enhancedTotalDepLength g = List.foldl (fun (acc : ℕ) (d : DepGrammar.Dependency) => acc + DepGrammar.DependencyLength.depLength d) 0 g.deps

theorem DepGrammar.EnhancedDependencies.enhanced_dep_length_ge_coord : enhancedTotalDepLength DepGrammar.EnhancedDependencies.coordEnhancedGraph✝ ≥ DependencyLength.totalDepLength DepGrammar.EnhancedDependencies.coordBasicTree✝

Enhanced dep length ≥ basic dep length for coordination example. More edges → more total length.

theorem DepGrammar.EnhancedDependencies.enhanced_dep_length_ge_relclause : enhancedTotalDepLength DepGrammar.EnhancedDependencies.relClauseEnhancedGraph✝ ≥ DependencyLength.totalDepLength DepGrammar.EnhancedDependencies.relClauseBasicTree✝

Enhanced dep length ≥ basic dep length for relative clause example.

theorem DepGrammar.EnhancedDependencies.basic_relclause_projective : isProjective DepGrammar.EnhancedDependencies.relClauseBasicTree✝ = true

The basic relative clause tree IS projective.

theorem DepGrammar.EnhancedDependencies.enhanced_coord_edges_increase : DepGrammar.EnhancedDependencies.coordEnhancedGraph✝.deps.length > DepGrammar.EnhancedDependencies.coordBasicTree✝.deps.length

The coordination enhanced graph has strictly more edges than the basic tree (enhanced obj edge from hears to Mary).

def DepGrammar.EnhancedDependencies.classifyEnhancement (basicDeps : List Dependency) (enhanced : Dependency) : Option EnhancementType

Classify an enhanced edge by what type of enhancement it represents.

Equations

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

theorem DepGrammar.EnhancedDependencies.coord_enhancement_classified : classifyEnhancement DepGrammar.EnhancedDependencies.coordBasicTree✝.deps { headIdx := 3, depIdx := 4, depType := UD.DepRel.obj } = some EnhancementType.coordSharedDep

The enhanced edge in the coordination example is classified as coordSharedDep.

theorem DepGrammar.EnhancedDependencies.control_enhancement_classified : classifyEnhancement controlBasicTree.deps { headIdx := 3, depIdx := 0, depType := UD.DepRel.nsubj } = some EnhancementType.controlSubject

The enhanced edge in the control example is classified as controlSubject.