Coordination Parallelism and Sharing

@cite{osborne-2019}

Formalizes @cite{osborne-2019}'s analysis of coordination: conjuncts must have parallel structure, shared dependents form catenae, and the CSC falls out from the parallelism requirement.

Sharing Types

• Forward sharing: left-edge shared ("John [eats and drinks] beer")
• Backward sharing: right-edge shared / RNR ("John likes and Mary hates [pizza]")
• Symmetric: both edges shared (rare)

Key Insight

All types of shared material in coordination form catenae. Gapping in coordination is just catena-ellipsis. The CSC follows from requiring symmetric (ATB) extraction — asymmetric extraction violates parallelism.

Bridges

• → Coordination.lean: extends with sharing type classification; reuses ex_rnr, checkCatMatch, checkArgStrMatch
• → Catena.lean: shared material forms catenae (proven)
• → Ellipsis.lean: gapping = catena-ellipsis in coordination
• → Phenomena/Ellipsis/Gapping.lean: gapping direction ↔ sharing direction

inductive DepGrammar.CoordinationParallelism.SharingType : Type

Types of shared material in coordination (@cite{osborne-2019}, Ch 10).

• forward : SharingType
• backward : SharingType
• symmetric : SharingType
• none_ : SharingType

def DepGrammar.CoordinationParallelism.instReprSharingType.repr : SharingType → ℕ → Std.Format

Equations

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

instance DepGrammar.CoordinationParallelism.instReprSharingType : Repr SharingType

Equations

• DepGrammar.CoordinationParallelism.instReprSharingType = { reprPrec := DepGrammar.CoordinationParallelism.instReprSharingType.repr }

instance DepGrammar.CoordinationParallelism.instDecidableEqSharingType : DecidableEq SharingType

Equations

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

def DepGrammar.CoordinationParallelism.parallelConjuncts (t : DepTree) (c1 c2 : ℕ) : Bool

Check if two conjuncts have parallel core argument structure. Parallel = same set of core argument relations (nsubj, obj, iobj) from head, ignoring coordination-specific (conj, cc) and function-word (aux, mark, det) relations which don't affect parallelism. @cite{osborne-2019}.

Equations

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

def DepGrammar.CoordinationParallelism.sharedDepTypes (t : DepTree) (c1 c2 : ℕ) : List UD.DepRel

Get shared dependents between two conjuncts: deps that have the same depType in both heads. Returns the depTypes that are shared.

Equations

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

def DepGrammar.CoordinationParallelism.ex_forwardSharing : DepTree

Forward sharing: "John eats and drinks beer" Words: John(0) eats(1) and(2) drinks(3) beer(4) Deps: eats(1) → John(0:nsubj), eats(1) → drinks(3:conj), eats(1) → beer(4:obj), drinks(3) → and(2:cc) Shared = {John(0)} — nsubj of eats, implicitly of drinks too. @cite{osborne-2019}.

Equations

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

def DepGrammar.CoordinationParallelism.ex_forwardSharing_enhanced : DepGraph

Enhanced graph for forward sharing: John is nsubj of both eats AND drinks.

Equations

• DepGrammar.CoordinationParallelism.ex_forwardSharing_enhanced = DepGrammar.Coordination.enhanceSharedDeps DepGrammar.CoordinationParallelism.ex_forwardSharing

def DepGrammar.CoordinationParallelism.ex_gapping_preEllipsis : DepTree

Gapping-as-coordination: "Fred eats beans and Jim rice" Words: Fred(0) eats(1) beans(2) and(3) Jim(4) rice(5) This is the pre-gapping tree. Gapping elides the second "eats". In UD: eats(1) → Fred(0:nsubj), eats(1) → beans(2:obj), eats(1) → eats_implied(→ orphan structure). We model the pre-gapping version with full second clause: eats(1) → Fred(0:nsubj), eats(1) → beans(2:obj), eats(1) → Jim(4:conj:orphan parent), Jim(4) → rice(5:orphan). But UD uses orphan for gapping; we model the pre-ellipsis tree instead.

Equations

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

def DepGrammar.CoordinationParallelism.ex_atbExtraction : DepTree

ATB extraction: "What did John buy and Mary sell?" Words: what(0) did(1) John(2) buy(3) and(4) Mary(5) sell(6) Deps: buy(3) → John(2:nsubj), buy(3) → what(0:obj), buy(3) → did(1:aux), buy(3) → sell(6:conj), sell(6) → Mary(5:nsubj), sell(6) → and(4:cc) Symmetric extraction from both conjuncts — grammatical. @cite{osborne-2019}.

Equations

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

def DepGrammar.CoordinationParallelism.ex_atbExtraction_enhanced : DepGraph

Enhanced ATB: what is obj of BOTH buy and sell.

Equations

