Herbstritt and Franke (2019): Complex probability expressions and higher-order uncertainty

This file formalizes the rational speech act model of Herbstritt and Franke for a speaker who has drawn some balls from an urn of ten and tells a listener how likely the next draw is to be red. The speaker's belief of (12) is the posterior over the number of red balls given her observation, belief, the Bayesian inverse of the hypergeometric observation kernel; a simple expression holds at a state by the threshold semantics of (13) and (14), Thresholds.meaning, and the literal listener of (15) conditions the prior on the extension. The speaker of (16) and (17), speaker, is the softmax of the negative Hellinger distance between her belief and the literal listener's, and the pragmatic listener of (18) inverts her against the joint prior over states, observations and accesses, whose marginals are (19) and (20). A complex expression holds at an observation by (23) when the belief it induces gives the inner expression's extension more than the outer threshold, ComplexThresholds.complex.

Because the Hellinger distance is bounded, every message is used with positive probability at every observation (speaker_apply_singleton_ne_zero), where the Kullback–Leibler speaker of Goodman and Stuhlmüller never uses a message whose extension misses a state of positive belief, the paper's probably red after three red balls of four. With complete access the belief is a point mass, so a true message beats a false one, and among true messages the one whose extension carries less prior mass wins, the scalar implicature of the paper's introductory example; the pragmatic listener never rules a state out entirely; and with complete access an outer modifier below one is vacuous.

Implementation notes

• The observation kernel normalizes the hypergeometric weight C(s, o) C(10 − s, a − o) row by row, and the priors over states and accesses are arbitrary measures where the paper fits beta-binomials; the thresholds are parameters, the paper's fitted values (Tables 6 and 9) being prose. The bare copula of Experiment 3 is the simple expression.
• The Kullback–Leibler speaker is stated to make the contrast of the paper's footnote on utilities a theorem; the paper does not run it.

TODO

• The complex utility of (26) and (27) and the complex speaker and listener of (28) and (29).
• The posterior predictive checks and the modal concord reading of might be possible (§6).

References

• [HF19]
• [GS13]
• [FH94]
• [FG12]
• [Zei07]

@[reducible, inline]

abbrev HerbstrittFranke2019.State : Type

A state records how many of the ten balls in the urn are red.

Equations

• HerbstrittFranke2019.State = Fin 11

@[reducible, inline]

abbrev HerbstrittFranke2019.Access : Type

The speaker's access is how many balls she draws.

Equations

• HerbstrittFranke2019.Access = Fin 11

@[reducible, inline]

abbrev HerbstrittFranke2019.Obs : Type

An observation records how many of the drawn balls are red.

Equations

• HerbstrittFranke2019.Obs = Fin 11

noncomputable def HerbstrittFranke2019.proportion (s : State) : ℝ

The probability of drawing a red ball in a state.

Equations

• HerbstrittFranke2019.proportion s = ↑↑s / 10

Belief formation, (12)

noncomputable def HerbstrittFranke2019.obs (a : Access) : ProbabilityTheory.Kernel State Obs

The observation kernel Hypergeometric(o | a, s, 10) gives the number of red balls among a drawn without replacement from ten of which s are red.

Equations

• HerbstrittFranke2019.obs a = ProbabilityTheory.hypergeometric 10 ↑a

instance HerbstrittFranke2019.instIsFiniteKernelStateObsObs (a : Access) : ProbabilityTheory.IsFiniteKernel (obs a)

theorem HerbstrittFranke2019.obs_apply_singleton_ne_zero_iff (a : Access) (s : State) (o : Obs) : ((obs a) s) {o} ≠ 0 ↔ ProbabilityTheory.hypergeometricCount 10 ↑s ↑a ↑o ≠ 0

An observation is possible at a state exactly when some draw yields it.

noncomputable def HerbstrittFranke2019.belief (P : MeasureTheory.Measure State) [MeasureTheory.IsFiniteMeasure P] (a : Access) : ProbabilityTheory.Kernel Obs State

The speaker's rational belief of (12) is the posterior over states given an observation at an access, against the prior.

Equations

