Kuhlmann (2013): Mildly Non-Projective Dependency Grammar

This file formalizes the structural side of [Kuh13], which reads lexicalized linear context-free rewriting systems as dependency grammars and measures the non-projectivity that parsing them has to pay for. The fan-out of a rule extracted from a treebank is the block-degree of its head, one more than the substrate's gap degree (blockDegree), so projectivity is block-degree one (isProjective_iff_blockDegree_eq_one). Well-nestedness, which makes parsing polynomial through binarization, fails exactly when two sibling nodes have interleaving yields (not_isWellNested_iff_siblings, the paper's Lemma 9 in the substrate's terms). The Dutch and German verb clusters of Figure 1 separate the projective from the non-projective order while keeping the dependencies fixed, and the trees of Figures 10 and 11 witness block-degrees 2 and 3 and the independence of well-nestedness from block-degree.

The treebank counts of Tables 3 and 4 are the rows of Data/Treebank/Coverage/Kuhlmann2013.json, over which the paper's percentages are recomputed: fan-out 1 loses between 11.16% and 23.15% of the trees (treeLoss_projective), allowing fan-out 2 recovers more than 94% of the lost rules and trees (reduction_gapDegreeLe1), and adding well-nestedness still recovers more than 92% of the rules (reduction_wellNested).

Implementation notes

Positions are zero-based, so node i of a figure is position i - 1. The substrate's Graph.IsWellNested is the paper's definition under the paper's own gloss: yields may overlap only when one node dominates the other. Block-degree is the gap degree plus one, as the paper's footnote on gap-degree observes. Percentages are recomputed from the rows as rounded hundredths of a percent, the precision the paper prints. The lexicalized LCFRS machinery, canonical grammars, the parsing algorithm, and the NP-hardness result are not formalized.

TODO

• Table 3 prints 5,839 rules for Arabic, on which the fan-out 1 loss of 411 rules is 7.04%, not the 0.74% the paper states; the printed value is kept and Arabic is excluded from ruleLoss_projective.
• The paper gives Turkish's well-nested rule-loss reduction as 92.65%; the rows give 92.64%.

Block-degree (§7.1)

def Kuhlmann2013.blockDegree {n : ℕ} (g : DependencyGrammar.Graph n) : ℕ

The block-degree of a graph: the maximal number of blocks a node's yield falls into, one more than the gap degree.

Equations

• Kuhlmann2013.blockDegree g = g.gapDegree + 1

theorem Kuhlmann2013.isProjective_iff_blockDegree_eq_one {n : ℕ} {g : DependencyGrammar.Graph n} : g.IsProjective ↔ blockDegree g = 1

A tree is projective iff its block-degree is 1.

Well-nestedness (§8.1)

theorem Kuhlmann2013.not_isWellNested_iff_siblings {n : ℕ} {g : DependencyGrammar.Graph n} (hT : g.IsTree) : ¬g.IsWellNested ↔ ∃ (p : Fin n) (u : Fin n) (v : Fin n), g.Adj p u ∧ g.Adj p v ∧ u ≠ v ∧ g.Interleave u v

Lemma 9: a tree is ill-nested iff two sibling nodes have interleaving yields.

Figure 1: nested against cross-serial

The German order nests the verb–argument dependencies and is projective; the Dutch order crosses them and is not, at gap degree 1.

def Kuhlmann2013.dutchCrossSerial : DependencyGrammar.Graph 7

Dutch cross-serial: dat Jan Piet Marie zag helpen lezen.

Equations

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

def Kuhlmann2013.germanNested : DependencyGrammar.Graph 7

German nested: dass Jan Piet Marie lesen helfen sah.

Equations

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

theorem Kuhlmann2013.dutchCrossSerial_isTree : dutchCrossSerial.IsTree

theorem Kuhlmann2013.germanNested_isTree : germanNested.IsTree

theorem Kuhlmann2013.figure1_projectivity : ¬dutchCrossSerial.IsProjective ∧ germanNested.IsProjective

The cross-serial order is non-projective and the nested order is projective.

theorem Kuhlmann2013.figure1_blockDegree : blockDegree dutchCrossSerial = 2 ∧ blockDegree germanNested = 1

Block-degree 2 against block-degree 1: the fan-out the extracted rule for zag needs.

theorem Kuhlmann2013.dutchCrossSerial_isWellNested : dutchCrossSerial.IsWellNested ∧ ¬dutchCrossSerial.IsPlanar

Cross-serial dependencies are well-nested, though not planar.

Figures 10 and 11: block-degree and well-nestedness

def Kuhlmann2013.dot : Morphology.Word

An unlabelled position.

Equations

• Kuhlmann2013.dot = Morphology.Word.mk' "•" UD.UPOS.X

def Kuhlmann2013.fig10D1 : DependencyGrammar.Graph 6

Figure 10, D₁: the yield of node 2 falls into the blocks {2, 3} and {6}.

Equations

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

def Kuhlmann2013.fig10D2 : DependencyGrammar.Graph 6

Figure 10, D₂: the yield of node 1 falls into the blocks {1}, {3} and {6}.

Equations

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

theorem Kuhlmann2013.figure10_blockDegree : blockDegree fig10D1 = 2 ∧ blockDegree fig10D2 = 3

Block-degrees 2 and 3 (Example 6).

def Kuhlmann2013.fig11D1 : DependencyGrammar.Graph 4

Figure 11, D₁: non-projective with no overlapping yields at all.

Equations

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

def Kuhlmann2013.fig11D2 : DependencyGrammar.Graph 4

Figure 11, D₂: the yields of nodes 1 and 2 overlap, but node 1 dominates node 2.

Equations

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

