Documentation

Studies.AckermanMalouf2013

Ackerman and Malouf (2013): Morphological Organization: The Low Conditional Entropy Conjecture #

Ackerman and Malouf separate the enumerative complexity of an inflectional system — how many cells, realizations, and inflection classes it has — from its integrative complexity, the average conditional entropy of one paradigm cell given another (Morphology.ParadigmSystem.avgCondEntropy), and conjecture that the latter stays low however large the former grows. Their Modern Greek nominal fragment carries the argument: its eight declensions violate paradigm economy and fill a tiny corner of the space its per-cell realizations allow, while implicative structure keeps the speaker's task small, and the paper's two worked conditional entropies come out as exact closed forms. Burmeso's vocabularly clear object agreement sits at the zero of the measure, and Chiquihuitlán Mazatec's final-vowel and tone classes sit far from it, the prose claim that only third-person vowels are diagnostic sharpened to what its Table 6 supports.

Main statements #

greek_not_paradigmEconomy, greek_principalParts: Greek violates the enumerative principles while keeping a small principal-part set.
greek_genSg_given_accPl_a, greek_genSg_given_accPl: the paper's worked conditional entropies (13) and (14) as exact closed forms, log 3 − (2/3) log 2 and (3/8) log 3 nats.
burmeso_avgCondEntropy: vocabular clarity makes Burmeso's average conditional entropy zero.
mazatec_vowels_diagnosticity, mazatec_tones_no_diagnostic_cell: how far the Mazatec final vowels and tones are from clarity.

Implementation notes #

Class probabilities are uniformOn Set.univ, the paper's (5), under which every printed number is computed; entropies are in nats, the paper's bits are these divided by log 2.
avgCondEntropy averages over ordered pairs of distinct cells, which reproduces Table 2's expected values and its grand average; the running text prints a different rounding of the latter.
Table 1 yields five rival genitive singulars and a realization-space of 25600 class candidates where pp. 445–446 count six and 46,080 on richer data than Table 1.

TODO #

greek_avgCondEntropy: the closed form of Table 2's grand average, provable from condEntropy_uniformOn_univ with a per-pair count table.
Table 5's average entropies and the tone system's realization count are computed on the appendix's full Table A6 data and do not follow from Tables 6–7, so they are not stated.

References #

Instances for the fragments' form types #

@[instance_reducible]

instance AckermanMalouf2013.instFintypeEnding_studies :

Fintype Greek.StandardModern.Declension.Ending

Equations

One or more equations did not get rendered due to their size.

instance AckermanMalouf2013.instNonemptyEnding_studies :

Nonempty Greek.StandardModern.Declension.Ending

@[instance_reducible]

instance AckermanMalouf2013.instMeasurableSpaceEnding_studies :

MeasurableSpace Greek.StandardModern.Declension.Ending

Equations

AckermanMalouf2013.instMeasurableSpaceEnding_studies = ⊤

instance AckermanMalouf2013.instMeasurableSingletonClassEnding_studies :

MeasurableSingletonClass Greek.StandardModern.Declension.Ending

@[instance_reducible]

instance AckermanMalouf2013.instFintypeAgreementPrefix_studies :

Fintype Burmeso.ObjectAgreement.AgreementPrefix

Equations

One or more equations did not get rendered due to their size.

instance AckermanMalouf2013.instNonemptyAgreementPrefix_studies :

Nonempty Burmeso.ObjectAgreement.AgreementPrefix

@[instance_reducible]

instance AckermanMalouf2013.instMeasurableSpaceAgreementPrefix_studies :

MeasurableSpace Burmeso.ObjectAgreement.AgreementPrefix

Equations

AckermanMalouf2013.instMeasurableSpaceAgreementPrefix_studies = ⊤

instance AckermanMalouf2013.instMeasurableSingletonClassAgreementPrefix_studies :

MeasurableSingletonClass Burmeso.ObjectAgreement.AgreementPrefix

@[instance_reducible]

instance AckermanMalouf2013.instMeasurableSpaceVowel_studies :

MeasurableSpace Mazatec.Verbs.Vowel

Equations

AckermanMalouf2013.instMeasurableSpaceVowel_studies = ⊤

