Documentation

Linglib.Studies.BergenGoodman2015

[BG15]: the strategic use of noise #

Topics in Cognitive Science 7(2), 336–350. RSA over a noisy channel P_N(u_p | u_i): the listener reasons about which intended utterance the perceived one came from (eq. 6), the speaker about which utterances survive noise (eqs. 7–8).

Main results #

l0_fragment_correct / l1_fragment_correct: "Bob" — no literal meaning — is interpreted as "Bob went to the movies" (§3 ellipsis): noise-deletion reasoning recovers the unique full-sentence source.
l0_fragment_robust: the fragment inference holds for every noise rate δ ∈ (0, 1), not just the sampled δ = 1/100.
stress_increases_exhaustivity: at every noise rate ε < 2/3, "BOB went" (stressed) is more likely than "Bob went" to mean only-Bob (§4) — stress reduces noise on the word it protects.
stress_increases_discrimination: the channel-level mechanism, for every ε ∈ (0, 1).

Implementation notes #

Ellipsis is exact ℚ≥0: each meaning has a unique truthful full sentence, so the eq. 7 softmax is degenerate and eq. 8 reduces to the channel row (s1nQ); listeners are PMF.ofScores. Prosody is transcendental — the eq. 7 utilities are channel-weighted geometric means of literal posteriors (xAtom, yAtom) — and fully parametric in ε: the mechanism theorem xAtom_lt_yAtom places the atoms strictly on either side of the unstressed posterior by the two-factor GM bounds in Pragmatics/RSA/Atoms.lean, and the headline reduces to that ordering plus algebra. No magnitude certificates.

Ellipsis (§3) #

Three meanings, seven utterances (full sentences plus fragments); only full sentences have literal meaning, and per-word deletion (rate δ) turns them into fragments.

inductive BergenGoodman2015.EllipsisModel.Meaning :

Meanings: who went to the movies.

aliceWent : Meaning
bobWent : Meaning
nobodyWent : Meaning

Instances For

@[implicit_reducible]

instance BergenGoodman2015.EllipsisModel.instDecidableEqMeaning :

DecidableEq Meaning

Equations

BergenGoodman2015.EllipsisModel.instDecidableEqMeaning x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance BergenGoodman2015.EllipsisModel.instFintypeMeaning :

Fintype Meaning

Equations

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

@[implicit_reducible]

instance BergenGoodman2015.EllipsisModel.instReprMeaning :

Equations

BergenGoodman2015.EllipsisModel.instReprMeaning = { reprPrec := BergenGoodman2015.EllipsisModel.instReprMeaning.repr }

def BergenGoodman2015.EllipsisModel.instReprMeaning.repr :

Meaning → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance BergenGoodman2015.EllipsisModel.instInhabitedMeaning :

Inhabited Meaning

Equations

BergenGoodman2015.EllipsisModel.instInhabitedMeaning = { default := BergenGoodman2015.EllipsisModel.instInhabitedMeaning.default }

inductive BergenGoodman2015.EllipsisModel.Utterance :

Utterances: full sentences and fragments. Fragments arise from noise deleting words from full sentences.

aliceWentToMovies : Utterance
bobWentToMovies : Utterance
nobodyWentToMovies : Utterance
alice : Utterance
bob : Utterance
nobody : Utterance
wentToMovies : Utterance

Instances For

@[implicit_reducible]

instance BergenGoodman2015.EllipsisModel.instDecidableEqUtterance :

DecidableEq Utterance

Equations

BergenGoodman2015.EllipsisModel.instDecidableEqUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance BergenGoodman2015.EllipsisModel.instFintypeUtterance :

Fintype Utterance

Equations

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

@[implicit_reducible]

instance BergenGoodman2015.EllipsisModel.instReprUtterance :

Equations

BergenGoodman2015.EllipsisModel.instReprUtterance = { reprPrec := BergenGoodman2015.EllipsisModel.instReprUtterance.repr }

def BergenGoodman2015.EllipsisModel.instReprUtterance.repr :

