Vocabulary Insertion (Distributed Morphology)

@cite{halle-marantz-1993} @cite{bobaljik-2000}

Vocabulary Insertion is the mechanism by which syntactic terminal nodes receive phonological exponents in Distributed Morphology. It is the formal realization of DM's List 2: a set of Vocabulary Items (VI rules) that compete for insertion at each terminal.

Architecture

A Vocabulary Item specifies:

1. A phonological exponent (the surface form)
2. A morphosyntactic context (the features the terminal must bear)
3. A root context (optional: which roots the rule applies to)

When multiple VI rules match a terminal, the Elsewhere Condition (@cite{halle-marantz-1993}) resolves the competition: the most specific matching rule wins. A rule is more specific if its context is a proper superset of another matching rule's context.

Root-Out Insertion

@cite{bobaljik-2000} argues that VI proceeds root-out: the root is inserted first, then inflectional affixes outward. This means VI for outer morphemes can only be phonologically conditioned by material already inserted (inward) — it cannot "look ahead" to morphemes not yet inserted. This is the basis for the claim that outward-sensitive phonologically conditioned suppletive allomorphy (OS-PCSA) should not exist.

Connection to Linglib

This module provides the generic VI framework. Language-specific VI rules live in Fragments/ or in phenomenon-specific Studies/ files. The Categorizer and CategorizedRoot types from Theories/Morphology/DM/Categorizer.lean provide the syntax-side terminal nodes that VI targets.

structure Morphology.DM.VI.VocabItem (Ctx : Type u_1) (Root : Type u_2) : Type (max u_1 u_2)

A Vocabulary Item: a rule mapping morphosyntactic context to a phonological exponent.

• Ctx: the type of morphosyntactic contexts (e.g., feature bundles)
• Root: the type of root identifiers (for root-specific rules)

The specificity field encodes the Elsewhere Condition: when multiple rules match, the highest-specificity rule wins. In practice, specificity equals the number of features the context checks — a rule conditioned on [ACC, +animate] (specificity 2) beats a default rule with no feature requirements (specificity 0).

• exponent : String

  The phonological exponent inserted at the terminal.

• contextMatch : Ctx → Bool

  Context check: does the terminal's feature bundle match?

• rootMatch : Option (Root → Bool)

  Root restriction: which roots this rule applies to. none means the rule is unrestricted (default/elsewhere).

• specificity : Nat

  Specificity for Elsewhere Condition resolution. Higher = more specific. When two rules both match, the higher-specificity rule wins.

def Morphology.DM.VI.VocabItem.matches {Ctx : Type u_1} {Root : Type u_2} (vi : VocabItem Ctx Root) (ctx : Ctx) (root : Root) : Bool

Does a Vocabulary Item match at a given terminal node? Checks both the morphosyntactic context and the root restriction.

Equations

• vi.matches ctx root = (vi.contextMatch ctx && match vi.rootMatch with | none => true | some f => f root)

def Morphology.DM.VI.vocabularyInsert {Ctx : Type u_1} {Root : Type u_2} (rules : List (VocabItem Ctx Root)) (ctx : Ctx) (root : Root) : Option String

Insert a Vocabulary Item at a terminal node. Tries all rules in specificity order (highest first); returns the exponent of the first matching rule. Returns none if no rule matches.

This implements the Subset Principle / Elsewhere Condition (@cite{halle-marantz-1993}): among all matching rules, the most specific one wins.

Equations

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

def Morphology.DM.VI.vocabularyInsertSimple {Ctx : Type u_1} (rules : List (VocabItem Ctx Unit)) (ctx : Ctx) : Option String

Simplified insertion when rules are not root-specific.

Equations

• Morphology.DM.VI.vocabularyInsertSimple rules ctx = Morphology.DM.VI.vocabularyInsert rules ctx ()

def Morphology.DM.VI.hasDefault {Ctx : Type u_1} {Root : Type u_2} (rules : List (VocabItem Ctx Root)) : Prop

A rule set has a default (elsewhere) rule if some rule matches every context.

Equations

• Morphology.DM.VI.hasDefault rules = ∃ (vi : Morphology.DM.VI.VocabItem Ctx Root), vi ∈ rules ∧ ∀ (ctx : Ctx) (root : Root), vi.matches ctx root = true

def Morphology.DM.VI.overrides {Ctx : Type u_1} {Root : Type u_2} (vi₁ vi₂ : VocabItem Ctx Root) (ctx : Ctx) (root : Root) : Prop

A rule overrides another: both match the same context, but the first has strictly higher specificity.

Equations

• Morphology.DM.VI.overrides vi₁ vi₂ ctx root = (vi₁.matches ctx root = true ∧ vi₂.matches ctx root = true ∧ vi₁.specificity > vi₂.specificity)

