The typological diversity of morphomes

[Her23] [Aro94]

Two paradigm fragments from [Her23] (The Typological Diversity of Morphomes, OUP) instantiate Morphology.IsMorphome: the Spanish L-morphome and a Darma agreement syncretism. Each is a systematic syncretism whose cell set is captured by no feature-value conjunction — the book's operationalization of "unnatural" (a natural class is one "coextensive with a value or conjunction of values", §1.4). Naturalness is supplied here as the value-or-conjunction predicate, the canonical instantiation of Morphology's Natural parameter.

Systematicity — recurrence under more than one exponent — is what distinguishes a morphome from an accidental homophony: the Spanish set recurs across three lexemes with three different stem alternations, the Darma set across two voice allomorphs.

Source caveat

The book's paradigm tables are images, so only cell sets and exponent labels recoverable from the surrounding prose are encoded (verbatim quotes cited below); full form-per-cell grids are not reproduced. Location cites are source-verified: Spanish §1.3 / Table 1.2, pp. 7-8; the definition §1.4, pp. 10-11; Darma §4.2.2.4, p. 149 (data from Willis 2007).

Main declarations

• Herce2023.spanishL_morphome_venir / _nacer / _caber — the L-morphome is a morphome under three distinct stem alternations
• Herce2023.darma_morphome_intr / _tr — the Darma 1PL/2 syncretism is a morphome under both voice allomorphs

Morphome from a kernel-class Finset

A reusable bridge: a nontrivial ker-class Finset that coincides with no Natural class is a Morphology.IsMorphome.

def Herce2023.kerClass {Cell : Type u_1} {S : Type u_2} [Fintype Cell] [DecidableEq S] (f : Cell → S) (a : Cell) : Finset Cell

The kernel class of a under f, as a Finset: the cells f sends to f a. Its coercion is Morphology.syncretismClass.

Equations

• Herce2023.kerClass f a = {c : Cell | f c = f a}

theorem Herce2023.coe_kerClass {Cell : Type u_1} {S : Type u_2} [Fintype Cell] [DecidableEq S] (f : Cell → S) (a : Cell) : ↑(kerClass f a) = Morphology.syncretismClass f a

theorem Herce2023.isMorphome_of_kerClass {Cell : Type u_1} {S : Type u_2} [Fintype Cell] [DecidableEq S] (f : Cell → S) (a : Cell) (X : Finset Cell) (Natural : Set Cell → Prop) (hker : kerClass f a = X) (hnt : 1 < X.card) (hnat : ¬Natural ↑X) : Morphology.IsMorphome f Natural ↑X

A nontrivial ker-class Finset that equals no natural class is a morphome.

Spanish L-morphome (§1.3, Table 1.2, pp. 7-8)

Verbatim (p. 7): the pattern "encompasses the 1SG present indicative and all the present subjunctive cells". The present-tense paradigm coordinates below are local slices (indicative/subjunctive × three persons × two numbers).

inductive Herce2023.Mood : Type

• ind : Mood
• sbjv : Mood

@[implicit_reducible]

instance Herce2023.instDecidableEqMood : DecidableEq Mood

Equations

• Herce2023.instDecidableEqMood x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Herce2023.instFintypeMood : Fintype Mood

Equations

• Herce2023.instFintypeMood = { elems := { val := ↑Herce2023.Mood.enumList, nodup := Herce2023.Mood.enumList_nodup }, complete := Herce2023.instFintypeMood._proof_1 }

def Herce2023.instReprMood.repr : Mood → ℕ → Std.Format

Equations

• Herce2023.instReprMood.repr Herce2023.Mood.ind prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Herce2023.Mood.ind")).group prec✝
• Herce2023.instReprMood.repr Herce2023.Mood.sbjv prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Herce2023.Mood.sbjv")).group prec✝

@[implicit_reducible]

instance Herce2023.instReprMood : Repr Mood

Equations

• Herce2023.instReprMood = { reprPrec := Herce2023.instReprMood.repr }

inductive Herce2023.Per : Type

• first : Per
• second : Per
• third : Per

@[implicit_reducible]

instance Herce2023.instDecidableEqPer : DecidableEq Per

Equations

• Herce2023.instDecidableEqPer x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Herce2023.instFintypePer : Fintype Per

Equations

• Herce2023.instFintypePer = { elems := { val := ↑Herce2023.Per.enumList, nodup := Herce2023.Per.enumList_nodup }, complete := Herce2023.instFintypePer._proof_1 }

def Herce2023.instReprPer.repr : Per → ℕ → Std.Format

Equations

• Herce2023.instReprPer.repr Herce2023.Per.first prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Herce2023.Per.first")).group prec✝
• Herce2023.instReprPer.repr Herce2023.Per.second prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Herce2023.Per.second")).group prec✝
• Herce2023.instReprPer.repr Herce2023.Per.third prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Herce2023.Per.third")).group prec✝

@[implicit_reducible]

instance Herce2023.instReprPer : Repr Per

