Proportional analogy

Word-and-paradigm morphology relates the forms of one lexeme to those of another by proportional analogy, cat : cats :: dog : dogs ([blevins-2016]): the operation taking the form at one cell to the form at another is the same for every lexeme. Which operations count is a parameter, affixation on strings or translation on vectors, so a lexeme-indexed family of paradigms p : L → Cell → F is analogical under a class of operations when every pair of cells is related by one operation of the class shared across lexemes (IsAnalogical). Analogy under any class makes each cell's form identify the lexeme's whole paradigm, Ackerman and Malouf's vocabular clarity (ParadigmSystem.isVocabularClear_of_isAnalogical in Complexity.lean). For forms in an additive group and translations as the operations, the cell contrast is a difference and the family is analogically regular (IsAnalogicallyRegular): every contrast is lexeme-independent, equivalently the family is a lexeme part plus a cell part (isAnalogicallyRegular_iff_exists_add), and the property is preserved by additive maps of the form space (IsAnalogicallyRegular.map). This is the case a discriminative lexicon realises exactly (Studies/HeitmeierChuangBaayen2026).

Main declarations

• Morphology.IsAnalogical ops p — every pair of cells is related by one operation of ops, the same for every lexeme.
• Morphology.IsAnalogicallyRegular p — analogy under the translations of an additive group; isAnalogicallyRegular_iff is its difference form.
• Morphology.isAnalogicallyRegular_iff_exists_add — regular iff a lexeme part plus a cell part.

References

• [J. P. Blevins, Word and Paradigm Morphology (2016)][blevins-2016]

def Morphology.IsAnalogical {L : Type u_1} {Cell : Type u_2} {F : Type u_3} (ops : Set (F → F)) (p : L → Cell → F) : Prop

A lexeme-indexed family of paradigms is analogical under a class of operations on forms when every pair of cells is related by one operation of the class, the same for every lexeme.

Equations

• Morphology.IsAnalogical ops p = ∀ (c c' : Cell), ∃ (g : F → F), g ∈ ops ∧ ∀ (l : L), p l c' = g (p l c)

def Morphology.IsAnalogicallyRegular {L : Type u_1} {Cell : Type u_2} {F : Type u_3} [AddCommGroup F] (p : L → Cell → F) : Prop

Analogy under translations: the form contrast between any two cells is the same for every lexeme.

Equations

• Morphology.IsAnalogicallyRegular p = Morphology.IsAnalogical (Set.range fun (v x : F) => x + v) p

theorem Morphology.isAnalogicallyRegular_iff {L : Type u_1} {Cell : Type u_2} {F : Type u_3} [AddCommGroup F] {p : L → Cell → F} : IsAnalogicallyRegular p ↔ ∀ (l l' : L) (c c' : Cell), p l c - p l c' = p l' c - p l' c'

The difference form of analogical regularity.

theorem Morphology.isAnalogicallyRegular_add {L : Type u_1} {Cell : Type u_2} {F : Type u_3} [AddCommGroup F] (a : L → F) (b : Cell → F) : IsAnalogicallyRegular fun (l : L) (c : Cell) => a l + b c

A lexeme part plus a cell part is analogically regular.

theorem Morphology.IsAnalogicallyRegular.map {L : Type u_1} {Cell : Type u_2} {F : Type u_3} {G : Type u_4} [AddCommGroup F] [AddCommGroup G] {p : L → Cell → F} (h : IsAnalogicallyRegular p) (f : F →+ G) : IsAnalogicallyRegular fun (l : L) (c : Cell) => f (p l c)

Analogical regularity is preserved by additive maps of the form space.

theorem Morphology.isAnalogicallyRegular_iff_exists_add {L : Type u_1} {Cell : Type u_2} {F : Type u_3} [AddCommGroup F] [Nonempty L] [Nonempty Cell] {p : L → Cell → F} : IsAnalogicallyRegular p ↔ ∃ (a : L → F), ∃ (b : Cell → F), ∀ (l : L) (c : Cell), p l c = a l + b c

Analogical regularity is additivity: a regular family is a lexeme part plus a cell part.