de Marneffe & Nivre 2019: UD enhanced dependencies for English LD and coordination

[dMN19]

Worked English examples illustrating Universal Dependencies' basic vs enhanced representations (cf. §4.2 and Figure 9 of [dMN19]). Enhanced graphs are built by adding the extra arcs with Graph.enhance; per UD v2, coordinators attach via cc to the conjunct they introduce.

Examples

Long-distance dependencies

• exWhatDidJohnSee, exWhoSawMary, exWhoDidJohnSee — wh-question fixtures (object extraction, subject question, object with who).
• exTheBookThatJohnRead / _enhanced — object relative clause and its enhanced graph.
• exJohnThinksThatMarySleeps, exJohnThinksMarySleeps, exJohnWondersIfMarySleeps, exJohnWondersWhatMarySaw — complement clauses with and without overt complementizer, with and without embedded extraction.

Coordination

• exJohnAndMarySleep, exJohnSleepsAndMarySleeps — NP and S coordination (no shared-dependent propagation needed).
• exJohnSeesAndHearsMary / _enhanced — VP coordination; the enhanced graph adds obj from hears to Mary.
• exHappyAndSmartBoy — adjective coordination.
• exRNR / _enhanced — Right Node Raising; the enhanced graph adds obj to the second-conjunct verb.

Implementation notes

Fixtures use Word.mk' (featureless) except the wh-words; the worked theorems are structural (Graph.IsTree, arc labels, decide).

Wh-question fixtures

def DeMarneffeNivre2019.exWhatDidJohnSee : DependencyGrammar.Graph 4

"What did John see?" — object wh-question (basic tree). Words: what(0) did(1) John(2) see(3). The wh-word attaches as obj of the main verb.

Equations

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

def DeMarneffeNivre2019.exWhoSawMary : DependencyGrammar.Graph 3

"Who saw Mary?" — subject wh-question (no gap needed).

Equations

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

def DeMarneffeNivre2019.exWhoDidJohnSee : DependencyGrammar.Graph 4

"Who did John see?" — object wh-question with who.

Equations

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

Relative-clause fixtures

def DeMarneffeNivre2019.exTheBookThatJohnRead : DependencyGrammar.Graph 5

"the book that John read" — object relative clause (basic tree). In UD the relative clause attaches via acl from head noun to RC verb; the gap (book as obj of read) is implicit.

Equations

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

def DeMarneffeNivre2019.exTheBookThatJohnRead_enhanced : DependencyGrammar.Graph 5

Enhanced graph for "the book that John read": book is added as obj of read.

Equations

• DeMarneffeNivre2019.exTheBookThatJohnRead_enhanced = DeMarneffeNivre2019.exTheBookThatJohnRead.enhance [(4, 1, UD.DepRel.obj)]

Complement-clause fixtures

def DeMarneffeNivre2019.exJohnThinksThatMarySleeps : DependencyGrammar.Graph 5

"John thinks that Mary sleeps" — that-complement (no gap).

Equations

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

def DeMarneffeNivre2019.exJohnThinksMarySleeps : DependencyGrammar.Graph 4

"John thinks Mary sleeps" — bare complement (that-omission, no gap).

Equations

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

def DeMarneffeNivre2019.exJohnWondersIfMarySleeps : DependencyGrammar.Graph 5

"John wonders if Mary sleeps" — if-complement (no gap).

Equations

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

def DeMarneffeNivre2019.exJohnWondersWhatMarySaw : DependencyGrammar.Graph 5

"John wonders what Mary saw" — embedded wh-question. Words: John(0) wonders(1) what(2) Mary(3) saw(4).

Equations

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

Coordination fixtures

def DeMarneffeNivre2019.exJohnAndMarySleep : DependencyGrammar.Graph 4

"John and Mary sleep" — NP coordination.

Equations

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

def DeMarneffeNivre2019.exJohnSleepsAndMarySleeps : DependencyGrammar.Graph 5

"John sleeps and Mary sleeps" — S coordination.

Equations

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

def DeMarneffeNivre2019.exJohnSeesAndHearsMary : DependencyGrammar.Graph 5

"John sees and hears Mary" — VP coordination (basic tree). Mary attaches as obj of sees only; hears is conj of sees.

Equations

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

def DeMarneffeNivre2019.exJohnSeesAndHearsMary_enhanced : DependencyGrammar.Graph 5

Enhanced graph for "John sees and hears Mary": Mary is obj of both sees and hears (shared-dep propagation).

