Prasertsom, Smith and Culbertson (2026): Domain-General Categorisation Explains Constrained Cross-Linguistic Variation in Noun Classification

This file formalizes the two formal claims of [PSC26]. The paper asks why animacy, but never colour, serves as a basis for noun classification although both are perceptually salient, and answers with a domain-general principle: a good category is one whose defining feature predicts the other features of its members, and animacy predicts more than colour. The typological premise is read off [Aik00]'s sample of noun categorization devices, where animacy is a basic semantic parameter and colour is none of any device's (animacy_not_colour). The predictive-power manipulation of Experiments 3a and 3b rests on two sixteen-stimulus sets, Tables 4 and 5 (predictiveAnimacy, predictiveColour), built so that the conditional entropy of horn type, body shape, and appendage shape is lower given the predictive dimension than given the other, and so that exchanging the animacy and colour columns of one set gives the other (mirror_images). The six entropy orderings of Table 6 that the design promises are proved from the tables under the uniform measure over the stimuli (predictiveAnimacy_horn, predictiveColour_horn, and their shape and appendage siblings).

Implementation notes

Each stimulus set has exactly one stimulus per animacy–colour pair, so a set is a function from the pair to the three remaining dimensions and its stimuli are the sixteen cells of the grid. Conditional entropy is the substrate's H[X | Y ; μ] under the uniform measure on the grid, reduced to counts by condEntropy_uniformOn_univ; each ordering then comes to a positive multiple of negMulLog (1/2), the entropy of the evenly split fibres that only the non-predictive dimension has. The learning and sorting results of Experiments 1a to 3b and the corpus measures of §4.1, which are means over participants and word embeddings, are not formalized.

TODO

The paper's reason for the mirror design, that animacy in one set has exactly the predictive power of colour in the other, is the invariance of conditional entropy under a relabelling of the population and of the conditioning variable; the substrate has no such lemma yet, so the predictive-colour orderings are computed directly rather than transferred from the predictive-animacy ones through mirror_images.

References

• [PSC26]
• [Aik00]

The typological premise (§1)

theorem PrasertsonSmithCulbertson2026.animacy_not_colour (l : Aikhenvald2000.Language) (hk : l.kind = some Classifier.Kind.nounClass ∨ l.kind = some Classifier.Kind.numeralClassifier) : (∃ p ∈ l.semantics, p = Classifier.Parameter.animacy ∨ p = Classifier.Parameter.humanness ∨ p = Classifier.Parameter.sex) ∧ Classifier.Parameter.colour ∉ l.semantics

Every noun class or numeral classifier device of the sample has animacy, humanness, or sex among its basic semantic parameters, and none has colour.

The stimulus dimensions (§4.2.2, Fig. 10)

inductive PrasertsonSmithCulbertson2026.Animacy : Type

The animacy dimension: two kinds of animate, with crescent or round eyes, and two of inanimate, dots forming a line or a triangle.

• crescentEyed : Animacy
• roundEyed : Animacy
• line : Animacy
• triangle : Animacy

@[instance_reducible]

instance PrasertsonSmithCulbertson2026.instDecidableEqAnimacy : DecidableEq Animacy

Equations

• PrasertsonSmithCulbertson2026.instDecidableEqAnimacy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def PrasertsonSmithCulbertson2026.instReprAnimacy.repr : Animacy → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance PrasertsonSmithCulbertson2026.instReprAnimacy : Repr Animacy

Equations

• PrasertsonSmithCulbertson2026.instReprAnimacy = { reprPrec := PrasertsonSmithCulbertson2026.instReprAnimacy.repr }

@[instance_reducible]

instance PrasertsonSmithCulbertson2026.instFintypeAnimacy : Fintype Animacy

Equations

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

inductive PrasertsonSmithCulbertson2026.Colour : Type

The colour dimension: two warm and two cool colours.

• red : Colour
• orange : Colour
• blue : Colour
• teal : Colour

@[instance_reducible]

instance PrasertsonSmithCulbertson2026.instDecidableEqColour : DecidableEq Colour

Equations

• PrasertsonSmithCulbertson2026.instDecidableEqColour x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance PrasertsonSmithCulbertson2026.instReprColour : Repr Colour

Equations

• PrasertsonSmithCulbertson2026.instReprColour = { reprPrec := PrasertsonSmithCulbertson2026.instReprColour.repr }

def PrasertsonSmithCulbertson2026.instReprColour.repr : Colour → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance PrasertsonSmithCulbertson2026.instFintypeColour : Fintype Colour

Equations

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

inductive PrasertsonSmithCulbertson2026.Horn : Type

Horn type.

• crescent : Horn
• jagged : Horn

@[instance_reducible]

instance PrasertsonSmithCulbertson2026.instDecidableEqHorn : DecidableEq Horn

Equations

• PrasertsonSmithCulbertson2026.instDecidableEqHorn x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def PrasertsonSmithCulbertson2026.instReprHorn.repr : Horn → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance PrasertsonSmithCulbertson2026.instReprHorn : Repr Horn

Equations

• PrasertsonSmithCulbertson2026.instReprHorn = { reprPrec := PrasertsonSmithCulbertson2026.instReprHorn.repr }

