inductive DepGrammar.LongDistance.GapType : Type

What type of element is missing in the gap

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

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

Equations

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

instance DepGrammar.LongDistance.instReprGapType : Repr GapType

Equations

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

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.instInhabitedGapType.default : GapType

Equations

• DepGrammar.LongDistance.instInhabitedGapType.default = DepGrammar.LongDistance.GapType.subjGap

instance DepGrammar.LongDistance.instInhabitedGapType : Inhabited GapType

Equations

• DepGrammar.LongDistance.instInhabitedGapType = { default := DepGrammar.LongDistance.instInhabitedGapType.default }

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

Convert GapType to UD dependency relation

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

structure DepGrammar.LongDistance.SLASH : Type

SLASH feature: tracks what's missing V/NP means "verb phrase missing a noun phrase"

• gapType : Option GapType

def DepGrammar.LongDistance.instReprSLASH.repr : SLASH → ℕ → Std.Format

Equations

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

instance DepGrammar.LongDistance.instReprSLASH : Repr SLASH

Equations

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

instance DepGrammar.LongDistance.instDecidableEqSLASH : DecidableEq SLASH

Equations

• DepGrammar.LongDistance.instDecidableEqSLASH = DepGrammar.LongDistance.instDecidableEqSLASH.decEq

def DepGrammar.LongDistance.instDecidableEqSLASH.decEq (x✝ x✝¹ : SLASH) : Decidable (x✝ = x✝¹)

Equations

