Tessler and Goodman (2019): The Language of Generalization

This file formalizes Tessler and Goodman's model of generic, habitual and causal language. A generalization has the threshold semantics of a gradable adjective on the scale of prevalence, the probability that an instance of the category has the property (2), genericMeaning, with the threshold underspecified and drawn from a prior. The interpretation model (1) conditions a prior over prevalence on the utterance with the threshold integrated out, so the marginalized meaning of the generalization at a prevalence is the threshold prior's mass below it, and silence is true everywhere, meaning, listener, the substrate's Kernel.ofDensity. The endorsement model (3) is the speaker who chooses between the generalization and silence by how well each conveys the referent prevalence, endorser, the substrate's RSA.speaker. Since silence returns the prior, listener_silent_apply, the speaker endorses the generalization exactly when the marginalized meaning at the referent prevalence exceeds its expectation under the prevalence prior, endorse_iff; with the uniform threshold prior on the unit interval the marginalized meaning is the prevalence itself, meaning_uniformThreshold, so a generalization is endorsed exactly when the referent prevalence exceeds the prior mean prevalence, endorse_iff_expectation_lt, the cue validity of Appendix A, whose normalizer is that mean, expectedPrevalence_map.

The worked examples of Table 1 are consequences of the prior mean. Endorsement is monotone in prevalence at a fixed prior (Figure 1), endorse_mono; at one referent prevalence a property whose prior mean lies below it is endorsed while one whose prior mean lies at or above it is not, endorse_of_expectation_lt, not_endorse_of_le_expectation, which is why dogs bark at a high prevalence and mosquitos carry malaria at a low one are endorsed while kangaroos have spots is not. A prior symmetric about one half has mean one half, expectedPrevalence_eq_half_of_symm, so robins are female at a prevalence of one half is exactly at the boundary, the generalization no more informative than silence, boundary_of_symm; mixing such a prior with a component at zero prevalence, the categories without the mechanism, lowers the mean below one half, expectedPrevalence_mixture, so robins lay eggs at the same prevalence is endorsed, endorse_of_mixture. Habituals use the same model on the scale of frequency, and causal generalizations on the rate at which the cause produces the effect, with the priors elicited in the experiments; the model's fits to the endorsement data of the three case studies are the paper's empirical content and are described, not formalized.

Implementation notes

The prevalence scale is a finite type carrying a real prevalence, and the prevalence prior a probability measure on it; the threshold prior is any finite measure on the reals, the paper's uniform prior on the support of the prevalence prior being the case treated on the real face. The rationality of the endorser is a parameter, so the theorems hold at every positive rationality; the paper's fitted values are not pinned.

References

• [TG19]
• [FG12]
• [LG17]
• [Les08]

inductive TesslerGoodman2019.Utterance : Type

In the endorsement model the speaker says the generalization or stays silent.

• generic : Utterance
• silent : Utterance

@[instance_reducible]

instance TesslerGoodman2019.instDecidableEqUtterance : DecidableEq Utterance

Equations

• TesslerGoodman2019.instDecidableEqUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance TesslerGoodman2019.instFintypeUtterance : Fintype Utterance

Equations

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

@[instance_reducible]

instance TesslerGoodman2019.instMeasurableSpaceUtterance : MeasurableSpace Utterance

Equations

• TesslerGoodman2019.instMeasurableSpaceUtterance = ⊤

instance TesslerGoodman2019.instDiscreteMeasurableSpaceUtterance : DiscreteMeasurableSpace Utterance

def TesslerGoodman2019.genericMeaning (θ p : ℝ) : Prop

Under the threshold semantics (2), a generalization is true when the prevalence exceeds the threshold.

Equations

• TesslerGoodman2019.genericMeaning θ p = (θ < p)

noncomputable def TesslerGoodman2019.meaning {W : Type u_1} (ν : MeasureTheory.Measure ℝ) (prev : W → ℝ) : Utterance → W → ENNReal

With the threshold of (1) integrated out against its prior ν, the generalization means the prior mass of thresholds below the prevalence, and silence means one.

Equations

• TesslerGoodman2019.meaning ν prev TesslerGoodman2019.Utterance.generic x✝ = ν {θ : ℝ | TesslerGoodman2019.genericMeaning θ (prev x✝)}
• TesslerGoodman2019.meaning ν prev TesslerGoodman2019.Utterance.silent x✝ = 1

noncomputable def TesslerGoodman2019.expectedMeaning {W : Type u_1} [Fintype W] [MeasurableSpace W] (μ : MeasureTheory.Measure W) (ν : MeasureTheory.Measure ℝ) (prev : W → ℝ) : ENNReal