@[instance_reducible]

instance PrasertsonSmithCulbertson2026.instFintypeHorn : Fintype Horn

Equations

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

inductive PrasertsonSmithCulbertson2026.Shape : Type

Body shape.

• circle : Shape
• inkblot : Shape

@[instance_reducible]

instance PrasertsonSmithCulbertson2026.instDecidableEqShape : DecidableEq Shape

Equations

• PrasertsonSmithCulbertson2026.instDecidableEqShape x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance PrasertsonSmithCulbertson2026.instReprShape : Repr Shape

Equations

• PrasertsonSmithCulbertson2026.instReprShape = { reprPrec := PrasertsonSmithCulbertson2026.instReprShape.repr }

def PrasertsonSmithCulbertson2026.instReprShape.repr : Shape → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance PrasertsonSmithCulbertson2026.instFintypeShape : Fintype Shape

Equations

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

inductive PrasertsonSmithCulbertson2026.Appendages : Type

Appendage shape.

• wavy : Appendages
• round : Appendages

@[instance_reducible]

instance PrasertsonSmithCulbertson2026.instDecidableEqAppendages : DecidableEq Appendages

Equations

• PrasertsonSmithCulbertson2026.instDecidableEqAppendages x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def PrasertsonSmithCulbertson2026.instReprAppendages.repr : Appendages → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance PrasertsonSmithCulbertson2026.instReprAppendages : Repr Appendages

Equations

• PrasertsonSmithCulbertson2026.instReprAppendages = { reprPrec := PrasertsonSmithCulbertson2026.instReprAppendages.repr }

@[instance_reducible]

instance PrasertsonSmithCulbertson2026.instFintypeAppendages : Fintype Appendages

Equations

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

@[instance_reducible]

instance PrasertsonSmithCulbertson2026.instMeasurableSpaceAnimacy : MeasurableSpace Animacy

Equations

• PrasertsonSmithCulbertson2026.instMeasurableSpaceAnimacy = ⊤

@[instance_reducible]

instance PrasertsonSmithCulbertson2026.instMeasurableSpaceColour : MeasurableSpace Colour

Equations

• PrasertsonSmithCulbertson2026.instMeasurableSpaceColour = ⊤

@[instance_reducible]

instance PrasertsonSmithCulbertson2026.instMeasurableSpaceHorn : MeasurableSpace Horn

Equations

• PrasertsonSmithCulbertson2026.instMeasurableSpaceHorn = ⊤

@[instance_reducible]

instance PrasertsonSmithCulbertson2026.instMeasurableSpaceShape : MeasurableSpace Shape

Equations

• PrasertsonSmithCulbertson2026.instMeasurableSpaceShape = ⊤

@[instance_reducible]

instance PrasertsonSmithCulbertson2026.instMeasurableSpaceAppendages : MeasurableSpace Appendages

Equations

• PrasertsonSmithCulbertson2026.instMeasurableSpaceAppendages = ⊤

theorem PrasertsonSmithCulbertson2026.Animacy.sum_univ {M : Type u_1} [AddCommMonoid M] (f : Animacy → M) : ∑ v : Animacy, f v = f crescentEyed + f roundEyed + f line + f triangle

theorem PrasertsonSmithCulbertson2026.Colour.sum_univ {M : Type u_1} [AddCommMonoid M] (f : Colour → M) : ∑ v : Colour, f v = f red + f orange + f blue + f teal

theorem PrasertsonSmithCulbertson2026.Horn.sum_univ {M : Type u_1} [AddCommMonoid M] (f : Horn → M) : ∑ v : Horn, f v = f crescent + f jagged

theorem PrasertsonSmithCulbertson2026.Shape.sum_univ {M : Type u_1} [AddCommMonoid M] (f : Shape → M) : ∑ v : Shape, f v = f circle + f inkblot

theorem PrasertsonSmithCulbertson2026.Appendages.sum_univ {M : Type u_1} [AddCommMonoid M] (f : Appendages → M) : ∑ v : Appendages, f v = f wavy + f round

structure PrasertsonSmithCulbertson2026.Body : Type

The three dimensions of a stimulus that its animacy and colour may predict.

• horn : Horn
• shape : Shape
• appendages : Appendages

def PrasertsonSmithCulbertson2026.instDecidableEqBody.decEq (x✝ x✝¹ : Body) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance PrasertsonSmithCulbertson2026.instDecidableEqBody : DecidableEq Body

Equations

• PrasertsonSmithCulbertson2026.instDecidableEqBody = PrasertsonSmithCulbertson2026.instDecidableEqBody.decEq

def PrasertsonSmithCulbertson2026.instReprBody.repr : Body → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance PrasertsonSmithCulbertson2026.instReprBody : Repr Body

Equations

• PrasertsonSmithCulbertson2026.instReprBody = { reprPrec := PrasertsonSmithCulbertson2026.instReprBody.repr }

The stimulus sets (Tables 4 and 5)

def PrasertsonSmithCulbertson2026.predictiveAnimacy : Animacy × Colour → Body

