Distributed Morphology and the pieces of inflection

[HM93]'s English verb inflection: the seven suffixes of their (8) compete for the fused Tns–Agr node, and the principal parts of their (7) fall out. Their account of the regular verb's identical finite past and past participle is underspecification, not a participle rule — -d carries only [+past], and the only participle-specific past item is the stem-listed -n.

Main definitions

• Feature: the fused node's alphabet — binary [±past] and [±participle], the [3sg] agreement complex, and the stem the node is inserted next to (the paper's contextual feature).
• vocabulary: the items of (8), in the paper's order.
• tnsAgrFusion, tnsAgrSpellout: Agr, added at MS to [−participle] Tns nodes, fuses with Tns before insertion.

Main results

• principal_parts: every cell of (7) receives the suffix the paper segments.
• participle_eq_past_of_not_strong: the participle/finite-past syncretism of every stem outside the -n list, by underspecification.
• zero_morphemes_distinct: the stem-conditioned past ∅ and the Elsewhere ∅ are different Vocabulary Items.
• agr_only_on_finite: Fusion refuses a [+participle] Tns node.

Implementation notes

The paper says the ordering among the past block, [3sg] -z, and [+participle] -ing "is not determined by complexity" and "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 and is outside this file.

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 ⋯

@[instance_reducible]

instance HalleMarantz1993.instReprPart : Repr Part

Equations

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

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

Equations

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

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

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

Equations

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

@[instance_reducible]

instance HalleMarantz1993.instDecidableEqCell : DecidableEq Cell

Equations

• HalleMarantz1993.instDecidableEqCell = HalleMarantz1993.instDecidableEqCell.decEq

def HalleMarantz1993.instReprCell.repr : Cell → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance HalleMarantz1993.instReprCell : Repr Cell

Equations

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

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.ofExample (ex : Data.Examples.LinguisticExample) : 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_ofExample_isSome (ex : Data.Examples.LinguisticExample) : ex ∈ Examples.all → (Cell.ofExample 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.ofExample HalleMarantz1993.Examples.all

theorem HalleMarantz1993.principal_parts (c : Cell) : c ∈ cells → DistributedMorphology.subsetPrinciple vocabulary (DistributedMorphology.Neighborhood.ofBundle (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 (DistributedMorphology.Neighborhood.ofBundle (Part.pastParticiple.node v)) = DistributedMorphology.subsetPrinciple vocabulary (DistributedMorphology.Neighborhood.ofBundle (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 (DistributedMorphology.Neighborhood.ofBundle (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 (DistributedMorphology.Neighborhood.ofBundle (Part.pastFinite.node Verb.put)) ≠ DistributedMorphology.winner? vocabulary (DistributedMorphology.Neighborhood.ofBundle (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 (DistributedMorphology.Neighborhood.ofBundle (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.