Goodman and Stuhlmüller (2013): Knowledge and Implicature

Goodman and Stuhlmüller model scalar implicature under a speaker with incomplete knowledge. The state is how many of N objects have a property, and the speaker's access is how many of them she looks at. She observes how many of those have the property, a hypergeometric draw, believes her posterior over states, and softmax-optimizes the expected log-probability the literal listener gives the state under that belief. The listener, who knows her access but not her observation, models her with the observation drawn at the state (speaker) and applies Bayes' rule (listener).

Main statements

• speaker_real_singleton: the speaker says only what holds at every state her observation leaves possible, and weights such an utterance by the inverse size of its extension to the power of the rationality.
• listener_full_lt: with complete access the speaker knows the state, and of two states at which an utterance is true the listener favours the one at which fewer alternatives are true. For three objects, some implicates not all (some_full) and a numeral its exact reading (two_full, one_full).
• speaker_of_isUpperSet: when every meaning is upward closed, as the lower-bounded numerals are, the speaker who has seen k objects with the property speaks as one who knows there are exactly k.
• some_partial, one_minimal, two_partial, one_partial_three, one_partial_two: with access to one or two of three objects the some implicature is canceled, one after one object and two after two carry none, and one after two objects keeps the implicature against three but not against two.

Implementation notes

• The speaker is RSA.speaker at her posterior belief and no cost, composed with the draw of her observation. The literal listener is uniform on an utterance's extension, so only the support of the belief matters.
• The model takes any number of objects, and the alternatives and predictions are for three. An utterance's extension is a row of the tree of numbers, the numerals on their lower-bounded meaning.
• The alternatives are the paper's, none, some, all and one, two, three, without a silent option, so a speaker whose observation supports none of them says nothing.
• The prior is uniform, the regime of the paper's expository predictions; its fitted binomial prior and its rationality only reshape the plotted magnitudes. Experiment results and the quantitative fit are not formalized.

References

• [GS13]
• [FG12]
• [Hor72]

The states an observation leaves possible

def GoodmanStuhlmuller2013.compatible {N : ℕ} (n : ℕ) (k : Fin (N + 1)) : Finset (Fin (N + 1))

The states an observation leaves possible are those at which the speaker could see k objects with the property among the n she looks at.

Equations

• GoodmanStuhlmuller2013.compatible n k = {s : Fin (N + 1) | ProbabilityTheory.hypergeometricCount N (↑s) n ↑k ≠ 0}

@[simp]

theorem GoodmanStuhlmuller2013.mem_compatible {N n : ℕ} {k s : Fin (N + 1)} : s ∈ compatible n k ↔ ProbabilityTheory.hypergeometricCount N (↑s) n ↑k ≠ 0

theorem GoodmanStuhlmuller2013.posterior_ne_zero_iff_mem_compatible {N n : ℕ} {k : Fin (N + 1)} (hk : (compatible n k).Nonempty) (s : Fin (N + 1)) : ((ProbabilityTheory.posterior (ProbabilityTheory.hypergeometric N n) (ProbabilityTheory.uniformOn Set.univ)) k) {s} ≠ 0 ↔ s ∈ compatible n k

After a possible observation the posterior under the uniform prior charges exactly the states compatible with it.

The speaker and the listener

@[reducible, inline]

noncomputable abbrev GoodmanStuhlmuller2013.literal {N : ℕ} {U : Type u_1} [MeasurableSpace U] [Fintype U] [MeasurableSingletonClass U] (sem : U → Finset (Fin (N + 1))) : ProbabilityTheory.Kernel U (Fin (N + 1))

The literal listener Plex of section 1 conditions the uniform prior on the extension of the utterance.

Equations

• GoodmanStuhlmuller2013.literal sem = RSA.listener (ProbabilityTheory.uniformOn Set.univ) (RSA.truthful fun (u : U) => ↑(sem u))

@[reducible, inline]