structure Morphology.DM.VI.InsertionOrder : Type

Root-out ordering: a terminal at position i in the morphological structure (0 = root, increasing outward) is inserted at step i.

@cite{bobaljik-2000} argues this is the standard assumption in DM: the root is the first exponent to be inserted, then the innermost inflectional affix, then the next one out, etc.

The consequence: VI for terminal at position i can only be conditioned by the phonological shapes of terminals at positions 0..i−1 (already inserted). It cannot look ahead to position i+1.

• positions : Nat

  Number of terminal positions in the morphological word.

• order : Fin self.positions → Fin self.positions

  At each step, which position is being inserted. For root-out: step i inserts position i.

def Morphology.DM.VI.rootOutOrder (n : Nat) : InsertionOrder

A root-out insertion order: position 0 (root) first, then outward.

Equations

• Morphology.DM.VI.rootOutOrder n = { positions := n, order := id }

def Morphology.DM.VI.isInwardConditioned (conditioningPos targetPos : Nat) : Bool

The constraint that OS-PCSA imposes: the conditioning environment for VI at position i can only include positions inward of i (i.e., positions 0..i−1).

If the alternation at position i is conditioned by the phonological shape of a morpheme at position i+1 or beyond, it is outward-sensitive and problematic for standard root-out DM.

Equations

• Morphology.DM.VI.isInwardConditioned conditioningPos targetPos = decide (conditioningPos < targetPos)

def Morphology.DM.VI.isOutwardSensitive (conditioningPos targetPos : Nat) : Bool

The Telugu weak alternation is outward-sensitive: the alternation on the n head (closer to root) is conditioned by case/agreement suffixes (further from root). This is the key diagnostic that motivates the phonological analysis.

Equations

• Morphology.DM.VI.isOutwardSensitive conditioningPos targetPos = decide (conditioningPos ≥ targetPos)

theorem Morphology.DM.VI.rootOut_starts_at_root (n : Nat) (h : 0 < n) : (rootOutOrder n).order ⟨0, h⟩ = ⟨0, h⟩

In root-out order, position 0 is inserted first.

theorem Morphology.DM.VI.root_conditions_affix : isInwardConditioned 0 1 = true

Inward conditioning: position 0 can condition position 1.

theorem Morphology.DM.VI.outer_cannot_condition_inner : isOutwardSensitive 2 1 = true

Outward conditioning: position 2 cannot condition position 1 under root-out VI (it hasn't been inserted yet).

structure Morphology.DM.VI.FeatureVI (F : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A feature-set vocabulary item for the Subset Principle. Simpler than the full VocabItem: a feature specification paired with an exponent. The Subset Principle selects the most specific item whose features are all present in the target.

Used when VI is purely determined by feature-subset matching (e.g., gender agreement class selection in @cite{adamson-anagnostopoulou-2025}).

• features : List F
• exponent : E

def Morphology.DM.VI.instDecidableEqFeatureVI.decEq {F✝ : Type u_1} {E✝ : Type u_2} [DecidableEq F✝] [DecidableEq E✝] (x✝ x✝¹ : FeatureVI F✝ E✝) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Morphology.DM.VI.instDecidableEqFeatureVI {F✝ : Type u_1} {E✝ : Type u_2} [DecidableEq F✝] [DecidableEq E✝] : DecidableEq (FeatureVI F✝ E✝)

Equations

• Morphology.DM.VI.instDecidableEqFeatureVI = Morphology.DM.VI.instDecidableEqFeatureVI.decEq

def Morphology.DM.VI.instReprFeatureVI.repr {F✝ : Type u_1} {E✝ : Type u_2} [Repr F✝] [Repr E✝] : FeatureVI F✝ E✝ → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.DM.VI.instReprFeatureVI {F✝ : Type u_1} {E✝ : Type u_2} [Repr F✝] [Repr E✝] : Repr (FeatureVI F✝ E✝)

Equations

• Morphology.DM.VI.instReprFeatureVI = { reprPrec := Morphology.DM.VI.instReprFeatureVI.repr }

def Morphology.DM.VI.subsetPrinciple {F : Type u_1} {E : Type u_2} [BEq F] (items : List (FeatureVI F E)) (target : List F) : Option E

The Subset Principle (@cite{halle-marantz-1993}): among vocabulary items whose feature specification is a subset of the target, select the most specific (longest feature list).

Returns none only if items is empty. When items include an elsewhere entry (empty feature list), subsetPrinciple always succeeds — the elsewhere item matches any target.

Equations

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

theorem Morphology.DM.VI.elsewhere_always_matches {F : Type u_1} {E : Type u_2} [BEq F] (e : E) (target : List F) : ({ features := [], exponent := e }.features.all fun (x : F) => target.contains x) = true

An elsewhere item (empty features) matches any target.