instance AckermanMalouf2013.instMeasurableSingletonClassVowel_studies :

MeasurableSingletonClass Mazatec.Verbs.Vowel

Modern Greek: enumerative complexity #

theorem AckermanMalouf2013.greek_maxRealizations :

Greek.StandardModern.Declension.nominal.maxRealizations = 5

theorem AckermanMalouf2013.greek_not_paradigmEconomy :

¬Greek.StandardModern.Declension.nominal.ParadigmEconomy

Eight declensions exceed the five rival realizations of the most varied cell.

theorem AckermanMalouf2013.greek_realization_count :

(Finset.univ.biUnion Greek.StandardModern.Declension.nominal.realizations).card = 12

Table 3's Greek row counts twelve realizations over the eight cells.

theorem AckermanMalouf2013.greek_classes_vs_product :

(Finset.image Greek.StandardModern.Declension.nominal Finset.univ).card = 8 ∧ ∏ c : Fin 8, (Greek.StandardModern.Declension.nominal.realizations c).card = 25600

Eight classes against the 25600 the per-cell realizations of Table 1 would allow ("it has fewer inflection classes than it could").

Modern Greek: implicative structure #

theorem AckermanMalouf2013.greek_predicts :

Greek.StandardModern.Declension.nominal.Predicts {Greek.StandardModern.Declension.vocSg} Greek.StandardModern.Declension.accSg ∧ Greek.StandardModern.Declension.nominal.Predicts {Greek.StandardModern.Declension.accSg} Greek.StandardModern.Declension.vocSg ∧ Greek.StandardModern.Declension.nominal.Predicts {Greek.StandardModern.Declension.accPl} Greek.StandardModern.Declension.nomPl

theorem AckermanMalouf2013.greek_not_predicts :

¬Greek.StandardModern.Declension.nominal.Predicts {Greek.StandardModern.Declension.accPl} Greek.StandardModern.Declension.genSg

The accusative plural does not predict the genitive singular; after -a two genitives remain.

theorem AckermanMalouf2013.greek_accPl_i_genSg (d : Fin 8) :

Greek.StandardModern.Declension.nominal d Greek.StandardModern.Declension.accPl = Greek.StandardModern.Declension.Ending.i → Greek.StandardModern.Declension.nominal d Greek.StandardModern.Declension.genSg = Greek.StandardModern.Declension.Ending.us

An accusative plural in -i fixes the genitive singular in -us.

theorem AckermanMalouf2013.greek_principalParts :

Greek.StandardModern.Declension.nominal.IsPrincipalPartSet {Greek.StandardModern.Declension.nomSg, Greek.StandardModern.Declension.genSg, Greek.StandardModern.Declension.accPl} ∧ ¬Greek.StandardModern.Declension.nominal.IsPrincipalPartSet {Greek.StandardModern.Declension.genSg, Greek.StandardModern.Declension.accPl}

Nominative singular, genitive singular, and accusative plural are principal parts; the last two alone are not.

theorem AckermanMalouf2013.greek_not_clear :

¬Greek.StandardModern.Declension.nominal.IsVocabularClear

Modern Greek: entropy #

theorem AckermanMalouf2013.greek_declensionEntropy :

InformationTheory.measureEntropy (ProbabilityTheory.uniformOn Set.univ) = Real.log 8

The declension entropy of the eight classes is log 8 nats, the paper's 3 bits.

theorem AckermanMalouf2013.greek_cellEntropy_genPl :

InformationTheory.entropy (fun (x : Fin 8) => Greek.StandardModern.Declension.nominal x Greek.StandardModern.Declension.genPl) (ProbabilityTheory.uniformOn Set.univ) = 0

The genitive plural has a single realization and no entropy.

theorem AckermanMalouf2013.greek_condEntropy_nomPl_accPl :

InformationTheory.condEntropy (fun (x : Fin 8) => Greek.StandardModern.Declension.nominal x Greek.StandardModern.Declension.nomPl) (fun (x : Fin 8) => Greek.StandardModern.Declension.nominal x Greek.StandardModern.Declension.accPl) (ProbabilityTheory.uniformOn Set.univ) = 0