Equations

• Herce2023.instReprPer = { reprPrec := Herce2023.instReprPer.repr }

inductive Herce2023.Num : Type

• sg : Num
• pl : Num

@[implicit_reducible]

instance Herce2023.instDecidableEqNum : DecidableEq Num

Equations

• Herce2023.instDecidableEqNum x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Herce2023.instFintypeNum : Fintype Num

Equations

• Herce2023.instFintypeNum = { elems := { val := ↑Herce2023.Num.enumList, nodup := Herce2023.Num.enumList_nodup }, complete := Herce2023.instFintypeNum._proof_1 }

@[implicit_reducible]

instance Herce2023.instReprNum : Repr Num

Equations

• Herce2023.instReprNum = { reprPrec := Herce2023.instReprNum.repr }

def Herce2023.instReprNum.repr : Num → ℕ → Std.Format

Equations

• Herce2023.instReprNum.repr Herce2023.Num.sg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Herce2023.Num.sg")).group prec✝
• Herce2023.instReprNum.repr Herce2023.Num.pl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Herce2023.Num.pl")).group prec✝

@[reducible, inline]

abbrev Herce2023.SpCell : Type

A present-tense cell: mood, person, number.

Equations

• Herce2023.SpCell = (Herce2023.Mood × Herce2023.Per × Herce2023.Num)

def Herce2023.Lset : Finset SpCell

The L-morphome cell set: 1SG present indicative together with all six present subjunctive cells (7 cells).

Equations

• Herce2023.Lset = insert (Herce2023.Mood.ind, Herce2023.Per.first, Herce2023.Num.sg) {c : Herce2023.SpCell | c.1 = Herce2023.Mood.sbjv}

def Herce2023.venirStem : SpCell → String

venir 'come': velar /g/ stem in the L-cells (vengo, venga…), base elsewhere. Defined by position, not by Lset — the syncretism is derived.

Equations

• Herce2023.venirStem (Herce2023.Mood.ind, Herce2023.Per.first, Herce2023.Num.sg) = "veng"
• Herce2023.venirStem (Herce2023.Mood.sbjv, fst, snd) = "veng"
• Herce2023.venirStem x✝ = "ven"

def Herce2023.nacerStem : SpCell → String

nacer 'be born': velar /k/ stem in the L-cells (nazco, nazca…).

Equations

• Herce2023.nacerStem (Herce2023.Mood.ind, Herce2023.Per.first, Herce2023.Num.sg) = "naθk"
• Herce2023.nacerStem (Herce2023.Mood.sbjv, fst, snd) = "naθk"
• Herce2023.nacerStem x✝ = "naθ"

def Herce2023.caberStem : SpCell → String

caber 'fit': suppletive stem in the L-cells (quepo, quepa…).

Equations

• Herce2023.caberStem (Herce2023.Mood.ind, Herce2023.Per.first, Herce2023.Num.sg) = "kep"
• Herce2023.caberStem (Herce2023.Mood.sbjv, fst, snd) = "kep"
• Herce2023.caberStem x✝ = "kab"

@[reducible, inline]

abbrev Herce2023.SpSpec : Type

A feature specification: each feature is fixed to a value or left open. A natural class is the set of cells matching some spec (coextensive with a value or conjunction of values, [Her23] §1.4).

Equations

• Herce2023.SpSpec = (Option Herce2023.Mood × Option Herce2023.Per × Option Herce2023.Num)

def Herce2023.spMatches (s : SpSpec) (c : SpCell) : Bool

Does cell c match spec s (open features vacuously match)?

Equations

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

def Herce2023.spNaturalClass (s : SpSpec) : Finset SpCell

The cells matching spec s.

Equations

• Herce2023.spNaturalClass s = {c : Herce2023.SpCell | Herce2023.spMatches s c = true}

def Herce2023.SpNatural (X : Set SpCell) : Prop

Naturalness for the Spanish space: coextensive with some feature-value conjunction.

Equations

• Herce2023.SpNatural X = ∃ (s : Herce2023.SpSpec), ↑(Herce2023.spNaturalClass s) = X

theorem Herce2023.venir_kerClass : kerClass venirStem (Mood.ind, Per.first, Num.sg) = Lset

theorem Herce2023.nacer_kerClass : kerClass nacerStem (Mood.ind, Per.first, Num.sg) = Lset

theorem Herce2023.caber_kerClass : kerClass caberStem (Mood.ind, Per.first, Num.sg) = Lset

theorem Herce2023.Lset_card : 1 < Lset.card

theorem Herce2023.Lset_no_natural_class (s : SpSpec) : spNaturalClass s ≠ Lset

No feature-value conjunction is coextensive with the L-set: it crosses the indicative/subjunctive divide, so it is unnatural.

theorem Herce2023.Lset_not_SpNatural : ¬SpNatural ↑Lset

theorem Herce2023.spanishL_morphome_venir : Morphology.IsMorphome venirStem SpNatural ↑Lset

