Vocabulary Insertion

A Vocabulary Item pairs its insertion site with the exponent that realizes it: the features of the terminal it spells out, together with the features it requires of the neighboring terminals, its contextual environment / __ ]X]. Form and meaning share the type, an alloseme being an item whose exponent is a denotation (DistributedMorphology/Allosemy.lean). The 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. The competition is the shared exponence engine's selection by specificity, so it inherits that engine's laws: Impoverishment changes the winner only by deleting a feature the winning item mentions, and an antihomophonous vocabulary realizes no ABA pattern across nested neighborhoods.

Main definitions

• DistributedMorphology.VocabularyItem: a site and its exponent.
• DistributedMorphology.VocabularyItem.specificity: the features an item puts on its terminal, then those it puts on the context.
• DistributedMorphology.winner?, DistributedMorphology.subsetPrinciple: the Subset Principle's winning item and its exponent.

Main statements

• DistributedMorphology.winner?_isElsewhereWinner: the winner is an Elsewhere winner of the shared core.
• DistributedMorphology.winner?_retreat: deleting features from the neighborhood can only make the winner less specific, retreat to the general case.
• DistributedMorphology.isContiguous_subsetPrinciple: an antihomophonous vocabulary realizes contiguous patterns over neighborhoods ordered by inclusion.

References

• [HM93]
• [Hal97a]
• [McG13]
• [AN12]

