Lassiter and Goodman (2017): Adjectival Vagueness in a Bayesian Model of Interpretation

This file formalizes the free-variable Rational Speech Act model of [LG17] on the RSA kernel pipeline. A positive-form gradable adjective compares a degree with a threshold the semantics leaves open (sem); the pragmatic listener resolves the threshold jointly with the state, threading each candidate assignment through a threshold-indexed literal listener and speaker (L0, S1) and inverting the family against the product of the degree prior and the threshold prior (L1). The threshold marginal of that posterior gives the metalinguistic probability that an individual counts as tall, the posterior mass of thresholds below the individual's height (metalinguistic), and borderline cases are those of intermediate metalinguistic probability.

The sorites dissolves as in Edgington. Read materially, the inductive premises fail exactly when the threshold falls in the gap between adjacent members, and the gap masses sum to the mass of the whole range (sum_gapMass), so each can be small while their sum is near one; Adams's theorem bounds the uncertainty of the conclusion of a valid argument by the summed uncertainty of its premises (adams), and the sorites is valid (sorites_uncertainty). Read by Adams's Thesis, each premise is a conditional probability of the threshold marginal and is at most the material premise (conditionalPremise_le).

Implementation notes

Degrees form a finite linear order so that the discrete pipeline applies; the paper's continuous scale and normal prior enter only through its simulations, which are not stated. The assignment of the paper's eq. 27 is the pair of thresholds for the adjective and its antonym, and the threshold prior is a parameter rather than the paper's uniform prior, which the model never uses beyond its being a prior.

TODO