The expectation under the prevalence prior of the marginalized meaning of the generalization.

Equations

• TesslerGoodman2019.expectedMeaning μ ν prev = ∑ w : W, TesslerGoodman2019.meaning ν prev TesslerGoodman2019.Utterance.generic w * μ {w}

theorem TesslerGoodman2019.expectedMeaning_ne_top {W : Type u_1} [Fintype W] [MeasurableSpace W] (μ : MeasureTheory.Measure W) [MeasureTheory.IsFiniteMeasure μ] (ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure ν] (prev : W → ℝ) : expectedMeaning μ ν prev ≠ ⊤

noncomputable def TesslerGoodman2019.listener {W : Type u_1} [MeasurableSpace W] (μ : MeasureTheory.Measure W) (ν : MeasureTheory.Measure ℝ) (prev : W → ℝ) : ProbabilityTheory.Kernel Utterance W

The interpretation model (1) conditions the prevalence prior on the marginalized meaning.

Equations

• TesslerGoodman2019.listener μ ν prev = ProbabilityTheory.Kernel.ofDensity μ (TesslerGoodman2019.meaning ν prev)

instance TesslerGoodman2019.instIsFiniteKernelUtteranceListener {W : Type u_1} [MeasurableSpace W] (μ : MeasureTheory.Measure W) (ν : MeasureTheory.Measure ℝ) (prev : W → ℝ) : ProbabilityTheory.IsFiniteKernel (listener μ ν prev)

noncomputable def TesslerGoodman2019.endorser {W : Type u_1} [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] (lam : ℝ) (μ : MeasureTheory.Measure W) (ν : MeasureTheory.Measure ℝ) (prev : W → ℝ) : ProbabilityTheory.Kernel W Utterance

The endorsement model (3) is the speaker at rationality lam, choosing between the generalization and silence at no cost.

Equations

• TesslerGoodman2019.endorser lam μ ν prev = RSA.speaker lam 0 (⇑(TesslerGoodman2019.listener μ ν prev)) MeasureTheory.Measure.dirac

def TesslerGoodman2019.Endorsed {W : Type u_1} [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] (lam : ℝ) (μ : MeasureTheory.Measure W) (ν : MeasureTheory.Measure ℝ) (prev : W → ℝ) (w : W) : Prop

The generalization is endorsed at a state when the speaker produces it more readily than silence.

Equations

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

theorem TesslerGoodman2019.listener_generic_apply {W : Type u_1} [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] (μ : MeasureTheory.Measure W) (ν : MeasureTheory.Measure ℝ) (prev : W → ℝ) (w : W) : ((listener μ ν prev) Utterance.generic) {w} = meaning ν prev Utterance.generic w * μ {w} / expectedMeaning μ ν prev

theorem TesslerGoodman2019.listener_silent_apply {W : Type u_1} [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] (μ : MeasureTheory.Measure W) (ν : MeasureTheory.Measure ℝ) (prev : W → ℝ) [MeasureTheory.IsProbabilityMeasure μ] (w : W) : ((listener μ ν prev) Utterance.silent) {w} = μ {w}

Silence returns the prior.

theorem TesslerGoodman2019.endorse_iff {W : Type u_1} [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] (μ : MeasureTheory.Measure W) (ν : MeasureTheory.Measure ℝ) (prev : W → ℝ) [MeasureTheory.IsProbabilityMeasure μ] {lam : ℝ} {w : W} [MeasureTheory.IsFiniteMeasure ν] (hlam : 0 < lam) (hw : μ {w} ≠ 0) (hZ : expectedMeaning μ ν prev ≠ 0) : Endorsed lam μ ν prev w ↔ expectedMeaning μ ν prev < meaning ν prev Utterance.generic w

The generalization is endorsed exactly when its marginalized meaning at the referent state exceeds the prior expectation of that meaning. This is the comparison of Figure 1C, the listener's posterior on hearing the generalization against the prior.

