Noisy Channel Model

A noisy channel is a stochastic matrix P_N(u_p | u_i) giving the probability that the listener perceives utterance u_p when the speaker intended u_i.

Key properties:

• Rows sum to 1 (it's a conditional distribution)
• Diagonal entries are typically high (usually perceived correctly)
• Off-diagonal entries represent noise (corruption)

structure RSA.BergenGoodman2015.NoisyChannel (U : Type) : Type

A noisy channel over utterances.

transmit u_i u_p is P_N(u_p | u_i): probability of perceiving u_p given intended u_i.

• transmit : U → U → ℚ

  Transition probability P_N(u_p | u_i)

• nonneg (ui up : U) : 0 ≤ self.transmit ui up

  All probabilities are non-negative

def RSA.BergenGoodman2015.NoisyChannel.identity {U : Type} [DecidableEq U] (allU : List U) : NoisyChannel U

Identity channel: no noise, perfect transmission

Equations

• RSA.BergenGoodman2015.NoisyChannel.identity allU = { transmit := fun (ui up : U) => if ui = up then 1 else 0, nonneg := ⋯ }

def RSA.BergenGoodman2015.NoisyChannel.symmetric {U : Type} [DecidableEq U] (allU : List U) (ε : ℚ) (hε : 0 ≤ ε ∧ ε ≤ 1) : NoisyChannel U

Symmetric noise channel: each word independently corrupted with probability ε

Equations

• RSA.BergenGoodman2015.NoisyChannel.symmetric allU ε hε = { transmit := fun (ui up : U) => if ui = up then 1 - ε else if allU.length > 1 then ε / (↑allU.length - 1) else 0, nonneg := ⋯ }

Ellipsis: Sentence Fragments

Example from paper:

• A: "Who went to the movies?"
• B: "Bob" (fragment, not full sentence)

The listener infers "Bob went to the movies" because:

1. "Bob" is not grammatical on its own
2. Listener assumes noise deleted the rest
3. "Bob went to the movies" → "Bob" via deletion is most probable

Model Setup

• Meanings M = {Alice went, Bob went, Nobody went}
• Full utterances U = {"Alice went", "Bob went", "Nobody went"}
• Fragments F = {"Alice", "Bob", "Nobody",...}
• Noise: word deletion with probability δ

inductive RSA.BergenGoodman2015.Ellipsis.Meaning : Type

Meanings: who went to the movies

• aliceWent : Meaning
• bobWent : Meaning
• nobodyWent : Meaning

instance RSA.BergenGoodman2015.Ellipsis.instDecidableEqMeaning : DecidableEq Meaning

Equations

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

def RSA.BergenGoodman2015.Ellipsis.instBEqMeaning.beq : Meaning → Meaning → Bool

Equations

• RSA.BergenGoodman2015.Ellipsis.instBEqMeaning.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.BergenGoodman2015.Ellipsis.instBEqMeaning : BEq Meaning

Equations

• RSA.BergenGoodman2015.Ellipsis.instBEqMeaning = { beq := RSA.BergenGoodman2015.Ellipsis.instBEqMeaning.beq }

instance RSA.BergenGoodman2015.Ellipsis.instReprMeaning : Repr Meaning

Equations

• RSA.BergenGoodman2015.Ellipsis.instReprMeaning = { reprPrec := RSA.BergenGoodman2015.Ellipsis.instReprMeaning.repr }

def RSA.BergenGoodman2015.Ellipsis.instReprMeaning.repr : Meaning → ℕ → Std.Format

Equations

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

instance RSA.BergenGoodman2015.Ellipsis.instInhabitedMeaning : Inhabited Meaning

Equations

• RSA.BergenGoodman2015.Ellipsis.instInhabitedMeaning = { default := RSA.BergenGoodman2015.Ellipsis.instInhabitedMeaning.default }

def RSA.BergenGoodman2015.Ellipsis.instInhabitedMeaning.default : Meaning

Equations

• RSA.BergenGoodman2015.Ellipsis.instInhabitedMeaning.default = RSA.BergenGoodman2015.Ellipsis.Meaning.aliceWent

def RSA.BergenGoodman2015.Ellipsis.allMeanings : List Meaning

Equations

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

inductive RSA.BergenGoodman2015.Ellipsis.Utterance : Type

Utterances: full sentences and fragments

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

instance RSA.BergenGoodman2015.Ellipsis.instDecidableEqUtterance : DecidableEq Utterance

Equations

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

def RSA.BergenGoodman2015.Ellipsis.instBEqUtterance.beq : Utterance → Utterance → Bool

Equations

• RSA.BergenGoodman2015.Ellipsis.instBEqUtterance.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.BergenGoodman2015.Ellipsis.instBEqUtterance : BEq Utterance

Equations

• RSA.BergenGoodman2015.Ellipsis.instBEqUtterance = { beq := RSA.BergenGoodman2015.Ellipsis.instBEqUtterance.beq }

def RSA.BergenGoodman2015.Ellipsis.instReprUtterance.repr : Utterance → ℕ → Std.Format

Equations

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

instance RSA.BergenGoodman2015.Ellipsis.instReprUtterance : Repr Utterance

Equations

• RSA.BergenGoodman2015.Ellipsis.instReprUtterance = { reprPrec := RSA.BergenGoodman2015.Ellipsis.instReprUtterance.repr }

def RSA.BergenGoodman2015.Ellipsis.instInhabitedUtterance.default : Utterance

Equations

• RSA.BergenGoodman2015.Ellipsis.instInhabitedUtterance.default = RSA.BergenGoodman2015.Ellipsis.Utterance.aliceWentToMovies

instance RSA.BergenGoodman2015.Ellipsis.instInhabitedUtterance : Inhabited Utterance

Equations

• RSA.BergenGoodman2015.Ellipsis.instInhabitedUtterance = { default := RSA.BergenGoodman2015.Ellipsis.instInhabitedUtterance.default }

def RSA.BergenGoodman2015.Ellipsis.allUtterances : List Utterance

Equations

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

def RSA.BergenGoodman2015.Ellipsis.fullSentences : List Utterance

Equations

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

def RSA.BergenGoodman2015.Ellipsis.literalMeaning : Utterance → Meaning → Bool

Literal meaning: only full sentences have truth conditions

Equations

• RSA.BergenGoodman2015.Ellipsis.literalMeaning RSA.BergenGoodman2015.Ellipsis.Utterance.aliceWentToMovies RSA.BergenGoodman2015.Ellipsis.Meaning.aliceWent = true
• RSA.BergenGoodman2015.Ellipsis.literalMeaning RSA.BergenGoodman2015.Ellipsis.Utterance.bobWentToMovies RSA.BergenGoodman2015.Ellipsis.Meaning.bobWent = true
• RSA.BergenGoodman2015.Ellipsis.literalMeaning RSA.BergenGoodman2015.Ellipsis.Utterance.nobodyWentToMovies RSA.BergenGoodman2015.Ellipsis.Meaning.nobodyWent = true
• RSA.BergenGoodman2015.Ellipsis.literalMeaning x✝¹ x✝ = false

def RSA.BergenGoodman2015.Ellipsis.utterancePrior : Utterance → ℚ

Prior over utterances (speaker's production probability)

Equations

• RSA.BergenGoodman2015.Ellipsis.utterancePrior RSA.BergenGoodman2015.Ellipsis.Utterance.aliceWentToMovies = 1
• RSA.BergenGoodman2015.Ellipsis.utterancePrior RSA.BergenGoodman2015.Ellipsis.Utterance.bobWentToMovies = 1
• RSA.BergenGoodman2015.Ellipsis.utterancePrior RSA.BergenGoodman2015.Ellipsis.Utterance.nobodyWentToMovies = 1
• RSA.BergenGoodman2015.Ellipsis.utterancePrior x✝ = 0

def RSA.BergenGoodman2015.Ellipsis.noiseChannel (δ : ℚ) : Utterance → Utterance → ℚ

Noise model: probability of perceiving u_p given intended u_i.

Simplified model with base noise rate δ:

• Same utterance: high probability (1 - δ)
• Full sentence → fragment (subject): probability δ (plausible deletion)
• Everything else: small probability

Equations

• RSA.BergenGoodman2015.Ellipsis.noiseChannel δ RSA.BergenGoodman2015.Ellipsis.Utterance.aliceWentToMovies RSA.BergenGoodman2015.Ellipsis.Utterance.aliceWentToMovies = 1 - δ
• RSA.BergenGoodman2015.Ellipsis.noiseChannel δ RSA.BergenGoodman2015.Ellipsis.Utterance.aliceWentToMovies RSA.BergenGoodman2015.Ellipsis.Utterance.alice = δ
• RSA.BergenGoodman2015.Ellipsis.noiseChannel δ RSA.BergenGoodman2015.Ellipsis.Utterance.bobWentToMovies RSA.BergenGoodman2015.Ellipsis.Utterance.bobWentToMovies = 1 - δ
• RSA.BergenGoodman2015.Ellipsis.noiseChannel δ RSA.BergenGoodman2015.Ellipsis.Utterance.bobWentToMovies RSA.BergenGoodman2015.Ellipsis.Utterance.bob = δ
• RSA.BergenGoodman2015.Ellipsis.noiseChannel δ RSA.BergenGoodman2015.Ellipsis.Utterance.nobodyWentToMovies RSA.BergenGoodman2015.Ellipsis.Utterance.nobodyWentToMovies = 1 - δ
• RSA.BergenGoodman2015.Ellipsis.noiseChannel δ RSA.BergenGoodman2015.Ellipsis.Utterance.nobodyWentToMovies RSA.BergenGoodman2015.Ellipsis.Utterance.nobody = δ
• RSA.BergenGoodman2015.Ellipsis.noiseChannel δ RSA.BergenGoodman2015.Ellipsis.Utterance.alice RSA.BergenGoodman2015.Ellipsis.Utterance.alice = 1
• RSA.BergenGoodman2015.Ellipsis.noiseChannel δ RSA.BergenGoodman2015.Ellipsis.Utterance.bob RSA.BergenGoodman2015.Ellipsis.Utterance.bob = 1
• RSA.BergenGoodman2015.Ellipsis.noiseChannel δ RSA.BergenGoodman2015.Ellipsis.Utterance.nobody RSA.BergenGoodman2015.Ellipsis.Utterance.nobody = 1
• RSA.BergenGoodman2015.Ellipsis.noiseChannel δ RSA.BergenGoodman2015.Ellipsis.Utterance.wentToMovies RSA.BergenGoodman2015.Ellipsis.Utterance.wentToMovies = 1
• RSA.BergenGoodman2015.Ellipsis.noiseChannel δ x✝¹ x✝ = 0

def RSA.BergenGoodman2015.Ellipsis.cost : Utterance → ℚ

Utterance cost (longer = more costly)

Equations

• RSA.BergenGoodman2015.Ellipsis.cost RSA.BergenGoodman2015.Ellipsis.Utterance.aliceWentToMovies = 5
• RSA.BergenGoodman2015.Ellipsis.cost RSA.BergenGoodman2015.Ellipsis.Utterance.bobWentToMovies = 5
• RSA.BergenGoodman2015.Ellipsis.cost RSA.BergenGoodman2015.Ellipsis.Utterance.nobodyWentToMovies = 5
• RSA.BergenGoodman2015.Ellipsis.cost RSA.BergenGoodman2015.Ellipsis.Utterance.alice = 1
• RSA.BergenGoodman2015.Ellipsis.cost RSA.BergenGoodman2015.Ellipsis.Utterance.bob = 1
• RSA.BergenGoodman2015.Ellipsis.cost RSA.BergenGoodman2015.Ellipsis.Utterance.nobody = 1
• RSA.BergenGoodman2015.Ellipsis.cost RSA.BergenGoodman2015.Ellipsis.Utterance.wentToMovies = 4

def RSA.BergenGoodman2015.Ellipsis.L0_noisy (δ : ℚ) (u_perceived : Utterance) : List (Meaning × ℚ)

L0: Literal listener with noise inference (Eq. 6 from paper)

L0(m | u_p) ∝ P(m) Σ_{u_i : m ∈ [[u_i]]} P(u_i) P_N(u_p | u_i)

The listener:

1. Considers all utterances u_i that could have produced perceived u_p
2. Weights by prior P(u_i) and noise probability P_N(u_p | u_i)
3. Assigns meaning based on literal semantics of u_i

Equations

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

def RSA.BergenGoodman2015.Ellipsis.S1_noisy (δ : ℚ) (m : Meaning) : List (Utterance × ℚ)

S1: Speaker considering noise (simplified)

The speaker chooses utterances that will likely be interpreted correctly. Utility = P(listener gets correct meaning) - cost

Equations

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

def RSA.BergenGoodman2015.Ellipsis.L1_noisy (δ : ℚ) (u_perceived : Utterance) : List (Meaning × ℚ)

L1: Pragmatic listener reasoning about noisy speaker

L1(m | u_p) ∝ P(m) Σ_{u_i} S1(u_i | m) P_N(u_p | u_i)

Equations

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

def RSA.BergenGoodman2015.Ellipsis.δ_default : ℚ

Noise rate for experiments

Equations

• RSA.BergenGoodman2015.Ellipsis.δ_default = 1 / 100

def RSA.BergenGoodman2015.Ellipsis.l0_bob : List (Meaning × ℚ)

Equations

• RSA.BergenGoodman2015.Ellipsis.l0_bob = RSA.BergenGoodman2015.Ellipsis.L0_noisy RSA.BergenGoodman2015.Ellipsis.δ_default RSA.BergenGoodman2015.Ellipsis.Utterance.bob

def RSA.BergenGoodman2015.Ellipsis.l1_bob : List (Meaning × ℚ)

Equations

• RSA.BergenGoodman2015.Ellipsis.l1_bob = RSA.BergenGoodman2015.Ellipsis.L1_noisy RSA.BergenGoodman2015.Ellipsis.δ_default RSA.BergenGoodman2015.Ellipsis.Utterance.bob

theorem RSA.BergenGoodman2015.Ellipsis.fragment_interpretation : RSA.BergenGoodman2015.getScore✝ l0_bob Meaning.bobWent > RSA.BergenGoodman2015.getScore✝¹ l0_bob Meaning.aliceWent ∧ RSA.BergenGoodman2015.getScore✝² l0_bob Meaning.bobWent > RSA.BergenGoodman2015.getScore✝³ l0_bob Meaning.nobodyWent

Ellipsis Theorem: The fragment "Bob" is interpreted as "Bob went".

Even though "Bob" has no literal meaning, the listener infers it via:

1. "Bob" most likely came from "Bob went to the movies" via deletion
2. "Bob went to the movies" means Bob went
3. Therefore "Bob" → Bob went

theorem RSA.BergenGoodman2015.Ellipsis.l0_fragment_works : RSA.BergenGoodman2015.getScore✝ l0_bob Meaning.bobWent = 1

L0 correctly interprets fragment

Prosody: Strategic Noise Reduction

Prosodic stress (BOB vs Bob) reduces noise rate on stressed words. This has pragmatic consequences:

Example:

• "Bob went to the movies" - compatible with others also going
• "BOB went to the movies" - exhaustive: ONLY Bob went

Mechanism

Speaker S1 with exhaustive knowledge (only Bob went):

• Needs listener to hear "Bob" correctly
• If listener mishears "Alice", wrong inference
• Therefore: stress "Bob" to reduce noise

Speaker with non-exhaustive knowledge (Bob went, maybe others too):

• Less critical if listener mishears "Bob" as "Alice"
• Both are compatible with speaker's knowledge
• Therefore: less likely to stress

Listener infers: stress → speaker had reason to protect that word → speaker has exhaustive knowledge

inductive RSA.BergenGoodman2015.Prosody.Meaning : Type

Meanings for exhaustivity example

• onlyAlice : Meaning
• onlyBob : Meaning
• both : Meaning

instance RSA.BergenGoodman2015.Prosody.instDecidableEqMeaning : DecidableEq Meaning

Equations

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

def RSA.BergenGoodman2015.Prosody.instBEqMeaning.beq : Meaning → Meaning → Bool

Equations

• RSA.BergenGoodman2015.Prosody.instBEqMeaning.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.BergenGoodman2015.Prosody.instBEqMeaning : BEq Meaning

Equations

• RSA.BergenGoodman2015.Prosody.instBEqMeaning = { beq := RSA.BergenGoodman2015.Prosody.instBEqMeaning.beq }

instance RSA.BergenGoodman2015.Prosody.instReprMeaning : Repr Meaning

Equations

• RSA.BergenGoodman2015.Prosody.instReprMeaning = { reprPrec := RSA.BergenGoodman2015.Prosody.instReprMeaning.repr }

def RSA.BergenGoodman2015.Prosody.instReprMeaning.repr : Meaning → ℕ → Std.Format

Equations

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

instance RSA.BergenGoodman2015.Prosody.instInhabitedMeaning : Inhabited Meaning

Equations

• RSA.BergenGoodman2015.Prosody.instInhabitedMeaning = { default := RSA.BergenGoodman2015.Prosody.instInhabitedMeaning.default }

def RSA.BergenGoodman2015.Prosody.instInhabitedMeaning.default : Meaning

Equations

• RSA.BergenGoodman2015.Prosody.instInhabitedMeaning.default = RSA.BergenGoodman2015.Prosody.Meaning.onlyAlice

def RSA.BergenGoodman2015.Prosody.allMeanings : List Meaning

Equations

• RSA.BergenGoodman2015.Prosody.allMeanings = [RSA.BergenGoodman2015.Prosody.Meaning.onlyAlice, RSA.BergenGoodman2015.Prosody.Meaning.onlyBob, RSA.BergenGoodman2015.Prosody.Meaning.both]

inductive RSA.BergenGoodman2015.Prosody.Utterance : Type

Utterances with optional prosodic stress

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

instance RSA.BergenGoodman2015.Prosody.instDecidableEqUtterance : DecidableEq Utterance

Equations

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

def RSA.BergenGoodman2015.Prosody.instBEqUtterance.beq : Utterance → Utterance → Bool

Equations

• RSA.BergenGoodman2015.Prosody.instBEqUtterance.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.BergenGoodman2015.Prosody.instBEqUtterance : BEq Utterance

Equations

• RSA.BergenGoodman2015.Prosody.instBEqUtterance = { beq := RSA.BergenGoodman2015.Prosody.instBEqUtterance.beq }

instance RSA.BergenGoodman2015.Prosody.instReprUtterance : Repr Utterance

Equations

• RSA.BergenGoodman2015.Prosody.instReprUtterance = { reprPrec := RSA.BergenGoodman2015.Prosody.instReprUtterance.repr }

def RSA.BergenGoodman2015.Prosody.instReprUtterance.repr : Utterance → ℕ → Std.Format

Equations

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

def RSA.BergenGoodman2015.Prosody.instInhabitedUtterance.default : Utterance

Equations

• RSA.BergenGoodman2015.Prosody.instInhabitedUtterance.default = RSA.BergenGoodman2015.Prosody.Utterance.aliceWent

instance RSA.BergenGoodman2015.Prosody.instInhabitedUtterance : Inhabited Utterance

Equations

• RSA.BergenGoodman2015.Prosody.instInhabitedUtterance = { default := RSA.BergenGoodman2015.Prosody.instInhabitedUtterance.default }

def RSA.BergenGoodman2015.Prosody.allUtterances : List Utterance

Equations

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

def RSA.BergenGoodman2015.Prosody.literalMeaning : Utterance → Meaning → Bool

Literal meaning: lower-bound semantics

Equations

• RSA.BergenGoodman2015.Prosody.literalMeaning RSA.BergenGoodman2015.Prosody.Utterance.aliceWent RSA.BergenGoodman2015.Prosody.Meaning.onlyAlice = true
• RSA.BergenGoodman2015.Prosody.literalMeaning RSA.BergenGoodman2015.Prosody.Utterance.aliceWent RSA.BergenGoodman2015.Prosody.Meaning.both = true
• RSA.BergenGoodman2015.Prosody.literalMeaning RSA.BergenGoodman2015.Prosody.Utterance.ALICE_went RSA.BergenGoodman2015.Prosody.Meaning.onlyAlice = true
• RSA.BergenGoodman2015.Prosody.literalMeaning RSA.BergenGoodman2015.Prosody.Utterance.ALICE_went RSA.BergenGoodman2015.Prosody.Meaning.both = true
• RSA.BergenGoodman2015.Prosody.literalMeaning RSA.BergenGoodman2015.Prosody.Utterance.bobWent RSA.BergenGoodman2015.Prosody.Meaning.onlyBob = true
• RSA.BergenGoodman2015.Prosody.literalMeaning RSA.BergenGoodman2015.Prosody.Utterance.bobWent RSA.BergenGoodman2015.Prosody.Meaning.both = true
• RSA.BergenGoodman2015.Prosody.literalMeaning RSA.BergenGoodman2015.Prosody.Utterance.BOB_went RSA.BergenGoodman2015.Prosody.Meaning.onlyBob = true
• RSA.BergenGoodman2015.Prosody.literalMeaning RSA.BergenGoodman2015.Prosody.Utterance.BOB_went RSA.BergenGoodman2015.Prosody.Meaning.both = true
• RSA.BergenGoodman2015.Prosody.literalMeaning RSA.BergenGoodman2015.Prosody.Utterance.aliceAndBobWent RSA.BergenGoodman2015.Prosody.Meaning.both = true
• RSA.BergenGoodman2015.Prosody.literalMeaning x✝¹ x✝ = false

def RSA.BergenGoodman2015.Prosody.noiseChannel (ε : ℚ) : Utterance → Utterance → ℚ

Noise channel with prosody.

Base noise rate ε. Stress reduces noise by factor of 2.

Model: probability of subject being misheard.

• No stress: ε chance of mishearing
• Stress: ε/2 chance of mishearing

Equations

• RSA.BergenGoodman2015.Prosody.noiseChannel ε RSA.BergenGoodman2015.Prosody.Utterance.aliceWent RSA.BergenGoodman2015.Prosody.Utterance.aliceWent = 1 - ε
• RSA.BergenGoodman2015.Prosody.noiseChannel ε RSA.BergenGoodman2015.Prosody.Utterance.aliceWent RSA.BergenGoodman2015.Prosody.Utterance.bobWent = ε
• RSA.BergenGoodman2015.Prosody.noiseChannel ε RSA.BergenGoodman2015.Prosody.Utterance.bobWent RSA.BergenGoodman2015.Prosody.Utterance.bobWent = 1 - ε
• RSA.BergenGoodman2015.Prosody.noiseChannel ε RSA.BergenGoodman2015.Prosody.Utterance.bobWent RSA.BergenGoodman2015.Prosody.Utterance.aliceWent = ε
• RSA.BergenGoodman2015.Prosody.noiseChannel ε RSA.BergenGoodman2015.Prosody.Utterance.ALICE_went RSA.BergenGoodman2015.Prosody.Utterance.ALICE_went = 1 - ε / 2
• RSA.BergenGoodman2015.Prosody.noiseChannel ε RSA.BergenGoodman2015.Prosody.Utterance.ALICE_went RSA.BergenGoodman2015.Prosody.Utterance.aliceWent = ε / 2
• RSA.BergenGoodman2015.Prosody.noiseChannel ε RSA.BergenGoodman2015.Prosody.Utterance.BOB_went RSA.BergenGoodman2015.Prosody.Utterance.BOB_went = 1 - ε / 2
• RSA.BergenGoodman2015.Prosody.noiseChannel ε RSA.BergenGoodman2015.Prosody.Utterance.BOB_went RSA.BergenGoodman2015.Prosody.Utterance.bobWent = ε / 2
• RSA.BergenGoodman2015.Prosody.noiseChannel ε RSA.BergenGoodman2015.Prosody.Utterance.aliceAndBobWent RSA.BergenGoodman2015.Prosody.Utterance.aliceAndBobWent = 1
• RSA.BergenGoodman2015.Prosody.noiseChannel ε x✝¹ x✝ = 0

inductive RSA.BergenGoodman2015.Prosody.Knowledge : Type

Speaker's knowledge state

• full : Knowledge
• incomplete : Knowledge

instance RSA.BergenGoodman2015.Prosody.instDecidableEqKnowledge : DecidableEq Knowledge

Equations

• RSA.BergenGoodman2015.Prosody.instDecidableEqKnowledge x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance RSA.BergenGoodman2015.Prosody.instBEqKnowledge : BEq Knowledge

Equations

• RSA.BergenGoodman2015.Prosody.instBEqKnowledge = { beq := RSA.BergenGoodman2015.Prosody.instBEqKnowledge.beq }

def RSA.BergenGoodman2015.Prosody.instBEqKnowledge.beq : Knowledge → Knowledge → Bool

Equations

• RSA.BergenGoodman2015.Prosody.instBEqKnowledge.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.BergenGoodman2015.Prosody.instReprKnowledge : Repr Knowledge

Equations

• RSA.BergenGoodman2015.Prosody.instReprKnowledge = { reprPrec := RSA.BergenGoodman2015.Prosody.instReprKnowledge.repr }

def RSA.BergenGoodman2015.Prosody.instReprKnowledge.repr : Knowledge → ℕ → Std.Format

Equations

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

def RSA.BergenGoodman2015.Prosody.speakerBelief (k : Knowledge) (m : Meaning) : ℚ

Speaker's belief given observation (for partial knowledge model)

Equations

• RSA.BergenGoodman2015.Prosody.speakerBelief RSA.BergenGoodman2015.Prosody.Knowledge.full m = 1
• RSA.BergenGoodman2015.Prosody.speakerBelief RSA.BergenGoodman2015.Prosody.Knowledge.incomplete RSA.BergenGoodman2015.Prosody.Meaning.onlyBob = 1 / 2
• RSA.BergenGoodman2015.Prosody.speakerBelief RSA.BergenGoodman2015.Prosody.Knowledge.incomplete RSA.BergenGoodman2015.Prosody.Meaning.both = 1 / 2
• RSA.BergenGoodman2015.Prosody.speakerBelief RSA.BergenGoodman2015.Prosody.Knowledge.incomplete RSA.BergenGoodman2015.Prosody.Meaning.onlyAlice = 0

def RSA.BergenGoodman2015.Prosody.L0 (ε : ℚ) (u_p : Utterance) : List (Meaning × ℚ)

L0 with noise

Equations

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

def RSA.BergenGoodman2015.Prosody.S1 (ε : ℚ) (_k : Knowledge) (m : Meaning) : List (Utterance × ℚ)

S1: Speaker choosing utterance given meaning and knowledge

Equations

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

def RSA.BergenGoodman2015.Prosody.L1 (ε : ℚ) (u_p : Utterance) : List (Meaning × ℚ)

L1: Pragmatic listener

Equations

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

def RSA.BergenGoodman2015.Prosody.ε_default : ℚ

Equations

• RSA.BergenGoodman2015.Prosody.ε_default = 1 / 100

def RSA.BergenGoodman2015.Prosody.l1_BOB_went : List (Meaning × ℚ)

Equations

• RSA.BergenGoodman2015.Prosody.l1_BOB_went = RSA.BergenGoodman2015.Prosody.L1 RSA.BergenGoodman2015.Prosody.ε_default RSA.BergenGoodman2015.Prosody.Utterance.BOB_went

def RSA.BergenGoodman2015.Prosody.l1_bob_went : List (Meaning × ℚ)

Equations

• RSA.BergenGoodman2015.Prosody.l1_bob_went = RSA.BergenGoodman2015.Prosody.L1 RSA.BergenGoodman2015.Prosody.ε_default RSA.BergenGoodman2015.Prosody.Utterance.bobWent

theorem RSA.BergenGoodman2015.Prosody.stress_increases_exhaustivity : RSA.BergenGoodman2015.getScore✝ l1_BOB_went Meaning.onlyBob ≥ RSA.BergenGoodman2015.getScore✝¹ l1_bob_went Meaning.onlyBob

Prosody Theorem: Stress increases exhaustive interpretation.

"BOB went" is more likely to mean "only Bob" than "Bob went" (no stress).

theorem RSA.BergenGoodman2015.Prosody.both_compatible : RSA.BergenGoodman2015.getScore✝ l1_BOB_went Meaning.both > 0 ∧ RSA.BergenGoodman2015.getScore✝¹ l1_bob_went Meaning.both > 0

Both utterances are compatible with the "both" meaning

Connection to Other Noise Models

@cite{bergen-goodman-2015} (This File)

• Channel noise: P_N(u_p | u_i)
• Words can be deleted, inserted, replaced
• Noise is in transmission, not semantics
• Prosody reduces channel noise

@cite{degen-etal-2020} (DegenEtAl2020.lean)

• Semantic noise: φ(u, o) ∈ [0,1]
• Feature matching is probabilistic
• Noise is in perception of features
• No explicit channel model

Potential Unification

Could Degen's semantic noise emerge from channel noise?

Hypothesis: If utterances are descriptions of features, and features can be "misheard", then:

• φ(u, o) = E_{u' ~ P_N(·|u)}[[u']]

That is, graded truth = expected Boolean truth over noisy channel.

This would show:

• Degen's continuous φ = Bergen's discrete channel + Boolean semantics
• Similar to: Degen φ = Boolean × noise channel (proven in DegenEtAl2020.lean)

Information-Theoretic View

Both noise models reduce mutual information I(M; U):

• Channel noise: I(U_intended; U_perceived) decreases
• Semantic noise: I(U; O) decreases (less discrimination)

Higher noise → less informative communication → worse utility.

This suggests a unified "informativeness" measure applicable to both.

def RSA.BergenGoodman2015.TheoreticalConnections.channelCapacity (ε : ℚ) (_numUtts : ℕ) : ℚ

Channel noise reduces channel capacity.

With noise rate ε, the mutual information I(U; U') between intended and perceived utterance decreases.

At ε = 0: I(U; U') = H(U) (perfect channel) At ε = 1: I(U; U') = 0 (completely noisy, no information transmitted)

Equations

• RSA.BergenGoodman2015.TheoreticalConnections.channelCapacity ε _numUtts = if ε < 1 then 1 - ε else 0

theorem RSA.BergenGoodman2015.TheoreticalConnections.noise_reduces_capacity (ε₁ ε₂ : ℚ) (h : ε₁ < ε₂) (hε₂ : ε₂ ≤ 1) (n : ℕ) : channelCapacity ε₂ n ≤ channelCapacity ε₁ n

Higher noise → lower capacity

Summary

From the Paper

1. Ellipsis (Section 3)

   • Fragment "Bob" → meaning "Bob went to the movies"
   • Works via noise inference: listener assumes words were deleted
   • fragment_interpretation: proven

2. Prosody (Section 4)

   • Stress reduces noise rate
   • "BOB went" → exhaustive (only Bob)
   • "Bob went" → non-exhaustive (maybe others too)
   • stress_increases_exhaustivity: proven

Innovation

The noisy channel model explains phenomena that standard RSA cannot:

• Fragments have NO literal meaning, yet are interpreted
• Prosody has NO semantic content, yet affects meaning

Both emerge from strategic reasoning about noise.

Relation to @cite{degen-etal-2020}

Property	Bergen & Goodman	Degen et al.
Noise location	Channel	Semantics
Type	P_N(u_p|u_i)	φ(u,o) ∈ [0,1]
Effect	Word corruption	Graded match

Potential unification: semantic noise as expectation over channel noise.