Utterance → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance BergenGoodman2015.EllipsisModel.instInhabitedUtterance :

Inhabited Utterance

Equations

BergenGoodman2015.EllipsisModel.instInhabitedUtterance = { default := BergenGoodman2015.EllipsisModel.instInhabitedUtterance.default }

def BergenGoodman2015.EllipsisModel.literalMeaning :

Utterance → Meaning → Bool

Literal meaning: only full sentences have truth conditions. Fragments have no literal meaning — this is the key to the model.

Equations

Instances For

noncomputable def BergenGoodman2015.EllipsisModel.utterancePrior :

Utterance → ℝ

Prior over utterances (speaker's production probability). Only full sentences are in the speaker's production distribution.

Equations

Instances For

noncomputable def BergenGoodman2015.EllipsisModel.noiseChannel (δ : ℝ) :

Utterance → Utterance → ℝ

Deletion channel: a full sentence survives with probability 1 − δ or loses its predicate with probability δ (the path relevant to "Bob").

Equations

Instances For

The ellipsis chain #

def BergenGoodman2015.EllipsisModel.δQ :

ℚ≥0

ℚ noise rate (1%; Fig. 1 shows robustness across 10⁻⁵–10⁻¹).

Equations

BergenGoodman2015.EllipsisModel.δQ = 1 / 100

Instances For

def BergenGoodman2015.EllipsisModel.noiseQ :

Utterance → Utterance → ℚ≥0

ℚ noise channel (word deletion, mirroring noiseChannel).

Equations

Instances For

def BergenGoodman2015.EllipsisModel.utterancePriorQ :

Utterance → ℚ≥0

ℚ utterance prior (only full sentences are produced).

Equations

Instances For

def BergenGoodman2015.EllipsisModel.noisyMeaningQ (u_p : Utterance) (m : Meaning) :

ℚ≥0

ℚ noisy literal-listener score (eq. 6 numerator).

Equations

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

Instances For

def BergenGoodman2015.EllipsisModel.fullOf :

Meaning → Utterance

The unique full sentence expressing each meaning.

Equations

Instances For

def BergenGoodman2015.EllipsisModel.s1nQ (m : Meaning) (u_p : Utterance) :

ℚ≥0

The noise-folded pragmatic speaker (eqs. 7–8). Each meaning has exactly one truthful full sentence, so eq. 7's softmax has singleton support and the intended-speaker distribution is degenerate at fullOf m; eq. 8's fold then reduces to the channel row of fullOf m.

Equations

BergenGoodman2015.EllipsisModel.s1nQ m u_p = BergenGoodman2015.EllipsisModel.noiseQ (BergenGoodman2015.EllipsisModel.fullOf m) u_p

Instances For

noncomputable def BergenGoodman2015.EllipsisModel.l0 (u_p : Utterance) :

Literal listener over meanings (eq. 6).

Equations

BergenGoodman2015.EllipsisModel.l0 u_p = PMF.ofScores PMF.Fallback.uniform fun (m : BergenGoodman2015.EllipsisModel.Meaning) => BergenGoodman2015.EllipsisModel.noisyMeaningQ u_p m

Instances For

noncomputable def BergenGoodman2015.EllipsisModel.l1 (u_p : Utterance) :

Pragmatic listener over meanings (eq. 8, uniform meaning prior).

Equations

BergenGoodman2015.EllipsisModel.l1 u_p = PMF.ofScores PMF.Fallback.uniform fun (m : BergenGoodman2015.EllipsisModel.Meaning) => BergenGoodman2015.EllipsisModel.s1nQ m u_p

Instances For

noncomputable def BergenGoodman2015.EllipsisModel.noisyMeaning (δ : ℝ) (u_p : Utterance) (m : Meaning) :

ℝ

Noisy L0 meaning (Eq. 6 numerator).

meaning(u_p, m) = Σ_{u_i} ⟦u_i⟧(m) · P(u_i) · P_N(u_p | u_i)

The listener considers all intended utterances u_i with meaning m, weighted by how likely noise would produce the perceived u_p.

Equations

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

Instances For

Ellipsis Predictions #

theorem BergenGoodman2015.EllipsisModel.l0_fragment_correct :

(l0 Utterance.bob) Meaning.aliceWent < (l0 Utterance.bob) Meaning.bobWent ∧ (l0 Utterance.bob) Meaning.nobodyWent < (l0 Utterance.bob) Meaning.bobWent

Hearing the fragment "Bob" — no literal meaning — L0 infers "Bob went": the only full sentence producing "Bob" by deletion.

theorem BergenGoodman2015.EllipsisModel.l0_nobody_correct :

(l0 Utterance.nobody) Meaning.aliceWent < (l0 Utterance.nobody) Meaning.nobodyWent ∧ (l0 Utterance.nobody) Meaning.bobWent < (l0 Utterance.nobody) Meaning.nobodyWent

The same for the "Nobody" fragment.

theorem BergenGoodman2015.EllipsisModel.l0_full_sentence_correct :

(l0 Utterance.bobWentToMovies) Meaning.aliceWent < (l0 Utterance.bobWentToMovies) Meaning.bobWent ∧ (l0 Utterance.bobWentToMovies) Meaning.nobodyWent < (l0 Utterance.bobWentToMovies) Meaning.bobWent

Full sentences are interpreted literally (sanity check).

theorem BergenGoodman2015.EllipsisModel.l1_fragment_correct :

(l1 Utterance.bob) Meaning.aliceWent < (l1 Utterance.bob) Meaning.bobWent ∧ (l1 Utterance.bob) Meaning.nobodyWent < (l1 Utterance.bob) Meaning.bobWent

The pragmatic listener agrees on the fragment.

Parametric robustness (Fig. 1, left panel) #

theorem BergenGoodman2015.EllipsisModel.noisyMeaning_bob_bobWent (δ : ℝ) :

noisyMeaning δ Utterance.bob Meaning.bobWent = δ

The noisy meaning at "bob" is δ for bobWent and 0 for all others.

Only "Bob went to the movies" can produce "Bob" via noise deletion, and only with meaning bobWent. Therefore L0("bob") = δ/δ = 1.

theorem BergenGoodman2015.EllipsisModel.noisyMeaning_bob_aliceWent (δ : ℝ) :

noisyMeaning δ Utterance.bob Meaning.aliceWent = 0

theorem BergenGoodman2015.EllipsisModel.noisyMeaning_bob_nobodyWent (δ : ℝ) :

noisyMeaning δ Utterance.bob Meaning.nobodyWent = 0

theorem BergenGoodman2015.EllipsisModel.l0_fragment_robust (δ₀ : ℝ) (hδ : δ₀ ≠ 0) :

noisyMeaning δ₀ Utterance.bob Meaning.bobWent / (noisyMeaning δ₀ Utterance.bob Meaning.aliceWent + noisyMeaning δ₀ Utterance.bob Meaning.bobWent + noisyMeaning δ₀ Utterance.bob Meaning.nobodyWent) = 1

Fragment interpretation at every noise rate δ > 0 — "this reasoning will work even if the noise rate is arbitrarily close to 0, so long as it is positive": "Bob" only arises from "Bob went", so L0 gives it probability δ/δ = 1.

Prosody (§4) #

Stress halves the noise rate on the stressed word (§4.1's ε/n at n = 2). An exhaustive-knowledge speaker must protect "Bob" from mishearing, a non-exhaustive one need not — so the listener reads stress as exhaustivity.

inductive BergenGoodman2015.ProsodyModel.Meaning :

Meanings: who went to the movies (exhaustive vs non-exhaustive).

onlyAlice : Meaning
onlyBob : Meaning
both : Meaning

Instances For

@[implicit_reducible]

instance BergenGoodman2015.ProsodyModel.instDecidableEqMeaning :

DecidableEq Meaning

Equations

BergenGoodman2015.ProsodyModel.instDecidableEqMeaning x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance BergenGoodman2015.ProsodyModel.instFintypeMeaning :

Fintype Meaning

Equations

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

@[implicit_reducible]

instance BergenGoodman2015.ProsodyModel.instReprMeaning :

Equations

BergenGoodman2015.ProsodyModel.instReprMeaning = { reprPrec := BergenGoodman2015.ProsodyModel.instReprMeaning.repr }

def BergenGoodman2015.ProsodyModel.instReprMeaning.repr :

Meaning → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance BergenGoodman2015.ProsodyModel.instInhabitedMeaning :

Inhabited Meaning

Equations

BergenGoodman2015.ProsodyModel.instInhabitedMeaning = { default := BergenGoodman2015.ProsodyModel.instInhabitedMeaning.default }

inductive BergenGoodman2015.ProsodyModel.Utterance :

Utterances: with and without prosodic stress (CAPS = stress).

aliceWent : Utterance
ALICE_went : Utterance
bobWent : Utterance
BOB_went : Utterance
aliceAndBobWent : Utterance

Instances For

@[implicit_reducible]

instance BergenGoodman2015.ProsodyModel.instDecidableEqUtterance :

DecidableEq Utterance

Equations

BergenGoodman2015.ProsodyModel.instDecidableEqUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance BergenGoodman2015.ProsodyModel.instFintypeUtterance :

Fintype Utterance

Equations

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

def BergenGoodman2015.ProsodyModel.instReprUtterance.repr :

Utterance → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance BergenGoodman2015.ProsodyModel.instReprUtterance :

Equations

BergenGoodman2015.ProsodyModel.instReprUtterance = { reprPrec := BergenGoodman2015.ProsodyModel.instReprUtterance.repr }

@[implicit_reducible]

instance BergenGoodman2015.ProsodyModel.instInhabitedUtterance :

Inhabited Utterance

Equations

BergenGoodman2015.ProsodyModel.instInhabitedUtterance = { default := BergenGoodman2015.ProsodyModel.instInhabitedUtterance.default }

def BergenGoodman2015.ProsodyModel.literalMeaning :

Utterance → Meaning → Bool

Literal meaning: lower-bound semantics. "Alice went" is true if Alice went (regardless of others).

Equations

Instances For

noncomputable def BergenGoodman2015.ProsodyModel.noiseChannel (ε : ℝ) :

Utterance → Utterance → ℝ

Noise channel with prosody.

The confusion is between subjects: "Alice" ↔ "Bob".

No stress: ε chance of subject confusion
With stress: ε/2 chance (stress reduces noise)

Equations

Instances For

noncomputable def BergenGoodman2015.ProsodyModel.noisyMeaning (ε : ℝ) (u_p : Utterance) (m : Meaning) :

ℝ

Noisy L0 meaning (Eq. 6 numerator) for the prosody model.

Equations

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

Instances For

noncomputable def BergenGoodman2015.ProsodyModel.l0 (ε : ℝ) (u_p : Utterance) (m : Meaning) :

ℝ

Literal listener over meanings given the perceived utterance (eq. 6, uniform priors).

Equations

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

Instances For

noncomputable def BergenGoodman2015.ProsodyModel.xAtom (ε : ℝ) :

ℝ

Unstressed speaker-utility atom (eq. 7): the channel-weighted geometric mean of the literal posteriors for uttering "Bob went".

Equations

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

Instances For

noncomputable def BergenGoodman2015.ProsodyModel.yAtom (ε : ℝ) :

ℝ

Stressed speaker-utility atom (eq. 7) for "BOB went".

Equations

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

Instances For

theorem BergenGoodman2015.ProsodyModel.xAtom_lt_yAtom {ε : ℝ} (hε0 : 0 < ε) (hε : ε < 2 / 3) :

xAtom ε < yAtom ε

The paper's mechanism, at every noise rate ε < 2/3: the stressed atom strictly exceeds the unstressed one. Stress both concentrates the channel on the informative percept and sharpens that percept's posterior, so the weighted geometric means separate across the unstressed posterior (1 − ε/2)/(2 + ε) — no magnitude computation involved.

theorem BergenGoodman2015.ProsodyModel.xAtom_pos {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) :

0 < xAtom ε

theorem BergenGoodman2015.ProsodyModel.yAtom_pos {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) :

0 < yAtom ε

theorem BergenGoodman2015.ProsodyModel.xAtom_eq_exp {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) :

xAtom ε = Real.exp ((1 - ε) * Real.log (l0 ε Utterance.bobWent Meaning.onlyBob) + ε * Real.log (l0 ε Utterance.aliceWent Meaning.onlyBob))

The atoms are the paper's exponentiated eq.-7 utilities.

noncomputable def BergenGoodman2015.ProsodyModel.eAtom (ε : ℝ) :

Meaning → Utterance → ℝ

Speaker-utility atoms per (meaning, utterance): the truthful subject utterances carry xAtom/yAtom (by Alice/Bob symmetry), the both meaning's subject atoms are identically 1/2, and the conjunction is noise-free.

Equations

Instances For

noncomputable def BergenGoodman2015.ProsodyModel.l1Score (ε : ℝ) (u_p : Utterance) (m : Meaning) :

ℝ

Pragmatic-listener score (eq. 8): speaker-normalized atoms folded through the channel.

Equations

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

Instances For

noncomputable def BergenGoodman2015.ProsodyModel.l1PMF (ε : ℝ) (u_p : Utterance) :

Pragmatic listener (eq. 8).

Equations

BergenGoodman2015.ProsodyModel.l1PMF ε u_p = PMF.normalizeOrUniform fun (m : BergenGoodman2015.ProsodyModel.Meaning) => ENNReal.ofReal (BergenGoodman2015.ProsodyModel.l1Score ε u_p m)

Instances For

theorem BergenGoodman2015.ProsodyModel.stress_increases_exhaustivity {ε : ℝ} (hε0 : 0 < ε) (hε : ε < 2 / 3) :

(l1PMF ε Utterance.bobWent) Meaning.onlyBob < (l1PMF ε Utterance.BOB_went) Meaning.onlyBob

Stress increases the exhaustive interpretation, at every noise rate ε < 2/3: "BOB went" is strictly more likely than "Bob went" to mean only Bob went (§4). By posterior dominance (Finset.div_sum_lt_div_sum), the comparison is cell-by-cell odds dominance: trivial at onlyAlice (the stressed row is zero there) and onlyBob, and the atom ordering xAtom < yAtom — the paper's mechanism — at both.

def BergenGoodman2015.ProsodyModel.uttOf (row : Data.Examples.LinguisticExample) :

Option Utterance

Utterance adapter: a row's stress feature as an utterance.

Equations

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

Instances For

theorem BergenGoodman2015.ProsodyModel.model_matches_stress_rows :

∃ (u_s : Utterance) (u_u : Utterance), uttOf Examples.stressed_subject = some u_s ∧ uttOf Examples.unstressed_subject = some u_u ∧ (l1PMF (1 / 100) u_u) Meaning.onlyBob < (l1PMF (1 / 100) u_s) Meaning.onlyBob

The model's L1 assigns the exhaustive meaning more probability at the stressed row's utterance than at the unstressed row's, matching the rows' recorded reading contrast.

theorem BergenGoodman2015.ProsodyModel.stress_increases_discrimination {ε : ℝ} (hε : 0 < ε) :

noiseChannel ε Utterance.BOB_went Utterance.BOB_went - noiseChannel ε Utterance.BOB_went Utterance.bobWent > noiseChannel ε Utterance.bobWent Utterance.bobWent - noiseChannel ε Utterance.bobWent Utterance.aliceWent

Stress widens the channel's correct-vs-confused gap by exactly ε (1 − ε stressed versus 1 − 2ε unstressed) — the channel-level face of the mechanism, at every noise rate.