noncomputable abbrev GoodmanStuhlmuller2013.informed {N : ℕ} {U : Type u_1} [MeasurableSpace U] [Fintype U] [MeasurableSingletonClass U] (sem : U → Finset (Fin (N + 1))) (α : ℝ) : ProbabilityTheory.Kernel (Fin (N + 1)) U

The informed speaker knows the state and addresses the literal listener.

Equations

• GoodmanStuhlmuller2013.informed sem α = RSA.speaker α 0 (⇑(GoodmanStuhlmuller2013.literal sem)) MeasureTheory.Measure.dirac

noncomputable def GoodmanStuhlmuller2013.speaker {N : ℕ} {U : Type u_1} [MeasurableSpace U] [Fintype U] [MeasurableSingletonClass U] (sem : U → Finset (Fin (N + 1))) (α : ℝ) (n : ℕ) : ProbabilityTheory.Kernel (Fin (N + 1)) U

The speaker of equations (2) and (3) sees how many of the n objects she looks at have the property, believes her posterior over states under the uniform prior, and addresses the literal listener. The listener cannot see her observation, so the speaker he models (equation 4) draws it at the state.

Equations

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

instance GoodmanStuhlmuller2013.instIsFiniteKernelFinHAddNatOfNatSpeaker {N : ℕ} {U : Type u_1} [MeasurableSpace U] [Fintype U] [MeasurableSingletonClass U] (sem : U → Finset (Fin (N + 1))) (α : ℝ) (n : ℕ) : ProbabilityTheory.IsFiniteKernel (speaker sem α n)

noncomputable def GoodmanStuhlmuller2013.listener {N : ℕ} {U : Type u_1} [MeasurableSpace U] [Fintype U] [MeasurableSingletonClass U] (sem : U → Finset (Fin (N + 1))) (α : ℝ) (n : ℕ) : ProbabilityTheory.Kernel U (Fin (N + 1))

The listener (equation 1) inverts the speaker against a uniform prior.

Equations

• GoodmanStuhlmuller2013.listener sem α n = RSA.listener (ProbabilityTheory.uniformOn Set.univ) ⇑(GoodmanStuhlmuller2013.speaker sem α n)