• HerbstrittFranke2019.belief P a = ProbabilityTheory.posterior (HerbstrittFranke2019.obs a) P

instance HerbstrittFranke2019.instIsMarkovKernelObsStateBelief (P : MeasureTheory.Measure State) [MeasureTheory.IsFiniteMeasure P] (a : Access) : ProbabilityTheory.IsMarkovKernel (belief P a)

theorem HerbstrittFranke2019.belief_apply_singleton_ne_zero (P : MeasureTheory.Measure State) [MeasureTheory.IsFiniteMeasure P] {a : Access} {o : Obs} {s : State} (hP : P {s} ≠ 0) (h : ProbabilityTheory.hypergeometricCount 10 ↑s ↑a ↑o ≠ 0) : ((belief P a) o) {s} ≠ 0

A state of positive prior at which the observation is possible keeps positive belief.

theorem HerbstrittFranke2019.belief_full (P : MeasureTheory.Measure State) [MeasureTheory.IsFiniteMeasure P] {o : Obs} (hP : P {o} ≠ 0) : (belief P 10) o = MeasureTheory.Measure.dirac o

With complete access the belief is the point mass at the observed state.

Simple expressions, (13) to (15)

inductive HerbstrittFranke2019.SimpleExpr : Type

The five simple expressions of Experiment 2.

• certainlyNot : SimpleExpr
• probablyNot : SimpleExpr
• possibly : SimpleExpr
• probably : SimpleExpr
• certainly : SimpleExpr

@[instance_reducible]

instance HerbstrittFranke2019.instDecidableEqSimpleExpr : DecidableEq SimpleExpr

Equations

• HerbstrittFranke2019.instDecidableEqSimpleExpr x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HerbstrittFranke2019.instFintypeSimpleExpr : Fintype SimpleExpr

Equations

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

instance HerbstrittFranke2019.instNonemptySimpleExpr : Nonempty SimpleExpr

@[instance_reducible]

instance HerbstrittFranke2019.instMeasurableSpaceSimpleExpr : MeasurableSpace SimpleExpr

Equations

• HerbstrittFranke2019.instMeasurableSpaceSimpleExpr = ⊤

structure HerbstrittFranke2019.Thresholds : Type

The semantic thresholds of the three uncertainty expressions, free parameters of the model.

• certainly : ℝ

  The threshold of certainly.

• probably : ℝ

  The threshold of probably.

• possibly : ℝ

  The threshold of possibly.

def HerbstrittFranke2019.Thresholds.meaning (θ : Thresholds) : SimpleExpr → State → Prop

Under the threshold semantics of (13) and (14), a positive expression holds where the proportion of red balls exceeds its threshold, and a negated one where the proportion falls below one less the threshold.

Equations

• θ.meaning HerbstrittFranke2019.SimpleExpr.certainly x✝ = (θ.certainly < HerbstrittFranke2019.proportion x✝)
• θ.meaning HerbstrittFranke2019.SimpleExpr.probably x✝ = (θ.probably < HerbstrittFranke2019.proportion x✝)
• θ.meaning HerbstrittFranke2019.SimpleExpr.possibly x✝ = (θ.possibly < HerbstrittFranke2019.proportion x✝)
• θ.meaning HerbstrittFranke2019.SimpleExpr.probablyNot x✝ = (HerbstrittFranke2019.proportion x✝ < 1 - θ.probably)
• θ.meaning HerbstrittFranke2019.SimpleExpr.certainlyNot x✝ = (HerbstrittFranke2019.proportion x✝ < 1 - θ.certainly)

def HerbstrittFranke2019.Thresholds.ext (θ : Thresholds) (m : SimpleExpr) : Set State

The extension of a simple expression.

Equations

• θ.ext m = {s : HerbstrittFranke2019.State | θ.meaning m s}

theorem HerbstrittFranke2019.Thresholds.ext_certainly_subset (θ : Thresholds) (h : θ.probably ≤ θ.certainly) : θ.ext SimpleExpr.certainly ⊆ θ.ext SimpleExpr.probably

Certainly entails probably when its threshold is the higher.