• DepGrammar.CoordinationParallelism.ex_atbExtraction_enhanced = DepGrammar.Coordination.enhanceSharedDeps DepGrammar.CoordinationParallelism.ex_atbExtraction

theorem DepGrammar.CoordinationParallelism.forwardSharing_shared_is_catena : Catena.isCatena ex_forwardSharing.deps [0] = true

In forward sharing, the shared subject {John(0)} is trivially a catena.

theorem DepGrammar.CoordinationParallelism.rnr_shared_is_catena : Catena.isCatena Coordination.ex_rnr.deps [5] = true

In RNR (Coordination.ex_rnr), the shared object {pizza(5)} is a catena.

theorem DepGrammar.CoordinationParallelism.gapping_shared_verb_is_catena : Catena.isCatena ex_gapping_preEllipsis.deps [1] = true

In gapping, the shared verb {eats(1)} is a catena (links to both clauses).

theorem DepGrammar.CoordinationParallelism.atb_shared_is_catena : Catena.isCatena ex_atbExtraction.deps [0] = true

In ATB extraction, the shared object {what(0)} is a catena.

theorem DepGrammar.CoordinationParallelism.gapping_conjuncts_parallel : parallelConjuncts ex_gapping_preEllipsis 1 4 = true

Gapping conjuncts are parallel: both eats(1) and eats(4) have the same set of dependency relations (nsubj, obj).

theorem DepGrammar.CoordinationParallelism.atb_conjuncts_parallel_enhanced : have enhanced := ex_atbExtraction_enhanced; have t := { words := enhanced.words, deps := enhanced.deps, rootIdx := enhanced.rootIdx }; parallelConjuncts t 3 6 = true

ATB conjuncts are parallel in the enhanced graph: buy(3) and sell(6) both have nsubj and obj after shared dep propagation.

def DepGrammar.CoordinationParallelism.isATBExtraction (enhanced : DepGraph) (fillerIdx : ℕ) (conjuncts : List ℕ) : Bool

Check if extraction from coordination is across-the-board (ATB): the filler is an argument of ALL conjuncts in the enhanced graph. @cite{osborne-2019}: asymmetric extraction violates parallelism.

Equations

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

def DepGrammar.CoordinationParallelism.cscViolation (enhanced : DepGraph) (fillerIdx : ℕ) (conjuncts : List ℕ) : Bool

Check if extraction violates the CSC: extracted from some but not all conjuncts.

Equations

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

theorem DepGrammar.CoordinationParallelism.atb_extraction_is_atb : isATBExtraction ex_atbExtraction_enhanced 0 [3, 6] = true

ATB extraction in "What did John buy and Mary sell?" is ATB: what(0) is obj of both buy(3) and sell(6) in the enhanced graph.

theorem DepGrammar.CoordinationParallelism.atb_no_csc_violation : cscViolation ex_atbExtraction_enhanced 0 [3, 6] = false

ATB extraction does NOT violate the CSC.

theorem DepGrammar.CoordinationParallelism.coordination_cat_match_preserved : Coordination.checkCatMatch ex_gapping_preEllipsis = true ∧ Coordination.checkCatMatch ex_atbExtraction = true

Bridge → Coordination.lean: category matching still holds for all our coordination examples.

theorem DepGrammar.CoordinationParallelism.gapping_argstr_match : Coordination.checkArgStrMatch ex_gapping_preEllipsis = true

Bridge → Coordination.lean: argument structure matching holds for gapping (both verbs are transitive).

theorem DepGrammar.CoordinationParallelism.forward_sharing_enhanced_propagates : (ex_forwardSharing_enhanced.deps.any fun (d : Dependency) => d.headIdx == 3 && d.depIdx == 0 && d.depType == UD.DepRel.nsubj) = true

Bridge → Coordination.lean: enhanced graph propagates shared deps.

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

Bridge → Coordination.ex_rnr: RNR enhanced graph has shared obj.

theorem DepGrammar.CoordinationParallelism.all_shared_are_catenae : Catena.isCatena ex_forwardSharing.deps [0] = true ∧ Catena.isCatena Coordination.ex_rnr.deps [5] = true ∧ Catena.isCatena ex_gapping_preEllipsis.deps [1] = true ∧ Catena.isCatena ex_atbExtraction.deps [0] = true

Bridge → Catena.lean: all shared material in coordination forms catenae — singletons are trivially connected.

theorem DepGrammar.CoordinationParallelism.gapping_is_catena_ellipsis : Catena.isCatena ex_gapping_preEllipsis.deps [1] = true ∧ Catena.isCatena Ellipsis.gappingTree.deps [0] = true

Bridge → Ellipsis.lean: gapping is catena-ellipsis in coordination. The gapped verb is a singleton catena, just like in Ellipsis.gappingElided.