theorem GoodmanStuhlmuller2013.speaker_real_singleton {N : ℕ} {U : Type u_1} [MeasurableSpace U] [Fintype U] [MeasurableSingletonClass U] {sem : U → Finset (Fin (N + 1))} {α : ℝ} {n : ℕ} (hα : 0 < α) (s : Fin (N + 1)) (u : U) : ((speaker sem α n) s).real {u} = ∑ k : Fin (N + 1), ((ProbabilityTheory.hypergeometric N n) s).real {k} * ((if compatible n k ⊆ sem u then (↑(sem u).card)⁻¹ ^ α else 0) / ∑ u' : U, if compatible n k ⊆ sem u' then (↑(sem u').card)⁻¹ ^ α else 0)

The speaker says only what holds at every state her observation leaves possible, and weights such an utterance by the inverse size of its extension to the power α.

theorem GoodmanStuhlmuller2013.speaker_real_singleton_le_one {N : ℕ} {U : Type u_1} [MeasurableSpace U] [Fintype U] [MeasurableSingletonClass U] {sem : U → Finset (Fin (N + 1))} {α : ℝ} {n : ℕ} (s : Fin (N + 1)) (u : U) : ((speaker sem α n) s).real {u} ≤ 1

theorem GoodmanStuhlmuller2013.speaker_full {N : ℕ} {U : Type u_1} [MeasurableSpace U] [Fintype U] [MeasurableSingletonClass U] {sem : U → Finset (Fin (N + 1))} {α : ℝ} : speaker sem α N = informed sem α

With complete access the speaker knows the state.

theorem GoodmanStuhlmuller2013.speaker_last {N : ℕ} {U : Type u_1} [MeasurableSpace U] [Fintype U] [MeasurableSingletonClass U] {sem : U → Finset (Fin (N + 1))} {α : ℝ} {n : ℕ} (hα : 0 < α) (hn : n ≤ N) {s : Fin (N + 1)} (h : ∀ (u : U), compatible n ⟨n, ⋯⟩ ⊆ sem u ↔ s ∈ sem u) : (speaker sem α n) (Fin.last N) = (informed sem α) s

When every object has the property the speaker sees it of each object she looks at. If the utterances true at every state this leaves possible are those true at s, she speaks as one who knows the state is s.

theorem GoodmanStuhlmuller2013.speaker_of_isUpperSet {N : ℕ} {U : Type u_1} [MeasurableSpace U] [Fintype U] [MeasurableSingletonClass U] {sem : U → Finset (Fin (N + 1))} {α : ℝ} {n : ℕ} (hα : 0 < α) (hsem : ∀ (u : U), IsUpperSet ↑(sem u)) (hn : n ≤ N) : speaker sem α n = (informed sem α).comp (ProbabilityTheory.hypergeometric N n)

When every meaning is upward closed, as the lower-bounded numerals are, the speaker draws her observation and speaks as one who knows it to be the state, what she has seen being her lower bound.

theorem GoodmanStuhlmuller2013.listener_full_lt {N : ℕ} {U : Type u_1} [MeasurableSpace U] [Fintype U] [MeasurableSingletonClass U] {sem : U → Finset (Fin (N + 1))} {α : ℝ} {u : U} (hα : 0 < α) {s s' : Fin (N + 1)} (hu : s ∈ sem u) (h : {x : U | s ∈ sem x} ⊂ {x : U | s' ∈ sem x}) : ((listener sem α N) u).real {s'} < ((listener sem α N) u).real {s}

With complete access, of two states at which an utterance is true the listener favours the one at which fewer alternatives are true, since the speaker's choice is spread over them.

The alternatives of section 1.1, for three objects

inductive GoodmanStuhlmuller2013.QUtt : Type

The quantifier alternatives none, some, all.

• none_ : QUtt
• some_ : QUtt
• all : QUtt

@[instance_reducible]

instance GoodmanStuhlmuller2013.instDecidableEqQUtt : DecidableEq QUtt

Equations

• GoodmanStuhlmuller2013.instDecidableEqQUtt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance GoodmanStuhlmuller2013.instFintypeQUtt : Fintype QUtt

Equations

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

@[instance_reducible]

instance GoodmanStuhlmuller2013.instMeasurableSpaceQUtt : MeasurableSpace QUtt

Equations

• GoodmanStuhlmuller2013.instMeasurableSpaceQUtt = ⊤

instance GoodmanStuhlmuller2013.instDiscreteMeasurableSpaceQUtt : DiscreteMeasurableSpace QUtt

def GoodmanStuhlmuller2013.QUtt.extension : QUtt → Finset (Fin 4)

The states at which a quantifier holds of the three objects, the row of its tree of numbers.

Equations

• GoodmanStuhlmuller2013.QUtt.none_.extension = Quantifier.NumberTree.no.row 3
• GoodmanStuhlmuller2013.QUtt.some_.extension = Quantifier.NumberTree.some.row 3
• GoodmanStuhlmuller2013.QUtt.all.extension = Quantifier.NumberTree.all.row 3

inductive GoodmanStuhlmuller2013.NumUtt : Type

The numeral alternatives one, two, three.

• one : NumUtt
• two : NumUtt
• three : NumUtt

@[instance_reducible]

instance GoodmanStuhlmuller2013.instDecidableEqNumUtt : DecidableEq NumUtt

Equations

• GoodmanStuhlmuller2013.instDecidableEqNumUtt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance GoodmanStuhlmuller2013.instFintypeNumUtt : Fintype NumUtt

Equations

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

@[instance_reducible]

instance GoodmanStuhlmuller2013.instMeasurableSpaceNumUtt : MeasurableSpace NumUtt

Equations

• GoodmanStuhlmuller2013.instMeasurableSpaceNumUtt = ⊤

instance GoodmanStuhlmuller2013.instDiscreteMeasurableSpaceNumUtt : DiscreteMeasurableSpace NumUtt

def GoodmanStuhlmuller2013.NumUtt.value : NumUtt → ℕ

The number a numeral names.

Equations

• GoodmanStuhlmuller2013.NumUtt.one.value = 1
• GoodmanStuhlmuller2013.NumUtt.two.value = 2
• GoodmanStuhlmuller2013.NumUtt.three.value = 3

def GoodmanStuhlmuller2013.NumUtt.extension (u : NumUtt) : Finset (Fin 4)

The states at which a numeral holds of the three objects on the lower-bounded meaning of [Hor72], its number or more.

Equations

• u.extension = (Quantifier.NumberTree.cardinal (Degree.Comparison.ge.interval u.value)).row 3

theorem GoodmanStuhlmuller2013.NumUtt.mem_extension {u : NumUtt} {s : Fin 4} : s ∈ u.extension ↔ u.value ≤ ↑s

theorem GoodmanStuhlmuller2013.NumUtt.isUpperSet_extension (u : NumUtt) : IsUpperSet ↑u.extension

The predictions of section 1.1, for every rationality

theorem GoodmanStuhlmuller2013.some_full {α : ℝ} (hα : 0 < α) : ((listener QUtt.extension α 3) QUtt.some_).real {3} < ((listener QUtt.extension α 3) QUtt.some_).real {2}

With complete access some is read as some but not all; the state with two objects is more probable than the state with three, where the speaker could have said all.

theorem GoodmanStuhlmuller2013.some_partial {α : ℝ} (hα : 0 < α) {n : ℕ} (hn : n = 1 ∨ n = 2) : ((listener QUtt.extension α n) QUtt.some_).real {2} ≤ ((listener QUtt.extension α n) QUtt.some_).real {3}

With access to one or two objects the implicature is canceled; the state with two objects is no more probable than the state with three, since a speaker who has seen only objects with the property can say nothing stronger than some.

theorem GoodmanStuhlmuller2013.two_full {α : ℝ} (hα : 0 < α) : ((listener NumUtt.extension α 3) NumUtt.two).real {3} < ((listener NumUtt.extension α 3) NumUtt.two).real {2}

With complete access two is read as exactly two; the state with two objects is more probable than the state with three, where the speaker could have said three.

theorem GoodmanStuhlmuller2013.one_full {α : ℝ} (hα : 0 < α) {s : Fin 4} (hs : 1 < s) : ((listener NumUtt.extension α 3) NumUtt.one).real {s} < ((listener NumUtt.extension α 3) NumUtt.one).real {1}

With complete access one is read as exactly one; the state with one object is more probable than a state with more.

theorem GoodmanStuhlmuller2013.one_minimal {α : ℝ} (hα : 0 < α) {s s' : Fin 4} (h : s ≤ s') : ((listener NumUtt.extension α 1) NumUtt.one).real {s} ≤ ((listener NumUtt.extension α 1) NumUtt.one).real {s'}

After one object one carries no implicature; a state with more objects with the property is at least as probable, since the speaker says one exactly when the object she looks at has the property.

theorem GoodmanStuhlmuller2013.two_partial {α : ℝ} (hα : 0 < α) : ((listener NumUtt.extension α 2) NumUtt.two).real {2} ≤ ((listener NumUtt.extension α 2) NumUtt.two).real {3}

After two objects two carries no implicature; the state with two objects is no more probable than the state with three, since the speaker says two only when both objects she looks at have the property.

theorem GoodmanStuhlmuller2013.one_partial_three {α : ℝ} (hα : 0 < α) : ((listener NumUtt.extension α 2) NumUtt.one).real {3} < ((listener NumUtt.extension α 2) NumUtt.one).real {1}

After two objects one keeps its implicature against three; the state with one object is more probable than the state with three, where the speaker saw two objects with the property and would rather have said two.

theorem GoodmanStuhlmuller2013.one_partial_two {α : ℝ} (hα : 0 < α) : ((listener NumUtt.extension α 2) NumUtt.one).real {1} ≤ ((listener NumUtt.extension α 2) NumUtt.one).real {2}

After two objects one loses its implicature against two; the state with one object is no more probable than the state with two, where the speaker may have seen only one object with the property.