[HM93]: Distributed Morphology and the Pieces of Inflection

[HM93]

This study file formalizes the core architecture and predictions of Distributed Morphology as presented in [HM93], Chapter 3 of The View from Building 20 (Hale & Keyser, eds.).

Structure

• §1: English Verb Inflection — the context-free Tns/Agr paradigm, formalized using FeatureVI and subsetPrinciple, demonstrating Elsewhere Condition competition
• §2: Conditioned Allomorphy — root-specific past tense exponents (-t, ∅) illustrating the Paninian principle (most specific wins)
• §3: Tns + Agr Fusion — the MS operation that merges Tns and Agr into a single terminal before VI
• §4: Impoverishment and Syncretism — feature deletion before VI derives syncretism (past participle falling together with simple past)
• §5: Baker 1985 Bridge — English Tns/Agr features are outside GF-rule categories in [Byb85]'s relevance hierarchy, connecting [Bak85], [Byb85], and [HM93]

Architecture

[HM93] adopt a Y-model (DS → SS → {LF, MS → PF}). Terminal nodes bear morphosyntactic features but no phonological content until Vocabulary Insertion at MS — this is Late Insertion. The VI mechanism (subsetPrinciple) IS Late Insertion in action: it maps feature bundles to exponents, making DM realizational by construction.

Impoverishment — also introduced in this paper — is formalized as a general mechanism in Morphology/DM/Impoverishment.lean. This study file instantiates impoverishment on the English paradigm to derive syncretism (§4). Fusion is defined inline (§3) since this file is its only consumer.

The Subset Principle and English Tns/Agr

[HM93] give the Vocabulary Items for English verbal inflection. The terminal node for Tns+Agr (after fusion — see §3) bears features drawn from {[+past], [+participle], [3sg]}. The Subset Principle / Elsewhere Condition selects the most specific matching VI entry: the entry whose feature specification is the largest subset of the terminal's features.

Context-free VI entries:

Features	Exponent	Example
[+past, +participle]	-n	taken, eaten
[+past]	-d	walked, played
[+participle]	-ing	walking, playing
[3sg]	-z	walks, plays
∅ (elsewhere)	∅	walk, play

inductive HalleMarantz1993.EngInflFeature : Type

Features on the English Tns+Agr terminal after fusion. [HM93].

• past : EngInflFeature
• participle : EngInflFeature
• sg3 : EngInflFeature

@[implicit_reducible]

instance HalleMarantz1993.instDecidableEqEngInflFeature : DecidableEq EngInflFeature

Equations

• HalleMarantz1993.instDecidableEqEngInflFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance HalleMarantz1993.instBEqEngInflFeature : BEq EngInflFeature

Equations

• HalleMarantz1993.instBEqEngInflFeature = { beq := HalleMarantz1993.instBEqEngInflFeature.beq }

def HalleMarantz1993.instBEqEngInflFeature.beq : EngInflFeature → EngInflFeature → Bool

Equations

• HalleMarantz1993.instBEqEngInflFeature.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def HalleMarantz1993.instReprEngInflFeature.repr : EngInflFeature → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HalleMarantz1993.instReprEngInflFeature : Repr EngInflFeature

Equations

• HalleMarantz1993.instReprEngInflFeature = { reprPrec := HalleMarantz1993.instReprEngInflFeature.repr }

def HalleMarantz1993.englishTnsVI : List (Morphology.DM.VI.FeatureVI EngInflFeature String)

Context-free VI entries for English verbal inflection. [HM93].

Equations

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

theorem HalleMarantz1993.past_participle_gets_n : Morphology.DM.VI.subsetPrinciple englishTnsVI [EngInflFeature.past, EngInflFeature.participle] = some "-n"

Past participle: [+past, +participle] → -n. -n beats -d and -ing because its feature set {past, participle} is the largest subset of the target. [HM93].

theorem HalleMarantz1993.past_finite_gets_d : Morphology.DM.VI.subsetPrinciple englishTnsVI [EngInflFeature.past] = some "-d"

Past finite: [+past] → -d. -n does not match because [+participle] ⊄ {past}. [HM93].

theorem HalleMarantz1993.nonpast_participle_gets_ing : Morphology.DM.VI.subsetPrinciple englishTnsVI [EngInflFeature.participle] = some "-ing"

