Paradigms: forms over cells

import Linglib.Morphology.Paradigm.Basic · namespace Morphology

A paradigm assigns a surface form to each of n linearly ordered cells, and its syncretism is the kernel setoid Setoid.ker p of that assignment, decidable over finitely many cells. The ordered carrier serves realization-pattern typology (*ABA and contiguity). A paradigm system assigns a form to each row and cell of a table whose rows are lexemes or inflection classes and whose cells form any type; it carries implicative structure and entropy over the cells (Complexity.lean) and proportional analogy (Analogy.lean).

Main declarations

Morphology.Paradigm n F: a form for each of n ordered cells.
Morphology.formsAt: the forms an inventory offers for each cell.
Morphology.ParadigmSystem D Cell Form: a form for each row of D at each cell of Cell.
Morphology.ParadigmSystem.toRealization: a paradigm system as a total, univalent Realization.

References

Ackerman & Malouf 2013, Morphological Organization: The Low Conditional Entropy Conjecture formalized
Bobaljik 2012, Universals in comparative morphology: Suppletion, superlatives, and the structure of words formalized

Declarations

A paradigm over n linearly ordered cells assigns the form occupying each cell, the carrier of Bobaljik 2012's realization patterns such as AAA, ABB and ABC.

@[reducible, inline] abbrev Paradigm L35–37

(n : ℕ) (F : Type u_1) :

Type u_1

Paradigm n F = (Fin n → F)

Used in Suppletion/Bobaljik2012, Suppletion/SmithMoskalEtAl2019, Suppletion/Theory, Morphology/Exponence/Containment/Contiguity, Morphology/Exponence/Containment/Selection and 7 more

The paradigm of an inventory

The forms an inventory I offers for the cell c, where the item i has the form form i and realizes the cells cells i. A cell no item realizes gets ∅ and an overabundant cell several forms, and Setoid.ker (formsAt cells form I) relates the cells the inventory does not distinguish.

def formsAt L46–51

{ι : Type u_1} {Cell : Type u_2} {F : Type u_3} [DecidableEq Cell] [DecidableEq F] (cells : ι → Finset Cell) (form : ι → F) (I : Finset ι) (c : Cell) :

Finset F

formsAt cells form I c = Finset.image form ({x ∈ I | c ∈ cells x})

Used by mem_formsAt, formsAt_mono, formsAt_union

Used in Syntax/Category/Pronoun/Indefinite, Syntax/Category/Pronoun/Personal, Syntax/Category/Pronoun/Reflexive

L53–54

L56–59

L61–63

A paradigm system assigns a form to each row of a table, a lexeme or an inflection class, at each cell, such as the inflection-class table of Ackerman & Malouf 2013's Table 1, whose class count (the enumerative complexity of that paper's Table 3) is Fintype.card D.

@[reducible, inline] abbrev ParadigmSystem L67–70

(D : Type u_1) (Cell : Type u_2) (Form : Type u_3) :

Type (max (max u_1 u_2) u_3)

ParadigmSystem D Cell Form = (D → Cell → Form)

Used by ParadigmSystem.toRealization, ParadigmSystem.toRealization_realize, ParadigmSystem.isTotal_toRealization, ParadigmSystem.isUnivalent_toRealization

Used in Fragments/Burmeso/ObjectAgreement, Fragments/Greek/StandardModern/Declension, Fragments/Mazatec/Verbs, Morphology/Paradigm/Analogy, Morphology/Paradigm/Complexity and 2 more

A paradigm system realizes each row at each cell by its one form.

def ParadigmSystem.toRealization L76–77

{D : Type u_1} {Cell : Type u_2} {Form : Type u_3} (M : ParadigmSystem D Cell Form) :

Realization D Cell Form

M.toRealization = { realize := fun (d : D) (c : Cell) => {M d c} }

Built from

Used by ParadigmSystem.toRealization_realize, ParadigmSystem.isTotal_toRealization, ParadigmSystem.isUnivalent_toRealization

L79–80

L82

L84–85