Morphomes: syncretism classes with no natural characterization

A realization map p : Cell → F assigns a form to each paradigm cell. Its syncretism relation — cells receiving the same form — is exactly mathlib's kernel setoid Setoid.ker p, and the syncretism classes are its equivalence classes. A morphome ([aronoff-1994] coined the term) is a systematic syncretism that does not define a natural class; [herce-2023] adopts the working definition "a systematic morphological syncretism which does not define a (syntactically or semantically) natural class" (Trommer 2016, quoted approvingly).

Naturalness is a parameter Natural : Set Cell → Prop, not stipulated here. [herce-2023] operationalizes a natural class as one "coextensive with a value (e.g. SG) or conjunction of values (e.g. 1SG)" and treats naturalness as gradient, so Natural is best read as a threshold slice of that scale; the value-or-conjunction predicate is its canonical instantiation, IsValueConjunction: the cells agreeing with some cell on some of the paradigm's features, each feature given as the partition of cells it induces. Systematicity — recurrence of the pattern under more than one exponent or allomorph — is a separate criterion the consumer establishes.

Two limitations, per [baerman-2015]'s three-way analysis space for syncretism (morphosyntactic identity / underspecification / morphological stipulation, p. 146): an elsewhere form's fiber is typically also nontrivial and non-natural (one specified cell, the default covers the unnatural rest — Skou, p. 145), so IsMorphome is necessary but not sufficient for stipulation-hood; distinguishing the two needs opposition structure or the systematicity criterion above. And directional syncretism (a cell wearing another cell's form "in place of the expected" one, p. 142) is invisible to the symmetric kernel.

The vocabulary here is deliberately just "morphome": [herce-2023] rejects Round's rhizomorphome metamorphome meromorphome subdivision as needless jargon, and "metasyncretism" does not appear in the book.

Main declarations

• Morphology.syncretism — the syncretism setoid of a realization map (Setoid.ker)
• Morphology.syncretismClass — the class (fiber) of a given cell
• Morphology.formCells — the cells a form realizes, the Finset face of the class
• Morphology.IsMorphome — a nontrivial syncretism class failing Natural
• Morphology.IsValueConjunction — the cells agreeing with a witness on a set of features, [herce-2023]'s natural class

@[reducible, inline]

abbrev Morphology.syncretism {Cell : Type u_1} {F : Type u_2} (p : Cell → F) : Setoid Cell

The syncretism relation of a realization map p: two cells are syncretic iff p assigns them the same form. Exactly the kernel setoid Setoid.ker p; its equivalence classes are the paradigm's syncretism patterns.

Equations

• Morphology.syncretism p = Setoid.ker p

theorem Morphology.syncretism_eq_iff {Cell : Type u_1} {F : Type u_2} {G : Type u_3} {p : Cell → F} {q : Cell → G} : syncretism p = syncretism q ↔ ∀ (a b : Cell), p a = p b ↔ q a = q b

Two realization maps have the same syncretism pattern iff they identify the same pairs of cells.

def Morphology.syncretismClass {Cell : Type u_1} {F : Type u_2} (p : Cell → F) (a : Cell) : Set Cell

The syncretism class of a cell a: every cell realized as a is.

Equations

• Morphology.syncretismClass p a = {x : Cell | p x = p a}

theorem Morphology.syncretismClass_mem_classes {Cell : Type u_1} {F : Type u_2} (p : Cell → F) (a : Cell) : syncretismClass p a ∈ (syncretism p).classes

def Morphology.formCells {Cell : Type u_1} {F : Type u_2} [Fintype Cell] [DecidableEq F] (p : Cell → F) (f : F) : Finset Cell

The cells p realizes as the form f: the syncretism class of any cell realized as f, as a Finset.

Equations

• Morphology.formCells p f = {x : Cell | p x = f}

@[simp]

theorem Morphology.mem_formCells {Cell : Type u_1} {F : Type u_2} [Fintype Cell] [DecidableEq F] {p : Cell → F} {f : F} {c : Cell} : c ∈ formCells p f ↔ p c = f

theorem Morphology.coe_formCells {Cell : Type u_1} {F : Type u_2} [Fintype Cell] [DecidableEq F] (p : Cell → F) (a : Cell) : ↑(formCells p (p a)) = syncretismClass p a

def Morphology.IsMorphome {Cell : Type u_1} {F : Type u_2} (p : Cell → F) (Natural : Set Cell → Prop) (c : Set Cell) : Prop

A morphome ([herce-2023]): a syncretism class of p that groups more than one cell (Set.Nontrivial) yet is not a Natural class — a grouping visible only in the realization, with no phonological, syntactic, or semantic characterization ([aronoff-1994]'s "morphology by itself"). Natural is a parameter (see the module docstring).

Equations

• Morphology.IsMorphome p Natural c = (c ∈ (Morphology.syncretism p).classes ∧ c.Nontrivial ∧ ¬Natural c)

theorem Morphology.isMorphome_syncretismClass {Cell : Type u_1} {F : Type u_2} (p : Cell → F) (Natural : Set Cell → Prop) (a : Cell) (hnt : (syncretismClass p a).Nontrivial) (hnat : ¬Natural (syncretismClass p a)) : IsMorphome p Natural (syncretismClass p a)

The syncretism class of a is a morphome once it is nontrivial and unnatural — the shape a concrete paradigm instantiates.

theorem Morphology.isMorphome_of_formCells {Cell : Type u_1} {F : Type u_2} [Fintype Cell] [DecidableEq F] (p : Cell → F) (a : Cell) (Natural : Set Cell → Prop) {X : Finset Cell} (hX : formCells p (p a) = X) (hnt : 1 < X.card) (hnat : ¬Natural ↑X) : IsMorphome p Natural ↑X

The Finset face of isMorphome_syncretismClass: the cells a form realizes are a morphome once there are at least two of them and they are not a natural class.

Natural classes as value conjunctions

[herce-2023] takes a natural class to be one "coextensive with a value or conjunction of values". A paradigm's features are the partitions of its cells they induce, the kernels of the feature projections; a value conjunction is then the set of cells agreeing with some cell on some of the features.

def Morphology.IsValueConjunction {Cell : Type u_1} {ι : Type u_4} (feats : ι → Setoid Cell) (X : Set Cell) : Prop

A set of cells is a value conjunction for the features feats when it consists of the cells agreeing with some cell on some of the features.

Equations

• Morphology.IsValueConjunction feats X = ∃ (S : Finset ι) (c₀ : Cell), X = {c : Cell | ∀ i ∈ S, (feats i) c c₀}

theorem Morphology.isValueConjunction_coe_iff {Cell : Type u_1} {ι : Type u_4} [Fintype Cell] [DecidableEq Cell] (feats : ι → Setoid Cell) [(i : ι) → DecidableRel ⇑(feats i)] (X : Finset Cell) : IsValueConjunction feats ↑X ↔ ∃ (S : Finset ι) (c₀ : Cell), {c : Cell | ∀ i ∈ S, (feats i) c c₀} = X

On a finite paradigm, being a value conjunction is a finite search over the features and the witness cell.

Shared exponents in segmented realizations

Whole-form kernels cannot see a piece shared across cells whose full forms differ (a suffix shared by two segmented stems, like Chuj -aj inside -chaj and -waj). For a realization map valued in exponent sequences, exponentCells tracks a piece's distribution; whether that distribution is a natural class is then the same question IsMorphome asks of whole-form classes.

def Morphology.exponentCells {Cell : Type u_1} {E : Type u_5} (p : Cell → List E) (e : E) : Set Cell

The cells whose segmented realization contains the exponent e — the piece-level analogue of syncretismClass.

Equations

• Morphology.exponentCells p e = {c : Cell | e ∈ p c}

@[simp]

theorem Morphology.mem_exponentCells {Cell : Type u_1} {E : Type u_5} {p : Cell → List E} {e : E} {c : Cell} : c ∈ exponentCells p e ↔ e ∈ p c

theorem Morphology.exponentCells_congr {Cell : Type u_1} {E : Type u_5} (p : Cell → List E) (e : E) {c₁ c₂ : Cell} (h : p c₁ = p c₂) : c₁ ∈ exponentCells p e ↔ c₂ ∈ exponentCells p e

Wholly syncretic cells agree on every shared exponent.