Equations

• DeMarneffeNivre2019.exJohnSeesAndHearsMary_enhanced = DeMarneffeNivre2019.exJohnSeesAndHearsMary.enhance [(3, 4, UD.DepRel.obj)]

def DeMarneffeNivre2019.exHappyAndSmartBoy : DependencyGrammar.Graph 5

"the happy and smart boy" — adjective coordination.

Equations

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

def DeMarneffeNivre2019.exRNR : DependencyGrammar.Graph 6

"John likes and Mary hates pizza" — Right Node Raising (basic tree). pizza attaches to likes only.

Equations

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

def DeMarneffeNivre2019.exRNR_enhanced : DependencyGrammar.Graph 6

Enhanced graph for RNR: pizza is obj of both verbs.

Equations

• DeMarneffeNivre2019.exRNR_enhanced = DeMarneffeNivre2019.exRNR.enhance [(4, 5, UD.DepRel.obj)]

def DeMarneffeNivre2019.ConjunctsCatMatch {n : ℕ} (g : DependencyGrammar.Graph n) : Prop

Conjuncts share their category — the parallelism constraint on coordination ([dMN19] §4.2), study-locally.

Equations

• DeMarneffeNivre2019.ConjunctsCatMatch g = ∀ (v w : Fin n), g.label v w = some UD.DepRel.conj → (g.words v).cat = (g.words w).cat

@[instance_reducible]

instance DeMarneffeNivre2019.instDecidableConjunctsCatMatch {n : ℕ} (g : DependencyGrammar.Graph n) : Decidable (ConjunctsCatMatch g)

Equations

• DeMarneffeNivre2019.instDecidableConjunctsCatMatch g = DeMarneffeNivre2019.instDecidableConjunctsCatMatch._aux_1 g

Worked theorems — long-distance dependencies

theorem DeMarneffeNivre2019.whatDidJohnSee_has_wh : (exWhatDidJohnSee.words 0).features.isWh = true

Object wh-questions have a [wh] filler at position 0.

theorem DeMarneffeNivre2019.relclause_enhancement : exTheBookThatJohnRead_enhanced.label 4 1 = some UD.DepRel.obj ∧ exTheBookThatJohnRead.label 4 1 = none

The enhanced graph for "the book that John read" has the obj-gap arc; the basic tree lacks it.

theorem DeMarneffeNivre2019.relclause_gap_recovered : DependencyGrammar.HasUnrepresentedArg exTheBookThatJohnRead exTheBookThatJohnRead_enhanced 1

book gains an unrepresented argument — the gap made explicit.

theorem DeMarneffeNivre2019.relclause_enhanced_not_tree : ¬exTheBookThatJohnRead_enhanced.IsTree ∧ exTheBookThatJohnRead.IsTree

The enhanced relclause graph violates tree-hood (book now has two heads), per [dMN19] §4.4; the basic tree is a tree.

Worked theorems — coordination

theorem DeMarneffeNivre2019.johnAndMary_cat_match : ConjunctsCatMatch exJohnAndMarySleep

theorem DeMarneffeNivre2019.johnSleepsAndMarySleeps_cat_match : ConjunctsCatMatch exJohnSleepsAndMarySleeps

theorem DeMarneffeNivre2019.happyAndSmart_cat_match : ConjunctsCatMatch exHappyAndSmartBoy

theorem DeMarneffeNivre2019.coord_enhancement : exJohnSeesAndHearsMary_enhanced.label 3 4 = some UD.DepRel.obj ∧ exJohnSeesAndHearsMary.label 3 4 = none

Shared-dependent propagation adds the missing obj arc from hears to Mary; the basic tree lacks it.

theorem DeMarneffeNivre2019.coord_gap_recovered : DependencyGrammar.HasUnrepresentedArg exJohnSeesAndHearsMary exJohnSeesAndHearsMary_enhanced 4

Mary gains an unrepresented argument in the enhanced graph.

theorem DeMarneffeNivre2019.coord_enhanced_not_tree : ¬exJohnSeesAndHearsMary_enhanced.IsTree ∧ exJohnSeesAndHearsMary.IsTree

The enhanced coordination graph violates tree-hood; the basic tree is a tree.

theorem DeMarneffeNivre2019.rnr_enhancement : exRNR_enhanced.label 4 5 = some UD.DepRel.obj ∧ ¬exRNR_enhanced.IsTree

RNR enhancement propagates obj to the second-conjunct verb, and the result is no longer a tree.