Docs / Morphology / Paradigm / Complexity

Paradigm complexity: implicative structure and entropy over cells

import Linglib.Morphology.Paradigm.Complexity · namespace Morphology.ParadigmSystem

Source

This file gives 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 (Function.FactorsThrough), a principal-part set predicts every cell, and a system is vocabularly clear (Carstairs-McCarthy 2010) when every single cell is. Enumerative complexity is counted by the realizations of each cell: their product bounds the number of distinct paradigms, and paradigm economy bounds the classes by the most varied cell.

The quantitative face is Core/InformationTheory/Entropy/Basic.lean applied to the data: under a probability measure μ on the classes — uniform in every computation of Ackerman & Malouf 2013, type frequencies in its general definitions — the cell c is the random variable (M · c), so declension entropy is Hm[μ], cell entropy is H[(M · c) ; μ], and the conditional entropy of one cell given another is H[(M · c₁) | (M · c₂) ; μ]. Only the average over ordered pairs of distinct cells, Ackerman & Malouf 2013's I-complexity, needs a definition. The two faces meet at zero: under the uniform measure, one cell predicts another iff the conditional entropy vanishes, and a system is vocabularly clear iff its average conditional entropy is zero.

Main declarations

Main statements

References

Implicative structure

A set of cells S predicts cell j when the form at j factors through the forms at S, so that any two classes agreeing on every cell of S agree at j.

def PredictsL69–72
{D : Type u_1} {Cell : Type u_2} {Form : Type u_3} (M : ParadigmSystem D Cell Form) (S : Finset Cell) (j : Cell) :
Prop
  • M.Predicts S j = Function.FactorsThrough (fun (x : D) => M x j) fun (d : D) => S.restrict (M d)

Used by IsPrincipalPartSet, predicts_iff, predicts_singleton_iff, Predicts.mono, predicts_of_mem, instDecidablePredicts, instDecidableIsPrincipalPartSetOfFintype, condEntropy_eq_zero_of_predicts, predicts_iff_condEntropy_eq_zero

Used in AckermanMalouf2013

A system is vocabularly clear when every cell on its own predicts every cell, so that each realization identifies the class (Carstairs-McCarthy 2010 via Ackerman & Malouf 2013).

def IsVocabularClearL78–80
{D : Type u_1} {Cell : Type u_2} {Form : Type u_3} (M : ParadigmSystem D Cell Form) :
Prop

Built from

Used by instDecidableIsVocabularClearOfFintype, avgCondEntropy_eq_zero_of_isVocabularClear, isVocabularClear_iff_avgCondEntropy_eq_zero, isVocabularClear_iff_isAnalogical

Used in AckermanMalouf2013

L84–86
L88–91
L103

Enumerative counts

L120–121
L123–125
L138–145

Entropy

The entropy face is Core notation applied to the data: Hm[μ] is the declension entropy, H[(M · c) ; μ] the cell entropy, H[(M · c₁) | (M · c₂) ; μ] the conditional entropy of one cell given another. Only the average needs a definition.

The average conditional entropy of one cell given another, over ordered pairs of distinct cells, is Ackerman & Malouf 2013's I-complexity.

avgCondEntropyL164–168
noncomputable def Morphology.ParadigmSystem.avgCondEntropy {D : Type u_1} {Cell : Type u_2} {Form : Type u_3} (M : ParadigmSystem D Cell Form) [MeasurableSpace D] [MeasurableSpace Form] [Fintype Cell] [DecidableEq Cell] (μ : MeasureTheory.Measure D) :
ℝ

The definition is too large to print here; read it in the source.

Used by avgCondEntropy_nonneg, avgCondEntropy_le_measureEntropy, avgCondEntropy_eq_zero_of_isVocabularClear, isVocabularClear_iff_avgCondEntropy_eq_zero

Used in AckermanMalouf2013

L170–172
L178–186
L190–199
L201–209

Under the uniform measure on the classes, one cell predicts another exactly when the conditional entropy of the second given the first vanishes.

theorem predicts_iff_condEntropy_eq_zeroL211–219
{D : Type u_1} {Cell : Type u_2} {Form : Type u_3} {M : ParadigmSystem D Cell Form} [MeasurableSpace D] [MeasurableSpace Form] {c₁ c₂ : Cell} [Fintype D] [MeasurableSingletonClass Form] [DecidableEq Form] [MeasurableSingletonClass D] [Nonempty D] :
M.Predicts {c₂} c₁ ↔ InformationTheory.condEntropy (fun (x : D) => M x c₁) (fun (x : D) => M x c₂) (ProbabilityTheory.uniformOn Set.univ) = 0

Built from

The average conditional entropy is at most the declension entropy ("guessing a lexeme's declension on the basis of a single word form can never be harder than guessing the declension with no information at all", Ackerman & Malouf 2013).

theorem avgCondEntropy_le_measureEntropyL223–242
{D : Type u_1} {Cell : Type u_2} {Form : Type u_3} {M : ParadigmSystem D Cell Form} [MeasurableSpace D] [MeasurableSpace Form] [Fintype D] [MeasurableSingletonClass Form] [DecidableEq Form] [MeasurableSingletonClass D] [Fintype Cell] [DecidableEq Cell] (μ : MeasureTheory.Measure D) [MeasureTheory.IsProbabilityMeasure μ] :
M.avgCondEntropy μ ≤ InformationTheory.measureEntropy μ

Built from

L244–248

Vocabular clarity is zero average conditional entropy under the uniform measure (Ackerman & Malouf 2013: "average conditional entropy, as a consequence, should be zero").

theorem isVocabularClear_iff_avgCondEntropy_eq_zeroL250–267
{D : Type u_1} {Cell : Type u_2} {Form : Type u_3} {M : ParadigmSystem D Cell Form} [MeasurableSpace D] [MeasurableSpace Form] [Fintype D] [MeasurableSingletonClass Form] [DecidableEq Form] [MeasurableSingletonClass D] [Fintype Cell] [DecidableEq Cell] [Nonempty D] :
M.IsVocabularClear ↔ M.avgCondEntropy (ProbabilityTheory.uniformOn Set.univ) = 0

Built from ,