structure DistributedMorphology.VocabularyItem (F : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A Vocabulary Item pairs the site it is inserted at, the features it spells out and those it requires of the adjacent terminals, with its exponent, and applies at any neighborhood containing every feature it mentions.

• site : Neighborhood (List F)

  The features the item spells out, with those it requires of the adjacent terminals.

• exponent : E

  The exponent the item inserts.

def DistributedMorphology.instDecidableEqVocabularyItem.decEq {F✝ : Type u_1} {E✝ : Type u_2} [DecidableEq F✝] [DecidableEq E✝] (x✝ x✝¹ : VocabularyItem F✝ E✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance DistributedMorphology.instDecidableEqVocabularyItem {F✝ : Type u_1} {E✝ : Type u_2} [DecidableEq F✝] [DecidableEq E✝] : DecidableEq (VocabularyItem F✝ E✝)

Equations

• DistributedMorphology.instDecidableEqVocabularyItem = DistributedMorphology.instDecidableEqVocabularyItem.decEq

def DistributedMorphology.instReprVocabularyItem.repr {F✝ : Type u_1} {E✝ : Type u_2} [Repr F✝] [Repr E✝] : VocabularyItem F✝ E✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DistributedMorphology.instReprVocabularyItem {F✝ : Type u_1} {E✝ : Type u_2} [Repr F✝] [Repr E✝] : Repr (VocabularyItem F✝ E✝)

Equations

• DistributedMorphology.instReprVocabularyItem = { reprPrec := DistributedMorphology.instReprVocabularyItem.repr }

def DistributedMorphology.VocabularyItem.features {F : Type u_1} {E : Type u_2} (i : VocabularyItem F E) : List F

The features the item spells out at its own terminal.

Equations

• i.features = i.site.focus

def DistributedMorphology.VocabularyItem.ofFeatures {F : Type u_1} {E : Type u_2} (fs : List F) (e : E) : VocabularyItem F E

A context-free item: the features it spells out and its exponent.

Equations

• DistributedMorphology.VocabularyItem.ofFeatures fs e = { site := ↑fs, exponent := e }

def DistributedMorphology.«term_⟷_» : Lean.TrailingParserDescr

fs ⟷ e is the context-free Vocabulary Item spelling out fs as e.

Equations

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

@[simp]

theorem DistributedMorphology.VocabularyItem.site_ofFeatures {F : Type u_1} {E : Type u_2} (fs : List F) (e : E) : (ofFeatures fs e).site = ↑fs

@[simp]

theorem DistributedMorphology.VocabularyItem.exponent_ofFeatures {F : Type u_1} {E : Type u_2} (fs : List F) (e : E) : (ofFeatures fs e).exponent = e

@[instance_reducible]

instance DistributedMorphology.VocabularyItem.instRuleNeighborhoodList {F : Type u_1} {E : Type u_2} : Morphology.Exponence.Rule (VocabularyItem F E) (Neighborhood (List F)) E

A Vocabulary Item exposes the shared exponence interface, its contexts neighborhoods and its applicability inclusion of its site.

Equations

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

@[instance_reducible]

instance DistributedMorphology.VocabularyItem.instPreorder {F : Type u_1} {E : Type u_2} : Preorder (VocabularyItem F E)

Equations

• DistributedMorphology.VocabularyItem.instPreorder = Morphology.Exponence.toPreorder

theorem DistributedMorphology.VocabularyItem.applies_iff {F : Type u_1} {E : Type u_2} {i : VocabularyItem F E} {n : Neighborhood (List F)} : Morphology.Exponence.Applies i n ↔ i.site ⊆ n

theorem DistributedMorphology.VocabularyItem.elsewhere_applies {F : Type u_1} {E : Type u_2} (e : E) (n : Neighborhood (List F)) : Morphology.Exponence.Applies { site := ∅, exponent := e } n

The Elsewhere item applies at every neighborhood.

theorem DistributedMorphology.VocabularyItem.le_iff_applies {F : Type u_1} {E : Type u_2} {i j : VocabularyItem F E} : i ≤ j ↔ ∀ ⦃n : Neighborhood (List F)⦄, i.site ⊆ n → j.site ⊆ n

theorem DistributedMorphology.VocabularyItem.le_iff {F : Type u_1} {E : Type u_2} {i j : VocabularyItem F E} : i ≤ j ↔ j.site ⊆ i.site

The engine's specificity order is reverse inclusion of sites.

theorem DistributedMorphology.VocabularyItem.site_strictAnti {F : Type u_1} {E : Type u_2} : StrictAnti site

A strictly more specific item has a strictly larger site.

@[instance_reducible]

instance DistributedMorphology.VocabularyItem.instDecidableRelNeighborhoodListApplies {F : Type u_1} {E : Type u_2} [DecidableEq F] : DecidableRel Morphology.Exponence.Applies

Equations

• i.instDecidableRelNeighborhoodListApplies n = { decide := decide (i.site.positioned ⊆ n.positioned), reflects_decide := ⋯ }

def DistributedMorphology.VocabularyItem.specificity {F : Type u_1} {E : Type u_2} [DecidableEq F] (i : VocabularyItem F E) : Lex (ℕ × ℕ)

An item's specificity counts the distinct features its site puts on the terminal, then those it puts on the context: the terminal's features decide, as the Subset Principle chooses the item matching most of them ([Hal97a]), and context breaks ties ([McG13]).

Equations

• i.specificity = i.site.weight

theorem DistributedMorphology.VocabularyItem.specificity_strictAnti {F : Type u_1} {E : Type u_2} [DecidableEq F] : StrictAnti specificity

@[simp]

theorem DistributedMorphology.VocabularyItem.not_specificity_lt_elsewhere {F : Type u_1} {E : Type u_2} [DecidableEq F] (i : VocabularyItem F E) (e : E) : ¬i.specificity < (ofFeatures [] e).specificity

No item is less specific than an Elsewhere item.

The Subset Principle

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

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

Equations

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

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

The Subset Principle yields the exponent of the most specific item whose site the neighborhood contains, and none iff no item applies.

Equations

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

theorem DistributedMorphology.subsetPrinciple_winner_mem {F : Type u_1} {E : Type u_2} [DecidableEq F] {items : Morphology.Exponence.RuleSet (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, so 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 : Morphology.Exponence.RuleSet (VocabularyItem F E)} {n : Neighborhood (List F)} : (winner? items n).isSome = true ↔ ∃ i ∈ items, i.site ⊆ n

theorem DistributedMorphology.winner?_isElsewhereWinner {F : Type u_1} {E : Type u_2} [DecidableEq F] {items : Morphology.Exponence.RuleSet (VocabularyItem F E)} {n : Neighborhood (List F)} {i : VocabularyItem F E} (h : winner? items n = some i) : items.IsElsewhereWinner 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 : Morphology.Exponence.RuleSet (VocabularyItem F E)} {n : Neighborhood (List F)} {e : E} (h : subsetPrinciple items n = some e) : items.Realizes n e

theorem DistributedMorphology.winner?_eq_of_subset {F : Type u_1} {E : Type u_2} [DecidableEq F] {items : Morphology.Exponence.RuleSet (VocabularyItem F E)} {n n' : Neighborhood (List F)} {i : VocabularyItem F E} (hsub : n' ⊆ n) (h : winner? items n = some i) (hi : i.site ⊆ n') : winner? items n' = some i

Impoverishment that deletes only features the winning item does not mention leaves the winner in place, since every item applicable after the deletion was applicable before it.

theorem DistributedMorphology.winner?_retreat {F : Type u_1} {E : Type u_2} [DecidableEq F] {items : Morphology.Exponence.RuleSet (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.

theorem DistributedMorphology.isContiguous_subsetPrinciple {F : Type u_1} {E : Type u_2} [DecidableEq F] {items : Morphology.Exponence.RuleSet (VocabularyItem F E)} (hv : items.Antihomophonous) : Morphology.IsContiguous (subsetPrinciple items)

An antihomophonous vocabulary realizes no ABA pattern over neighborhoods ordered by inclusion: an exponent inserted at two nested neighborhoods is inserted at every neighborhood between them.