The free-variable reading of the inductive premise (the paper's eq. 44), the antonym symmetry of the simulations, and the scalar-implicature warm-up of §3 are not stated.

References

• [LG17]

inductive LassiterGoodman2017.Utterance : Type

The utterances: the adjective, its antonym, and saying nothing.

• tall : Utterance
• short : Utterance
• silent : Utterance

@[instance_reducible]

instance LassiterGoodman2017.instDecidableEqUtterance : DecidableEq Utterance

Equations

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

def LassiterGoodman2017.instReprUtterance.repr : Utterance → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LassiterGoodman2017.instReprUtterance : Repr Utterance

Equations

• LassiterGoodman2017.instReprUtterance = { reprPrec := LassiterGoodman2017.instReprUtterance.repr }

@[instance_reducible]

instance LassiterGoodman2017.instFintypeUtterance : Fintype Utterance

Equations

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

@[instance_reducible]

instance LassiterGoodman2017.instMeasurableSpaceUtterance : MeasurableSpace Utterance

Equations

• LassiterGoodman2017.instMeasurableSpaceUtterance = ⊤

instance LassiterGoodman2017.instDiscreteMeasurableSpaceUtterance : DiscreteMeasurableSpace Utterance

instance LassiterGoodman2017.instNonemptyUtterance : Nonempty Utterance

def LassiterGoodman2017.sem {D : Type u_1} [LinearOrder D] (θ : D × D) : Utterance → Set D

The meaning of an utterance at a degree under an assignment of thresholds to the adjective and its antonym (eqs. 22–23): tall holds above the first threshold, short below the second, and silence everywhere.

Equations

• LassiterGoodman2017.sem θ LassiterGoodman2017.Utterance.tall = Set.Ioi θ.1
• LassiterGoodman2017.sem θ LassiterGoodman2017.Utterance.short = Set.Iio θ.2
• LassiterGoodman2017.sem θ LassiterGoodman2017.Utterance.silent = Set.univ

noncomputable def LassiterGoodman2017.L0 {D : Type u_1} [LinearOrder D] [MeasurableSpace D] (μ : MeasureTheory.Measure D) (θ : D × D) : ProbabilityTheory.Kernel Utterance D

The literal listener at an assignment (eq. 27): the degree prior conditioned on the truth of the utterance.

Equations

• LassiterGoodman2017.L0 μ θ = RSA.literalListener μ fun (u : LassiterGoodman2017.Utterance) => (LassiterGoodman2017.sem θ u).indicator 1

theorem LassiterGoodman2017.L0_apply_singleton_ne_zero_iff {D : Type u_1} [LinearOrder D] [MeasurableSpace D] [DiscreteMeasurableSpace D] (μ : MeasureTheory.Measure D) [MeasureTheory.IsFiniteMeasure μ] (θ : D × D) (u : Utterance) (d : D) : ((L0 μ θ) u) {d} ≠ 0 ↔ d ∈ sem θ u ∧ μ {d} ≠ 0

noncomputable def LassiterGoodman2017.S1 {D : Type u_1} [LinearOrder D] [MeasurableSpace D] [DiscreteMeasurableSpace D] [Fintype D] (μ : MeasureTheory.Measure D) (α : ℝ) (cost : Utterance → ENNReal) : ProbabilityTheory.Kernel (D × D × D) Utterance

The speaker at an assignment (eq. 28): the family speaker over degrees and assignments at rationality α with cost factors cost.

Equations

• LassiterGoodman2017.S1 μ α cost = RSA.familySpeaker (LassiterGoodman2017.L0 μ) α cost

noncomputable def LassiterGoodman2017.L1 {D : Type u_1} [LinearOrder D] [MeasurableSpace D] [DiscreteMeasurableSpace D] [Fintype D] [Nonempty D] (μ : MeasureTheory.Measure D) [MeasureTheory.IsProbabilityMeasure μ] (ν : MeasureTheory.Measure (D × D)) [MeasureTheory.IsProbabilityMeasure ν] (α : ℝ) (cost : Utterance → ENNReal) : ProbabilityTheory.Kernel Utterance (D × D × D)

The pragmatic listener (eq. 29): the family listener against the product of the degree prior and the threshold prior. Its first marginal is the degree posterior (eq. 31), its second the posterior over assignments (eq. 30).

Equations

• LassiterGoodman2017.L1 μ ν α cost = RSA.familyListener (LassiterGoodman2017.L0 μ) α cost (μ.prod ν)

theorem LassiterGoodman2017.S1_apply_singleton_ne_zero_iff {D : Type u_1} [LinearOrder D] [MeasurableSpace D] [DiscreteMeasurableSpace D] [Fintype D] (μ : MeasureTheory.Measure D) [MeasureTheory.IsProbabilityMeasure μ] (α : ℝ) (cost : Utterance → ENNReal) (hα : 0 < α) (hc0 : ∀ (u : Utterance), cost u ≠ 0) (hctop : ∀ (u : Utterance), cost u ≠ ⊤) (d : D) (θ : D × D) (u : Utterance) : ((S1 μ α cost) (d, θ)) {u} ≠ 0 ↔ d ∈ sem θ u ∧ μ {d} ≠ 0

The speaker produces an utterance at a degree and assignment exactly when it is true there and the degree has positive prior.

theorem LassiterGoodman2017.comp_S1_ne_zero {D : Type u_1} [LinearOrder D] [MeasurableSpace D] [DiscreteMeasurableSpace D] [Fintype D] (μ : MeasureTheory.Measure D) [MeasureTheory.IsProbabilityMeasure μ] (ν : MeasureTheory.Measure (D × D)) (α : ℝ) (cost : Utterance → ENNReal) (hα : 0 < α) (hc0 : ∀ (u : Utterance), cost u ≠ 0) (hctop : ∀ (u : Utterance), cost u ≠ ⊤) {u : Utterance} {d : D} {θ : D × D} (hd : μ {d} ≠ 0) (hθ : ν {θ} ≠ 0) (hu : d ∈ sem θ u) : ((μ.prod ν).bind ⇑(S1 μ α cost)) {u} ≠ 0

An utterance true at a degree of positive prior under an assignment of positive prior has a positive marginal.

instance LassiterGoodman2017.instIsMarkovKernelUtteranceProdL1 {D : Type u_1} [LinearOrder D] [MeasurableSpace D] [DiscreteMeasurableSpace D] [Fintype D] (μ : MeasureTheory.Measure D) [MeasureTheory.IsProbabilityMeasure μ] (ν : MeasureTheory.Measure (D × D)) (α : ℝ) (cost : Utterance → ENNReal) [Nonempty D] [MeasureTheory.IsProbabilityMeasure ν] : ProbabilityTheory.IsMarkovKernel (L1 μ ν α cost)

theorem LassiterGoodman2017.L1_apply_singleton_ne_zero_iff {D : Type u_1} [LinearOrder D] [MeasurableSpace D] [DiscreteMeasurableSpace D] [Fintype D] (μ : MeasureTheory.Measure D) [MeasureTheory.IsProbabilityMeasure μ] (ν : MeasureTheory.Measure (D × D)) (α : ℝ) (cost : Utterance → ENNReal) [Nonempty D] [MeasureTheory.IsProbabilityMeasure ν] (hα : 0 < α) (hc0 : ∀ (u : Utterance), cost u ≠ 0) (hctop : ∀ (u : Utterance), cost u ≠ ⊤) {u : Utterance} (hu : ((μ.prod ν).bind ⇑(S1 μ α cost)) {u} ≠ 0) (d : D) (θ : D × D) : ((L1 μ ν α cost) u) {(d, θ)} ≠ 0 ↔ μ {d} ≠ 0 ∧ ν {θ} ≠ 0 ∧ d ∈ sem θ u

Truthfulness: the pragmatic listener puts positive mass on a degree and assignment exactly when both have positive prior and the utterance is true at the degree under the assignment.

noncomputable def LassiterGoodman2017.thresholdPosterior {D : Type u_1} [LinearOrder D] [MeasurableSpace D] [DiscreteMeasurableSpace D] [Fintype D] (μ : MeasureTheory.Measure D) [MeasureTheory.IsProbabilityMeasure μ] (ν : MeasureTheory.Measure (D × D)) (α : ℝ) (cost : Utterance → ENNReal) [Nonempty D] [MeasureTheory.IsProbabilityMeasure ν] (u : Utterance) : MeasureTheory.Measure D

The posterior over the adjective's threshold (eq. 30): the marginal of the listener on the first coordinate of the assignment.

Equations

• LassiterGoodman2017.thresholdPosterior μ ν α cost u = ((LassiterGoodman2017.L1 μ ν α cost) u).snd.fst

instance LassiterGoodman2017.instIsProbabilityMeasureThresholdPosterior {D : Type u_1} [LinearOrder D] [MeasurableSpace D] [DiscreteMeasurableSpace D] [Fintype D] (μ : MeasureTheory.Measure D) [MeasureTheory.IsProbabilityMeasure μ] (ν : MeasureTheory.Measure (D × D)) (α : ℝ) (cost : Utterance → ENNReal) [Nonempty D] [MeasureTheory.IsProbabilityMeasure ν] (u : Utterance) : MeasureTheory.IsProbabilityMeasure (thresholdPosterior μ ν α cost u)

noncomputable def LassiterGoodman2017.metalinguistic {D : Type u_1} [LinearOrder D] [MeasurableSpace D] (ρ : MeasureTheory.Measure D) (d : D) : ENNReal

The metalinguistic probability that a degree counts as tall under a threshold measure (eq. 32): the mass of thresholds below it.

Equations

• LassiterGoodman2017.metalinguistic ρ d = ρ (Set.Iio d)

theorem LassiterGoodman2017.metalinguistic_thresholdPosterior {D : Type u_1} [LinearOrder D] [MeasurableSpace D] [DiscreteMeasurableSpace D] [Fintype D] (μ : MeasureTheory.Measure D) [MeasureTheory.IsProbabilityMeasure μ] (ν : MeasureTheory.Measure (D × D)) (α : ℝ) (cost : Utterance → ENNReal) [Nonempty D] [MeasureTheory.IsProbabilityMeasure ν] (u : Utterance) (d : D) : metalinguistic (thresholdPosterior μ ν α cost u) d = ((L1 μ ν α cost) u) {p : D × D × D | p.2.1 < d}

The metalinguistic probability marginalizes the joint posterior over the degree and the antonym's threshold.

def LassiterGoodman2017.Borderline {D : Type u_1} [LinearOrder D] [MeasurableSpace D] (ρ : MeasureTheory.Measure D) (d : D) : Prop

A borderline case: a degree of intermediate metalinguistic probability.

Equations

• LassiterGoodman2017.Borderline ρ d = (0 < LassiterGoodman2017.metalinguistic ρ d ∧ LassiterGoodman2017.metalinguistic ρ d < 1)

The sorites

noncomputable def LassiterGoodman2017.gapMass {D : Type u_1} [LinearOrder D] [MeasurableSpace D] (ρ : MeasureTheory.Measure D) (a b : D) : ENNReal

The failure probability of a material inductive premise (eq. 37): the threshold falls between two adjacent members.

Equations

• LassiterGoodman2017.gapMass ρ a b = ρ (Set.Ico a b)

theorem LassiterGoodman2017.sum_gapMass {D : Type u_1} [LinearOrder D] [MeasurableSpace D] [DiscreteMeasurableSpace D] (ρ : MeasureTheory.Measure D) (x : ℕ → D) (hx : Monotone x) (n : ℕ) : ∑ i ∈ Finset.range n, gapMass ρ (x i) (x (i + 1)) = gapMass ρ (x 0) (x n)

Along a monotone sequence the gap masses sum to the mass of the whole range.

theorem LassiterGoodman2017.adams {Ω : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (s : Finset ι) (A : ι → Set Ω) (hA : ∀ i ∈ s, MeasurableSet (A i)) {C : Set Ω} (hC : ⋂ i ∈ s, A i ⊆ C) : 1 - μ C ≤ ∑ i ∈ s, (1 - μ (A i))

Adams's theorem: the uncertainty of the conclusion of a valid argument is at most the summed uncertainty of its premises.

theorem LassiterGoodman2017.sorites_valid {D : Type u_1} [LinearOrder D] (x : ℕ → D) (n : ℕ) {θ : D} (hθ : θ < x n) (hgap : ∀ i ∈ Finset.range n, θ ∉ Set.Ico (x i) (x (i + 1))) : θ < x 0

The material sorites is valid: if the top member is tall and no gap holds the threshold, the bottom member is tall.

theorem LassiterGoodman2017.sorites_uncertainty {D : Type u_1} [LinearOrder D] [MeasurableSpace D] [DiscreteMeasurableSpace D] (ρ : MeasureTheory.Measure D) [MeasureTheory.IsProbabilityMeasure ρ] (x : ℕ → D) (hx : Monotone x) (n : ℕ) : 1 - metalinguistic ρ (x 0) ≤ 1 - metalinguistic ρ (x n) + gapMass ρ (x 0) (x n)

The uncertainty of the sorites conclusion is bounded by the uncertainty that the top member is tall plus the summed gap masses, which is the mass of the whole range.

theorem LassiterGoodman2017.conditionalPremise_le {D : Type u_1} [LinearOrder D] [MeasurableSpace D] [DiscreteMeasurableSpace D] (ρ : MeasureTheory.Measure D) [MeasureTheory.IsProbabilityMeasure ρ] {a b : D} (hab : a ≤ b) : ρ[Set.Iio a | Set.Iio b] ≤ ρ (Set.Ico a b)ᶜ

Under Adams's Thesis (eq. 40) an inductive premise is the conditional probability that the lower member is tall given that the upper one is, which is at most the material premise, the probability that the threshold avoids the gap.