Paradigm complexity: implicative structure and entropy over cells

This file defines the two faces of the paradigm cell filling problem over a ParadigmSystem. The qualitative face is categorical: a set of cells predicts another when the forms filling it determine the form filling the target across the inflection classes, a principal-part set predicts every cell, and a system is vocabularly clear when every single cell does. The quantitative face measures the same relations by entropy: the entropy of the class assignment, of the form distribution at a cell, and the conditional entropy of one cell given another — the integrand of average conditional entropy. The two faces meet at zero: a cell predicted by another has zero conditional entropy given it, so a vocabularly clear system is transparent. Enumerative complexity is counted by the realizations of each cell, whose product bounds the number of classes.

Main definitions

• ParadigmSystem.Predicts, ParadigmSystem.IsPrincipalPartSet, ParadigmSystem.IsVocabularClear: the implicative relations.
• ParadigmSystem.realizations, ParadigmSystem.maxRealizations, ParadigmSystem.ParadigmEconomy: enumerative counts and the paradigm economy principle.
• ParadigmSystem.declensionEntropy, ParadigmSystem.cellEntropy, ParadigmSystem.conditionalCellEntropy, ParadigmSystem.mutualCellInfo: entropies and mutual information in nats, from the class weights.
• ParadigmSystem.IsImplicative, ParadigmSystem.IsTransparent: zero conditional entropy.

Main statements

• ParadigmSystem.conditionalCellEntropy_eq_zero_of_predicts, ParadigmSystem.isTransparent_of_isVocabularClear: prediction is zero conditional entropy.
• ParadigmSystem.isVocabularClear_of_isAnalogical: classes related by proportional analogy (Morphology.IsAnalogical) are vocabularly clear.
• ParadigmSystem.cellEntropy_eq_zero_of_card_le_one: a cell with one realization has zero entropy.
• ParadigmSystem.card_paradigms_le_prod_card_realizations: classes are bounded by the product of realizations.

References

• [ackerman-malouf-2013]
• [bonami-beniamine-2016]
• [carstairs-mccarthy-2010]

Implicative structure

def Morphology.ParadigmSystem.Predicts {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) (S : Finset (Fin n)) (j : Fin n) : Prop

A set of cells S predicts cell j when any two classes agreeing on every cell of S agree at j.

Equations

• ps.Predicts S j = ∀ p ∈ ps.entries, ∀ q ∈ ps.entries, (∀ c ∈ S, p.1 c = q.1 c) → p.1 j = q.1 j

def Morphology.ParadigmSystem.IsPrincipalPartSet {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) (S : Finset (Fin n)) : Prop

A principal-part set predicts every cell.

Equations

• ps.IsPrincipalPartSet S = ∀ (j : Fin n), ps.Predicts S j

def Morphology.ParadigmSystem.IsVocabularClear {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) : Prop

Vocabular clarity: every cell on its own predicts every cell — each realization identifies the class.

Equations

• ps.IsVocabularClear = ∀ (c : Fin n), ps.IsPrincipalPartSet {c}

theorem Morphology.ParadigmSystem.Predicts.mono {n : ℕ} {Form : Type u_1} {ps : ParadigmSystem n Form} {S T : Finset (Fin n)} {j : Fin n} (hST : S ⊆ T) (h : ps.Predicts S j) : ps.Predicts T j

theorem Morphology.ParadigmSystem.predicts_of_mem {n : ℕ} {Form : Type u_1} {ps : ParadigmSystem n Form} {S : Finset (Fin n)} {j : Fin n} (hj : j ∈ S) : ps.Predicts S j

@[instance_reducible]

instance Morphology.ParadigmSystem.instDecidablePredicts {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) [DecidableEq Form] {S : Finset (Fin n)} {j : Fin n} : Decidable (ps.Predicts S j)

Equations

• ps.instDecidablePredicts = Morphology.ParadigmSystem.instDecidablePredicts._aux_1 ps

@[instance_reducible]

