Mildly Non-Projective Dependency Structures

@cite{kuhlmann-nivre-2006} @cite{kuhlmann-2013} @cite{mueller-2013}

Formalizes the structural theory of non-projectivity from:

• @cite{kuhlmann-nivre-2006}. Mildly Non-Projective Dependency Structures. COLING/ACL 2006, pp. 507–514.
• @cite{kuhlmann-2013}. Mildly Non-Projective Dependency Grammar. Computational Linguistics 39(2):355–387.
• @cite{mueller-2013}. Unifying Everything. Language 89(4):920–950.
• @cite{hudson-1984}. Word Grammar.

Core Concepts

Five structural constraints on dependency trees, ordered by restrictiveness:

projective ⊂ planar ⊂ well-nested ⊂ unrestricted

• Projective: every projection is an interval (gap degree 0, block-degree 1)
• Planar: no edges cross when drawn above the sentence
• Well-nested: no two disjoint subtrees interleave
• Gap degree: max number of discontinuities in any node's projection
• Block-degree: max number of contiguous blocks (= gap degree + 1 = LCFRS fan-out)
• Edge degree: max number of non-dominated components spanned by any edge

Key Results

• Well-nestedness + gap degree ≤ 1 covers 99.89% of PDT and DDT (@cite{kuhlmann-nivre-2006} Table 1)
• Block-degree = fan-out of extracted LCFRS grammar
• Bounded block-degree + well-nestedness → polynomial parsing (@cite{kuhlmann-2013}, Lemma 10)

Bridges

• → Core/Basic.lean: projection, isProjective, gaps, blocks, gapDegreeAt, blockDegreeAt
• → Catena.lean: blocks are special catenae (contiguous, connected)
• → Discontinuity.lean: risen catenae witness non-projectivity
• → DependencyLength.lean: non-projective orderings tend to longer dep length

def DepGrammar.depsCross (d1 d2 : Dependency) : Bool

Two dependencies cross iff their spans overlap without containment. (@cite{kuhlmann-nivre-2006}, implicit in Definition 4)

Equations

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

def DepGrammar.nonProjectiveDeps (t : DepTree) : List Dependency

All non-projective (crossing) dependencies in a tree.

Equations

• DepGrammar.nonProjectiveDeps t = List.filter (fun (d1 : DepGrammar.Dependency) => t.deps.any fun (d2 : DepGrammar.Dependency) => DepGrammar.depsCross d1 d2) t.deps

def DepGrammar.isNonProjectiveDep (t : DepTree) (d : Dependency) : Bool

Whether a specific dependency crosses other arcs in the tree.

Equations

• DepGrammar.isNonProjectiveDep t d = t.deps.any fun (d2 : DepGrammar.Dependency) => DepGrammar.depsCross d d2

def DepGrammar.hasFillerGap (t : DepTree) : Bool

Whether a tree has any non-projective dependencies.

Equations

• DepGrammar.hasFillerGap t = decide ((DepGrammar.nonProjectiveDeps t).length > 0)

structure DepGrammar.FillerGapDep : Type

A filler-gap dependency is a non-projective dependency modelling extraction.

In DG, wh-fronting creates crossing arcs — the analogue of:

• Minimalism: Internal Merge (movement)
• HPSG: SLASH feature propagation + Head-Filler discharge
• CCG: function composition for extraction

• dep : Dependency
• tree : DepTree
• inTree : self.dep ∈ self.tree.deps
• nonProj : isNonProjectiveDep self.tree self.dep = true

def DepGrammar.linked (deps : List Dependency) (a b : ℕ) : Bool

Whether two positions are linked by an edge (in either direction).

Equations

• DepGrammar.linked deps a b = deps.any fun (d : DepGrammar.Dependency) => d.headIdx == a && d.depIdx == b || d.headIdx == b && d.depIdx == a

def DepGrammar.DepTree.isPlanar (t : DepTree) : Bool

A dependency tree is planar if its edges can be drawn above the sentence without crossing. Formally: no nodes a < b < c < d with linked(a,c) ∧ linked(b,d).

(@cite{kuhlmann-nivre-2006}, Definition 4; traced to @cite{melcuk-1988})

Equations

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

def DepGrammar.projectionsInterleave (p1 p2 : List ℕ) : Bool

Two subtrees interleave if there exist nodes l₁, r₁ in T₁ and l₂, r₂ in T₂ such that l₁ < l₂ < r₁ < r₂. (@cite{kuhlmann-nivre-2006}, Definition 8)

Equations

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

def DepGrammar.disjoint (deps : List Dependency) (u v : ℕ) : Bool

Two nodes are disjoint if neither dominates the other — i.e., neither appears in the other's projection.

Equations

• DepGrammar.disjoint deps u v = (!(DepGrammar.projection deps u).contains v && !(DepGrammar.projection deps v).contains u)

