Halle and Marantz (1993): Distributed Morphology and the Pieces of Inflection

This file formalizes the English verb inflection of [HM93], section 3.1. The seven suffixes of (8) compete under the Subset Principle for the fused Tns–Agr node, vocabulary, and the principal parts of (7) fall out, principal_parts. The node's features are the binary [±past] and [±participle], the [3sg] agreement complex, and the stem the node is inserted next to, the paper's contextual feature; Agr is added at MS to [−participle] Tns nodes and fuses with Tns before insertion, tnsAgrFusion, so a participial node takes no Agr, agr_only_on_finite. The regular verb's identical finite past and past participle is underspecification rather than a participle rule: -d carries only [+past], and the only participle-specific past item is the stem-listed -n, participle_eq_past_of_not_strong; the stem-conditioned past ∅ and the Elsewhere ∅ are distinct items, zero_morphemes_distinct.

Implementation notes

The paper says the ordering between the ∅ and -t pasts "is not determined by complexity" and needs none, since their stem lists are disjoint, and that the ordering among the past block, [3sg] -z, and [+participle] -ing "must be stipulated"; the Subset Principle's count ties at those points, and the list order of vocabulary carries the stipulation, past_precedes_agreement. Stem readjustment (dwel-t, brough-t) is the paper's separate rule system (10) and is outside this file.

References

• [HM93]

The fused Tns–Agr node

inductive HalleMarantz1993.Verb : Type

The four stems of (7), one per past-suffix class.

• beat : Verb
• put : Verb
• dwell : Verb
• play : Verb

@[instance_reducible]

instance HalleMarantz1993.instDecidableEqVerb : DecidableEq Verb

Equations

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

def HalleMarantz1993.instReprVerb.repr : Verb → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• HalleMarantz1993.instReprVerb.repr HalleMarantz1993.Verb.put prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HalleMarantz1993.Verb.put")).group prec✝

@[instance_reducible]

instance HalleMarantz1993.instReprVerb : Repr Verb

Equations

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

inductive HalleMarantz1993.Feature : Type

Features at the fused Tns–Agr node: the paper's binary [±past] and [±participle], its [3sg] person–number complex, and the adjacent stem.

• past (b : Bool) : Feature
• participle (b : Bool) : Feature
• sg3 : Feature
• stem (v : Verb) : Feature

def HalleMarantz1993.instDecidableEqFeature.decEq (x✝ x✝¹ : Feature) : Decidable (x✝ = x✝¹)

Equations

