Vocabulary items as exponence rules

A VocabularyItem exposes the shared exponence interface (Morphology.Exponence.Rule) over neighborhoods: it applies where its site is included in the neighborhood, and its specificity — the number of positioned features it mentions — is strictly antitone in the engine's order, so score selection is Elsewhere selection.

@[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: contexts are neighborhoods, applicability is inclusion of the item's 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.

@[instance_reducible]

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

Equations

• i.instDecidableRelNeighborhoodListApplies n = i.site.instDecidableRelListSubsetOfDecidableEq n

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

The number of distinct positioned features an item mentions — the Subset Principle's specificity score.

Equations

• i.specificity = i.site.positioned.toFinset.card

theorem DistributedMorphology.VocabularyItem.toFinset_subset_toFinset {F : Type u_1} {E : Type u_2} {i j : VocabularyItem F E} [DecidableEq F] : i.site.positioned.toFinset ⊆ j.site.positioned.toFinset ↔ i.site ⊆ j.site

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