Multidominance: Substrate for Shared-Material Syntax

@cite{citko-2014} @cite{wilder-2008}

A multidominance (MD) structure is a syntactic object built once that is structurally accessible from two (or more) dominating nodes. At PF, it linearizes once. MD is one of the two main mechanisms for producing PF-reduced representations (representations where some material is interpreted but not pronounced); the other is ellipsis.

This file is the substrate for MD primitives that any MD-using analysis needs:

• PFReductionMechanism — the two PF-reduction mechanisms (ellipsis vs multidominance);
• MDSharing — bulk vs non-bulk sharing in coordination;
• SharedNode — a multiply-dominated node + its category + whether it is pronounced;
• PFReducedCoordination — a coordinate &P with PF reduction.

Anchored on @cite{citko-2014} (textbook treatment of parallel-Merge MD) and @cite{wilder-2008} (constituent-sharing flavor). The canonical non-paper-specific apparatus; consumers include @cite{citko-gracanin-yuksek-2025}, and (when written) Bachrach-Katzir 2008, Larson 2012, and Belk-Neeleman-Philip 2023 on RNR.

Convention notes

• This file does not commit to a particular MD flavor (parallel-Merge vs constituent-sharing vs 3-D phrase structure). SharedNode records the multiply-dominated node abstractly; specific MD theories instantiate the dominance/sharing relation via their own apparatus.
• MDSharing was renamed from SharingType at 0.230.575 to avoid a bare-name collision with Theories/Syntax/DependencyGrammar/Formal/CoordinationParallelism.lean's SharingType (which classifies extraction symmetry, not constituent sharing).
• UsesMD / UsesEllipsis / UsesBoth are Prop with decidability instances (per feedback_no_intrinsic_bool discipline); decide-checked consumers continue to work.

inductive Minimalist.PFReductionMechanism : Type

The two mechanisms of PF reduction.

Both produce representations where material is interpreted but not pronounced. Economy (Theories/Syntax/Minimalist/Economy.lean) governs the choice between them.

• ellipsis : PFReductionMechanism

  E-feature on a functional head triggers deletion of its complement at PF. The deleted material is built in full during the derivation.

• multidominance : PFReductionMechanism

  A syntactic object is built once and shared between two dominating nodes. Pronounced at one position only.

def Minimalist.instReprPFReductionMechanism.repr : PFReductionMechanism → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprPFReductionMechanism : Repr PFReductionMechanism

Equations

• Minimalist.instReprPFReductionMechanism = { reprPrec := Minimalist.instReprPFReductionMechanism.repr }

@[implicit_reducible]

instance Minimalist.instDecidableEqPFReductionMechanism : DecidableEq PFReductionMechanism

Equations

• Minimalist.instDecidableEqPFReductionMechanism x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Minimalist.MDSharing : Type

How material is shared between conjuncts in an MD coordination.

