Spellout: Feature-to-Morphology Mapping

@cite{elkins-torrence-brown-2026} @cite{halle-marantz-1993} @cite{kiparsky-1973}

Bridges the gap between Agree (which values features in narrow syntax) and PF (which realizes valued feature bundles as phonological exponents). In Distributed Morphology terms, this is Vocabulary Insertion: a Vocabulary Item is inserted into a terminal node if its features are a subset of the node's features.

The key mechanism is the Elsewhere Condition: when multiple Vocabulary Items match, the most specific one (most features) wins. This captures e.g. Mam =(y)a' appearing specifically when Voice⁰ bears [+oblique], while a less specific entry would yield the default (zero) exponent.

structure Minimalism.VocabEntry : Type

A Vocabulary Item: a pairing of a feature set with a phonological exponent, optionally restricted to a particular syntactic context (the category of the terminal node being spelled out).

Vocabulary Insertion inserts the most specific matching entry.

• features : FeatureBundle

  Features this entry matches (must be a subset of the target)

• exponent : String

  The phonological exponent (morpheme string)

• context : Option Cat

  Optional context restriction: the category of the host head. none = unrestricted (can insert anywhere features match).

def Minimalism.instReprVocabEntry.repr : VocabEntry → ℕ → Std.Format

Equations

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

instance Minimalism.instReprVocabEntry : Repr VocabEntry

Equations

• Minimalism.instReprVocabEntry = { reprPrec := Minimalism.instReprVocabEntry.repr }

def Minimalism.VocabEntry.matchesFeatures (entry : VocabEntry) (target : FeatureBundle) : Bool

Does this entry's feature bundle match a target bundle? Matching means every feature in the entry is present (with matching type) in the target bundle. This is subset matching — the entry need not specify all features of the target.

Equations

• entry.matchesFeatures target = List.all entry.features fun (ef : Minimalism.GramFeature) => List.any target fun (tf : Minimalism.GramFeature) => ef == tf

def Minimalism.VocabEntry.matches (entry : VocabEntry) (target : FeatureBundle) (ctx : Option Cat) : Bool

Does this entry match a target bundle in a given syntactic context?

Equations

• entry.matches target ctx = (entry.matchesFeatures target && match entry.context with | none => true | some c => ctx == some c)

def Minimalism.VocabEntry.specificity (entry : VocabEntry) : ℕ

Specificity of a vocabulary entry: the number of features it specifies. Used for Elsewhere ordering — more specific entries take priority.

Equations

• entry.specificity = List.length entry.features

@[reducible, inline]

abbrev Minimalism.Vocabulary : Type

A vocabulary: an ordered list of vocabulary entries. Entries are tried in order; the most specific matching entry wins.

Equations

• Minimalism.Vocabulary = List Minimalism.VocabEntry

def Minimalism.bestMatch (vocab : Vocabulary) (target : FeatureBundle) (ctx : Option Cat) : Option VocabEntry

Find the best (most specific) matching vocabulary entry for a target feature bundle in a given syntactic context.

Implements the Elsewhere Condition: among all matching entries, the one with the most features wins. Ties are broken by list order.

Equations

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

def Minimalism.spellout (vocab : Vocabulary) (target : FeatureBundle) (ctx : Option Cat) : Option String

Spell out a feature bundle: find the best matching entry's exponent. Returns none if no vocabulary entry matches (zero/null exponent).

Equations

• Minimalism.spellout vocab target ctx = Option.map (fun (x : Minimalism.VocabEntry) => x.exponent) (Minimalism.bestMatch vocab target ctx)

theorem Minimalism.empty_features_matches_any (entry : VocabEntry) (h : entry.features = []) (target : FeatureBundle) : entry.matchesFeatures target = true

A vocabulary entry with no features matches any target (Elsewhere entry).