VocabSimple: Minimalist-specific Vocabulary Insertion

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

A concrete Minimalist specialization of Vocabulary Insertion. VocabEntry carries features : FeatureBundle (the Minimalist global) + exponent : String + optional context restriction Option Cat. Sits alongside the more general parametric type Theories.Morphology.DM.VI.VocabItem (Ctx Root : Type) in VocabularyInsertion.lean: same Distributed Morphology mechanism (Halle-Marantz late insertion + Elsewhere Condition), specialized to Minimalist's feature-bundle ergonomics so downstream consumers don't have to instantiate the parametric Ctx/Root each call.

Bridges Agree (which values features in narrow syntax) and PF (which realizes the valued bundles as phonological exponents). When multiple Vocabulary Items match, the most specific one (most features) wins — the Elsewhere Condition. Captures e.g. Mam =(y)a' surfacing only when Voice⁰ bears [+oblique], while a less specific entry yields the default (zero) exponent.

The makePersonVocab builder at the end of this file constructs Vocabularies from per-cell paradigm functions; used by Mayan, Romance, and Bantu agreement studies (Scott2023, Preminger2014, ElkinsTorrenceBrown2026).

structure Minimalist.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).

@[implicit_reducible]

instance Minimalist.instReprVocabEntry : Repr VocabEntry

Equations

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

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

Equations

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

def Minimalist.VocabEntry.MatchesFeatures (entry : VocabEntry) (target : FeatureBundle) : Prop

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 : Minimalist.GramFeature) => List.any target fun (tf : Minimalist.GramFeature) => ef == tf) = true)

@[implicit_reducible]

instance Minimalist.instDecidableMatchesFeatures (entry : VocabEntry) (target : FeatureBundle) : Decidable (entry.MatchesFeatures target)

Equations

• Minimalist.instDecidableMatchesFeatures entry target = Minimalist.instDecidableMatchesFeatures._aux_1 entry target

def Minimalist.VocabEntry.Matches (entry : VocabEntry) (target : FeatureBundle) (ctx : Option Cat) : Prop

Does this entry match a target bundle in a given syntactic context? Combines feature-bundle subset matching with the optional context restriction.

Equations

• entry.Matches target ctx = (entry.MatchesFeatures target ∧ (entry.context = none ∨ entry.context = ctx))

@[implicit_reducible]

instance Minimalist.instDecidableMatches (entry : VocabEntry) (target : FeatureBundle) (ctx : Option Cat) : Decidable (entry.Matches target ctx)

Equations

• Minimalist.instDecidableMatches entry target ctx = Minimalist.instDecidableMatches._aux_1 entry target ctx

def Minimalist.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 Minimalist.Vocabulary : Type

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

Equations

• Minimalist.Vocabulary = List Minimalist.VocabEntry

def Minimalist.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 Minimalist.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

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

theorem Minimalist.empty_features_matches_any (entry : VocabEntry) (h : entry.features = []) (target : FeatureBundle) : entry.MatchesFeatures target

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

def Minimalist.makePersonVocab {PN : Type u_1} (cells : List PN) (toPhi : PN → List PhiFeature) (exponentOf : PN → String) (ctx : Option Cat := none) : Vocabulary

Build a Vocabulary from a paradigm cell type. For each cell pn, emits one VocabEntry whose features are toPhi pn lifted into valued FeatureValues, whose exponent is exponentOf pn, and whose context is ctx. Used to deduplicate the per-cell paradigm-to-vocabulary construction shared across study files (e.g., Kaqchikel Set A on Voice/v, Kaqchikel Set B on Infl/T). Elsewhere entries (no features) are appended separately by the caller — this helper covers only the regular cells. The ctx argument matches VocabEntry.context's Option Cat shape; default none admits unrestricted contexts.

Equations

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