Coordination in UD enhanced graphs

Implements coordination in Universal Dependencies' enhanced-dependency graphs ([dMN19], §4.2 and Figure 9, applied to coordinate structures): the basic dependency tree attaches each shared dependent to the first conjunct only, and the enhanced graph recovers the parallel attachments by propagating obj / nsubj / iobj edges from the first-conjunct head to every other conjunct.

Word Grammar ([Hud10], §7.5.4 "Non-constituent coordination") handles the same data via a different device: a contiguous string of words may be treated as a single chunk ("word string") and entered into a dependency relation as a whole, eliminating the need to propagate shared dependents. For the historical phrase-structure approach to coordination (Coordinate Structure Constraint, ATB extraction as theorems of a complex-symbol grammar), see [Gaz81].

Main declarations

• getConjuncts, hasConjuncts, allConjuncts — inspect the conjunct structure of a head node in a basic dependency tree.
• checkCatMatch — verifies that every conj edge connects words of matching UPOS categories.
• checkArgStrMatch — for verbal conj edges, verifies matching valence.
• enhanceSharedDeps — produce a DepGraph from a basic DepTree by propagating shared obj / nsubj / iobj edges from the first conjunct's head to each subsequent conjunct.

Implementation notes

• The Bool-valued predicates follow DepGrammar's substrate convention; migrating to Prop + Decidable is a substrate-wide refactor not done here.
• Paper-replication fixtures and worked theorems for enhanceSharedDeps live in Studies/DeMarneffeNivre2019.lean. Downstream substrate consumers (Formal/EnhancedDependencies.lean, Formal/CoordinationParallelism.lean) define their own local minimal fixtures.
• checkArgStrMatch is a coarse heuristic over DepTree.frames. Real coordination-parallelism judgements (gapping, ATB extraction) live in Formal/CoordinationParallelism.lean.

Coordinate structure

def DepGrammar.Coordination.getConjuncts (t : DepTree) (headIdx : ℕ) : List ℕ

Conjuncts of a head: words linked by conj edges from headIdx. In UD basic-tree convention these are the second-and-later conjuncts; the first conjunct is headIdx.

Equations

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

def DepGrammar.Coordination.hasConjuncts (t : DepTree) (i : ℕ) : Bool

Word i heads a coordinate structure iff it has at least one outgoing conj edge.

Equations

• DepGrammar.Coordination.hasConjuncts t i = decide ¬(DepGrammar.Coordination.getConjuncts t i).isEmpty = true

def DepGrammar.Coordination.allConjuncts (t : DepTree) (headIdx : ℕ) : List ℕ

All conjuncts of a coordinate structure headed at headIdx: headIdx itself (first conjunct, which heads the structure in UD basic-tree convention) plus the words linked via conj.

Equations

• DepGrammar.Coordination.allConjuncts t headIdx = headIdx :: DepGrammar.Coordination.getConjuncts t headIdx

Parallelism heuristics

def DepGrammar.Coordination.checkCatMatch (t : DepTree) : Bool

Every conj edge connects words of matching UPOS categories.

Equations

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

def DepGrammar.Coordination.checkArgStrMatch (t : DepTree) : Bool

For verbal conj edges, conjuncts have matching frames. Coarse heuristic — does not handle clausal coordination (ccomp / xcomp) or finer subcategorization.

Equations

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

UD enhanced-edge construction

def DepGrammar.Coordination.enhanceSharedDeps (t : DepTree) : DepGraph

Enhance a basic tree by propagating shared dependents from the first conjunct to all subsequent conjuncts. For each conj edge head→dep, propagates the head's obj / nsubj / iobj edges to dep. Returns a DepGraph (words may have multiple incoming edges). Cf. [dMN19] Figure 9 for the relative-clause analogue.

Equations

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