The L-morphome under venir's velar /g/ alternation.

theorem Herce2023.spanishL_morphome_nacer : Morphology.IsMorphome nacerStem SpNatural ↑Lset

The same cell set under nacer's velar /k/ alternation — recurrence across a distinct exponent is what makes it systematic.

theorem Herce2023.spanishL_morphome_caber : Morphology.IsMorphome caberStem SpNatural ↑Lset

The same cell set under caber's stem suppletion.

Darma 1PL/2 syncretism (§4.2.2.4, p. 149; Willis 2007)

Verbatim: "verbal agreement is characterized by a syncretism of 1PL and 2 … The formal affinity … is, therefore, morphomic." The shared n-based suffix is -he in intransitive verbs, -de in transitive verbs. Only the attested three-cell set and the two allomorph labels are encoded; the full grid is an image (see the source caveat).

inductive Herce2023.Voice : Type

The two voice allomorphs of the n-suffix (-he intr, -de tr).

• intr : Voice
• tr : Voice

@[implicit_reducible]

instance Herce2023.instDecidableEqVoice : DecidableEq Voice

Equations

• Herce2023.instDecidableEqVoice x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Herce2023.instFintypeVoice : Fintype Voice

Equations

• Herce2023.instFintypeVoice = { elems := { val := ↑Herce2023.Voice.enumList, nodup := Herce2023.Voice.enumList_nodup }, complete := Herce2023.instFintypeVoice._proof_1 }

def Herce2023.instReprVoice.repr : Voice → ℕ → Std.Format

Equations

• Herce2023.instReprVoice.repr Herce2023.Voice.intr prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Herce2023.Voice.intr")).group prec✝
• Herce2023.instReprVoice.repr Herce2023.Voice.tr prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Herce2023.Voice.tr")).group prec✝

@[implicit_reducible]

instance Herce2023.instReprVoice : Repr Voice

Equations

• Herce2023.instReprVoice = { reprPrec := Herce2023.instReprVoice.repr }

@[reducible, inline]

abbrev Herce2023.DCell : Type

A Darma agreement cell: person, number.

Equations

• Herce2023.DCell = (Herce2023.Per × Herce2023.Num)

def Herce2023.Dset : Finset DCell

The syncretic set: 1PL, 2SG, 2PL (three cells).

Equations

• Herce2023.Dset = {(Herce2023.Per.first, Herce2023.Num.pl), (Herce2023.Per.second, Herce2023.Num.sg), (Herce2023.Per.second, Herce2023.Num.pl)}

def Herce2023.darmaAgr (v : Voice) : DCell → Option Voice

The n-based agreement suffix, keyed by voice: the syncretic cells bear it (value = the voice allomorph), other cells are left uncharacterized (none), since the full grid is not recoverable. Defined by position.

Equations

• Herce2023.darmaAgr v (Herce2023.Per.first, Herce2023.Num.pl) = some v
• Herce2023.darmaAgr v (Herce2023.Per.second, snd) = some v
• Herce2023.darmaAgr v x✝ = none

@[reducible, inline]

abbrev Herce2023.DSpec : Type

A Darma feature spec (person × number).

Equations

• Herce2023.DSpec = (Option Herce2023.Per × Option Herce2023.Num)

def Herce2023.dMatches (s : DSpec) (c : DCell) : Bool

Equations

• Herce2023.dMatches s c = ((match s.1 with | none => true | some p => decide (p = c.1)) && match s.2 with | none => true | some n => decide (n = c.2))

def Herce2023.dNaturalClass (s : DSpec) : Finset DCell

Equations

• Herce2023.dNaturalClass s = {c : Herce2023.DCell | Herce2023.dMatches s c = true}

def Herce2023.DNatural (X : Set DCell) : Prop

Equations

• Herce2023.DNatural X = ∃ (s : Herce2023.DSpec), ↑(Herce2023.dNaturalClass s) = X

theorem Herce2023.darma_kerClass_intr : kerClass (darmaAgr Voice.intr) (Per.second, Num.sg) = Dset

theorem Herce2023.darma_kerClass_tr : kerClass (darmaAgr Voice.tr) (Per.second, Num.sg) = Dset

theorem Herce2023.Dset_card : 1 < Dset.card

theorem Herce2023.Dset_no_natural_class (s : DSpec) : dNaturalClass s ≠ Dset

{1PL, 2SG, 2PL} crosses persons 1 and 2 and fixes no number, so no feature-value conjunction is coextensive with it.

theorem Herce2023.Dset_not_DNatural : ¬DNatural ↑Dset

theorem Herce2023.darma_morphome_intr : Morphology.IsMorphome (darmaAgr Voice.intr) DNatural ↑Dset

The 1PL/2 syncretism is a morphome under the intransitive allomorph -he.

theorem Herce2023.darma_morphome_tr : Morphology.IsMorphome (darmaAgr Voice.tr) DNatural ↑Dset

…and under the transitive allomorph -de: recurrence across the two allomorphs establishes systematicity.