Mildly non-projective dependency structures

Formalizes the structural theory of [KN06], [Kuh13], [Mul13]: planarity, well-nestedness, and the hierarchy

projective ⊂ planar ⊂ well-nested ⊂ unrestricted.

The cross-serial / nested verb-cluster pair ([Kuh13] Figure 1) witnesses the gap between projectivity and well-nestedness in attested language data.

Main declarations

• depsCross, linked, disjoint, projectionsInterleave — arc-crossing primitives.
• DepTree.isPlanar, DepTree.isWellNested — the two restrictiveness classes between projective and unrestricted.
• projective_iff_gapDegree_zero, projective_iff_blockDegree_one, blockDegree_eq_gapDegree_succ — equivalences in the hierarchy.
• projective_implies_planar — every well-formed projective tree is planar.
• planar_implies_wellNested — every well-formed planar tree is well-nested.
• nonProjective_implies_gapDeg_ge1 — bridge to Core/Basic.lean's gapDegree.
• dutchCrossSerial, germanNested, nonProjectiveTree — example trees used in Discontinuity.lean, DependencyLength.lean, and Studies/Mueller2013.lean.

Implementation notes

• Predicate-shape definitions return Bool; this matches the substrate-wide DG convention and forces ... = true in theorem statements. A Prop + Decidable refactor is tracked at the substrate level.
• The headline proof planar_implies_wellNested proceeds by contrapositive through interleaving_not_planar, a long chain of private infrastructure lemmas (exists_spanning_edge, escape_gives_crossing, the discrete intermediate-value lemmas find_exit_step / find_entry_step).
• FillerGapDep (a { tree, dep, inTree, nonProj } wrapper formerly here) was dropped — no downstream consumer; the cross-framework "filler-gap" abstraction the prior docstring gestured at belongs in a shared substrate (the LongDistance.lean Todo articulates this), not as a thin subtype here.

Arc-crossing detection

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

Two dependencies cross iff their spans overlap without containment. ([KN06], 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.hasFillerGap (t : DepTree) : Bool

Whether a tree has any non-projective dependencies.

Equations

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

Planarity ([KN06], Definition 4)

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 iff its edges can be drawn above the sentence without crossing: no nodes a < b < c < d with linked a c and linked b d. ([KN06], Definition 4)

Equations

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

Well-nestedness ([KN06], Definition 8)

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

Two projections interleave if there exist l₁, r₁ ∈ p1 and l₂, r₂ ∈ p2 with l₁ < l₂ < r₁ < r₂.

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.

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 nodes have interleaving projections. ([KN06], Definition 8)

Equations

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

Example trees

Cross-serial Dutch and nested German from [Kuh13] Figure 1 — the canonical pair witnessing that mild non-projectivity (well-nested, gap degree 1) covers attested data.

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.

def DepGrammar.dutchCrossSerial : DepTree

Dutch cross-serial: "dat Jan Piet Marie zag helpen lezen". Dependencies zag→Jan, helpen→Piet, lezen→Marie cross.

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 as dutchCrossSerial but verbs in reverse order → projective.

Equations

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

Verified properties of the example trees

Hierarchy theorems

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. ([KN06], 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 for non-empty trees.

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. ([Kuh13], §7.1 footnote 2)

Projective ⊂ planar

The forward direction of the hierarchy. The proof goes by contrapositive: if planarity fails, the four witness nodes generate a dominance cycle via dominates_to_parent, contradicting acyclicity. The hasUniqueHeads precondition is essential — a multi-headed node can be projective yet non-planar.

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. ([KN06], §3.5)

Planar ⊂ well-nested

By contrapositive: an interleaving witness produces a spanning-edge crossing that breaks planarity. The infrastructure below — dominance comparability under unique heads, parent-chain extraction, the discrete IVT-style exit/entry steps — feeds the core interleaving_not_planar lemma.

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

Planar ⊂ well-nested for well-formed trees. ([KN06], Theorem 1)

Bridge to gapDegree

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

Non-projective ⇒ gap degree ≥ 1. Contrapositive of projective_iff_gapDegree_zero.