[QF15]

[FG12] [Gri75] [DR95]

Variations on a Bayesian theme: comparing Bayesian models of referential reasoning. In Bayesian Natural Language Semantics and Pragmatics, 91–117.

One referential game (green square, green circle, blue circle; Fig. 1) and a family of models decomposed along three design dimensions: the speaker's goal (belief-oriented log-informativity, eq. 10, vs action-oriented raw informativity, eq. 9), the speaker's belief about the literal listener (uniform vs salience prior), and the listener's own prior (eqs. 12–13). Utterance cost is a constant c on adjectives (eq. 11), marginalized over (−0.4, 0.4) in the paper's model comparison.

Main results

The belief-oriented chain is stated parametrically in the cost factor k = exp(−c) (k < 1 ↔ a noun preference c > 0), so each prediction carries its exact validity region:

• speaker_prefers_unique_shape (k < 2) / speaker_prefers_unique_color (k > 1/2, i.e. c < ln 2) / cost_breaks_symmetry (k < 1) / no_cost_symmetry (k = 1): σ_bU matches all three Table-1 directions on the whole noun-preference regime 1/2 < k < 1 (σ_bU_matches_speaker_data).
• salience_reversal_circle / salience_reversal_green: at every k > 0, the uniform-prior listener follows pragmatic narrowing while the salience-prior listener follows salience — the reversals are pure prior effects, needing no cost regime at all.
• σ_bS_blue_circ_iff (k vs 139/169) / σ_bS_green_circ_iff (k vs 101/169): the salience-belief speaker's predictions flip inside the paper's cost support — thresholds, not directions, are that model's content.
• σ_aU_blue_circ_threshold (c < 1/2) vs σ_bU_blue_circ_threshold (c < ln 2): the goal dimension shifts the blue-circle boundary; the σ_aU tie at c = 1/2 is the boundary case.
• beliefGoal_gt_iff / actionGoal_gt_iff: speaker rankings are λ-independent — the paper's rejection of λ = 1 affects fit, not direction.
• speakerData_matches_model / listenerData_circle_matches_salience / listenerData_green_matches_pragmatic: Tables 1–2, with "green" following the pragmatic direction against salience (p. 212).
• zeroCost_beliefGoal_eq: at zero cost the belief-oriented score is [FG12]'s scoring rule.
• cost_is_q2: the cost dimension is [Gri75]'s Q2 sub-maxim, in [DR95]'s No-Brevity reading at strength 0.

Implementation notes

At λ = 1 the belief-oriented weight is L0 · k, so the chain is rational in k and every prediction is symbolic algebra over PMF.normalizeOrUniform — no transcendental atoms; c re-enters only through the threshold identities (k = 1/2 ↔ c = ln 2).

inductive QingFranke2015.Object : Type

The three objects in the reference game context (Fig. 1): unique shape, unique color, and both features shared.

• green_square : Object
• blue_circle : Object
• green_circle : Object

@[implicit_reducible]

instance QingFranke2015.instDecidableEqObject : DecidableEq Object

Equations

• QingFranke2015.instDecidableEqObject x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance QingFranke2015.instReprObject : Repr Object

Equations

• QingFranke2015.instReprObject = { reprPrec := QingFranke2015.instReprObject.repr }

def QingFranke2015.instReprObject.repr : Object → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance QingFranke2015.instInhabitedObject : Inhabited Object

Equations

• QingFranke2015.instInhabitedObject = { default := QingFranke2015.instInhabitedObject.default }

@[implicit_reducible]

instance QingFranke2015.instFintypeObject : Fintype Object

Equations

• QingFranke2015.instFintypeObject = { elems := { val := ↑QingFranke2015.Object.enumList, nodup := QingFranke2015.Object.enumList_nodup }, complete := QingFranke2015.instFintypeObject._proof_1 }

instance QingFranke2015.instNonemptyObject : Nonempty Object

inductive QingFranke2015.Utterance : Type

The four single-word utterances (feature predicates).

• square : Utterance
• circle : Utterance
• green : Utterance
• blue : Utterance

@[implicit_reducible]

