de Marneffe and Nivre (2019): Dependency grammar

This file formalizes the formal claims of the review of dependency grammar in [dMN19] on the library's dependency graphs, whose projectivity is that of [KN06]. A dependency tree is a spanning tree over the words of a sentence, §2.4, and its projectivity has two formulations the review takes as equivalent, that every word between the endpoints of an arc is dominated by the arc's head and that the yield of every subtree is a contiguous substring; Figure 3 is nonprojective on both counts. Dependency trees are insensitive to word order, §3.1, so the two orders of (1) are one graph relabelled along a rotation of the positions. Dependency length, §3.2, explains the preference for (2a) over (2b) and its absence between (3a) and (3b), the minimization of [Beh32] and [Tem07], and the object relative (4a) of [Gib98] holds its filler at a longer distance than the subject relative (4b). Universal Dependencies, §4, puts content words above function words, Figure 4b against the function-word-headed Figure 4a, the function words attaching to the content word with which they form a nucleus in the sense of [Tes59], so that the content-word skeleton of a sentence is shared across languages, Figure 7; its basic representation is a tree and its enhanced representation a general graph, in which the subject of Figure 9 has three heads and lies on a cycle, §4.4.

Implementation notes

The review's figures carry traditional grammatical-function labels, its footnote 2; the fixtures use their Universal Dependencies counterparts, and the function-word-headed arcs of Figure 4a, for which UD has no relation, carry dep. Punctuation is dropped from (1) so that its two orders are exactly a rotation. The coreference relation of Figure 9's enhanced graph is not in the library's relation inventory and is omitted; the multiple heads and the cycle do not depend on it. The word strings and bubble trees of Figure 2, the nuclei of Figure 5 and the three label inventories of Figure 6 are not representable on a single-labelled graph over words and are not formalized.

References

• [dMN19]
• [KN06]
• [Beh32]
• [Tem07]
• [Gib98]
• [Tes59]

Dependency trees and projectivity, §2.4

def DeMarneffeNivre2019.fig1 : DependencyGrammar.Tree 5

Figure 1: small dogs chase cats happily.

Equations

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

def DeMarneffeNivre2019.fig3 : DependencyGrammar.Tree 4

Figure 3: bigger dogs than mine.

Equations

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

theorem DeMarneffeNivre2019.fig3_not_isArcProjective : ¬fig3.IsArcProjective

Figure 3 is nonprojective: dogs lies between the head bigger and its dependent mine without being dominated by bigger.

theorem DeMarneffeNivre2019.fig3_projection : fig3.projection 0 = [0, 2, 3] ∧ ¬fig3.IsProjective

Equivalently, the yield of bigger is bigger than mine, not a contiguous substring.

Insensitivity to word order, §3.1

def DeMarneffeNivre2019.ex1a : DependencyGrammar.Tree 9

(1a) While it was snowing, I went for a run.

Equations

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

def DeMarneffeNivre2019.ex1b : DependencyGrammar.Tree 9

(1b) I went for a run, while it was snowing.

Equations

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

theorem DeMarneffeNivre2019.ex1b_eq_map : ex1b.toGraph = ex1a.map (Equiv.addRight 5)

§3.1: the two orders of (1) have identical dependency representations: (1b) is (1a) relabelled along the rotation of the positions by five.

Dependency length, §3.2

def DeMarneffeNivre2019.ex2a : DependencyGrammar.Tree 8

(2a) She threw out the bin with old trash.

Equations

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

def DeMarneffeNivre2019.ex2b : DependencyGrammar.Tree 8

(2b) She threw the bin with old trash out.

Equations

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

def DeMarneffeNivre2019.ex3a : DependencyGrammar.Tree 5

(3a) She threw out the bin.

Equations

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

def DeMarneffeNivre2019.ex3b : DependencyGrammar.Tree 5

(3b) She threw the bin out.

Equations

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

theorem DeMarneffeNivre2019.particle_shift_length : ex2b.totalLength - ex2a.totalLength = 4 ∧ ex3b.totalLength - ex3a.totalLength = 1

§3.2: postposing the particle lengthens the dependencies of threw by four words with the long object of (2) and by one with the short object of (3), the dependency length minimization of [Tem07] behind the preference for (2a) and its absence in (3).

def DeMarneffeNivre2019.ex4a : DependencyGrammar.Tree 9

(4a) The reporter who the senator attacked admitted the error.

Equations

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

def DeMarneffeNivre2019.ex4b : DependencyGrammar.Tree 9

(4b) The reporter who attacked the senator admitted the error.

Equations

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

theorem DeMarneffeNivre2019.relative_filler_distance : (↑(ex4a.headOf 2)).dist 2 = 3 ∧ (↑(ex4b.headOf 2)).dist 2 = 1

(4): who depends on attacked in both relatives, three positions away in the object relative (4a) and adjacent in the subject relative (4b), the locality of [Gib98] behind the object-relative penalty.