Because the accusative plural predicts the nominative plural, the latter's conditional entropy given it vanishes.

theorem AckermanMalouf2013.greek_genSg_given_accPl_a :

InformationTheory.entropy (fun (x : Fin 8) => Greek.StandardModern.Declension.nominal x Greek.StandardModern.Declension.genSg) (ProbabilityTheory.uniformOn ((fun (x : Fin 8) => Greek.StandardModern.Declension.nominal x Greek.StandardModern.Declension.accPl) ⁻¹' {Greek.StandardModern.Declension.Ending.a})) = Real.log 3 - 2 / 3 * Real.log 2

In the paper's (13), an accusative plural in -a leaves the genitive singular split two to one, carrying log 3 − (2/3) log 2 nats = 0.918 bits.

theorem AckermanMalouf2013.greek_genSg_given_accPl :

InformationTheory.condEntropy (fun (x : Fin 8) => Greek.StandardModern.Declension.nominal x Greek.StandardModern.Declension.genSg) (fun (x : Fin 8) => Greek.StandardModern.Declension.nominal x Greek.StandardModern.Declension.accPl) (ProbabilityTheory.uniformOn Set.univ) = 3 / 8 * Real.log 3

In the paper's (14), the genitive singular given the accusative plural carries (3/8) log 3 nats = 0.594 bits.

theorem AckermanMalouf2013.greek_avgCondEntropy :

Greek.StandardModern.Declension.nominal.avgCondEntropy (ProbabilityTheory.uniformOn Set.univ) = 69 / 224 * Real.log 2 + 3 / 32 * Real.log 3 + 5 / 56 * Real.log 5

Table 2's grand average, the average conditional entropy of the Greek paradigms, equals this closed form, 0.664 bits.

Burmeso #

theorem AckermanMalouf2013.burmeso_clear :

Burmeso.ObjectAgreement.objectAgreement.IsVocabularClear

Every cell identifies the class.

theorem AckermanMalouf2013.burmeso_realizations :

(Finset.univ.biUnion Burmeso.ObjectAgreement.objectAgreement.realizations).card = 6 ∧ Burmeso.ObjectAgreement.objectAgreement.maxRealizations = 2

Table 3's Burmeso row counts six realizations, at most two per cell.

theorem AckermanMalouf2013.burmeso_avgCondEntropy :

Burmeso.ObjectAgreement.objectAgreement.avgCondEntropy (ProbabilityTheory.uniformOn Set.univ) = 0

Being vocabularly clear, Burmeso has average conditional entropy zero.

Chiquihuitlán Mazatec #

theorem AckermanMalouf2013.mazatec_vowels_not_clear :

¬Mazatec.Verbs.finalVowels.IsVocabularClear

theorem AckermanMalouf2013.mazatec_vowels_constant :

InformationTheory.entropy (fun (x : Fin 10) => Mazatec.Verbs.finalVowels x Mazatec.Verbs.firstPl) (ProbabilityTheory.uniformOn Set.univ) = 0 ∧ InformationTheory.entropy (fun (x : Fin 10) => Mazatec.Verbs.finalVowels x Mazatec.Verbs.secondPl) (ProbabilityTheory.uniformOn Set.univ) = 0

The first and second person plural vowels are constant across classes.

theorem AckermanMalouf2013.mazatec_vowels_diagnosticity :

Mazatec.Verbs.finalVowels.Predicts {Mazatec.Verbs.third} Mazatec.Verbs.secondSg ∧ ¬Mazatec.Verbs.finalVowels.IsPrincipalPartSet {Mazatec.Verbs.third} ∧ Mazatec.Verbs.finalVowels.Predicts {Mazatec.Verbs.firstSg} Mazatec.Verbs.firstIncl

Over Table 6, "only the third-person forms are in any way diagnostic" comes to this much. The third person predicts the second singular yet is no principal part, while the first singular predicts the first inclusive.

theorem AckermanMalouf2013.mazatec_tones_no_diagnostic_cell (c : Fin 6) :

¬Mazatec.Verbs.tones.IsPrincipalPartSet {c}

No cell of the tone patterns is diagnostic of class membership.