def DepGrammar.DepTree.isWellNested (t : DepTree) : Bool

A dependency tree is well-nested if no two disjoint subtrees interleave. (@cite{kuhlmann-nivre-2006}, Definition 8)

Equivalent to: no sibling nodes u, v have blocks ū₁, ū₂ of u and v̄₁, v̄₂ of v such that ū₁ < v̄₁ < ū₂ < v̄₂ (@cite{kuhlmann-2013}, Lemma 9).

Equations

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

def DepGrammar.edgeSpan (d : Dependency) : List ℕ

The span of an edge (i, j): the interval [min(i,j), max(i,j)].

Equations

• DepGrammar.edgeSpan d = List.map (fun (x : ℕ) => x + min d.headIdx d.depIdx) (List.range (max d.headIdx d.depIdx - min d.headIdx d.depIdx + 1))

def DepGrammar.edgeDegreeOf (deps : List Dependency) (d : Dependency) (fuel : ℕ) : ℕ

The degree of an edge e: the number of connected components in the subgraph induced by span(e) whose root is NOT dominated by head(e). (@cite{kuhlmann-nivre-2006}, Definition 9)

Edge degree measures intervening "foreign" material within an arc's span.

Equations

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

def DepGrammar.DepTree.edgeDegree (t : DepTree) : ℕ

Edge degree of a tree: max edge degree over all edges. (@cite{kuhlmann-nivre-2006}, Definition 9) Edge degree 0 ⟺ projective.

Equations

• t.edgeDegree = List.foldl max 0 (List.map (fun (x : DepGrammar.Dependency) => DepGrammar.edgeDegreeOf t.deps x (t.words.length + 1)) t.deps)

def DepGrammar.isWellFormedNonProj (t : DepTree) : Bool

Relaxed well-formedness allowing non-projective dependencies. Drops the projectivity constraint from isWellFormed.

Equations

• DepGrammar.isWellFormedNonProj t = (DepGrammar.hasUniqueHeads t && DepGrammar.isAcyclic t && DepGrammar.checkSubjVerbAgr t && DepGrammar.checkDetNounAgr t && DepGrammar.checkVerbSubcat t)

theorem DepGrammar.nonProj_implies_structural (t : DepTree) : isWellFormedNonProj t = true → hasUniqueHeads t = true ∧ isAcyclic t = true

Non-projective well-formedness implies unique heads and acyclicity.

theorem DepGrammar.projective_implies_nonProj_wf (t : DepTree) : isWellFormed t = true → isWellFormedNonProj t = true

Projective well-formedness implies non-projective well-formedness.

Figure 3 examples: gap degree, edge degree, well-nestedness

def DepGrammar.kn_fig3a : DepTree

@cite{kuhlmann-nivre-2006} Figure 3a: gd=0, ed=0, well-nested. 6 nodes, edges form nested (projective) structure. j(0) ← 4(root) i(1) ← 0 2 ← 1, 3 ← 1, 4 ← 1 → 5

Equations

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

def DepGrammar.kn_fig3b : DepTree

@cite{kuhlmann-nivre-2006} Figure 3b: gd=1, ed=1, well-nested. Node i has projection [2, 3, 6] — one gap at (3, 6). 1 ← 0(root), 2 ← 1, 3 ← 2, 4 ← 1 → 5, 2 → 6

Equations

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

def DepGrammar.kn_fig3c : DepTree

@cite{kuhlmann-nivre-2006} Figure 3c: gd=2, ed=1, NOT well-nested. Nodes i and j have interleaving projections. i at 1: projection includes {2, 4}; j at 2: includes {3, 5} These interleave: 2 < 3 < 4 < 5.

Equations

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

def DepGrammar.nonProjectiveTree : DepTree

Minimal crossing tree: arcs 0→2 and 1→3 cross.

Equations

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

Cross-serial dependencies (@cite{kuhlmann-2013}, Figure 1)

The canonical motivation for non-projectivity. In Dutch, verb–argument dependencies cross ("cross-serial"), producing a non-projective tree. In German, the same dependencies nest, producing a projective tree.

Dutch: dat Jan₁ Piet₂ Marie₃ zag₁ helpen₂ lezen₃ German: dass Jan₁ Piet₂ Marie₃ lesen₃ helfen₂ sah₁

def DepGrammar.dutchCrossSerial : DepTree

Dutch cross-serial: "dat Jan Piet Marie zag helpen lezen" Dependencies: zag→Jan, helpen→Piet, lezen→Marie These cross: zag(4)→Jan(1) spans helpen(5)→Piet(2).

Equations

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

def DepGrammar.germanNested : DepTree

German nested: "dass Jan Piet Marie lesen helfen sah" Same dependencies, but verbs are in reverse order → nested, projective.

