Vocabulary items

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 is an item whose exponent is a denotation (DistributedMorphology/Allosemy.lean). The selection-engine instance lives in DistributedMorphology/Basic.lean.

References

• M. Halle and A. Marantz, Distributed Morphology and the pieces of inflection

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

A Vocabulary Item: the site it is inserted at — the features it spells out and those it requires of the adjacent terminals — paired with its exponent; applicable 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.

@[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.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.

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 := DistributedMorphology.Neighborhood.ofBundle fs, exponent := e }

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

fs ⟷ e: 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 = Neighborhood.ofBundle 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