instance Morphology.ParadigmSystem.instDecidableIsPrincipalPartSet {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) [DecidableEq Form] {S : Finset (Fin n)} : Decidable (ps.IsPrincipalPartSet S)

Equations

• ps.instDecidableIsPrincipalPartSet = Morphology.ParadigmSystem.instDecidableIsPrincipalPartSet._aux_1 ps

@[instance_reducible]

instance Morphology.ParadigmSystem.instDecidableIsVocabularClear {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) [DecidableEq Form] : Decidable ps.IsVocabularClear

Equations

• ps.instDecidableIsVocabularClear = Morphology.ParadigmSystem.instDecidableIsVocabularClear._aux_1 ps

Enumerative counts

def Morphology.ParadigmSystem.realizations {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) [DecidableEq Form] (c : Fin n) : Finset Form

The forms realizing cell c.

Equations

• ps.realizations c = (List.map (fun (e : Morphology.Paradigm n Form × ℚ) => e.1 c) ps.entries).toFinset

theorem Morphology.ParadigmSystem.mem_realizations {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) [DecidableEq Form] {c : Fin n} {r : Form} : r ∈ ps.realizations c ↔ ∃ e ∈ ps.entries, e.1 c = r

def Morphology.ParadigmSystem.maxRealizations {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) [DecidableEq Form] : ℕ

The largest number of rival realizations of a single cell.

Equations

• ps.maxRealizations = Finset.univ.sup fun (c : Fin n) => (ps.realizations c).card

def Morphology.ParadigmSystem.ParadigmEconomy {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) [DecidableEq Form] : Prop

Paradigm economy: no more classes than rival realizations of the most varied cell.

Equations

• ps.ParadigmEconomy = (ps.eComplexity ≤ ps.maxRealizations)

@[instance_reducible]

instance Morphology.ParadigmSystem.instDecidableParadigmEconomy {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) [DecidableEq Form] : Decidable ps.ParadigmEconomy

Equations

• ps.instDecidableParadigmEconomy = Morphology.ParadigmSystem.instDecidableParadigmEconomy._aux_1 ps

theorem Morphology.ParadigmSystem.card_paradigms_le_prod_card_realizations {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) [DecidableEq Form] : (List.map Prod.fst ps.entries).toFinset.card ≤ ∏ c : Fin n, (ps.realizations c).card

The distinct paradigms of the system are bounded by the product of the realizations of the cells.

Entropy

def Morphology.ParadigmSystem.total {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) : ℚ

The total weight of the classes.

Equations

• ps.total = (List.map Prod.snd ps.entries).sum

def Morphology.ParadigmSystem.cellWeight {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) [DecidableEq Form] (c : Fin n) (r : Form) : ℚ

The weight of the classes realizing r at c.

Equations

• ps.cellWeight c r = (List.map Prod.snd (List.filter (fun (e : Morphology.Paradigm n Form × ℚ) => decide (e.1 c = r)) ps.entries)).sum

def Morphology.ParadigmSystem.jointWeight {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) [DecidableEq Form] (ci cj : Fin n) (ri rj : Form) : ℚ

The weight of the classes realizing ri at ci and rj at cj.

Equations

• ps.jointWeight ci cj ri rj = (List.map Prod.snd (List.filter (fun (e : Morphology.Paradigm n Form × ℚ) => decide (e.1 ci = ri ∧ e.1 cj = rj)) ps.entries)).sum

def Morphology.ParadigmSystem.jointRealizations {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) [DecidableEq Form] (ci cj : Fin n) : Finset (Form × Form)

The pairs of forms realized at a pair of cells.

Equations

• ps.jointRealizations ci cj = (List.map (fun (e : Morphology.Paradigm n Form × ℚ) => (e.1 ci, e.1 cj)) ps.entries).toFinset