• HalleMarantz1993.instDecidableEqFeature.decEq (HalleMarantz1993.Feature.past a) (HalleMarantz1993.Feature.past b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• HalleMarantz1993.instDecidableEqFeature.decEq (HalleMarantz1993.Feature.past b) (HalleMarantz1993.Feature.participle b_1) = isFalse ⋯
• HalleMarantz1993.instDecidableEqFeature.decEq (HalleMarantz1993.Feature.past b) HalleMarantz1993.Feature.sg3 = isFalse ⋯
• HalleMarantz1993.instDecidableEqFeature.decEq (HalleMarantz1993.Feature.past b) (HalleMarantz1993.Feature.stem v) = isFalse ⋯
• HalleMarantz1993.instDecidableEqFeature.decEq (HalleMarantz1993.Feature.participle b) (HalleMarantz1993.Feature.past b_1) = isFalse ⋯
• HalleMarantz1993.instDecidableEqFeature.decEq (HalleMarantz1993.Feature.participle a) (HalleMarantz1993.Feature.participle b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• HalleMarantz1993.instDecidableEqFeature.decEq (HalleMarantz1993.Feature.participle b) HalleMarantz1993.Feature.sg3 = isFalse ⋯
• HalleMarantz1993.instDecidableEqFeature.decEq (HalleMarantz1993.Feature.participle b) (HalleMarantz1993.Feature.stem v) = isFalse ⋯
• HalleMarantz1993.instDecidableEqFeature.decEq HalleMarantz1993.Feature.sg3 (HalleMarantz1993.Feature.past b) = isFalse ⋯
• HalleMarantz1993.instDecidableEqFeature.decEq HalleMarantz1993.Feature.sg3 (HalleMarantz1993.Feature.participle b) = isFalse ⋯
• HalleMarantz1993.instDecidableEqFeature.decEq HalleMarantz1993.Feature.sg3 HalleMarantz1993.Feature.sg3 = isTrue ⋯
• HalleMarantz1993.instDecidableEqFeature.decEq HalleMarantz1993.Feature.sg3 (HalleMarantz1993.Feature.stem v) = isFalse ⋯
• HalleMarantz1993.instDecidableEqFeature.decEq (HalleMarantz1993.Feature.stem v) (HalleMarantz1993.Feature.past b) = isFalse ⋯
• HalleMarantz1993.instDecidableEqFeature.decEq (HalleMarantz1993.Feature.stem v) (HalleMarantz1993.Feature.participle b) = isFalse ⋯
• HalleMarantz1993.instDecidableEqFeature.decEq (HalleMarantz1993.Feature.stem v) HalleMarantz1993.Feature.sg3 = isFalse ⋯
• HalleMarantz1993.instDecidableEqFeature.decEq (HalleMarantz1993.Feature.stem a) (HalleMarantz1993.Feature.stem b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HalleMarantz1993.instDecidableEqFeature : DecidableEq Feature

Equations

• HalleMarantz1993.instDecidableEqFeature = HalleMarantz1993.instDecidableEqFeature.decEq

@[instance_reducible]

instance HalleMarantz1993.instReprFeature : Repr Feature

Equations

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

def HalleMarantz1993.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

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

def HalleMarantz1993.tns (v : Verb) (past participle : Bool) : List Feature

A Tns node next to stem v.

Equations

• HalleMarantz1993.tns v past participle = [HalleMarantz1993.Feature.past past, HalleMarantz1993.Feature.participle participle, HalleMarantz1993.Feature.stem v]

def HalleMarantz1993.agr (sg3 : Bool) : List Feature

The Agr node added at MS: the [3sg] complex or the unmarked one.

Equations

• HalleMarantz1993.agr sg3 = if sg3 = true then [HalleMarantz1993.Feature.sg3] else []

def HalleMarantz1993.tnsAgrFusion : DistributedMorphology.FusionRule Feature

Agr fuses with a [−participle] Tns node into one terminal bearing both bundles.

Equations

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

def HalleMarantz1993.tnsAgr (v : Verb) (past sg3 : Bool) : List Feature

The fused node of a finite form.

Equations

• HalleMarantz1993.tnsAgr v past sg3 = HalleMarantz1993.tns v past false ++ HalleMarantz1993.agr sg3

theorem HalleMarantz1993.agr_only_on_finite (v : Verb) (past sg3 : Bool) : tnsAgrFusion.apply (tns v past true) (agr sg3) = none

Agr is added only to [−participle] nodes: Fusion rejects a participial Tns.

The Vocabulary (8)

def HalleMarantz1993.strongParticiple : List Verb

Stems taking -n in the past participle (beat-en).

Equations

• HalleMarantz1993.strongParticiple = [HalleMarantz1993.Verb.beat]

def HalleMarantz1993.strongPast : List Verb

Stems taking the ∅ past (beat, put).

Equations

• HalleMarantz1993.strongPast = [HalleMarantz1993.Verb.beat, HalleMarantz1993.Verb.put]

def HalleMarantz1993.tPast : List Verb

Stems taking the -t past (dwel-t).

Equations

• HalleMarantz1993.tPast = [HalleMarantz1993.Verb.dwell]

def HalleMarantz1993.forStems (features : List Feature) (e : String) (stems : List Verb) : List (DistributedMorphology.VocabularyItem Feature String)

The items of a stem-conditioned suffix: one per listed stem, the paper's disjunctive list in a contextual feature.

Equations

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

def HalleMarantz1993.vocabulary : List (DistributedMorphology.VocabularyItem Feature String)

The seven suffixes of (8): the past block (-n, the unordered ∅ and -t, default -d), then [3sg] -z, [+participle] -ing, and the Elsewhere ∅.

Equations

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

theorem HalleMarantz1993.strongPast_disjoint_tPast : strongPast.Disjoint tPast

The ∅ and -t pasts "are not ordered by complexity" and need no ordering: their stem lists are disjoint.

The principal parts (7)

inductive HalleMarantz1993.Part : Type

A row of (7).

• pastParticiple : Part
• pastFinite : Part
• nonpast3sg : Part
• nonpastParticiple : Part
• nonpastFinite : Part

@[instance_reducible]

instance HalleMarantz1993.instDecidableEqPart : DecidableEq Part

Equations

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

def HalleMarantz1993.instReprPart.repr : Part → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance HalleMarantz1993.instReprPart : Repr Part

Equations

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

def HalleMarantz1993.Part.node : Part → Verb → List Feature

The fused node a row is spelled out at; participles take no Agr.

Equations

• HalleMarantz1993.Part.pastParticiple.node x✝ = HalleMarantz1993.tns x✝ true true
• HalleMarantz1993.Part.pastFinite.node x✝ = HalleMarantz1993.tnsAgr x✝ true false
• HalleMarantz1993.Part.nonpast3sg.node x✝ = HalleMarantz1993.tnsAgr x✝ false true
• HalleMarantz1993.Part.nonpastParticiple.node x✝ = HalleMarantz1993.tns x✝ false true
• HalleMarantz1993.Part.nonpastFinite.node x✝ = HalleMarantz1993.tnsAgr x✝ false false

structure HalleMarantz1993.Cell : Type

A cell of (7): stem, row, and the suffix the paper segments.

• verb : Verb
• part : Part
• suffix : String

@[instance_reducible]

instance HalleMarantz1993.instDecidableEqCell : DecidableEq Cell

Equations

• HalleMarantz1993.instDecidableEqCell = HalleMarantz1993.instDecidableEqCell.decEq

def HalleMarantz1993.instDecidableEqCell.decEq (x✝ x✝¹ : Cell) : Decidable (x✝ = x✝¹)

Equations

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

def HalleMarantz1993.Verb.ofString : String → Option Verb

Equations

• HalleMarantz1993.Verb.ofString "beat" = some HalleMarantz1993.Verb.beat
• HalleMarantz1993.Verb.ofString "put" = some HalleMarantz1993.Verb.put
• HalleMarantz1993.Verb.ofString "dwell" = some HalleMarantz1993.Verb.dwell
• HalleMarantz1993.Verb.ofString "play" = some HalleMarantz1993.Verb.play
• HalleMarantz1993.Verb.ofString x✝ = none

def HalleMarantz1993.Part.ofString : String → Option Part

Equations

• HalleMarantz1993.Part.ofString "past_participle" = some HalleMarantz1993.Part.pastParticiple
• HalleMarantz1993.Part.ofString "past_finite" = some HalleMarantz1993.Part.pastFinite
• HalleMarantz1993.Part.ofString "nonpast_3sg" = some HalleMarantz1993.Part.nonpast3sg
• HalleMarantz1993.Part.ofString "nonpast_participle" = some HalleMarantz1993.Part.nonpastParticiple
• HalleMarantz1993.Part.ofString "nonpast_finite" = some HalleMarantz1993.Part.nonpastFinite
• HalleMarantz1993.Part.ofString x✝ = none

def HalleMarantz1993.Cell.ofDatum (ex : Datum) : Option Cell

The cell an example of (7) records, from its paperFeatures.

Equations

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

theorem HalleMarantz1993.cell_ofDatum_isSome (ex : Datum) : ex ∈ Examples.all → (Cell.ofDatum ex).isSome = true

Every row of the data pool is a well-formed cell.

def HalleMarantz1993.cells : List Cell

The cells of (7).

Equations

• HalleMarantz1993.cells = List.filterMap HalleMarantz1993.Cell.ofDatum HalleMarantz1993.Examples.all

theorem HalleMarantz1993.principal_parts (c : Cell) : c ∈ cells → DistributedMorphology.subsetPrinciple vocabulary ↑(c.part.node c.verb) = some c.suffix

The principal parts: the Subset Principle over (8) spells out every cell of (7) with the suffix the paper segments.

What the competition explains

theorem HalleMarantz1993.participle_eq_past_of_not_strong (v : Verb) (hv : v ∉ strongParticiple) : DistributedMorphology.subsetPrinciple vocabulary ↑(Part.pastParticiple.node v) = DistributedMorphology.subsetPrinciple vocabulary ↑(Part.pastFinite.node v)

Syncretism by underspecification: outside the -n list, the past participle and the finite past receive the same suffix, because every past item but -n carries only [+past].

theorem HalleMarantz1993.zero_past_blocks_default : DistributedMorphology.winner? vocabulary ↑(Part.pastFinite.node Verb.put) = some (DistributedMorphology.VocabularyItem.ofFeatures [Feature.past true, Feature.stem Verb.put] "∅")

The stem-conditioned past ∅ (put) blocks the default -d: the winner is the stem-listed item.

theorem HalleMarantz1993.zero_morphemes_distinct : DistributedMorphology.winner? vocabulary ↑(Part.pastFinite.node Verb.put) ≠ DistributedMorphology.winner? vocabulary ↑(Part.nonpastFinite.node Verb.put)

The paper's two zero morphemes are different items: the stem-conditioned past ∅ and the Elsewhere ∅ of the nonpast finite node.

theorem HalleMarantz1993.past_precedes_agreement : DistributedMorphology.subsetPrinciple vocabulary ↑(tnsAgr Verb.play true true) = some "-d"

The stipulated block order: at a [+past] node that is also [3sg], -d and -z tie on specificity and the past block's precedence in vocabulary decides — play-ed, not play-s.

Fusion in the spell-out pipeline

def HalleMarantz1993.tnsAgrSpellout : DistributedMorphology.Spellout (List Feature) String

Fusion of adjacent Tns and Agr, then insertion by the Subset Principle.

Equations

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

theorem HalleMarantz1993.plays_pf : tnsAgrSpellout.pf [tns Verb.play false false, agr true] = [["-z"]]

play-s: the domain [Tns, Agr] spells out as the single exponent -z.

theorem HalleMarantz1993.plays_misalignment : [tns Verb.play false false, agr true].length = 2 ∧ (tnsAgrSpellout.pf [tns Verb.play false false, agr true]).length = 1

Two terminals enter, one exponent slot leaves: the misalignment is carried by the fusion module.