theorem HerbstrittFranke2019.Thresholds.ext_probably_subset (θ : Thresholds) (h : θ.possibly ≤ θ.probably) : θ.ext SimpleExpr.probably ⊆ θ.ext SimpleExpr.possibly

Probably entails possibly when its threshold is the higher.

theorem HerbstrittFranke2019.Thresholds.ext_certainlyNot_subset (θ : Thresholds) (h : θ.probably ≤ θ.certainly) : θ.ext SimpleExpr.certainlyNot ⊆ θ.ext SimpleExpr.probablyNot

Certainly not entails probably not when the threshold of certainly is the higher.

noncomputable def HerbstrittFranke2019.L0 (θ : Thresholds) (P : MeasureTheory.Measure State) : ProbabilityTheory.Kernel SimpleExpr State

The literal listener of (15) conditions the prior on the expression's extension.

Equations

• HerbstrittFranke2019.L0 θ P = RSA.listener P (RSA.truthful θ.ext)

instance HerbstrittFranke2019.instIsFiniteKernelSimpleExprStateL0 (θ : Thresholds) (P : MeasureTheory.Measure State) : ProbabilityTheory.IsFiniteKernel (L0 θ P)

theorem HerbstrittFranke2019.L0_apply_singleton_of_notMem (θ : Thresholds) (P : MeasureTheory.Measure State) {m : SimpleExpr} {s : State} (h : s ∉ θ.ext m) : ((L0 θ P) m) {s} = 0

theorem HerbstrittFranke2019.L0_apply_singleton_of_mem (θ : Thresholds) (P : MeasureTheory.Measure State) {m : SimpleExpr} {s : State} (h : s ∈ θ.ext m) : ((L0 θ P) m) {s} = (P (θ.ext m))⁻¹ * P {s}

theorem HerbstrittFranke2019.L0_real_of_notMem (θ : Thresholds) (P : MeasureTheory.Measure State) {m : SimpleExpr} {s : State} (h : s ∉ θ.ext m) : ((L0 θ P) m).real {s} = 0

theorem HerbstrittFranke2019.L0_real_of_mem (θ : Thresholds) (P : MeasureTheory.Measure State) {m : SimpleExpr} {s : State} (h : s ∈ θ.ext m) : ((L0 θ P) m).real {s} = P.real {s} / P.real (θ.ext m)

The speaker, (16) and (17)

noncomputable def HerbstrittFranke2019.utility (θ : Thresholds) (P : MeasureTheory.Measure State) [MeasureTheory.IsFiniteMeasure P] (x : Obs × Access) (m : SimpleExpr) : ℝ

The expected utility of (16) is the negative Hellinger distance between the speaker's belief after her observation and the literal listener's belief after the message.

Equations

• HerbstrittFranke2019.utility θ P x m = -InformationTheory.hellingerDist ((HerbstrittFranke2019.belief P x.2) x.1) ((HerbstrittFranke2019.L0 θ P) m)

noncomputable def HerbstrittFranke2019.speaker (lam : ℝ) (θ : Thresholds) (P : MeasureTheory.Measure State) [MeasureTheory.IsFiniteMeasure P] : ProbabilityTheory.Kernel (Obs × Access) SimpleExpr

The speaker of (17) is the softmax of the utility at the rationality lam.

Equations

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

theorem HerbstrittFranke2019.speaker_apply_singleton_ne_zero (lam : ℝ) (θ : Thresholds) (P : MeasureTheory.Measure State) [MeasureTheory.IsFiniteMeasure P] (x : Obs × Access) (m : SimpleExpr) : ((speaker lam θ P) x) {m} ≠ 0

The Hellinger utility is finite, so every message is used with positive probability at every observation, and pragmatically true-enough messages can be sent.

instance HerbstrittFranke2019.instIsMarkovKernelProdObsAccessSimpleExprSpeaker (lam : ℝ) (θ : Thresholds) (P : MeasureTheory.Measure State) [MeasureTheory.IsFiniteMeasure P] : ProbabilityTheory.IsMarkovKernel (speaker lam θ P)

