Long-distance dependencies in UD enhanced graphs

Implements the gap-filling step of Universal Dependencies' enhanced dependency graphs ([dMN19]): the basic tree obeys a unique-heads constraint that loses the predicate–argument relation across a filler–gap configuration, and the enhanced graph recovers it by adding an explicit edge from the gap-host word to the filler.

Main declarations

• GapType — the four core UD argument positions a missing element may fill (subject, object, indirect object, oblique).
• gapToDepRel — the UD DepRel corresponding to a GapType.
• fillGap — enhanced-edge construction: produce a DepGraph from a basic DepTree by appending an edge that records gap-filling.
• extractionLabel — recover the gap-type label at a node by diffing the basic tree against the enhanced graph.
• checkNoIslandViolation — coarse modifier/conjunct heuristic over a list of gap sites; not a full Ross-1967 inventory.
• isLDWellFormed — structural well-formedness plus the coarse island heuristic plus filler-licensing.

Implementation notes

• The Bool-valued predicates follow DepGrammar.isWellFormed's substrate convention; converting them to Prop + Decidable is a substrate-wide refactor not done here.
• hasGapInModifierOrConjunct is deliberately coarse: it flags any gap whose direct head is nmod or conj. It does not recognise CNPC, CSC, adjunct, or subject islands. Richer island handling lives in Syntax/DependencyGrammar/Formal/Islands.lean.
• Word Grammar ([Hud10]) handles the same data with a structurally analogous hopping mechanism; GPSG ([Gaz81]) uses SLASH-feature percolation. Neither is implemented here.

Todo

• Consume the Ross-1967 ConstraintType enum (Studies/Ross1967.lean) here and in Formal/Islands.lean so the two files share a single inventory.
• Build a cross-framework FillerGap abstraction so the RSRL GAP (Syntax/HPSG/Construction), LongDistance.GapType, and Minimalist movement labels all specialise a shared interface.

Gap types and the UD relation map

inductive DepGrammar.LongDistance.GapType : Type

Argument position of the missing element: the four core UD argument relations subject, object, indirect object, and oblique.

• subjGap : GapType
• objGap : GapType
• iobjGap : GapType
• oblGap : GapType

@[implicit_reducible]

instance DepGrammar.LongDistance.instReprGapType : Repr GapType

Equations

• DepGrammar.LongDistance.instReprGapType = { reprPrec := DepGrammar.LongDistance.instReprGapType.repr }

def DepGrammar.LongDistance.instReprGapType.repr : GapType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance DepGrammar.LongDistance.instDecidableEqGapType : DecidableEq GapType

Equations

• DepGrammar.LongDistance.instDecidableEqGapType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DepGrammar.LongDistance.gapToDepRel : GapType → UD.DepRel

The UD DepRel corresponding to a GapType.

Equations

• DepGrammar.LongDistance.gapToDepRel DepGrammar.LongDistance.GapType.subjGap = UD.DepRel.nsubj
• DepGrammar.LongDistance.gapToDepRel DepGrammar.LongDistance.GapType.objGap = UD.DepRel.obj
• DepGrammar.LongDistance.gapToDepRel DepGrammar.LongDistance.GapType.iobjGap = UD.DepRel.iobj
• DepGrammar.LongDistance.gapToDepRel DepGrammar.LongDistance.GapType.oblGap = UD.DepRel.obl

Enhanced-edge construction

def DepGrammar.LongDistance.fillGap (t : DepTree) (fillerIdx gapHostIdx : ℕ) (gapType : GapType) : DepGraph

Add a single enhanced edge to t: the filler becomes a dependent of the gap host with the UD relation corresponding to gapType.

Equations

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

def DepGrammar.LongDistance.extractionLabel (basic : DepTree) (enhanced : DepGraph) (nodeIdx : ℕ) : Option GapType

Recover the gap-type label at nodeIdx by diffing basic against enhanced: returns the first enhanced-only argument-shaped edge's GapType, or none.

Equations

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

Island heuristic and well-formedness

def DepGrammar.LongDistance.hasGapInModifierOrConjunct (t : DepTree) (gapIdx : ℕ) : Bool

Coarse check: does the word at gapIdx head an nmod or conj relation. This does not recognise any of the four classical Ross-1967 islands.

Equations

• DepGrammar.LongDistance.hasGapInModifierOrConjunct t gapIdx = t.deps.any fun (d : DepGrammar.Dependency) => (d.depType == UD.DepRel.nmod || d.depType == UD.DepRel.conj) && d.depIdx == gapIdx

def DepGrammar.LongDistance.checkNoIslandViolation (t : DepTree) (gaps : List (ℕ × ℕ × GapType)) : Bool

No gap is reported inside the coarse modifier/conjunct heuristic.

Equations

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

def DepGrammar.LongDistance.isLDWellFormed (t : DepTree) (gaps : List (ℕ × ℕ × GapType)) : Bool

Combined well-formedness for trees with long-distance gaps: substrate tree-level checks (minus checkVerbSubcat, since LD trees inherently have argument gaps), the coarse island heuristic, and filler-licensing (wh-word, leftward topicalization, or relative-clause head).

Equations

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