Universal Dependencies, §4

def DeMarneffeNivre2019.IsFunctionWord : UD.UPOS → Prop

Function words in the sense of §2.5 and §4: adpositions, auxiliaries, conjunctions, determiners and particles.

Equations

• DeMarneffeNivre2019.IsFunctionWord UD.UPOS.ADP = True
• DeMarneffeNivre2019.IsFunctionWord UD.UPOS.AUX = True
• DeMarneffeNivre2019.IsFunctionWord UD.UPOS.CCONJ = True
• DeMarneffeNivre2019.IsFunctionWord UD.UPOS.DET = True
• DeMarneffeNivre2019.IsFunctionWord UD.UPOS.PART = True
• DeMarneffeNivre2019.IsFunctionWord UD.UPOS.SCONJ = True
• DeMarneffeNivre2019.IsFunctionWord x✝ = False

@[instance_reducible]

instance DeMarneffeNivre2019.instDecidablePredUPOSIsFunctionWord : DecidablePred IsFunctionWord

Equations

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

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

§4.5: content words are higher in the tree than function words: a function word heads nothing but the further parts of a fixed expression.

Equations

• DeMarneffeNivre2019.ContentWordsHigher g = ∀ (v w : Fin n) (r : UD.DepRel), g.label v w = some r → DeMarneffeNivre2019.IsFunctionWord (g.words v).cat → r = UD.DepRel.fixed

@[instance_reducible]

instance DeMarneffeNivre2019.instDecidableContentWordsHigher {n : ℕ} (g : DependencyGrammar.Graph n) : Decidable (ContentWordsHigher g)

Equations

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

@[reducible, inline]

abbrev DeMarneffeNivre2019.fig4Words : List Morphology.Word

The words of Figure 4, Sue believes that Kim will rely on her.

Equations

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

def DeMarneffeNivre2019.fig4a : DependencyGrammar.Tree 8

Figure 4a: function words as heads.

Equations

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

def DeMarneffeNivre2019.fig4b : DependencyGrammar.Tree 8

Figure 4b: content words as heads, as in Universal Dependencies.

Equations

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

theorem DeMarneffeNivre2019.fig4_contentWordsHigher : ContentWordsHigher fig4b.toGraph ∧ ¬ContentWordsHigher fig4a.toGraph

Figure 4: the content-word-headed tree satisfies §4.5's principle and the function-word-headed tree does not, that, will and on heading will, rely and her.

def DeMarneffeNivre2019.fig7en : DependencyGrammar.Tree 10

Figure 7, English: the dog will chase the cat out of the room.

Equations

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

def DeMarneffeNivre2019.fig7fi : DependencyGrammar.Tree 4

Figure 7, Finnish: koira jahtaa kissan huoneesta, the relations marked by case.

Equations

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

def DeMarneffeNivre2019.IsContentSkeleton {m n : ℕ} (t : Fin m → Fin n) (g₁ : DependencyGrammar.Graph m) (g₂ : DependencyGrammar.Graph n) : Prop

g₁ is the content-word skeleton of g₂ along t: t maps the positions of g₁ onto the content words of g₂ and preserves every relation among them, the solid arcs of Figure 7.

Equations

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

theorem DeMarneffeNivre2019.fig7_parallel : IsContentSkeleton ![1, 3, 5, 9] fig7fi.toGraph fig7en.toGraph ∧ ContentWordsHigher fig7en.toGraph

Figure 7: Finnish, which marks the relations by case, is the content-word skeleton of the English sentence, which marks them by function words and word order, and the English function words attach below their content words: the core structure is parallel, §4.

@[reducible, inline]

abbrev DeMarneffeNivre2019.fig9Words : List Morphology.Word

The words of Figure 9, Students who forgot to come failed the oral and written exam.

Equations

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

def DeMarneffeNivre2019.fig9 : DependencyGrammar.Tree 12

Figure 9, the basic representation: a spanning tree.

Equations

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

def DeMarneffeNivre2019.fig9Enhanced : DependencyGrammar.Graph 12

Figure 9, the enhanced representation: the relative pronoun's subject relation gives way to one from forgot to students, the controlled subject of come is made explicit, and the modifier relation is propagated to written.

Equations

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

theorem DeMarneffeNivre2019.fig9Enhanced_not_isTree : ¬fig9Enhanced.IsTree ∧ (fig9Enhanced.parents 0).card = 3 ∧ Relation.TransGen fig9Enhanced.Adj 0 0

§4.4: the enhanced representation is a general graph: students has three heads and lies on a cycle, heading forgot through the relative clause and headed by it as its subject.

theorem DeMarneffeNivre2019.fig9_unrepresented : DependencyGrammar.HasUnrepresentedArg fig9.toGraph fig9Enhanced 0 ∧ DependencyGrammar.HasUnrepresentedArg fig9.toGraph fig9Enhanced 9

The enhanced graph gives students and written relations the basic tree leaves implicit.