theorem TesslerGoodman2019.endorse_mono {W : Type u_1} [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] (μ : MeasureTheory.Measure W) (ν : MeasureTheory.Measure ℝ) (prev : W → ℝ) [MeasureTheory.IsProbabilityMeasure μ] {lam : ℝ} [MeasureTheory.IsFiniteMeasure ν] (hlam : 0 < lam) (hZ : expectedMeaning μ ν prev ≠ 0) {w w' : W} (hw : μ {w} ≠ 0) (hw' : μ {w'} ≠ 0) (hle : prev w ≤ prev w') (h : Endorsed lam μ ν prev w) : Endorsed lam μ ν prev w'

Endorsement is monotone in prevalence at a fixed prior (Figure 1C).

The uniform threshold prior

noncomputable def TesslerGoodman2019.uniformThreshold : MeasureTheory.Measure ℝ

The uniform threshold prior on the unit interval, the support of a prevalence prior.

Equations

• TesslerGoodman2019.uniformThreshold = MeasureTheory.volume.restrict (Set.Icc 0 1)

instance TesslerGoodman2019.instIsFiniteMeasureRealUniformThreshold : MeasureTheory.IsFiniteMeasure uniformThreshold

theorem TesslerGoodman2019.uniformThreshold_Iio {p : ℝ} (h1 : p ≤ 1) : uniformThreshold (Set.Iio p) = ENNReal.ofReal p

The uniform threshold prior's mass below a prevalence in the unit interval is the prevalence.

theorem TesslerGoodman2019.meaning_uniformThreshold {W : Type u_1} (prev : W → ℝ) (hp : ∀ (w : W), 0 ≤ prev w ∧ prev w ≤ 1) (w : W) : meaning uniformThreshold prev Utterance.generic w = ENNReal.ofReal (prev w)

Under the uniform threshold prior the marginalized meaning of the generalization is the prevalence.

noncomputable def TesslerGoodman2019.expectedPrevalence {W : Type u_1} [MeasurableSpace W] (μ : MeasureTheory.Measure W) (prev : W → ℝ) : ℝ

The mean prevalence under the prior.

Equations

• TesslerGoodman2019.expectedPrevalence μ prev = ∫ (w : W), prev w ∂μ

theorem TesslerGoodman2019.expectedPrevalence_map {W : Type u_1} [MeasurableSpace W] (prev : W → ℝ) {K : Type u_2} [MeasurableSpace K] [DiscreteMeasurableSpace K] [Countable K] (P : MeasureTheory.Measure K) (prevK : K → W) (hprev : Measurable prevK) (hf : Measurable prev) : expectedPrevalence (MeasureTheory.Measure.map prevK P) prev = ∫ (k : K), prev (prevK k) ∂P

When the prevalence prior is the pushforward of a prior over categories along their prevalences, the normalizer of cue validity, the mean prevalence over categories, is the mean of the prevalence prior (Appendix A).

theorem TesslerGoodman2019.expectedPrevalence_eq_sum {W : Type u_1} [MeasurableSpace W] (prev : W → ℝ) [Fintype W] [DiscreteMeasurableSpace W] (μ : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure μ] : expectedPrevalence μ prev = ∑ w : W, μ.real {w} * prev w

theorem TesslerGoodman2019.expectedMeaning_uniformThreshold {W : Type u_1} [MeasurableSpace W] (prev : W → ℝ) [Fintype W] [DiscreteMeasurableSpace W] (μ : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure μ] (hp : ∀ (w : W), 0 ≤ prev w ∧ prev w ≤ 1) : expectedMeaning μ uniformThreshold prev = ENNReal.ofReal (expectedPrevalence μ prev)

theorem TesslerGoodman2019.endorse_iff_expectation_lt {W : Type u_1} [MeasurableSpace W] (prev : W → ℝ) [Fintype W] [DiscreteMeasurableSpace W] (μ : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure μ] {lam : ℝ} {w : W} (hlam : 0 < lam) (hp : ∀ (w : W), 0 ≤ prev w ∧ prev w ≤ 1) (hw : μ {w} ≠ 0) (hZ : 0 < expectedPrevalence μ prev) : Endorsed lam μ uniformThreshold prev w ↔ expectedPrevalence μ prev < prev w

The generalization is endorsed exactly when the referent prevalence exceeds the mean prevalence under the prior, the cue validity of Appendix A.

theorem TesslerGoodman2019.endorse_of_expectation_lt {W : Type u_1} [MeasurableSpace W] (prev : W → ℝ) [Fintype W] [DiscreteMeasurableSpace W] (μ : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure μ] {lam : ℝ} {w : W} (hlam : 0 < lam) (hp : ∀ (w : W), 0 ≤ prev w ∧ prev w ≤ 1) (hw : μ {w} ≠ 0) (hZ : 0 < expectedPrevalence μ prev) (h : expectedPrevalence μ prev < prev w) : Endorsed lam μ uniformThreshold prev w

A property whose prior mean lies below the referent prevalence is endorsed.

theorem TesslerGoodman2019.not_endorse_of_le_expectation {W : Type u_1} [MeasurableSpace W] (prev : W → ℝ) [Fintype W] [DiscreteMeasurableSpace W] (μ : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure μ] {lam : ℝ} {w : W} (hlam : 0 < lam) (hp : ∀ (w : W), 0 ≤ prev w ∧ prev w ≤ 1) (hw : μ {w} ≠ 0) (hZ : 0 < expectedPrevalence μ prev) (h : prev w ≤ expectedPrevalence μ prev) : ¬Endorsed lam μ uniformThreshold prev w

A property whose prior mean lies at or above the referent prevalence is not endorsed.

Table 1: symmetric and bimodal priors

theorem TesslerGoodman2019.isProbabilityMeasure_mixture {W : Type u_1} [MeasurableSpace W] (ν₁ ν₀ : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure ν₁] [MeasureTheory.IsProbabilityMeasure ν₀] {φ : ℝ} (h0 : 0 ≤ φ) (h1 : φ ≤ 1) : MeasureTheory.IsProbabilityMeasure (φ.toNNReal • ν₁ + (1 - φ).toNNReal • ν₀)

A mixture of a probability measure with mass φ and another with mass 1 - φ is a probability measure.

theorem TesslerGoodman2019.expectedPrevalence_eq_half_of_symm {W : Type u_1} [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] (prev : W → ℝ) (μ : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure μ] (σ : W ≃ W) (hσ : ∀ (w : W), prev (σ w) = 1 - prev w) (hμ : ∀ (w : W), μ {σ w} = μ {w}) : expectedPrevalence μ prev = 1 / 2

A prior invariant under a reflection of the scale about one half has mean one half.

theorem TesslerGoodman2019.expectedPrevalence_mixture {W : Type u_1} [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] (prev : W → ℝ) (ν₁ ν₀ : MeasureTheory.Measure W) [MeasureTheory.IsFiniteMeasure ν₁] [MeasureTheory.IsFiniteMeasure ν₀] (c d : NNReal) : expectedPrevalence (c • ν₁ + d • ν₀) prev = ↑c * expectedPrevalence ν₁ prev + ↑d * expectedPrevalence ν₀ prev

The mean prevalence of a mixture is the mixture of the means.

theorem TesslerGoodman2019.boundary_of_symm {W : Type u_1} [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] (prev : W → ℝ) (μ : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure μ] (σ : W ≃ W) (hσ : ∀ (w : W), prev (σ w) = 1 - prev w) (hμ : ∀ (w : W), μ {σ w} = μ {w}) {lam : ℝ} (hlam : 0 < lam) (hp : ∀ (w : W), 0 ≤ prev w ∧ prev w ≤ 1) {w : W} (hw : μ {w} ≠ 0) (hhalf : prev w = 1 / 2) : ((endorser lam μ uniformThreshold prev) w).real {Utterance.generic} = ((endorser lam μ uniformThreshold prev) w).real {Utterance.silent}

For robins are female, a prior symmetric about one half puts a referent prevalence of one half exactly at the boundary, where the generalization and silence are produced alike.

theorem TesslerGoodman2019.expectedPrevalence_bimodal {W : Type u_1} [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] (prev : W → ℝ) (ν₁ : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure ν₁] (σ : W ≃ W) (hσ : ∀ (w : W), prev (σ w) = 1 - prev w) (hν : ∀ (w : W), ν₁ {σ w} = ν₁ {w}) (w₀ : W) (hw₀ : prev w₀ = 0) {φ : ℝ} (h0 : 0 ≤ φ) : expectedPrevalence (φ.toNNReal • ν₁ + (1 - φ).toNNReal • MeasureTheory.Measure.dirac w₀) prev = φ / 2

For robins lay eggs, mixing a prior symmetric about one half with a component at zero prevalence, the categories without the mechanism, at weight 1 - φ gives mean φ / 2.

theorem TesslerGoodman2019.endorse_of_mixture {W : Type u_1} [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] (prev : W → ℝ) (ν₁ : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure ν₁] (σ : W ≃ W) (hσ : ∀ (w : W), prev (σ w) = 1 - prev w) (hν : ∀ (w : W), ν₁ {σ w} = ν₁ {w}) (w₀ : W) (hw₀ : prev w₀ = 0) {φ : ℝ} (h0 : 0 < φ) (h1 : φ < 1) {lam : ℝ} (hlam : 0 < lam) (hp : ∀ (w : W), 0 ≤ prev w ∧ prev w ≤ 1) {w : W} (hw : ν₁ {w} ≠ 0) (hhalf : prev w = 1 / 2) : Endorsed lam (φ.toNNReal • ν₁ + (1 - φ).toNNReal • MeasureTheory.Measure.dirac w₀) uniformThreshold prev w

At a referent prevalence of one half the bimodal prior endorses the generalization whenever some categories lack the mechanism, φ < 1, while the symmetric prior alone, φ = 1, sits at the boundary.