Enhanced dependencies

[dMN19]

Basic dependency trees enforce a unique-heads constraint: every word (except root) has exactly one head, so certain predicate-argument relations that hold semantically cannot be represented as tree edges — shared dependents in coordination, controlled subjects, and relative-clause gaps are the canonical cases. Enhanced dependencies relax the tree to a directed graph in which words may have multiple heads.

Main declarations

• EnhancementType — coarse classification of an enhanced edge.
• hasUnrepresentedArg — a word has an argument relation in the enhanced graph that the basic tree fails to encode.
• classifyEnhancement — assign an EnhancementType to an enhanced edge.

Implementation notes

Predicate-shape definitions inherit the substrate-wide Bool convention; statements use ... = true / = false. Worked fixtures for the three phenomena (coordination, control, relative-clause gap) are kept minimal — feature-rich Word payloads were dropped because the theorems are structural. Coordination.enhanceSharedDeps is the bridge used to build the coordination enhanced graph; the control and relative-clause graphs are stipulated.

Enhancement classification

inductive DepGrammar.EnhancedDependencies.EnhancementType : Type

The kind of implicit relation an enhanced edge makes explicit. Each variant corresponds to a phenomenon where the basic tree loses information.

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

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

Equations

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

@[implicit_reducible]

instance DepGrammar.EnhancedDependencies.instReprEnhancementType : Repr EnhancementType

Equations

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

@[implicit_reducible]

instance DepGrammar.EnhancedDependencies.instDecidableEqEnhancementType : DecidableEq EnhancementType

Equations

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

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

A word has an unrepresented argument in the basic tree if it appears as a dependent in the enhanced graph under some head to which the basic tree has no edge.

Equations

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

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

Classify an enhanced edge by what type of enhancement it represents. Returns none when the edge is already in the basic tree.

Equations

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

Coordination fixture: "John sees and hears Mary"

def DepGrammar.EnhancedDependencies.coordBasicTree : DepTree

Equations

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

def DepGrammar.EnhancedDependencies.coordEnhancedGraph : DepGraph

Equations

• DepGrammar.EnhancedDependencies.coordEnhancedGraph = DepGrammar.Coordination.enhanceSharedDeps DepGrammar.EnhancedDependencies.coordBasicTree

Control fixture: "Students forgot to come"

def DepGrammar.EnhancedDependencies.controlBasicTree : DepTree

Equations

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

def DepGrammar.EnhancedDependencies.controlEnhancedGraph : DepGraph

Equations

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

Relative-clause fixture: "the book that John read"

def DepGrammar.EnhancedDependencies.relClauseBasicTree : DepTree

Equations

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

def DepGrammar.EnhancedDependencies.relClauseEnhancedGraph : DepGraph

Equations

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

Basic tree loses information

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

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

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

Enhancement preserves basic edges

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

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

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

Enhanced graphs violate unique-heads

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

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

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

Enhanced edges classify correctly

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

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