Equations

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

Projectivity

Gap degree and block-degree (Core/Basic.lean)

Planarity

Well-nestedness

theorem DepGrammar.projective_iff_gapDegree_zero (t : DepTree) : isProjective t = true ↔ t.gapDegree = 0

Projective ⟺ gap degree 0: a tree is projective iff no node's projection has any gaps. (@cite{kuhlmann-nivre-2006}, Definition 3 + Definition 7)

theorem DepGrammar.projective_iff_blockDegree_one (t : DepTree) (hne_tree : t.words.length > 0) : isProjective t = true ↔ t.blockDegree = 1

Projective ⟺ block-degree 1: every node has exactly one block. Requires at least one word (blockDegree of empty tree is 0, not 1).

Proof: projective ↔ gap degree 0 (Theorem 1). When gap degree = 0, every gapDegreeAt = 0, so by blocks_length = gaps_length + 1, every blockDegreeAt = 1, so foldl max 0 = 1.

theorem DepGrammar.blockDegree_eq_gapDegree_succ (deps : List Dependency) (root : ℕ) : blockDegreeAt deps root = gapDegreeAt deps root + 1

Block-degree = gap degree + 1 for non-empty projections. (@cite{kuhlmann-2013}, §7.1 footnote 2)

theorem DepGrammar.projective_implies_planar (t : DepTree) (hwf : t.WF) (hacyc : isAcyclic t = true) (hproj : isProjective t = true) : t.isPlanar = true

Projective ⊂ planar (for well-formed trees): every projective tree with unique heads and no cycles is planar. (@cite{kuhlmann-nivre-2006}, §3.5: projectivity implies no crossing edges)

The hasUniqueHeads precondition is necessary: without it, a node can have two heads, and the resulting multi-headed graph can be projective (all projections are intervals) yet non-planar (edges cross).

Counterexample without hasUniqueHeads: 4 nodes, edges (0,1), (0,2), (1,2), (1,3). Node 2 has two heads (0 and 1). All projections are intervals, but linked(0,2) and linked(1,3) cross.

The isAcyclic precondition is necessary: without it, hasUniqueHeads allows cycles (e.g., edges (1,2),(2,1) with root=0), and the dominance antisymmetry argument fails.

Proof: by contrapositive. If ¬planar, there exist a < b < c < d with edges linking a–c and b–d. Each edge endpoint pair shares a projection (the head's). Projectivity makes that projection an interval. The interval containing {a, c} must contain b; the interval containing {b, d} must contain c. With unique heads, dominates_to_parent lifts the intermediate dominance to the other edge's head, creating a dominance cycle v→w→v. By dominates_antisymm (acyclicity), v = w, contradicting v < w.

theorem DepGrammar.planar_implies_wellNested (t : DepTree) (hwf : t.WF) (hplanar : t.isPlanar = true) : t.isWellNested = true

Planar ⊂ well-nested (for well-formed trees): every planar tree with unique heads is well-nested. (@cite{kuhlmann-nivre-2006}, Theorem 1)

Proof: by contrapositive. If ¬wellNested, there exist disjoint subtrees u, v whose projections interleave: l₁ < l₂ < r₁ < r₂ with l₁, r₁ ∈ π(u) and l₂, r₂ ∈ π(v). By interleaving_not_planar, this forces crossing edges, contradicting planarity.

theorem DepGrammar.wellNested_not_projective_witness : dutchCrossSerial.isWellNested = true ∧ isProjective dutchCrossSerial = false

Dutch cross-serial witnesses the gap: non-projective yet well-nested. (@cite{kuhlmann-nivre-2006}, §4: 99.89% of treebank data is well-nested)

theorem DepGrammar.not_wellNested_witness : nonProjectiveTree.isWellNested = false ∧ nonProjectiveTree.isPlanar = false

The minimal crossing tree witnesses: not well-nested and not planar.

theorem DepGrammar.nonProjective_implies_gapDeg_ge1 (t : DepTree) (h : isProjective t = false) : t.gapDegree ≥ 1

Non-projective dependencies → gap degree ≥ 1. Contrapositive of projective_iff_gapDegree_zero.

theorem DepGrammar.dutch_mildly_nonProjective : isProjective dutchCrossSerial = false ∧ dutchCrossSerial.isWellNested = true ∧ dutchCrossSerial.gapDegree = 1

Dutch cross-serial is non-projective but well-nested with gap degree 1. This exemplifies K&N's key finding: the vast majority of non-projective structures in treebanks are well-nested with low gap degree.

theorem DepGrammar.german_fully_projective : isProjective germanNested = true ∧ germanNested.gapDegree = 0

German nested is fully projective (gap degree 0), confirming that the nested verb order avoids crossing dependencies.