Herce (2023): The Typological Diversity of Morphomes

This file formalizes two morphomes of [herce-2023] as instances of Morphology.IsMorphome, the book's working definition of a morphome as a systematic syncretism that is not a natural class (§1.4), with a natural class one coextensive with a value or conjunction of values, Morphology.IsValueConjunction. The Spanish L-morphome of Table 1.2, the first person singular of the present indicative together with the whole present subjunctive, is the syncretism class of the velar stems of venir and nacer and of the suppletive stem of caber (venir_morphome); the Darma syncretism of Table 4.32, the first person plural with the second person, is the class of the non-past suffix -he-n and of the past suffix -n-su of ra 'come' (nonpast_morphome). Each class is a value conjunction of none of its paradigm's features (Lset_not_natural), and its recurrence under distinct exponents is the systematicity the definition asks for.

Implementation notes

• The paradigms are Table 1.2 and Table 4.32 as printed, stems and suffixes typed as the tables segment them: venir has the diphthongized stem in the second and third singular and third plural of the indicative, the optional final -i of the Darma second person plural non-past is dropped, and the transitive allomorph -de is prose.
• The definition also returns the past-tense class of -ju, the elsewhere form, the limitation the substrate records.

References

• [herce-2023]
• [aronoff-1994]

The Spanish L-morphome (Table 1.2)

inductive Herce2023.Mood : Type

The moods of the present tense.

• ind : Mood
• sbjv : Mood

@[instance_reducible]

instance Herce2023.instDecidableEqMood : DecidableEq Mood

Equations

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

@[instance_reducible]

instance Herce2023.instFintypeMood : Fintype Mood

Equations

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

inductive Herce2023.Per : Type

Grammatical person.

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

@[instance_reducible]

instance Herce2023.instDecidableEqPer : DecidableEq Per

Equations

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

@[instance_reducible]

instance Herce2023.instFintypePer : Fintype Per

Equations

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

inductive Herce2023.Num : Type

Grammatical number.

• sg : Num
• pl : Num

@[instance_reducible]

instance Herce2023.instDecidableEqNum : DecidableEq Num

Equations

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

@[instance_reducible]

instance Herce2023.instFintypeNum : Fintype Num

Equations

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

@[reducible, inline]

abbrev Herce2023.SpCell : Type

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

Equations

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

inductive Herce2023.SpFeature : Type

The features of a present-tense cell.

• mood : SpFeature
• person : SpFeature
• number : SpFeature

@[instance_reducible]

instance Herce2023.instDecidableEqSpFeature : DecidableEq SpFeature

Equations

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

@[instance_reducible]

instance Herce2023.instFintypeSpFeature : Fintype SpFeature

Equations

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

def Herce2023.spFeatures : SpFeature → Setoid SpCell

The partition of the present-tense cells a feature induces.

Equations

• Herce2023.spFeatures Herce2023.SpFeature.mood = Setoid.ker Prod.fst
• Herce2023.spFeatures Herce2023.SpFeature.person = Setoid.ker fun (c : Herce2023.SpCell) => c.2.1
• Herce2023.spFeatures Herce2023.SpFeature.number = Setoid.ker fun (c : Herce2023.SpCell) => c.2.2

@[instance_reducible]

instance Herce2023.instDecidableRelSpCellR (i : SpFeature) : DecidableRel ⇑(spFeatures i)

Equations

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

inductive Herce2023.Stem : Type

The stems of Table 1.2: venir with /ven/, diphthongized /vjen/ and velar /veng/; nacer with /naθ/ and velar /naθk/; caber with /kab/ and weakly suppletive /kep/.

• ven : Stem
• vjen : Stem
• veng : Stem
• naθ : Stem
• naθk : Stem
• kab : Stem
• kep : Stem

@[instance_reducible]

instance Herce2023.instDecidableEqStem : DecidableEq Stem

Equations

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

@[instance_reducible]

instance Herce2023.instFintypeStem : Fintype Stem

Equations

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

def Herce2023.venir : SpCell → Stem

The stem of venir 'come' in each present-tense cell.

Equations

• Herce2023.venir (Herce2023.Mood.ind, Herce2023.Per.first, Herce2023.Num.sg) = Herce2023.Stem.veng
• Herce2023.venir (Herce2023.Mood.ind, Herce2023.Per.second, Herce2023.Num.sg) = Herce2023.Stem.vjen
• Herce2023.venir (Herce2023.Mood.ind, Herce2023.Per.third, Herce2023.Num.sg) = Herce2023.Stem.vjen
• Herce2023.venir (Herce2023.Mood.ind, Herce2023.Per.third, Herce2023.Num.pl) = Herce2023.Stem.vjen
• Herce2023.venir (Herce2023.Mood.ind, fst, Herce2023.Num.pl) = Herce2023.Stem.ven
• Herce2023.venir (Herce2023.Mood.sbjv, fst, snd) = Herce2023.Stem.veng

