Fusion

Fusion merges two adjacent terminal nodes into a single terminal bearing both feature bundles, which a single Vocabulary Item then spells out — the Tns+Agr fusion of English finite verbs; French du = P[de] fused with D[le] is the portmanteau case. It is the inverse misalignment from Fission: fission yields more positions of exponence than syntactic terminals, fusion fewer. The fused bundle is the two bundles together; a rule contributes only the condition under which the two terminals fuse.

Main definitions

• FusionRule: the licensing condition on two adjacent bundles.
• FusionRule.apply: the fused bundle when the condition holds.

Main results

• portmanteau_needs_fusion: an exponent whose items all draw on both bundles is insertable at neither unfused node.

References

• M. Halle and A. Marantz, Distributed Morphology and the pieces of inflection
• L. Kalin, B. Bjorkman et al. §4.4

structure DistributedMorphology.FusionRule (F : Type u_3) : Type u_3

A Fusion rule: the condition under which two adjacent terminals, the structurally higher first, fuse into one bearing both bundles.

• condition : List F → List F → Prop

  The condition on the two fusing bundles.

• decCond (p q : List F) : Decidable (self.condition p q)

  Decidability witness for condition.

@[instance_reducible]

instance DistributedMorphology.FusionRule.instDecidableCondition {F : Type u_1} (rule : FusionRule F) (p q : List F) : Decidable (rule.condition p q)

Equations

• rule.instDecidableCondition p q = rule.decCond p q

def DistributedMorphology.FusionRule.apply {F : Type u_1} (rule : FusionRule F) (p q : List F) : Option (List F)

Apply Fusion: the two bundles together when the condition holds; otherwise none.

Equations

• rule.apply p q = if rule.condition p q then some (p ++ q) else none

theorem DistributedMorphology.FusionRule.apply_pos {F : Type u_1} {rule : FusionRule F} {p q : List F} (h : rule.condition p q) : rule.apply p q = some (p ++ q)

theorem DistributedMorphology.FusionRule.apply_neg {F : Type u_1} {rule : FusionRule F} {p q : List F} (h : ¬rule.condition p q) : rule.apply p q = none

@[simp]

theorem DistributedMorphology.FusionRule.apply_eq_some_iff {F : Type u_1} {rule : FusionRule F} {p q out : List F} : rule.apply p q = some out ↔ rule.condition p q ∧ p ++ q = out

@[simp]

theorem DistributedMorphology.FusionRule.apply_eq_none_iff {F : Type u_1} {rule : FusionRule F} {p q : List F} : rule.apply p q = none ↔ ¬rule.condition p q

theorem DistributedMorphology.FusionRule.isSome_apply {F : Type u_1} {rule : FusionRule F} {p q : List F} : (rule.apply p q).isSome = true ↔ rule.condition p q

theorem DistributedMorphology.portmanteau_needs_fusion {F : Type u_1} {E : Type u_2} [DecidableEq F] {items : List (VocabularyItem F E)} {p q : Neighborhood (List F)} {e : E} (he : ∀ i ∈ items, i.exponent = e → ¬i.site ⊆ p ∧ ¬i.site ⊆ q) : subsetPrinciple items p ≠ some e ∧ subsetPrinciple items q ≠ some e

A portmanteau exponent needs fusion: when every item carrying the exponent draws on features missing from each unfused bundle, the Subset Principle can select it at neither unfused node — only the fused bundle contains its item's features (subsetPrinciple_winner_mem).