instance QingFranke2015.instDecidableEqUtterance : DecidableEq Utterance

Equations

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

@[implicit_reducible]

instance QingFranke2015.instReprUtterance : Repr Utterance

Equations

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

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

Equations

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

@[implicit_reducible]

instance QingFranke2015.instInhabitedUtterance : Inhabited Utterance

Equations

• QingFranke2015.instInhabitedUtterance = { default := QingFranke2015.instInhabitedUtterance.default }

@[implicit_reducible]

instance QingFranke2015.instFintypeUtterance : Fintype Utterance

Equations

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

instance QingFranke2015.instNonemptyUtterance : Nonempty Utterance

def QingFranke2015.Utterance.appliesTo : Utterance → Object → Bool

Boolean semantics ⟦utterance⟧(object) (Fig. 1b).

Equations

• QingFranke2015.Utterance.square.appliesTo QingFranke2015.Object.green_square = true
• QingFranke2015.Utterance.circle.appliesTo QingFranke2015.Object.blue_circle = true
• QingFranke2015.Utterance.circle.appliesTo QingFranke2015.Object.green_circle = true
• QingFranke2015.Utterance.green.appliesTo QingFranke2015.Object.green_square = true
• QingFranke2015.Utterance.green.appliesTo QingFranke2015.Object.green_circle = true
• QingFranke2015.Utterance.blue.appliesTo QingFranke2015.Object.blue_circle = true
• x✝¹.appliesTo x✝ = false

theorem QingFranke2015.extension_characterization (w : Object) : (Utterance.square.appliesTo w = true ↔ w = Object.green_square) ∧ (Utterance.blue.appliesTo w = true ↔ w = Object.blue_circle) ∧ (Utterance.circle.appliesTo w = true ↔ w ≠ Object.green_square) ∧ (Utterance.green.appliesTo w = true ↔ w ≠ Object.blue_circle)

"square" and "blue" each denote a single object; "circle" and "green" are two-ways ambiguous.

Empirical data (Tables 1–2)

def QingFranke2015.speakerData : Object → Utterance → ℕ

Speaker production data (Table 1, N = 144 per target).

Equations

• QingFranke2015.speakerData QingFranke2015.Object.green_square QingFranke2015.Utterance.square = 135
• QingFranke2015.speakerData QingFranke2015.Object.green_square QingFranke2015.Utterance.green = 9
• QingFranke2015.speakerData QingFranke2015.Object.blue_circle QingFranke2015.Utterance.blue = 119
• QingFranke2015.speakerData QingFranke2015.Object.blue_circle QingFranke2015.Utterance.circle = 25
• QingFranke2015.speakerData QingFranke2015.Object.green_circle QingFranke2015.Utterance.circle = 81
• QingFranke2015.speakerData QingFranke2015.Object.green_circle QingFranke2015.Utterance.green = 63
• QingFranke2015.speakerData x✝¹ x✝ = 0

def QingFranke2015.listenerData : Utterance → Object → ℕ

Listener comprehension data (Table 2, N = 180 per ambiguous utterance).

Equations

• QingFranke2015.listenerData QingFranke2015.Utterance.circle QingFranke2015.Object.blue_circle = 117
• QingFranke2015.listenerData QingFranke2015.Utterance.circle QingFranke2015.Object.green_circle = 62
• QingFranke2015.listenerData QingFranke2015.Utterance.circle QingFranke2015.Object.green_square = 1
• QingFranke2015.listenerData QingFranke2015.Utterance.green QingFranke2015.Object.green_square = 65
• QingFranke2015.listenerData QingFranke2015.Utterance.green QingFranke2015.Object.green_circle = 115
• QingFranke2015.listenerData x✝¹ x✝ = 0

def QingFranke2015.saliencePrior : Object → ℝ

Salience prior: the salience condition of Table 2 (N = 240), the paper's empirical estimate of S(t).

Equations

• QingFranke2015.saliencePrior QingFranke2015.Object.green_square = 71
• QingFranke2015.saliencePrior QingFranke2015.Object.blue_circle = 139
• QingFranke2015.saliencePrior QingFranke2015.Object.green_circle = 30