• DepGrammar.LongDistance.instDecidableEqSLASH.decEq { gapType := a } { gapType := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

inductive DepGrammar.LongDistance.IslandType : Type

Island constraint types

• complex_NP : IslandType
• coordinate : IslandType
• adjunct : IslandType
• subject : IslandType

instance DepGrammar.LongDistance.instReprIslandType : Repr IslandType

Equations

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

def DepGrammar.LongDistance.instReprIslandType.repr : IslandType → ℕ → Std.Format

Equations

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

instance DepGrammar.LongDistance.instDecidableEqIslandType : DecidableEq IslandType

Equations

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

def DepGrammar.LongDistance.instInhabitedIslandType.default : IslandType

Equations

• DepGrammar.LongDistance.instInhabitedIslandType.default = DepGrammar.LongDistance.IslandType.complex_NP

instance DepGrammar.LongDistance.instInhabitedIslandType : Inhabited IslandType

Equations

• DepGrammar.LongDistance.instInhabitedIslandType = { default := DepGrammar.LongDistance.instInhabitedIslandType.default }

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

Check if a position is inside an island (simplified). Works on a DepTree directly.

Equations

• DepGrammar.LongDistance.isInsideIsland 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

Validate that no extraction site is inside an island. Takes explicit filler-gap pairs as (fillerIdx, gapHostIdx, gapType).

Equations

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

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

Fill a gap by adding an argument edge to the enhanced graph. The fillerIdx word becomes a dependent of gapHostIdx with the relation corresponding to gapType.

Equations

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

def DepGrammar.LongDistance.fillGaps (t : DepTree) (gaps : List (ℕ × ℕ × GapType)) : DepGraph

Fill multiple gaps at once.

Equations

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

def DepGrammar.LongDistance.getSLASH (basic : DepTree) (enhanced : DepGraph) (nodeIdx : ℕ) : SLASH

Get SLASH feature at a node by comparing basic tree vs enhanced graph. If the enhanced graph has an argument edge to a word that the basic tree doesn't, that word has a SLASH feature.

Equations

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

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

A long-distance dependency tree is well-formed if:

1. Structural constraints (unique heads, acyclicity, projectivity, agreement)
2. No island violations
3. Fillers are wh-words, fronted, or relative clause heads Note: checkVerbSubcat is omitted because LD trees inherently have argument gaps (the whole point of long-distance dependencies).

Equations

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

def DepGrammar.LongDistance.ex_whatDidJohnSee : DepTree

"What did John see?" - Object wh-question (basic tree). Words: what(0) did(1) John(2) see(3) In UD, the wh-word attaches as obj of the main verb.

Equations

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

def DepGrammar.LongDistance.ex_whoSawMary : DepTree

"Who saw Mary?" - Subject wh-question (no gap needed).

Equations

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

def DepGrammar.LongDistance.ex_whoDidJohnSee : DepTree

"Who did John see?" - Object wh-question with "who".

Equations

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

def DepGrammar.LongDistance.ex_theBookThatJohnRead : DepTree

"the book that John read" - Object relative clause (basic tree). Words: the(0) book(1) that(2) John(3) read(4) In UD, the relative clause attaches via acl from head noun to RC verb. The gap (book as obj of read) is implicit.

Equations

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

def DepGrammar.LongDistance.ex_theBookThatJohnRead_enhanced : DepGraph

Enhanced graph for "the book that John read" — gap filled. Book (1) is added as obj of read (4).

Equations

• DepGrammar.LongDistance.ex_theBookThatJohnRead_enhanced = DepGrammar.LongDistance.fillGap DepGrammar.LongDistance.ex_theBookThatJohnRead 1 4 DepGrammar.LongDistance.GapType.objGap

def DepGrammar.LongDistance.ex_theBookThatJohnGaveMary : DepTree

"the book that John gave Mary" - Object relative with ditransitive.

Equations

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

def DepGrammar.LongDistance.ex_johnThinksThatMarySleeps : DepTree

"John thinks that Mary sleeps" - That-complement (no gap).

Equations

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

def DepGrammar.LongDistance.ex_johnThinksMarySleeps : DepTree

"John thinks Mary sleeps" - Bare complement (that-omission, no gap).

Equations

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

def DepGrammar.LongDistance.ex_johnWondersIfMarySleeps : DepTree

"John wonders if Mary sleeps" - If-complement (no gap).

Equations

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

def DepGrammar.LongDistance.ex_johnWondersWhatMarySaw : DepTree

"John wonders what Mary saw" - Embedded wh-question. Words: john(0) wonder(1) what(2) mary(3) sees(4)

Equations

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

theorem DepGrammar.LongDistance.whatDidJohnSee_has_wh : Option.map (fun (x : Word) => x.features.wh) ex_whatDidJohnSee.words[0]? = some true

Object wh-questions have wh-word at index 0.

theorem DepGrammar.LongDistance.whoSawMary_no_gap : isLDWellFormed ex_whoSawMary [] = true

Subject wh-questions don't need gaps (empty gap list).

theorem DepGrammar.LongDistance.relclause_enhanced_has_obj : (ex_theBookThatJohnRead_enhanced.deps.any fun (d : Dependency) => d.headIdx == 4 && d.depIdx == 1 && d.depType == UD.DepRel.obj) = true

Enhanced graph for relative clause has the filled gap edge.

theorem DepGrammar.LongDistance.relclause_basic_lacks_obj : ¬(ex_theBookThatJohnRead.deps.any fun (d : Dependency) => d.headIdx == 4 && d.depIdx == 1 && d.depType == UD.DepRel.obj) = true

The basic tree of "the book that John read" does NOT have this obj edge.

theorem DepGrammar.LongDistance.relclause_enhanced_more_edges : ex_theBookThatJohnRead_enhanced.deps.length > ex_theBookThatJohnRead.deps.length

Enhanced graph has more edges than the basic tree.

theorem DepGrammar.LongDistance.relclause_enhanced_not_tree : hasUniqueHeads { words := ex_theBookThatJohnRead_enhanced.words, deps := ex_theBookThatJohnRead_enhanced.deps, rootIdx := ex_theBookThatJohnRead_enhanced.rootIdx } = false

Enhanced graph violates unique-heads (book has edges from both det and obj).

theorem DepGrammar.LongDistance.relclause_basic_is_tree : hasUniqueHeads ex_theBookThatJohnRead = true

The basic tree IS a tree (unique heads).

theorem DepGrammar.LongDistance.relclause_slash_derived : getSLASH ex_theBookThatJohnRead ex_theBookThatJohnRead_enhanced 1 = { gapType := some GapType.objGap }

SLASH derivation: book (1) gets an obj SLASH from comparing basic vs enhanced.

theorem DepGrammar.LongDistance.complement_no_gap : checkNoIslandViolation ex_johnThinksThatMarySleeps [] = true

Complement clauses have no filler-gap dependencies.