The predictive-animacy set (Table 4): the body of the stimulus in each animacy–colour cell. The eight animates are alike; among the inanimates each body dimension departs once per kind of inanimate from its inanimate value.

Equations

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

def PrasertsonSmithCulbertson2026.predictiveColour : Animacy × Colour → Body

The predictive-colour set (Table 5).

Equations

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

def PrasertsonSmithCulbertson2026.Animacy.toColour : Animacy → Colour

The colour that stands in for a kind of animacy when the two columns are exchanged: the animates for the warm colours, the inanimates for the cool ones.

Equations

• PrasertsonSmithCulbertson2026.Animacy.crescentEyed.toColour = PrasertsonSmithCulbertson2026.Colour.red
• PrasertsonSmithCulbertson2026.Animacy.roundEyed.toColour = PrasertsonSmithCulbertson2026.Colour.orange
• PrasertsonSmithCulbertson2026.Animacy.line.toColour = PrasertsonSmithCulbertson2026.Colour.blue
• PrasertsonSmithCulbertson2026.Animacy.triangle.toColour = PrasertsonSmithCulbertson2026.Colour.teal

def PrasertsonSmithCulbertson2026.Colour.toAnimacy : Colour → Animacy

The kind of animacy that stands in for a colour.

Equations

• PrasertsonSmithCulbertson2026.Colour.red.toAnimacy = PrasertsonSmithCulbertson2026.Animacy.crescentEyed
• PrasertsonSmithCulbertson2026.Colour.orange.toAnimacy = PrasertsonSmithCulbertson2026.Animacy.roundEyed
• PrasertsonSmithCulbertson2026.Colour.blue.toAnimacy = PrasertsonSmithCulbertson2026.Animacy.line
• PrasertsonSmithCulbertson2026.Colour.teal.toAnimacy = PrasertsonSmithCulbertson2026.Animacy.triangle

def PrasertsonSmithCulbertson2026.mirror : Animacy × Colour → Animacy × Colour

The exchange of the animacy and colour columns.

Equations

• PrasertsonSmithCulbertson2026.mirror (a, c) = (c.toAnimacy, a.toColour)

theorem PrasertsonSmithCulbertson2026.mirror_images (p : Animacy × Colour) : predictiveColour (mirror p) = predictiveAnimacy p ∧ predictiveAnimacy (mirror p) = predictiveColour p

The two sets are mirror images of each other: each is the other with the animacy and colour columns exchanged.

Predictive power (Table 6)

theorem PrasertsonSmithCulbertson2026.predictiveAnimacy_horn : InformationTheory.condEntropy (Body.horn ∘ predictiveAnimacy) Prod.fst (ProbabilityTheory.uniformOn Set.univ) < InformationTheory.condEntropy (Body.horn ∘ predictiveAnimacy) Prod.snd (ProbabilityTheory.uniformOn Set.univ)

In the predictive-animacy set, animacy predicts horn type better than colour does.

theorem PrasertsonSmithCulbertson2026.predictiveAnimacy_shape : InformationTheory.condEntropy (Body.shape ∘ predictiveAnimacy) Prod.fst (ProbabilityTheory.uniformOn Set.univ) < InformationTheory.condEntropy (Body.shape ∘ predictiveAnimacy) Prod.snd (ProbabilityTheory.uniformOn Set.univ)

In the predictive-animacy set, animacy predicts body shape better than colour does.

theorem PrasertsonSmithCulbertson2026.predictiveAnimacy_appendages : InformationTheory.condEntropy (Body.appendages ∘ predictiveAnimacy) Prod.fst (ProbabilityTheory.uniformOn Set.univ) < InformationTheory.condEntropy (Body.appendages ∘ predictiveAnimacy) Prod.snd (ProbabilityTheory.uniformOn Set.univ)

In the predictive-animacy set, animacy predicts appendage shape better than colour does.

theorem PrasertsonSmithCulbertson2026.predictiveColour_horn : InformationTheory.condEntropy (Body.horn ∘ predictiveColour) Prod.snd (ProbabilityTheory.uniformOn Set.univ) < InformationTheory.condEntropy (Body.horn ∘ predictiveColour) Prod.fst (ProbabilityTheory.uniformOn Set.univ)

In the predictive-colour set, colour predicts horn type better than animacy does.

theorem PrasertsonSmithCulbertson2026.predictiveColour_shape : InformationTheory.condEntropy (Body.shape ∘ predictiveColour) Prod.snd (ProbabilityTheory.uniformOn Set.univ) < InformationTheory.condEntropy (Body.shape ∘ predictiveColour) Prod.fst (ProbabilityTheory.uniformOn Set.univ)

In the predictive-colour set, colour predicts body shape better than animacy does.

theorem PrasertsonSmithCulbertson2026.predictiveColour_appendages : InformationTheory.condEntropy (Body.appendages ∘ predictiveColour) Prod.snd (ProbabilityTheory.uniformOn Set.univ) < InformationTheory.condEntropy (Body.appendages ∘ predictiveColour) Prod.fst (ProbabilityTheory.uniformOn Set.univ)

In the predictive-colour set, colour predicts appendage shape better than animacy does.