Coordination parallelism and sharing

Formalizes [Osb19]'s analysis of coordination in dependency grammar: conjuncts have parallel core-argument structure, shared dependents form catenae, and the Coordinate Structure Constraint follows from requiring symmetric (ATB) extraction.

Main declarations

• SharingType — typology of shared material (forward / backward / symmetric / none).
• parallelConjuncts, sharedDepTypes — predicates over a DepTree detecting core-argument parallelism and the shared-dep typeset between two conjunct heads.
• isATBExtraction, cscViolation — Bool predicates over an enhanced DepGraph detecting across-the-board extraction and CSC violations.
• forwardSharing, rnrBasic, gappingPreEllipsis, atbExtraction — worked example trees from Osborne 2019.

Implementation notes

• Predicate-shape definitions inherit the substrate-wide Bool convention; theorems read as ... = true. A project-wide Bool → Prop + [DecidablePred] migration is out of scope here.
• none_ constructor renamed to noSharing to avoid the Option.none clash without the trailing-underscore hack.
• Substrate bridges (Coordination.checkCatMatch, enhanceSharedDeps, Catena.isCatena) are exercised on the example trees; redundant re-statements bundling those checks into single conjunctive theorems have been dropped.

Sharing typology

inductive DepGrammar.CoordinationParallelism.SharingType : Type

Types of shared material in coordination.

• forward : SharingType

  Left-edge sharing: "John [eats and drinks] beer".

• backward : SharingType

  Right-edge sharing (RNR): "John likes and Mary hates [pizza]".

• symmetric : SharingType

  Both edges shared: rare.

• noSharing : SharingType

  No sharing: "John eats and Mary drinks".

@[implicit_reducible]

instance DepGrammar.CoordinationParallelism.instReprSharingType : Repr SharingType

Equations

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

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

Equations

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

@[implicit_reducible]

instance DepGrammar.CoordinationParallelism.instDecidableEqSharingType : DecidableEq SharingType

Equations

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

Parallel structure detection

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

Two conjuncts are parallel when they take the same set of core argument relations (nsubj, obj, iobj), ignoring coordination markers (conj, cc) and function-word relations that don't affect parallelism.

Equations

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

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

The dependency types that appear under both c1 and c2.

Equations

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

Example trees

def DepGrammar.CoordinationParallelism.forwardSharing : DepTree

Forward sharing: "John eats and drinks beer", with John(0) the shared subject of both verbs.

Equations

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

def DepGrammar.CoordinationParallelism.forwardSharingEnhanced : DepGraph

Enhanced graph for forwardSharing: John is nsubj of both verbs.

Equations

• DepGrammar.CoordinationParallelism.forwardSharingEnhanced = DepGrammar.Coordination.enhanceSharedDeps DepGrammar.CoordinationParallelism.forwardSharing

def DepGrammar.CoordinationParallelism.rnrBasic : DepTree

Right-node-raising: "John likes and Mary hates pizza". The basic tree attaches pizza to likes(1) only; enhanceSharedDeps propagates it as obj of hates(4) too.

Equations

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

def DepGrammar.CoordinationParallelism.rnrEnhanced : DepGraph

Enhanced graph for rnrBasic.

Equations

• DepGrammar.CoordinationParallelism.rnrEnhanced = DepGrammar.Coordination.enhanceSharedDeps DepGrammar.CoordinationParallelism.rnrBasic

def DepGrammar.CoordinationParallelism.gappingPreEllipsis : DepTree

Pre-gapping tree for "Fred eats beans and Jim eats rice", with the second eats still overt; downstream gapping treatments elide it.

Equations

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

def DepGrammar.CoordinationParallelism.atbExtraction : DepTree

ATB extraction: "What did John buy and Mary sell?", symmetric extraction of what from both conjuncts.

Equations

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

def DepGrammar.CoordinationParallelism.atbExtractionEnhanced : DepGraph

Enhanced ATB graph: what is obj of both buy and sell.

Equations

• DepGrammar.CoordinationParallelism.atbExtractionEnhanced = DepGrammar.Coordination.enhanceSharedDeps DepGrammar.CoordinationParallelism.atbExtraction

Shared material forms catenae

theorem DepGrammar.CoordinationParallelism.forwardSharing_shared_isCatena : Catena.isCatena forwardSharing.deps [0] = true

theorem DepGrammar.CoordinationParallelism.rnr_shared_isCatena : Catena.isCatena rnrBasic.deps [5] = true

theorem DepGrammar.CoordinationParallelism.gapping_sharedVerb_isCatena : Catena.isCatena gappingPreEllipsis.deps [1] = true

theorem DepGrammar.CoordinationParallelism.atb_shared_isCatena : Catena.isCatena atbExtraction.deps [0] = true

Parallelism

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

Gapping conjuncts are parallel: both verbs take nsubj and obj.

theorem DepGrammar.CoordinationParallelism.atb_conjuncts_parallel_enhanced : have enhanced := atbExtractionEnhanced; 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 and sell both have nsubj and obj after shared-dep propagation.

Coordinate Structure Constraint

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

Extraction is across-the-board when the filler is a dependent of every conjunct in the enhanced graph.

Equations

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

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

Extraction violates the CSC when the filler is 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_isATB : isATBExtraction atbExtractionEnhanced 0 [3, 6] = true

theorem DepGrammar.CoordinationParallelism.atb_no_cscViolation : cscViolation atbExtractionEnhanced 0 [3, 6] = false