Non-finite participle: [+participle] → -ing. [HM93].

theorem HalleMarantz1993.sg3_present_gets_z : Morphology.DM.VI.subsetPrinciple englishTnsVI [EngInflFeature.sg3] = some "-z"

Third singular present: [3sg] → -z. [HM93].

theorem HalleMarantz1993.elsewhere_gets_null : Morphology.DM.VI.subsetPrinciple englishTnsVI [] = some "∅"

Elsewhere (bare stem): [] → ∅. When no features are present, the elsewhere entry wins. [HM93].

theorem HalleMarantz1993.n_beats_d_for_past_participle : Morphology.DM.VI.subsetPrinciple englishTnsVI [EngInflFeature.past, EngInflFeature.participle] ≠ Morphology.DM.VI.subsetPrinciple englishTnsVI [EngInflFeature.past]

The Subset Principle resolves -n vs -d competition: for a [+past, +participle] target, -n (2 features) beats -d (1 feature).

theorem HalleMarantz1993.paradigm_total : (Morphology.DM.VI.subsetPrinciple englishTnsVI [EngInflFeature.past, EngInflFeature.participle]).isSome = true ∧ (Morphology.DM.VI.subsetPrinciple englishTnsVI [EngInflFeature.past]).isSome = true ∧ (Morphology.DM.VI.subsetPrinciple englishTnsVI [EngInflFeature.participle]).isSome = true ∧ (Morphology.DM.VI.subsetPrinciple englishTnsVI [EngInflFeature.sg3]).isSome = true ∧ (Morphology.DM.VI.subsetPrinciple englishTnsVI []).isSome = true

The paradigm is total: every possible feature combination receives an exponent (thanks to the elsewhere entry).

Root-Specific Past Tense Entries

The default past tense entry -d coexists with root-conditioned variants ([HM93]):

• -t: dwell → dwelt, buy → bought, send → sent, ...
• ∅: put → put, beat → beat, hit → hit, ...

These share the same morphosyntactic context ([+past]) but have different root restrictions. The Paninian principle (= Elsewhere Condition applied to root-conditioned entries) selects the most specific matching entry: a root-restricted rule overrides the unrestricted default when the root matches.

This section uses VocabItem (which supports root restrictions via rootMatch) rather than FeatureVI (which is context-free).

inductive HalleMarantz1993.SampleVerb : Type

Sample verb roots for demonstrating conditioned allomorphy.

• walk : SampleVerb
• play : SampleVerb
• dwell : SampleVerb
• buy : SampleVerb
• send : SampleVerb
• put : SampleVerb
• beat : SampleVerb
• hit : SampleVerb

@[implicit_reducible]

instance HalleMarantz1993.instDecidableEqSampleVerb : DecidableEq SampleVerb

Equations

• HalleMarantz1993.instDecidableEqSampleVerb x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance HalleMarantz1993.instBEqSampleVerb : BEq SampleVerb

Equations

• HalleMarantz1993.instBEqSampleVerb = { beq := HalleMarantz1993.instBEqSampleVerb.beq }

def HalleMarantz1993.instBEqSampleVerb.beq : SampleVerb → SampleVerb → Bool

Equations

• HalleMarantz1993.instBEqSampleVerb.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance HalleMarantz1993.instReprSampleVerb : Repr SampleVerb

Equations

• HalleMarantz1993.instReprSampleVerb = { reprPrec := HalleMarantz1993.instReprSampleVerb.repr }

def HalleMarantz1993.instReprSampleVerb.repr : SampleVerb → ℕ → Std.Format

Equations

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

def HalleMarantz1993.conditionedPastVI : List (Morphology.DM.VI.VocabItem Bool SampleVerb)

Root-conditioned past tense VI rules.

All three entries share [+past] context (modeled as Bool); they differ in root restriction and specificity. [HM93].

Equations

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

theorem HalleMarantz1993.walk_gets_d : Morphology.DM.VI.vocabularyInsert conditionedPastVI true SampleVerb.walk = some "-d"

Regular verbs get -d: no root-specific entry matches.

theorem HalleMarantz1993.play_gets_d : Morphology.DM.VI.vocabularyInsert conditionedPastVI true SampleVerb.play = some "-d"