def Herce2023.nacer : SpCell → Stem

The stem of nacer 'be born' in each present-tense cell.

Equations

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

def Herce2023.caber : SpCell → Stem

The stem of caber 'fit' in each present-tense cell.

Equations

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

def Herce2023.Lset : Finset SpCell

The cells of the L-morphome: the first person singular of the present indicative and the whole present subjunctive.

Equations

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

theorem Herce2023.venir_formCells : Morphology.formCells venir Stem.veng = Lset

theorem Herce2023.nacer_formCells : Morphology.formCells nacer Stem.naθk = Lset

theorem Herce2023.caber_formCells : Morphology.formCells caber Stem.kep = Lset

theorem Herce2023.Lset_not_natural : ¬Morphology.IsValueConjunction spFeatures ↑Lset

The L-morphome is a value conjunction of no features: it crosses the moods without exhausting either.

theorem Herce2023.venir_morphome : Morphology.IsMorphome venir (Morphology.IsValueConjunction spFeatures) ↑Lset

The L-morphome under the velar /g/ stem of venir.

theorem Herce2023.nacer_morphome : Morphology.IsMorphome nacer (Morphology.IsValueConjunction spFeatures) ↑Lset

The L-morphome under the velar /k/ stem of nacer: the same cells under a distinct exponent.

theorem Herce2023.caber_morphome : Morphology.IsMorphome caber (Morphology.IsValueConjunction spFeatures) ↑Lset

The L-morphome under the suppletive stem of caber.

The Darma first person plural and second person (§4.2.2.4, Table 4.32)

@[reducible, inline]

abbrev Herce2023.DCell : Type

A Darma agreement cell: person and number.

Equations

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

inductive Herce2023.DFeature : Type

The features of an agreement cell.

• person : DFeature
• number : DFeature

@[instance_reducible]

instance Herce2023.instDecidableEqDFeature : DecidableEq DFeature

Equations

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

@[instance_reducible]

instance Herce2023.instFintypeDFeature : Fintype DFeature

Equations

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

def Herce2023.dFeatures : DFeature → Setoid DCell

The partition of the agreement cells a feature induces.

Equations

• Herce2023.dFeatures Herce2023.DFeature.person = Setoid.ker Prod.fst
• Herce2023.dFeatures Herce2023.DFeature.number = Setoid.ker Prod.snd

@[instance_reducible]

instance Herce2023.instDecidableRelDCellR (i : DFeature) : DecidableRel ⇑(dFeatures i)

Equations

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

inductive Herce2023.Suffix : Type

The agreement suffixes of ra 'come' in Table 4.32: non-past -hi, -he-n and -ni, past -ju and -n-su.

• hi : Suffix
• hen : Suffix
• ni : Suffix
• ju : Suffix
• nsu : Suffix

@[instance_reducible]

instance Herce2023.instDecidableEqSuffix : DecidableEq Suffix

Equations

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

@[instance_reducible]

instance Herce2023.instFintypeSuffix : Fintype Suffix

Equations

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

def Herce2023.nonpast : DCell → Suffix

The non-past suffix of each agreement cell.

Equations

• Herce2023.nonpast (Herce2023.Per.first, Herce2023.Num.sg) = Herce2023.Suffix.hi
• Herce2023.nonpast (Herce2023.Per.first, Herce2023.Num.pl) = Herce2023.Suffix.hen
• Herce2023.nonpast (Herce2023.Per.second, snd) = Herce2023.Suffix.hen
• Herce2023.nonpast (Herce2023.Per.third, snd) = Herce2023.Suffix.ni

def Herce2023.past : DCell → Suffix

The past suffix of each agreement cell.

Equations

• Herce2023.past (Herce2023.Per.first, Herce2023.Num.pl) = Herce2023.Suffix.nsu
• Herce2023.past (Herce2023.Per.second, snd) = Herce2023.Suffix.nsu
• Herce2023.past x✝ = Herce2023.Suffix.ju

def Herce2023.Dset : Finset DCell

The syncretic cells: the first person plural and the second person.

Equations

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

theorem Herce2023.nonpast_formCells : Morphology.formCells nonpast Suffix.hen = Dset

theorem Herce2023.past_formCells : Morphology.formCells past Suffix.nsu = Dset

theorem Herce2023.Dset_not_natural : ¬Morphology.IsValueConjunction dFeatures ↑Dset

The syncretic cells are a value conjunction of no features: they cross the persons and fix no number.

theorem Herce2023.nonpast_morphome : Morphology.IsMorphome nonpast (Morphology.IsValueConjunction dFeatures) ↑Dset

The syncretism under the non-past suffix -he-n.

theorem Herce2023.past_morphome : Morphology.IsMorphome past (Morphology.IsValueConjunction dFeatures) ↑Dset

The syncretism under the past suffix -n-su: the same cells under a distinct exponent, across tenses.