The empirical motivation is @cite{citko-gracanin-yuksek-2025}: coordinated wh-questions use non-bulk-sharing (individual heads shared), while coordinated sluices use bulk-sharing (entire C' shared). The two sharing modes derive different syntactic and interpretive properties.

NB: name distinguished from Theories/Syntax/DependencyGrammar/Formal/CoordinationParallelism.SharingType (extraction symmetry, not constituent sharing).

• nonBulk : MDSharing

  Individual functional heads shared between conjuncts. Each conjunct remains a separate full phrase; only specific heads (e.g., C, T) are multiply dominated.

• bulk : MDSharing

  An entire constituent is shared between conjuncts. Both conjuncts dominate the same subtree, so they share all material inside it (C, TP, vP, VP, ...).

@[implicit_reducible]

instance Minimalist.instReprMDSharing : Repr MDSharing

Equations

• Minimalist.instReprMDSharing = { reprPrec := Minimalist.instReprMDSharing.repr }

def Minimalist.instReprMDSharing.repr : MDSharing → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Minimalist.instReprMDSharing.repr Minimalist.MDSharing.bulk prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.MDSharing.bulk")).group prec✝

@[implicit_reducible]

instance Minimalist.instDecidableEqMDSharing : DecidableEq MDSharing

Equations

• Minimalist.instDecidableEqMDSharing x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Minimalist.SharedNode : Type

A node shared between two conjuncts in a coordination structure.

The shared node is built once but is structurally accessible from both parent1 and parent2. At PF, it is linearized once.

• node : SyntacticObject

  The multiply dominated node.

• category : Option Cat

  Category of the shared node, when labelled.

• pronounced : Bool

  The shared node has PF content (vs. is silent).

@[implicit_reducible]

instance Minimalist.instReprSharedNode : Repr SharedNode

Equations

• Minimalist.instReprSharedNode = { reprPrec := Minimalist.instReprSharedNode.repr }

def Minimalist.instReprSharedNode.repr : SharedNode → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instDecidableEqSharedNode : DecidableEq SharedNode

Equations

• Minimalist.instDecidableEqSharedNode = Minimalist.instDecidableEqSharedNode.decEq

def Minimalist.instDecidableEqSharedNode.decEq (x✝ x✝¹ : SharedNode) : Decidable (x✝ = x✝¹)

Equations

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

structure Minimalist.PFReducedCoordination : Type

A coordination structure with PF reduction.

Models a coordinate &P where material is either multiply dominated (shared between conjuncts) or elided by an E-feature.

Substrate note (post-MCB Phase 1.0). The conjunct1 / conjunct2 field names are stipulated planar labels at the coord-structure meta-level, NOT inherited from the SO substrate (which is nonplanar via FreeCommMagma — see Minimalist.merge_comm). The first-vs-second conjunct distinction tracked by these fields is a coordination- specific stipulation about which conjunct hosts the shared / deleted material, parallel to BrueningAlKhalaf2020.mergeCoordSymmetry. Phase 2+: harmonize with @cite{citko-2011}'s symmetric-merge multidominance framework, where conjunct ordering is genuinely a multiset operation.

• conjunct1 : SyntacticObject

  First conjunct. Planar label is stipulated at coord-structure level (not inherited from substrate).

• conjunct2 : SyntacticObject

  Second conjunct.

• mechanisms : List PFReductionMechanism

  PF reduction mechanism(s) used.

• sharing : Option MDSharing

  Mode of sharing (for MD structures).

• sharedNodes : List SharedNode

  Nodes that are shared or deleted.

• pfOutput : List String

  PF output after reduction.

def Minimalist.instReprPFReducedCoordination.repr : PFReducedCoordination → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprPFReducedCoordination : Repr PFReducedCoordination

Equations

• Minimalist.instReprPFReducedCoordination = { reprPrec := Minimalist.instReprPFReducedCoordination.repr }

def Minimalist.instDecidableEqPFReducedCoordination.decEq (x✝ x✝¹ : PFReducedCoordination) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Minimalist.instDecidableEqPFReducedCoordination : DecidableEq PFReducedCoordination

Equations

• Minimalist.instDecidableEqPFReducedCoordination = Minimalist.instDecidableEqPFReducedCoordination.decEq

def Minimalist.PFReducedCoordination.UsesMD (c : PFReducedCoordination) : Prop

Does this coordination use multidominance?

Equations

• c.UsesMD = (Minimalist.PFReductionMechanism.multidominance ∈ c.mechanisms)

@[implicit_reducible]

instance Minimalist.PFReducedCoordination.instDecidableUsesMD (c : PFReducedCoordination) : Decidable c.UsesMD

Equations

• c.instDecidableUsesMD = id inferInstance

def Minimalist.PFReducedCoordination.UsesEllipsis (c : PFReducedCoordination) : Prop

Does this coordination use ellipsis?

Equations

• c.UsesEllipsis = (Minimalist.PFReductionMechanism.ellipsis ∈ c.mechanisms)

@[implicit_reducible]

instance Minimalist.PFReducedCoordination.instDecidableUsesEllipsis (c : PFReducedCoordination) : Decidable c.UsesEllipsis

Equations

• c.instDecidableUsesEllipsis = id inferInstance

def Minimalist.PFReducedCoordination.UsesBoth (c : PFReducedCoordination) : Prop

Does this coordination use both MD and ellipsis?

Equations

• c.UsesBoth = (c.UsesMD ∧ c.UsesEllipsis)

@[implicit_reducible]

instance Minimalist.PFReducedCoordination.instDecidableUsesBoth (c : PFReducedCoordination) : Decidable c.UsesBoth

Equations

• c.instDecidableUsesBoth = id inferInstance