def QingFranke2015.uniformPrior : Object → ℝ

Uniform prior.

Equations

• QingFranke2015.uniformPrior x✝ = 1

theorem QingFranke2015.speakerData_consistent : speakerData Object.green_square Utterance.square + speakerData Object.green_square Utterance.green = 144 ∧ speakerData Object.blue_circle Utterance.blue + speakerData Object.blue_circle Utterance.circle = 144 ∧ speakerData Object.green_circle Utterance.circle + speakerData Object.green_circle Utterance.green = 144

Speaker data sums to N = 144 per target.

theorem QingFranke2015.listenerData_consistent : listenerData Utterance.circle Object.blue_circle + listenerData Utterance.circle Object.green_circle + listenerData Utterance.circle Object.green_square = 180 ∧ listenerData Utterance.green Object.green_square + listenerData Utterance.green Object.green_circle = 180

Listener data sums to N = 180 per ambiguous utterance.

Speaker goal types

The goal dimension (eqs. 9–10), generic in the literal listener and λ.

noncomputable def QingFranke2015.adjCost (c : ℝ) : Utterance → ℝ

Adjective cost (eq. 11): shape words cost 0, color words cost c.

Equations

• QingFranke2015.adjCost c QingFranke2015.Utterance.square = 0
• QingFranke2015.adjCost c QingFranke2015.Utterance.circle = 0
• QingFranke2015.adjCost c QingFranke2015.Utterance.green = c
• QingFranke2015.adjCost c QingFranke2015.Utterance.blue = c

noncomputable def QingFranke2015.beliefGoalScore (cost : Utterance → ℝ) (l0 : Utterance → Object → ℝ) (α : ℝ) (w : Object) (u : Utterance) : ℝ