theorem HerbstrittFranke2019.speaker_real_lt_iff (lam : ℝ) (θ : Thresholds) (P : MeasureTheory.Measure State) [MeasureTheory.IsFiniteMeasure P] (hlam : 0 < lam) (x : Obs × Access) (m m' : SimpleExpr) : ((speaker lam θ P) x).real {m} < ((speaker lam θ P) x).real {m'} ↔ InformationTheory.hellingerDist ((belief P x.2) x.1) ((L0 θ P) m') < InformationTheory.hellingerDist ((belief P x.2) x.1) ((L0 θ P) m)

The speaker prefers the message whose literal listener lies closer to her belief.

noncomputable def HerbstrittFranke2019.klSpeaker (lam : ℝ) (θ : Thresholds) (P : MeasureTheory.Measure State) [MeasureTheory.IsFiniteMeasure P] : ProbabilityTheory.Kernel (Obs × Access) SimpleExpr

The speaker of [GS13], with the Kullback–Leibler divergence in place of the Hellinger distance (the paper's footnote on utilities).

Equations

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

theorem HerbstrittFranke2019.klSpeaker_probably_eq_zero (lam : ℝ) (θ : Thresholds) (P : MeasureTheory.Measure State) [MeasureTheory.IsFiniteMeasure P] (hlam : 0 < lam) (hθ : 3 / 10 ≤ θ.probably) (hP : P {3} ≠ 0) : ((klSpeaker lam θ P) (3, 4)) {SimpleExpr.probably} = 0

In the paper's example, after three red balls of four, probably excludes a state of three red balls that keeps positive belief, so the Kullback–Leibler speaker never says it.

Complete access: informativity from the Hellinger distance

theorem HerbstrittFranke2019.utility_full (θ : Thresholds) (P : MeasureTheory.Measure State) [MeasureTheory.IsFiniteMeasure P] {s : State} (hP : P {s} ≠ 0) (m : SimpleExpr) : utility θ P (s, 10) m = -√(1 - √(((L0 θ P) m).real {s}))

With complete access the utility of a message is minus the Hellinger distance of the point mass at the state from the literal listener.

theorem HerbstrittFranke2019.utility_full_of_notMem (θ : Thresholds) (P : MeasureTheory.Measure State) [MeasureTheory.IsFiniteMeasure P] {s : State} (hP : P {s} ≠ 0) {m : SimpleExpr} (h : s ∉ θ.ext m) : utility θ P (s, 10) m = -1

A false message has the worst utility, minus one.

theorem HerbstrittFranke2019.speaker_full_lt_of_notMem_of_mem {lam : ℝ} (θ : Thresholds) (P : MeasureTheory.Measure State) [MeasureTheory.IsFiniteMeasure P] {s : State} (hlam : 0 < lam) (hP : P {s} ≠ 0) {m m' : SimpleExpr} (h : s ∉ θ.ext m) (h' : s ∈ θ.ext m') : ((speaker lam θ P) (s, 10)).real {m} < ((speaker lam θ P) (s, 10)).real {m'}

With complete access a true message beats a false one.

theorem HerbstrittFranke2019.speaker_full_lt_iff_of_mem {lam : ℝ} (θ : Thresholds) (P : MeasureTheory.Measure State) [MeasureTheory.IsFiniteMeasure P] {s : State} (hlam : 0 < lam) (hP : P {s} ≠ 0) {m m' : SimpleExpr} (h : s ∈ θ.ext m) (h' : s ∈ θ.ext m') : ((speaker lam θ P) (s, 10)).real {m} < ((speaker lam θ P) (s, 10)).real {m'} ↔ P.real (θ.ext m') < P.real (θ.ext m)

With complete access, among true messages the one whose extension carries less prior mass, the more informative one, is preferred.

theorem HerbstrittFranke2019.speaker_full_lt_of_ssubset {lam : ℝ} (θ : Thresholds) (P : MeasureTheory.Measure State) [MeasureTheory.IsFiniteMeasure P] {s : State} (hlam : 0 < lam) (hP : ∀ (s : State), P {s} ≠ 0) {m m' : SimpleExpr} (hsub : θ.ext m ⊂ θ.ext m') (h : s ∈ θ.ext m) : ((speaker lam θ P) (s, 10)).real {m'} < ((speaker lam θ P) (s, 10)).real {m}

With complete access and a prior positive on every state, a message strictly entailing another is preferred to it whenever both are true, the scalar implicature of the introductory example.

The pragmatic listener, (18) to (20)

noncomputable def HerbstrittFranke2019.joint (P : MeasureTheory.Measure State) (A : MeasureTheory.Measure Access) : MeasureTheory.Measure (State × Obs × Access)

The joint prior of (18) over states, observations and accesses combines the state prior, the access prior, and the observation given both.

Equations

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

theorem HerbstrittFranke2019.joint_apply_singleton (P : MeasureTheory.Measure State) (A : MeasureTheory.Measure Access) (x : State × Obs × Access) : (joint P A) {x} = P {x.1} * A {x.2.2} * ((obs x.2.2) x.1) {x.2.1}

instance HerbstrittFranke2019.instIsFiniteMeasureProdStateObsAccessJoint (P : MeasureTheory.Measure State) (A : MeasureTheory.Measure Access) [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsFiniteMeasure A] : MeasureTheory.IsFiniteMeasure (joint P A)

noncomputable def HerbstrittFranke2019.jointSpeaker (lam : ℝ) (θ : Thresholds) (P : MeasureTheory.Measure State) [MeasureTheory.IsFiniteMeasure P] : ProbabilityTheory.Kernel (State × Obs × Access) SimpleExpr

As the listener models the speaker, her choice depends on the observation and the access alone.

Equations

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

instance HerbstrittFranke2019.instIsMarkovKernelProdStateObsAccessSimpleExprJointSpeaker (lam : ℝ) (θ : Thresholds) (P : MeasureTheory.Measure State) [MeasureTheory.IsFiniteMeasure P] : ProbabilityTheory.IsMarkovKernel (jointSpeaker lam θ P)

noncomputable def HerbstrittFranke2019.listener (lam : ℝ) (θ : Thresholds) (P : MeasureTheory.Measure State) (A : MeasureTheory.Measure Access) [MeasureTheory.IsFiniteMeasure P] : ProbabilityTheory.Kernel SimpleExpr (State × Obs × Access)

The pragmatic listener of (18) inverts the speaker against the joint prior; its first marginal is the state listener of (19), its second the observation listener of (20).

Equations

• HerbstrittFranke2019.listener lam θ P A = RSA.listener (HerbstrittFranke2019.joint P A) ⇑(HerbstrittFranke2019.jointSpeaker lam θ P)

theorem HerbstrittFranke2019.listener_fst_apply_singleton_ne_zero (lam : ℝ) (θ : Thresholds) (P : MeasureTheory.Measure State) (A : MeasureTheory.Measure Access) [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsFiniteMeasure A] {s : State} (hP : P {s} ≠ 0) (hA : A {0} ≠ 0) (m : SimpleExpr) : ((listener lam θ P A) m).fst {s} ≠ 0

No message rules out a state. A state of positive prior keeps positive posterior whenever drawing nothing has positive prior, since the speaker who drew nothing may send any message.

Complex expressions, (22) to (25)

inductive HerbstrittFranke2019.Inner : Type

The inner expressions of Experiment 3.

• likely : Inner
• possible : Inner
• unlikely : Inner

@[instance_reducible]

instance HerbstrittFranke2019.instDecidableEqInner : DecidableEq Inner

Equations

• HerbstrittFranke2019.instDecidableEqInner x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HerbstrittFranke2019.instFintypeInner : Fintype Inner

Equations

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

@[instance_reducible]

instance HerbstrittFranke2019.instMeasurableSpaceInner : MeasurableSpace Inner

Equations

• HerbstrittFranke2019.instMeasurableSpaceInner = ⊤

inductive HerbstrittFranke2019.Outer : Type

The outer modifiers of Experiment 3; the bare copula is the simple expression.

• certainly : Outer
• probably : Outer
• might : Outer

@[instance_reducible]

instance HerbstrittFranke2019.instDecidableEqOuter : DecidableEq Outer

Equations

• HerbstrittFranke2019.instDecidableEqOuter x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HerbstrittFranke2019.instFintypeOuter : Fintype Outer

Equations

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

@[instance_reducible]

instance HerbstrittFranke2019.instMeasurableSpaceOuter : MeasurableSpace Outer

Equations

• HerbstrittFranke2019.instMeasurableSpaceOuter = ⊤

structure HerbstrittFranke2019.ComplexThresholds : Type

The semantic thresholds of Experiment 3's inner and outer expressions.

• likely : ℝ

  The threshold of the inner likely.

• possible : ℝ

  The threshold of the inner possible.

• certainly : ℝ

  The threshold of the outer certainly.

• probably : ℝ

  The threshold of the outer probably.

• might : ℝ

  The threshold of the outer might.

def HerbstrittFranke2019.ComplexThresholds.inner (θ : ComplexThresholds) : Inner → State → Prop

The threshold semantics of the inner expressions (22), unlikely the negation of likely.

Equations

• θ.inner HerbstrittFranke2019.Inner.likely x✝ = (θ.likely < HerbstrittFranke2019.proportion x✝)
• θ.inner HerbstrittFranke2019.Inner.possible x✝ = (θ.possible < HerbstrittFranke2019.proportion x✝)
• θ.inner HerbstrittFranke2019.Inner.unlikely x✝ = (HerbstrittFranke2019.proportion x✝ < 1 - θ.likely)

def HerbstrittFranke2019.ComplexThresholds.outer (θ : ComplexThresholds) : Outer → ℝ

The threshold of an outer modifier.

Equations

• θ.outer HerbstrittFranke2019.Outer.certainly = θ.certainly
• θ.outer HerbstrittFranke2019.Outer.probably = θ.probably
• θ.outer HerbstrittFranke2019.Outer.might = θ.might

def HerbstrittFranke2019.ComplexThresholds.innerExt (θ : ComplexThresholds) (X : Inner) : Set State

The extension of an inner expression.

Equations

• θ.innerExt X = {s : HerbstrittFranke2019.State | θ.inner X s}

def HerbstrittFranke2019.ComplexThresholds.complex (θ : ComplexThresholds) (P : MeasureTheory.Measure State) [MeasureTheory.IsFiniteMeasure P] (Y : Outer) (X : Inner) : Set (Obs × Access)

Under the compositional semantics of (23), a complex expression holds at an observation exactly when the belief it induces gives the inner expression's extension more than the outer threshold.

Equations

• θ.complex P Y X = {x : HerbstrittFranke2019.Obs × HerbstrittFranke2019.Access | θ.outer Y < ((HerbstrittFranke2019.belief P x.2) x.1).real (θ.innerExt X)}

theorem HerbstrittFranke2019.ComplexThresholds.mem_complex_full (θ : ComplexThresholds) (P : MeasureTheory.Measure State) [MeasureTheory.IsFiniteMeasure P] {s : State} (hP : P {s} ≠ 0) {Y : Outer} (h0 : 0 ≤ θ.outer Y) (X : Inner) : (s, 10) ∈ θ.complex P Y X ↔ s ∈ θ.innerExt X ∧ θ.outer Y < 1

With complete access the belief is a point mass, so an outer modifier of threshold below one is vacuous and the complex expression holds exactly where the inner one does.

noncomputable def HerbstrittFranke2019.ComplexThresholds.complexL0 (θ : ComplexThresholds) (P : MeasureTheory.Measure State) [MeasureTheory.IsFiniteMeasure P] (A : MeasureTheory.Measure Access) [MeasureTheory.IsFiniteMeasure A] : ProbabilityTheory.Kernel (Outer × Inner) (Obs × Access)

The literal listener for complex expressions of (25) conditions the observation prior of (24), the marginal of the joint prior, on the expression's extension.

Equations

• θ.complexL0 P A = RSA.listener (HerbstrittFranke2019.joint P A).snd (RSA.truthful fun (m : HerbstrittFranke2019.Outer × HerbstrittFranke2019.Inner) => θ.complex P m.1 m.2)