Vocabulary insertion

Vocabulary Insertion supplies syntactic terminals with phonological exponents: the Vocabulary Items of List 2 compete for insertion at each terminal, and the Subset Principle picks the item whose site is the largest one the terminal's neighborhood contains — its own features and, for a contextual item, the features of the adjacent terminals. This file specializes the shared exponence engine (Morphology.Exponence.selectBy) to that competition.

Main definitions

• winner?, subsetPrinciple: the Subset Principle's winning item and its exponent.

Main results

• winner?_isElsewhereWinner: the winner is an Elsewhere winner of the shared core, with no faithfulness hypothesis — the engine's specificity order is reverse inclusion of sites (VocabularyItem.le_iff).
• winner?_retreat: deleting features from the neighborhood can only make the winner less specific — retreat to the general case.

References

• M. Halle and A. Marantz, Distributed Morphology and the pieces of inflection
• K. Arregi and A. Nevins, Morphotactics

The Subset Principle

def DistributedMorphology.winner? {F : Type u_1} {E : Type u_2} [DecidableEq F] (items : List (VocabularyItem F E)) (n : Neighborhood (List F)) : Option (VocabularyItem F E)

The Subset Principle's winning item: the applicable item of greatest specificity (the earliest, under ties).

Equations

• DistributedMorphology.winner? items n = Morphology.Exponence.selectBy DistributedMorphology.VocabularyItem.specificity items n

def DistributedMorphology.subsetPrinciple {F : Type u_1} {E : Type u_2} [DecidableEq F] (items : List (VocabularyItem F E)) (n : Neighborhood (List F)) : Option E

The Subset Principle: the exponent of the most specific item whose site the neighborhood contains; none iff no item applies.

Equations

• DistributedMorphology.subsetPrinciple items n = Morphology.Exponence.realize DistributedMorphology.VocabularyItem.specificity items n

theorem DistributedMorphology.winner?_mem {F : Type u_1} {E : Type u_2} [DecidableEq F] {items : List (VocabularyItem F E)} {n : Neighborhood (List F)} {i : VocabularyItem F E} (h : winner? items n = some i) : i ∈ Morphology.Exponence.applicable items n

theorem DistributedMorphology.winner?_spec {F : Type u_1} {E : Type u_2} [DecidableEq F] {items : List (VocabularyItem F E)} {n : Neighborhood (List F)} {i : VocabularyItem F E} (h : winner? items n = some i) : i ∈ items ∧ i.site ⊆ n

theorem DistributedMorphology.subsetPrinciple_winner_mem {F : Type u_1} {E : Type u_2} [DecidableEq F] {items : List (VocabularyItem F E)} {n : Neighborhood (List F)} {e : E} (h : subsetPrinciple items n = some e) : ∃ i ∈ items, i.exponent = e ∧ i.site ⊆ n

The Subset Principle's exponent comes from an applicable item — the selection never draws on features the neighborhood does not bear.

theorem DistributedMorphology.winner?_isSome_iff {F : Type u_1} {E : Type u_2} [DecidableEq F] {items : List (VocabularyItem F E)} {n : Neighborhood (List F)} : (winner? items n).isSome = true ↔ Morphology.Exponence.applicable items n ≠ []

theorem DistributedMorphology.winner?_max {F : Type u_1} {E : Type u_2} [DecidableEq F] {items : List (VocabularyItem F E)} {n : Neighborhood (List F)} {i : VocabularyItem F E} (h : winner? items n = some i) (j : VocabularyItem F E) : j ∈ Morphology.Exponence.applicable items n → j.specificity ≤ i.specificity

theorem DistributedMorphology.winner?_isElsewhereWinner {F : Type u_1} {E : Type u_2} [DecidableEq F] {items : List (VocabularyItem F E)} {n : Neighborhood (List F)} {i : VocabularyItem F E} (h : winner? items n = some i) : Morphology.Exponence.IsElsewhereWinner items n i

The winner is an Elsewhere winner of the shared core — with no faithfulness hypothesis, since VocabularyItem.specificity is strictly antitone outright.

theorem DistributedMorphology.subsetPrinciple_realizes {F : Type u_1} {E : Type u_2} [DecidableEq F] {items : List (VocabularyItem F E)} {n : Neighborhood (List F)} {e : E} (h : subsetPrinciple items n = some e) : Morphology.Exponence.Realizes items n e

theorem DistributedMorphology.applicable_mono {F : Type u_1} {E : Type u_2} [DecidableEq F] {items : List (VocabularyItem F E)} {n n' : Neighborhood (List F)} (hsub : n' ⊆ n) : Morphology.Exponence.applicable items n' ⊆ Morphology.Exponence.applicable items n

Applicability is monotone in the neighborhood.

theorem DistributedMorphology.winner?_retreat {F : Type u_1} {E : Type u_2} [DecidableEq F] {items : List (VocabularyItem F E)} {n n' : Neighborhood (List F)} {i' : VocabularyItem F E} (hsub : n' ⊆ n) (h' : winner? items n' = some i') : ∃ (i : VocabularyItem F E), winner? items n = some i ∧ i'.specificity ≤ i.specificity

Retreat to the general case: shrinking the neighborhood — deleting features by Impoverishment — can only make the winner weakly less specific, which is why impoverishment yields syncretism with a more general exponent rather than a different specific one.