theorem Morphology.ParadigmSystem.mem_jointRealizations {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) [DecidableEq Form] {ci cj : Fin n} {p : Form × Form} : p ∈ ps.jointRealizations ci cj ↔ ∃ e ∈ ps.entries, (e.1 ci, e.1 cj) = p

noncomputable def Morphology.ParadigmSystem.declensionEntropy {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) : ℝ

The entropy (in nats) of the class assignment.

Equations

• ps.declensionEntropy = (List.map (fun (e : Morphology.Paradigm n Form × ℚ) => (↑(e.2 / ps.total)).negMulLog) ps.entries).sum

noncomputable def Morphology.ParadigmSystem.cellEntropy {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) [DecidableEq Form] (c : Fin n) : ℝ

The entropy (in nats) of the form distribution at cell c.

Equations

• ps.cellEntropy c = ∑ r ∈ ps.realizations c, (↑(ps.cellWeight c r / ps.total)).negMulLog

noncomputable def Morphology.ParadigmSystem.jointCellEntropy {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) [DecidableEq Form] (ci cj : Fin n) : ℝ

The joint entropy (in nats) of two cells.

Equations

• ps.jointCellEntropy ci cj = ∑ p ∈ ps.jointRealizations ci cj, (↑(ps.jointWeight ci cj p.1 p.2 / ps.total)).negMulLog

noncomputable def Morphology.ParadigmSystem.conditionalCellEntropy {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) [DecidableEq Form] (ci cj : Fin n) : ℝ

The conditional entropy H(cᵢ | cⱼ) = H(cᵢ, cⱼ) − H(cⱼ) of cell ci given cell cj.

Equations

• ps.conditionalCellEntropy ci cj = ps.jointCellEntropy ci cj - ps.cellEntropy cj

noncomputable def Morphology.ParadigmSystem.mutualCellInfo {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) [DecidableEq Form] (ci cj : Fin n) : ℝ

The mutual information I(cᵢ : cⱼ) = H(cᵢ) − H(cᵢ | cⱼ) of cell ci and cell cj.

Equations

• ps.mutualCellInfo ci cj = ps.cellEntropy ci - ps.conditionalCellEntropy ci cj

def Morphology.ParadigmSystem.IsImplicative {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) [DecidableEq Form] (ci cj : Fin n) : Prop

Knowing cell cj leaves no uncertainty about cell ci.

Equations

• ps.IsImplicative ci cj = (ps.conditionalCellEntropy ci cj = 0)

def Morphology.ParadigmSystem.IsTransparent {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) [DecidableEq Form] : Prop

Every cell predicts every other cell.

Equations

• ps.IsTransparent = ∀ (ci cj : Fin n), ci ≠ cj → ps.IsImplicative ci cj

theorem Morphology.ParadigmSystem.cellEntropy_eq_zero_of_card_le_one {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) [DecidableEq Form] {c : Fin n} (h : (ps.realizations c).card ≤ 1) : ps.cellEntropy c = 0

A cell with at most one realization has zero entropy.

theorem Morphology.ParadigmSystem.conditionalCellEntropy_eq_zero_of_predicts {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) [DecidableEq Form] {ci cj : Fin n} (h : ps.Predicts {cj} ci) : ps.conditionalCellEntropy ci cj = 0

A cell predicted by another has zero conditional entropy given it.

theorem Morphology.ParadigmSystem.isTransparent_of_isVocabularClear {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) [DecidableEq Form] (h : ps.IsVocabularClear) : ps.IsTransparent

A vocabularly clear system is transparent.

theorem Morphology.ParadigmSystem.isVocabularClear_of_isAnalogical {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) {L : Type u_2} {ops : Set (Form → Form)} {p : L → Fin n → Form} (h : IsAnalogical ops p) (hps : ∀ e ∈ ps.entries, ∃ (l : L), e.1 = p l) : ps.IsVocabularClear

A system whose classes are the paradigms of a family related by proportional analogy under any operations is vocabularly clear: a cell's form fixes the lexeme's whole paradigm ([blevins-2016]'s analogy as implicative structure).