theorem HalleMarantz1993.dwell_gets_t : Morphology.DM.VI.vocabularyInsert conditionedPastVI true SampleVerb.dwell = some "-t"

Verbs in the -t class: root restriction overrides default.

theorem HalleMarantz1993.buy_gets_t : Morphology.DM.VI.vocabularyInsert conditionedPastVI true SampleVerb.buy = some "-t"

theorem HalleMarantz1993.put_gets_null : Morphology.DM.VI.vocabularyInsert conditionedPastVI true SampleVerb.put = some "∅"

Verbs in the ∅ class: no overt past tense marking.

theorem HalleMarantz1993.beat_gets_null : Morphology.DM.VI.vocabularyInsert conditionedPastVI true SampleVerb.beat = some "∅"

theorem HalleMarantz1993.root_restriction_overrides_default : Morphology.DM.VI.vocabularyInsert conditionedPastVI true SampleVerb.dwell ≠ Morphology.DM.VI.vocabularyInsert conditionedPastVI true SampleVerb.walk

The Paninian principle: root-restricted entries override the default for matching roots.

theorem HalleMarantz1993.nonpast_no_match : Morphology.DM.VI.vocabularyInsert conditionedPastVI false SampleVerb.walk = none

Non-past context: no entry matches (all require [+past]).

Fusion of Tns and Agr at MS

[HM93] argue that English Tns and Agr are separate syntactic heads. At MS, they undergo Fusion: the two adjacent terminals merge into a single terminal bearing the union of both feature bundles. A single VI entry then spells out the fused node.

This explains why English has a single affix (not two stacked affixes) for Tns+Agr: walk-s realizes both non-past Tns and 3sg Agr in one exponent, because Fusion merges the two terminals before VI applies.

We model fusion using FusionRule (inlined below; this study is its only consumer in linglib) and show that the fused features feed directly into the VI paradigm from §1.

structure HalleMarantz1993.FusionRule (Terminal : Type) : Type

Fusion ([HM93]): merges two adjacent terminal nodes into a single terminal before Vocabulary Insertion. The fused node bears the union of both terminals' features; a single VI then spells out the fused bundle, yielding a portmanteau.

Canonical example: French du = Fusion of P[de] and D[le.MASC.SG]. [KBC+26] §4.4.

• terminal1 : Terminal

  First terminal (structurally higher).

• terminal2 : Terminal

  Second terminal (structurally lower / complement head).

def HalleMarantz1993.FusionRule.apply {Terminal Features : Type} (r : FusionRule Terminal) (getFeatures : Terminal → Features) (union : Features → Features → Features) : Features

The result of Fusion: a single terminal bearing features from both inputs, parameterized over a feature-union operation.

Equations

• r.apply getFeatures union = union (getFeatures r.terminal1) (getFeatures r.terminal2)

inductive HalleMarantz1993.InflHead : Type

The two inflectional heads that fuse in English.

• tns (past participle : Bool) : InflHead

  Tns head: bears tense/aspect features.

• agr (sg3 : Bool) : InflHead

  Agr head: bears agreement features.