Belief-oriented S1 score (eq. 10): exp (λ (log L0 − Cost)), gated at false utterances (Lean's log 0 = 0 would otherwise leak mass).

Equations

• QingFranke2015.beliefGoalScore cost l0 α w u = if l0 u w = 0 then 0 else Real.exp (α * (Real.log (l0 u w) - cost u))

noncomputable def QingFranke2015.actionGoalScore (cost : Utterance → ℝ) (l0 : Utterance → Object → ℝ) (α : ℝ) (w : Object) (u : Utterance) : ℝ

Action-oriented S1 score (eq. 9): exp (λ (L0 − Cost)) — positive even on false utterances (the paper's fn. 7 restricts comparisons to truthful ones).

Equations

• QingFranke2015.actionGoalScore cost l0 α w u = Real.exp (α * (l0 u w - cost u))

theorem QingFranke2015.beliefGoal_gt_iff (cost : Utterance → ℝ) (l0 : Utterance → Object → ℝ) (u₁ u₂ : Utterance) (w : Object) {α : ℝ} (hα : 0 < α) (h1 : l0 u₁ w ≠ 0) (h2 : l0 u₂ w ≠ 0) : beliefGoalScore cost l0 α w u₁ > beliefGoalScore cost l0 α w u₂ ↔ Real.log (l0 u₁ w) - cost u₁ > Real.log (l0 u₂ w) - cost u₂

Belief-oriented ranking is λ-independent: it compares log L0 − cost.

theorem QingFranke2015.actionGoal_gt_iff (cost : Utterance → ℝ) (l0 : Utterance → Object → ℝ) (u₁ u₂ : Utterance) (w : Object) {α : ℝ} (hα : 0 < α) : actionGoalScore cost l0 α w u₁ > actionGoalScore cost l0 α w u₂ ↔ l0 u₁ w - cost u₁ > l0 u₂ w - cost u₂

Action-oriented ranking is λ-independent: it compares L0 − cost.

The belief-oriented chain, parametric in the cost factor

At λ = 1, exp (log L0 − c) = L0 · exp (−c), so the whole σ_b chain is rational in the cost factor k = exp (−c): k = 1 is zero cost, k < 1 a noun preference, and thresholds in k translate back to cost bounds (k > 1/2 ↔ c < ln 2).

def QingFranke2015.cf (k : ℝ) : Utterance → ℝ

Multiplicative cost factor: 1 on shape words, k on color words.

Equations

• QingFranke2015.cf k QingFranke2015.Utterance.square = 1
• QingFranke2015.cf k QingFranke2015.Utterance.circle = 1
• QingFranke2015.cf k QingFranke2015.Utterance.green = k
• QingFranke2015.cf k QingFranke2015.Utterance.blue = k

noncomputable def QingFranke2015.l0 (p : Object → ℝ) (u : Utterance) (w : Object) : ℝ

Literal listener at prior p (eq. 1): prior conditioned on the extension.

Equations

• QingFranke2015.l0 p u w = (if u.appliesTo w = true then p w else 0) / ∑ w' : QingFranke2015.Object, if u.appliesTo w' = true then p w' else 0

noncomputable def QingFranke2015.sbScore (p : Object → ℝ) (k : ℝ) (w : Object) (u : Utterance) : ℝ

Belief-oriented speaker weight at λ = 1: L0 · k^cost.

Equations

• QingFranke2015.sbScore p k w u = QingFranke2015.l0 p u w * QingFranke2015.cf k u

noncomputable def QingFranke2015.s1 (p : Object → ℝ) (k : ℝ) (w : Object) : PMF Utterance

Belief-oriented speaker (eq. 10).

Equations

• QingFranke2015.s1 p k w = PMF.normalizeOrUniform fun (u : QingFranke2015.Utterance) => ENNReal.ofReal (QingFranke2015.sbScore p k w u)

noncomputable def QingFranke2015.l1Score (prior : Object → ℝ) (k : ℝ) (u : Utterance) (w : Object) : ℝ

Pragmatic-listener score (eqs. 12–13): the listener's own prior times the σ_bU speaker (the paper's best-supported speaker model).

Equations

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

noncomputable def QingFranke2015.l1 (prior : Object → ℝ) (k : ℝ) (u : Utterance) : PMF Object

Pragmatic listener (eq. 6).

Equations

• QingFranke2015.l1 prior k u = PMF.normalizeOrUniform fun (w : QingFranke2015.Object) => ENNReal.ofReal (QingFranke2015.l1Score prior k u w)

Speaker predictions (Table 1 directions)

theorem QingFranke2015.speaker_prefers_unique_shape {k : ℝ} (hk : 0 ≤ k) (hk2 : k < 2) : (s1 uniformPrior k Object.green_square) Utterance.green < (s1 uniformPrior k Object.green_square) Utterance.square

For the green square, σ_bU prefers the unique "square" over the ambiguous "green" at every cost factor k < 2 (135/144 speakers, Table 1).

theorem QingFranke2015.speaker_prefers_unique_color {k : ℝ} (hk : 1 / 2 < k) : (s1 uniformPrior k Object.blue_circle) Utterance.circle < (s1 uniformPrior k Object.blue_circle) Utterance.blue

For the blue circle, σ_bU prefers the unique "blue" over "circle" once the cost factor exceeds 1/2 (c < ln 2); 119/144 speakers chose "blue".

theorem QingFranke2015.cost_breaks_symmetry {k : ℝ} (hk : 0 < k) (hk1 : k < 1) : (s1 uniformPrior k Object.green_circle) Utterance.green < (s1 uniformPrior k Object.green_circle) Utterance.circle

For the green circle, cost is the tiebreaker: any noun preference (k < 1) favors "circle" over "green" (81 vs 63, Table 1, n.s.).

theorem QingFranke2015.no_cost_symmetry : sbScore uniformPrior 1 Object.green_circle Utterance.circle = sbScore uniformPrior 1 Object.green_circle Utterance.green

Without cost (k = 1) the green-circle tie is unbroken: Q1 alone cannot distinguish two equally informative words.

theorem QingFranke2015.σ_bU_matches_speaker_data {k : ℝ} (hk : 1 / 2 < k) (hk1 : k < 1) : (s1 uniformPrior k Object.green_square) Utterance.green < (s1 uniformPrior k Object.green_square) Utterance.square ∧ (s1 uniformPrior k Object.blue_circle) Utterance.circle < (s1 uniformPrior k Object.blue_circle) Utterance.blue ∧ (s1 uniformPrior k Object.green_circle) Utterance.green < (s1 uniformPrior k Object.green_circle) Utterance.circle

σ_bU with any noun preference in (1/2, 1) — covering the paper's whole positive-cost support c ∈ (0, 0.4] — matches all three Table-1 majority directions.

Listener predictions: the salience reversal (Tables 2 and 4)

Both listeners embed the same σ_bU speaker and differ only in their prior (eqs. 12–13). The reversals hold at every k > 0: they are pure prior effects, independent of the cost regime.

theorem QingFranke2015.uniform_circle_green_circ {k : ℝ} (hk : 0 < k) : (l1 uniformPrior k Utterance.circle) Object.blue_circle < (l1 uniformPrior k Utterance.circle) Object.green_circle

Uniform-prior listener, "circle": pragmatic narrowing favors the green circle (a blue-circle speaker had "blue"), at every k > 0.

theorem QingFranke2015.salience_circle_blue_circ {k : ℝ} (hk : 0 < k) : (l1 saliencePrior k Utterance.circle) Object.green_circle < (l1 saliencePrior k Utterance.circle) Object.blue_circle

Salience-prior listener, "circle": salience (139 vs 30) overrides the pragmatic direction, at every k > 0. Matches Table 2 (117/180 blue).

theorem QingFranke2015.salience_reversal_circle {k : ℝ} (hk : 0 < k) : (l1 uniformPrior k Utterance.circle) Object.blue_circle < (l1 uniformPrior k Utterance.circle) Object.green_circle ∧ (l1 saliencePrior k Utterance.circle) Object.green_circle < (l1 saliencePrior k Utterance.circle) Object.blue_circle

Finding 5: the salience reversal for "circle", at every k > 0. The human data follow the salience direction.

theorem QingFranke2015.uniform_green_green_circ {k : ℝ} (hk : 0 < k) : (l1 uniformPrior k Utterance.green) Object.green_square < (l1 uniformPrior k Utterance.green) Object.green_circle

Uniform-prior listener, "green": pragmatic narrowing favors the green circle (a green-square speaker had "square"), at every k > 0.

theorem QingFranke2015.salience_green_green_sq {k : ℝ} (hk : 0 < k) : (l1 saliencePrior k Utterance.green) Object.green_circle < (l1 saliencePrior k Utterance.green) Object.green_square

Salience-prior listener, "green": salience (71 vs 30) overrides the pragmatic direction, at every k > 0. Here the humans go the other way (115/180 green circle, Table 2; p. 212).

theorem QingFranke2015.salience_reversal_green {k : ℝ} (hk : 0 < k) : (l1 uniformPrior k Utterance.green) Object.green_square < (l1 uniformPrior k Utterance.green) Object.green_circle ∧ (l1 saliencePrior k Utterance.green) Object.green_circle < (l1 saliencePrior k Utterance.green) Object.green_square

Finding 6: the salience reversal for "green", at every k > 0. The human data follow the pragmatic direction — no single listener prior gets both "circle" and "green" right.

The salience-belief speaker: thresholds inside the cost support

σ_bS replaces the speaker's literal-listener prior with the salience data (eq. 7). Its blue-circle and green-circle predictions flip at k = 139/169 and k = 101/169 — both inside the paper's cost support (c ∈ (0, 0.4) is k ∈ (0.67, 1)) — so that model's content is a pair of thresholds, not directions.

theorem QingFranke2015.σ_bS_blue_circ_iff {k : ℝ} : sbScore saliencePrior k Object.blue_circle Utterance.circle < sbScore saliencePrior k Object.blue_circle Utterance.blue ↔ 139 / 169 < k

σ_bS prefers "blue" at the blue circle iff k > 139/169.

theorem QingFranke2015.σ_bS_green_circ_iff {k : ℝ} : sbScore saliencePrior k Object.green_circle Utterance.circle < sbScore saliencePrior k Object.green_circle Utterance.green ↔ 101 / 169 < k

σ_bS prefers "green" at the green circle iff k > 101/169.

Cost thresholds across the goal dimension

The blue-circle boundary separates the goal types: action-oriented scoring flips at c = 1/2, belief-oriented at c = ln 2 ≈ 0.693 — the log transform amplifies informativity differences, widening the viable cost range. Figure 3's posterior over c peaks well below both.

theorem QingFranke2015.σ_aU_blue_circ_threshold {l0 : Utterance → Object → ℝ} {c α : ℝ} (hα : 0 < α) (hbl : l0 Utterance.blue Object.blue_circle = 1) (hci : l0 Utterance.circle Object.blue_circle = 1 / 2) : actionGoalScore (adjCost c) l0 α Object.blue_circle Utterance.blue > actionGoalScore (adjCost c) l0 α Object.blue_circle Utterance.circle ↔ c < 1 / 2

σ_aU threshold: "blue" > "circle" at the blue circle iff c < 1/2; the σ_aU tie at c = 1/2 is the boundary case.

theorem QingFranke2015.σ_bU_blue_circ_threshold {l0 : Utterance → Object → ℝ} {c α : ℝ} (hα : 0 < α) (hbl : l0 Utterance.blue Object.blue_circle = 1) (hci : l0 Utterance.circle Object.blue_circle = 1 / 2) (hbl_ne : l0 Utterance.blue Object.blue_circle ≠ 0) (hci_ne : l0 Utterance.circle Object.blue_circle ≠ 0) : beliefGoalScore (adjCost c) l0 α Object.blue_circle Utterance.blue > beliefGoalScore (adjCost c) l0 α Object.blue_circle Utterance.circle ↔ c < Real.log 2

σ_bU threshold: "blue" > "circle" at the blue circle iff c < ln 2 — the exponentiated form of speaker_prefers_unique_color's k > 1/2.

Data–model match

theorem QingFranke2015.speakerData_matches_model : speakerData Object.green_square Utterance.square > speakerData Object.green_square Utterance.green ∧ speakerData Object.blue_circle Utterance.blue > speakerData Object.blue_circle Utterance.circle ∧ speakerData Object.green_circle Utterance.circle > speakerData Object.green_circle Utterance.green

Speaker majority choices match the σ_bU rankings (Table 1).

theorem QingFranke2015.listenerData_circle_matches_salience : listenerData Utterance.circle Object.blue_circle > listenerData Utterance.circle Object.green_circle

For "circle", the listener majority follows the salience direction (117 vs 62).

theorem QingFranke2015.listenerData_green_matches_pragmatic : listenerData Utterance.green Object.green_circle > listenerData Utterance.green Object.green_square

For "green", the listener majority follows the pragmatic direction, not salience (115 vs 65; p. 212).

Bridges

theorem QingFranke2015.zeroCost_beliefGoal_eq (l0 : Utterance → Object → ℝ) (α : ℝ) (w : Object) (u : Utterance) : beliefGoalScore (fun (x : Utterance) => 0) l0 α w u = if l0 u w = 0 then 0 else Real.exp (α * Real.log (l0 u w))

At zero cost the belief-oriented score is [FG12]'s scoring rule — σ_bU generalizes FG2012 by the cost dimension.

theorem QingFranke2015.cost_is_q2 : sbScore uniformPrior 1 Object.green_circle Utterance.circle = sbScore uniformPrior 1 Object.green_circle Utterance.green ∧ (∀ (k : ℝ), 0 < k → k < 1 → (s1 uniformPrior k Object.green_circle) Utterance.green < (s1 uniformPrior k Object.green_circle) Utterance.circle) ∧ DaleReiter1995.BrevityInterpretation.noBrevity.strength = 0 ∧ Pragmatics.GriceanMaxims.QuantityViolation.underInformative.submaxim ≠ Pragmatics.GriceanMaxims.QuantityViolation.overInformative.submaxim

The cost dimension is [Gri75]'s Q2 sub-maxim (brevity): without cost the equally-informative words tie (Q1 alone cannot break it), any noun preference breaks it, and zero cost is [DR95]'s No-Brevity interpretation at strength 0, independent of Q1.