inductive DepGrammar.Coordination.ConjType : Type

Conjunction types

• and_ : ConjType
• or_ : ConjType
• but_ : ConjType

instance DepGrammar.Coordination.instReprConjType : Repr ConjType

Equations

• DepGrammar.Coordination.instReprConjType = { reprPrec := DepGrammar.Coordination.instReprConjType.repr }

def DepGrammar.Coordination.instReprConjType.repr : ConjType → ℕ → Std.Format

Equations

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

instance DepGrammar.Coordination.instDecidableEqConjType : DecidableEq ConjType

Equations

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

instance DepGrammar.Coordination.instInhabitedConjType : Inhabited ConjType

Equations

• DepGrammar.Coordination.instInhabitedConjType = { default := DepGrammar.Coordination.instInhabitedConjType.default }

def DepGrammar.Coordination.instInhabitedConjType.default : ConjType

Equations

• DepGrammar.Coordination.instInhabitedConjType.default = DepGrammar.Coordination.ConjType.and_

def DepGrammar.Coordination.getConjuncts (t : DepTree) (headIdx : ℕ) : List ℕ

Get conjuncts of a head: words linked by conj edges from headIdx.

Equations

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

def DepGrammar.Coordination.checkCatMatch (t : DepTree) : Bool

Check that for every conj edge, the conjuncts have matching categories.

Equations

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

def DepGrammar.Coordination.checkArgStrMatch (t : DepTree) : Bool

For verbal conj edges, check that conjuncts have matching argument structures.

Equations

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

def DepGrammar.Coordination.enhanceSharedDeps (t : DepTree) : DepGraph

Enhance a basic tree by propagating shared dependents from first conjunct to all other conjuncts. For each conj edge head→dep, propagates obj/nsubj/iobj edges from head to dep. Returns a DepGraph (multiple heads per word).

Equations

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

def DepGrammar.Coordination.ex_johnAndMarySleep : DepTree

"John and Mary sleep" - NP coordination. Words: John(0) and(1) Mary(2) sleep(3) Basic tree is sufficient — no shared deps needed.

Equations

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

def DepGrammar.Coordination.ex_johnSleepsAndMarySleeps : DepTree

"John sleeps and Mary sleeps" - S coordination. Words: John(0) sleeps(1) and(2) Mary(3) sleeps(4)

Equations

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

def DepGrammar.Coordination.ex_johnSeesAndHearsMary : DepTree

"John sees and hears Mary" - VP coordination (basic tree). Words: John(0) sees(1) and(2) hears(3) Mary(4) Mary attaches as obj of sees only. Hears is conj of sees.

Equations

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

def DepGrammar.Coordination.ex_johnSeesAndHearsMary_enhanced : DepGraph

Enhanced graph for "John sees and hears Mary". Mary is obj of BOTH sees and hears — the shared dep is propagated.

Equations

• DepGrammar.Coordination.ex_johnSeesAndHearsMary_enhanced = DepGrammar.Coordination.enhanceSharedDeps DepGrammar.Coordination.ex_johnSeesAndHearsMary

def DepGrammar.Coordination.ex_oldAndWiseMan : DepTree

"the old and wise man" - Adjective coordination. Words: the(0) happy(1) and(2) smart(3) boy(4)

Equations

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

def DepGrammar.Coordination.ex_rnr : DepTree

"John likes and Mary hates pizza" - Right Node Raising. Words: John(0) devours(1) and(2) Mary(3) devours(4) pizza(5) Pizza attaches to devours(1) only in the basic tree.

Equations

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

def DepGrammar.Coordination.ex_rnr_enhanced : DepGraph

Enhanced graph for RNR: pizza is obj of both verbs.

Equations

• DepGrammar.Coordination.ex_rnr_enhanced = DepGrammar.Coordination.enhanceSharedDeps DepGrammar.Coordination.ex_rnr

theorem DepGrammar.Coordination.johnAndMary_cat_match : checkCatMatch ex_johnAndMarySleep = true

NP coordination has matching categories.

theorem DepGrammar.Coordination.johnSleepsAndMarySleeps_cat_match : checkCatMatch ex_johnSleepsAndMarySleeps = true

S coordination has matching categories.

theorem DepGrammar.Coordination.seesAndHears_argstr_match : checkArgStrMatch ex_johnSeesAndHearsMary = true

VP coordination has matching argument structures.

theorem DepGrammar.Coordination.oldAndWise_cat_match : checkCatMatch ex_oldAndWiseMan = true

Adjective coordination has matching categories.

theorem DepGrammar.Coordination.enhanced_has_shared_obj : (ex_johnSeesAndHearsMary_enhanced.deps.any fun (d : Dependency) => d.headIdx == 3 && d.depIdx == 4 && d.depType == UD.DepRel.obj) = true

enhanceSharedDeps produces a graph with the missing obj edge from hears to Mary.

theorem DepGrammar.Coordination.basic_lacks_shared_obj : ¬(ex_johnSeesAndHearsMary.deps.any fun (d : Dependency) => d.headIdx == 3 && d.depIdx == 4 && d.depType == UD.DepRel.obj) = true

The basic tree does NOT have this edge.

theorem DepGrammar.Coordination.enhanced_more_edges : ex_johnSeesAndHearsMary_enhanced.deps.length > ex_johnSeesAndHearsMary.deps.length

Enhanced graph has more edges than the basic tree.

theorem DepGrammar.Coordination.enhanced_not_tree : hasUniqueHeads { words := ex_johnSeesAndHearsMary_enhanced.words, deps := ex_johnSeesAndHearsMary_enhanced.deps, rootIdx := ex_johnSeesAndHearsMary_enhanced.rootIdx } = false

Enhanced graph violates unique-heads — it's genuinely a graph, not a tree. Mary (idx 4) has two incoming obj edges (from sees and hears).

theorem DepGrammar.Coordination.basic_is_tree : hasUniqueHeads ex_johnSeesAndHearsMary = true

The basic tree IS a tree (unique heads).

theorem DepGrammar.Coordination.rnr_enhanced_has_shared_obj : (ex_rnr_enhanced.deps.any fun (d : Dependency) => d.headIdx == 4 && d.depIdx == 5 && d.depType == UD.DepRel.obj) = true

RNR enhancement propagates obj to second conjunct.

theorem DepGrammar.Coordination.rnr_enhanced_not_tree : hasUniqueHeads { words := ex_rnr_enhanced.words, deps := ex_rnr_enhanced.deps, rootIdx := ex_rnr_enhanced.rootIdx } = false

RNR enhanced graph violates unique-heads.