def Kuhlmann2013.fig11D3 : DependencyGrammar.Graph 5

Figure 11, D₃: the yields of the sibling nodes 2 and 3 overlap.

Equations

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

theorem Kuhlmann2013.figure11_wellNested : (fig11D1.IsWellNested ∧ ¬fig11D1.IsProjective) ∧ fig11D2.IsWellNested ∧ ¬fig11D2.IsProjective

Both well-nested trees of Figure 11 are non-projective (Example 8).

theorem Kuhlmann2013.fig11D2_interleave : fig11D2.Interleave 0 1 ∧ DependencyGrammar.Dominates fig11D2 0 1

In D₂ the overlapping yields belong to a node and its descendant.

theorem Kuhlmann2013.fig11D3_not_isWellNested : ¬fig11D3.IsWellNested

D₃ is ill-nested, with the siblings of Lemma 9 at positions 1 and 2.

theorem Kuhlmann2013.figure11_blockDegree : blockDegree fig11D2 = 2 ∧ blockDegree fig11D3 = 2

Well-nestedness is independent of block-degree beyond 1: D₂ and D₃ both have block-degree 2.

Tables 3 and 4: coverage on dependency treebanks (§7.4, §8.4)

@[reducible, inline]

abbrev Kuhlmann2013.rows : List Data.Treebank.Coverage.Row

The rows of Tables 3 and 4.

Equations

• Kuhlmann2013.rows = Data.Treebank.Coverage.Kuhlmann2013.rows

def Kuhlmann2013.lossBp (r : Data.Treebank.Coverage.Row) : ℤ

The loss under a row's constraint, in hundredths of a percent, rounded as the paper prints it.

Equations

• Kuhlmann2013.lossBp r = round ((1 - r.coverage) * 10000)

def Kuhlmann2013.lost (treebank : String) (item : Data.Treebank.Coverage.Item) (c : Data.Treebank.Coverage.Constraint) : ℕ

The items a treebank loses under a constraint.

Equations

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

def Kuhlmann2013.reductionBp (treebank : String) (item : Data.Treebank.Coverage.Item) (c : Data.Treebank.Coverage.Constraint) : ℤ

The reduction in loss under a constraint relative to the fan-out 1 baseline, in hundredths of a percent.

Equations

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

theorem Kuhlmann2013.treeLoss_projective (r : Data.Treebank.Coverage.Row) : r ∈ rows → r.item = Data.Treebank.Coverage.Item.trees → r.constraint = Data.Treebank.Coverage.Constraint.projective → 1116 ≤ lossBp r ∧ lossBp r ≤ 2315

Fan-out 1 loses between 11.16% (Arabic) and 23.15% (Czech) of the trees.

theorem Kuhlmann2013.ruleLoss_projective (r : Data.Treebank.Coverage.Row) : r ∈ rows → r.item = Data.Treebank.Coverage.Item.rules → r.constraint = Data.Treebank.Coverage.Constraint.projective → r.treebank ≠ "Arabic" → 123 ≤ lossBp r ∧ lossBp r ≤ 175

Fan-out 1 loses between 1.23% (Danish) and 1.75% (Slovene) of the rules, Arabic's printed total aside.

theorem Kuhlmann2013.reduction_gapDegreeLe1 (r : Data.Treebank.Coverage.Row) : r ∈ rows → r.constraint = Data.Treebank.Coverage.Constraint.gapDegreeLe 1 → (r.item = Data.Treebank.Coverage.Item.rules → 9416 ≤ reductionBp r.treebank Data.Treebank.Coverage.Item.rules (Data.Treebank.Coverage.Constraint.gapDegreeLe 1) ∧ reductionBp r.treebank Data.Treebank.Coverage.Item.rules (Data.Treebank.Coverage.Constraint.gapDegreeLe 1) ≤ 9976) ∧ (r.item = Data.Treebank.Coverage.Item.trees → 9431 ≤ reductionBp r.treebank Data.Treebank.Coverage.Item.trees (Data.Treebank.Coverage.Constraint.gapDegreeLe 1) ∧ reductionBp r.treebank Data.Treebank.Coverage.Item.trees (Data.Treebank.Coverage.Constraint.gapDegreeLe 1) ≤ 9939)

Allowing fan-out 2 reduces rule loss by 94.16% (Turkish) to 99.76% (Arabic) and tree loss by 94.31% (Turkish) to 99.39% (Arabic).

theorem Kuhlmann2013.czech_gapDegreeLe1 (r : Data.Treebank.Coverage.Row) : r ∈ rows → r.treebank = "Czech" → r.constraint = Data.Treebank.Coverage.Constraint.gapDegreeLe 1 → (r.item = Data.Treebank.Coverage.Item.rules → lossBp r = 2) ∧ (r.item = Data.Treebank.Coverage.Item.trees → lossBp r < 50)

Block-degree 2 costs Czech 0.02% of its rules and under 0.5% of its trees.

theorem Kuhlmann2013.reduction_wellNested (r : Data.Treebank.Coverage.Row) : r ∈ rows → r.constraint = Data.Treebank.Coverage.Constraint.gapDegreeLeWellNested 1 → r.item = Data.Treebank.Coverage.Item.rules → 9264 ≤ reductionBp r.treebank Data.Treebank.Coverage.Item.rules (Data.Treebank.Coverage.Constraint.gapDegreeLeWellNested 1) ∧ reductionBp r.treebank Data.Treebank.Coverage.Item.rules (Data.Treebank.Coverage.Constraint.gapDegreeLeWellNested 1) ≤ 9951

Well-nested rules of fan-out at most 2 still reduce rule loss by more than 92% relative to fan-out 1, up to 99.51% (Arabic).