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, their sum in the free commutative monoid on the features (coe_eq_add_of_apply_eq_some); 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

• FusionRule.coe_eq_add_of_apply_eq_some: Fusion adds the two bundles.
• 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 fuses two adjacent terminals, the structurally higher first, into one bearing both bundles when its decidable condition holds of them.

• condition : List F → List F → Prop

  The condition on the two fusing bundles.

• decCond : DecidableRel self.condition

@[instance_reducible]

instance DistributedMorphology.FusionRule.instDecidableRelListCondition {F : Type u_1} (rule : FusionRule F) : DecidableRel rule.condition

Equations

• rule.instDecidableRelListCondition = rule.decCond

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

Applying Fusion gives the two bundles together when the condition holds, and none otherwise.

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.FusionRule.coe_eq_add_of_apply_eq_some {F : Type u_1} {rule : FusionRule F} {p q out : List F} (h : rule.apply p q = some out) : ↑out = ↑p + ↑q

Fusion adds the two bundles in the free commutative monoid on the features.

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 selects it at neither unfused node, since only the fused bundle contains its item's features (subsetPrinciple_winner_mem).