def HalleMarantz1993.instDecidableEqInflHead.decEq (x✝ x✝¹ : InflHead) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• HalleMarantz1993.instDecidableEqInflHead.decEq (HalleMarantz1993.InflHead.tns past participle) (HalleMarantz1993.InflHead.agr sg3) = isFalse ⋯
• HalleMarantz1993.instDecidableEqInflHead.decEq (HalleMarantz1993.InflHead.agr sg3) (HalleMarantz1993.InflHead.tns past participle) = isFalse ⋯
• HalleMarantz1993.instDecidableEqInflHead.decEq (HalleMarantz1993.InflHead.agr a) (HalleMarantz1993.InflHead.agr b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance HalleMarantz1993.instDecidableEqInflHead : DecidableEq InflHead

Equations

• HalleMarantz1993.instDecidableEqInflHead = HalleMarantz1993.instDecidableEqInflHead.decEq

def HalleMarantz1993.instReprInflHead.repr : InflHead → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HalleMarantz1993.instReprInflHead : Repr InflHead

Equations

• HalleMarantz1993.instReprInflHead = { reprPrec := HalleMarantz1993.instReprInflHead.repr }

def HalleMarantz1993.InflHead.features : InflHead → List EngInflFeature

Extract inflectional features from each head type.

Equations

• (HalleMarantz1993.InflHead.tns true true).features = [HalleMarantz1993.EngInflFeature.past, HalleMarantz1993.EngInflFeature.participle]
• (HalleMarantz1993.InflHead.tns true false).features = [HalleMarantz1993.EngInflFeature.past]
• (HalleMarantz1993.InflHead.tns false true).features = [HalleMarantz1993.EngInflFeature.participle]
• (HalleMarantz1993.InflHead.tns false false).features = []
• (HalleMarantz1993.InflHead.agr true).features = [HalleMarantz1993.EngInflFeature.sg3]
• (HalleMarantz1993.InflHead.agr false).features = []

def HalleMarantz1993.fusedFeatures (tPast tPart aSg3 : Bool) : List EngInflFeature

Compute the fused feature bundle for a Tns+Agr combination. Uses FusionRule.apply with list concatenation as the union operation.

Equations

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

theorem HalleMarantz1993.fusion_3sg_present : Morphology.DM.VI.subsetPrinciple englishTnsVI (fusedFeatures false false true) = some "-z"

3sg present: Tns[−past,−part] fused with Agr[3sg] → [sg3] → -z. One exponent realizes both heads.

theorem HalleMarantz1993.fusion_past : Morphology.DM.VI.subsetPrinciple englishTnsVI (fusedFeatures true false false) = some "-d"

Past finite: Tns[+past] fused with Agr[−3sg] → [past] → -d.

theorem HalleMarantz1993.fusion_past_participle : Morphology.DM.VI.subsetPrinciple englishTnsVI (fusedFeatures true true false) = some "-n"

Past participle: Tns[+past,+part] fused with Agr[−3sg] → [past, participle] → -n.

theorem HalleMarantz1993.fusion_present_participle : Morphology.DM.VI.subsetPrinciple englishTnsVI (fusedFeatures false true false) = some "-ing"

Present participle: Tns[−past,+part] fused with Agr[−3sg] → [participle] → -ing.

theorem HalleMarantz1993.fusion_elsewhere : Morphology.DM.VI.subsetPrinciple englishTnsVI (fusedFeatures false false false) = some "∅"

Elsewhere: Tns[−past,−part] fused with Agr[−3sg] → [] → ∅.

theorem HalleMarantz1993.fusion_always_spellable (tPast tPart aSg3 : Bool) : (Morphology.DM.VI.subsetPrinciple englishTnsVI (fusedFeatures tPast tPart aSg3)).isSome = true

Every Tns+Agr fusion produces a feature bundle that the VI paradigm can spell out — the paradigm is complete.

Impoverishment Derives Syncretism

[HM93] introduce Impoverishment: deletion of features from a terminal node before Vocabulary Insertion. When a distinguishing feature is deleted, two formerly distinct contexts fall together at VI, producing syncretism — distinct morphosyntactic specifications receiving the same exponent.

The general Impoverishment mechanism is formalized in Morphology/DM/Impoverishment.lean. Here we instantiate it on the English Tns/Agr paradigm to demonstrate the derivation of syncretism: deleting [+participle] from [+past, +participle] causes the past participle to receive the same exponent as simple past.

This models the fact that regular English verbs have identical simple past and past participle forms (walked does both): the [+participle] feature is not visible at VI, leaving only [+past] to trigger -d.

def HalleMarantz1993.deleteFeature (bundle : List EngInflFeature) (target : EngInflFeature) : List EngInflFeature

Delete occurrences of a feature from a bundle.

This mirrors deleteFeature in Morphology/DM/Impoverishment.lean, instantiated for EngInflFeature. The structural parallel is exact: both filter a list, removing elements that match the target.

Equations

• HalleMarantz1993.deleteFeature bundle target = List.filter (fun (x : HalleMarantz1993.EngInflFeature) => x != target) bundle

theorem HalleMarantz1993.deleteFeature_idempotent (bundle : List EngInflFeature) (target : EngInflFeature) : deleteFeature (deleteFeature bundle target) target = deleteFeature bundle target

Impoverishment is idempotent: deleting a feature twice is the same as deleting it once.

This mirrors deleteFeature_idempotent in Impoverishment.lean — filter is idempotent when the predicate is stable.

theorem HalleMarantz1993.impoverish_produces_syncretism : Morphology.DM.VI.subsetPrinciple englishTnsVI (deleteFeature [EngInflFeature.past, EngInflFeature.participle] EngInflFeature.participle) = Morphology.DM.VI.subsetPrinciple englishTnsVI [EngInflFeature.past]

Impoverishing [+participle] from [+past, +participle] produces syncretism: the impoverished bundle receives the same exponent as simple [+past].

theorem HalleMarantz1993.without_impoverishment_gets_n : Morphology.DM.VI.subsetPrinciple englishTnsVI [EngInflFeature.past, EngInflFeature.participle] = some "-n"

Without impoverishment, [+past, +participle] gets -n (taken, eaten).

theorem HalleMarantz1993.with_impoverishment_gets_d : Morphology.DM.VI.subsetPrinciple englishTnsVI (deleteFeature [EngInflFeature.past, EngInflFeature.participle] EngInflFeature.participle) = some "-d"

With impoverishment of [+participle], the same context gets -d (walked as both simple past and past participle).

theorem HalleMarantz1993.pipeline_fusion_impoverishment_vi : Morphology.DM.VI.subsetPrinciple englishTnsVI (deleteFeature (fusedFeatures true true false) EngInflFeature.participle) = some "-d"

Full DM pipeline: Fusion → Impoverishment → VI.

Past participle with impoverishment of [+participle]:

1. Fusion: Tns[+past,+part] + Agr[−3sg] → [past, participle]
2. Impoverishment: delete [+participle] → [past]
3. VI: [past] → -d

Without impoverishment, step 3 would give -n (via fusion_past_participle). This full pipeline connects §1 (VI), §3 (fusion), and §4 (impoverishment).

Connecting to the Mirror Principle and Bybee's Hierarchy

[HM93] discuss how DM's post-syntactic architecture derives [Bak85]'s Mirror Principle: GF-rules (passive, causative, applicative, reflexive/reciprocal) are syntactic head movements, and Morphological Structure preserves the derivation order. Affix layering necessarily mirrors syntactic structure because MS is derived from syntax.

We formalize two connections:

1. English verb inflection is concatenative, placing it within [Bak85]'s scope.

2. All English Tns/Agr features map to [Byb85] categories that are OUTSIDE GF-rule categories in the relevance hierarchy. This is consistent with DM's clause structure: Tns and Agr sit structurally above GF-rule projections, so their exponents are outermost after head movement.

def HalleMarantz1993.EngInflFeature.toMorphCategory : EngInflFeature → Morphology.MorphCategory

Map English inflectional features to [Byb85]'s morphological categories.

Equations

• HalleMarantz1993.EngInflFeature.past.toMorphCategory = Morphology.MorphCategory.tense
• HalleMarantz1993.EngInflFeature.participle.toMorphCategory = Morphology.MorphCategory.aspect
• HalleMarantz1993.EngInflFeature.sg3.toMorphCategory = Morphology.MorphCategory.agreement Agreement.Controller.subj

theorem HalleMarantz1993.tnsAgr_outside_gfRules (f : EngInflFeature) (r : Morphology.MirrorPrinciple.GFRuleType) : r.toMorphCategory.RelevanceLT f.toMorphCategory

All English Tns/Agr features map to categories that are OUTSIDE GF-rule categories in [Byb85]'s relevance hierarchy.

GF-rules (passive → voice rank 3, causative/applicative/reciprocal → valence rank 2) are always closer to the stem than English Tns/Agr features (aspect rank 4, tense rank 5, agreement rank 8).

This is consistent with DM's clause structure: Tns and Agr are structurally above GF-rule projections (PassP, CausP, ApplP), so after head movement and fusion, the Tns+Agr exponent sits outermost. The relevance hierarchy and the syntactic hierarchy converge — connecting [Bak85], [Byb85], and [HM93].

theorem HalleMarantz1993.english_inflection_in_scope : Morphology.MirrorPrinciple.MorphDomain.concatenative.InScope

English verb inflection is concatenative: affixes are linearly concatenated to the stem. This places it within the scope of [Bak85]'s Mirror Principle ([Bak85] restricts the principle to concatenative morphology, excluding clitics and nonconcatenative processes).