Bergen & Goodman (2015): The strategic use of noise in pragmatic reasoning

This file formalizes Bergen and Goodman's two applications of rational speech acts over a noisy channel from the speaker's intended utterances to the perceived ones: the literal listener decodes the intended utterance before interpreting it (eq. 6), the speaker's utility is the channel-expected log posterior of the intended meaning (eq. 7), and the pragmatic listener inverts the speaker composed with the channel (eq. 8). The channel misperceives each utterance as at most one other, at a rate the speaker lowers by stressing a word (slipChannel). Sentence fragments have no literal meaning, yet both listeners read the fragment "Bob" as the point mass on Bob having gone, at every positive deletion rate (Ellipsis.L0_subject, Ellipsis.L1_subject), because only "Bob went to the movies" deletes to it. Stress halves the rate at which a subject is misheard as the other, so the exponentiated utility of a subject sentence is exp (-binEntropy rate) / 2, and a speaker who knows that only Bob went prefers "BOB went" to "Bob went" (Prosody.S1_bobWent_lt_BOB_went), the form the paper's exhaustive row records (Prosody.model_matches_stress_rows).

Main results

• Ellipsis.L0_subject, Ellipsis.L1_subject — a subject fragment is the point mass on its source, for every positive deletion rate; Ellipsis.S1_apply — the speaker utters the full sentence.
• Prosody.channelMix_eq_exp_neg_binEntropy — a subject sentence's exponentiated utility is exp (-binEntropy rate) / 2.
• Prosody.S1_bobWent_lt_BOB_went — the knowledgeable speaker prefers the stressed form.

Implementation notes

Priors are unit weights, the rationality parameter is 1, and costs are zero. The channel runs from the speaker's intended utterances to the perceived ones: for ellipsis the intended utterances are the three full sentences (the paper's simplification), for prosody all five forms. Prosody is perceived, so the stressed and unstressed forms are two copies of the subject-confusion channel at rates ε / 2 and ε. The prosody speaker is the paper's knowledgeable one, for whom the divergence utility is eq. 7.

TODO

• Fragment production (Fig. 1, right) needs utterance costs; the ignorant speaker's lower stress rate (Fig. 2, right) needs the divergence utility over observations.
• The listener's exhaustive reading of stress (Fig. 2, left) is the paper's depth-two result over knowledge states; at depth one it reduces to the monotonicity in the rate of the confusion odds (r ^ (1 - r) * (1 - r) ^ r) / ((1 - r) ^ (1 - r) * r ^ r), not yet proved.

References

• [BG15]
• [FG12]

The slip channel

noncomputable def BergenGoodman2015.slipChannel {U : Type u_1} [MeasurableSpace U] [Fintype U] [MeasurableSingletonClass U] (rate : U → ℝ) (slip : U → U) : ProbabilityTheory.Kernel U U

Under the channel of a slip rate and a slip target, an intended utterance is perceived intact with probability 1 - rate u and as slip u with probability rate u.

Equations

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

instance BergenGoodman2015.instIsFiniteKernelSlipChannel {U : Type u_1} [MeasurableSpace U] [Fintype U] [MeasurableSingletonClass U] (rate : U → ℝ) (slip : U → U) : ProbabilityTheory.IsFiniteKernel (slipChannel rate slip)

theorem BergenGoodman2015.slipChannel_apply_singleton {U : Type u_1} [MeasurableSpace U] [Fintype U] [MeasurableSingletonClass U] [DecidableEq U] (rate : U → ℝ) (slip : U → U) (u v : U) : ((slipChannel rate slip) u) {v} = (ENNReal.ofReal (1 - rate u) * if u = v then 1 else 0) + ENNReal.ofReal (rate u) * if slip u = v then 1 else 0

Rational speech acts over the channel

The literal listener decodes before interpreting, so the meaning of a perceived utterance is the meaning of each intended one weighted by the utterance prior and the channel (eq. 6). The speaker's informativity is the channel-expected log listener, whose exponential is the listener mass averaged geometrically over perceptions (channelMix), and the speaker is the power-weight best response to that mix (noisySpeaker, eqs. 4 and 7). The pragmatic listener inverts the speaker composed with the channel (eq. 8). At the identity channel each operator is its noiseless counterpart.

noncomputable def BergenGoodman2015.noisyMeaning {W : Type u_1} {I : Type u_2} {U : Type u_3} [MeasurableSpace I] [MeasurableSpace U] (N : ProbabilityTheory.Kernel I U) (ρ : MeasureTheory.Measure I) (m : I → W → ENNReal) (u_p : U) (w : W) : ENNReal

The meaning of a perceived utterance u_p is the meaning of each intended utterance, weighted by the utterance prior and the channel (eq. 6).

Equations

• BergenGoodman2015.noisyMeaning N ρ m u_p w = ∫⁻ (u_i : I), (N u_i) {u_p} * m u_i w ∂ρ

theorem BergenGoodman2015.noisyMeaning_apply {W : Type u_1} {I : Type u_2} {U : Type u_3} [MeasurableSpace I] [MeasurableSpace U] [Fintype I] [MeasurableSingletonClass I] (N : ProbabilityTheory.Kernel I U) (ρ : MeasureTheory.Measure I) (m : I → W → ENNReal) (u_p : U) (w : W) : noisyMeaning N ρ m u_p w = ∑ u_i : I, (N u_i) {u_p} * m u_i w * ρ {u_i}

theorem BergenGoodman2015.noisyMeaning_id {W : Type u_1} {U : Type u_3} [MeasurableSpace U] [Fintype U] [MeasurableSingletonClass U] (ρ : MeasureTheory.Measure U) (m : U → W → ENNReal) (u : U) (w : W) : noisyMeaning ProbabilityTheory.Kernel.id ρ m u w = ρ {u} * m u w

Without noise the perceived utterance is the intended one, weighted by its prior.

noncomputable def BergenGoodman2015.channelMix {W : Type u_1} {I : Type u_2} {U : Type u_3} [MeasurableSpace I] [MeasurableSpace U] [MeasurableSpace W] [Fintype U] (N : ProbabilityTheory.Kernel I U) (L : ProbabilityTheory.Kernel U W) (u_i : I) (w : W) : ENNReal

channelMix N L u_i w averages the listener mass at w geometrically over the perceptions of u_i; it is the exponential of the channel-expected log listener, eq. 7's informativity.

Equations

• BergenGoodman2015.channelMix N L u_i w = ∏ u_p : U, (L u_p) {w} ^ ((N u_i) {u_p}).toReal

theorem BergenGoodman2015.channelMix_eq_prod {W : Type u_1} {I : Type u_2} {U : Type u_3} [MeasurableSpace I] [MeasurableSpace U] [MeasurableSpace W] [Fintype U] (N : ProbabilityTheory.Kernel I U) (L : ProbabilityTheory.Kernel U W) {u_i : I} {s : Finset U} (hs : ∀ u_p ∉ s, (N u_i) {u_p} = 0) (w : W) : channelMix N L u_i w = ∏ u_p ∈ s, (L u_p) {w} ^ ((N u_i) {u_p}).toReal

The mix over the perceptions the channel can produce.

theorem BergenGoodman2015.channelMix_ne_top {W : Type u_1} {I : Type u_2} {U : Type u_3} [MeasurableSpace I] [MeasurableSpace U] [MeasurableSpace W] [Fintype U] (N : ProbabilityTheory.Kernel I U) (L : ProbabilityTheory.Kernel U W) [ProbabilityTheory.IsFiniteKernel L] (u_i : I) (w : W) : channelMix N L u_i w ≠ ⊤

noncomputable def BergenGoodman2015.noisySpeaker {W : Type u_1} {I : Type u_2} {U : Type u_3} [MeasurableSpace I] [MeasurableSpace U] [MeasurableSpace W] [Fintype U] [Fintype I] [Fintype W] [MeasurableSingletonClass W] (N : ProbabilityTheory.Kernel I U) (α : ℝ) (C : I → ℝ) (L : ProbabilityTheory.Kernel U W) : ProbabilityTheory.Kernel W I

The speaker over the channel (eqs. 4 and 7) weights each utterance by the channel-mixed listener to the power α, scaled by the cost weight exp (-(α * C u)).

Equations

• BergenGoodman2015.noisySpeaker N α C L = ProbabilityTheory.Kernel.ofWeights fun (w : W) (u : I) => BergenGoodman2015.channelMix N L u w ^ α * ENNReal.ofReal (Real.exp (-(α * C u)))

@[simp]

theorem BergenGoodman2015.noisySpeaker_apply_singleton {W : Type u_1} {I : Type u_2} {U : Type u_3} [MeasurableSpace I] [MeasurableSpace U] [MeasurableSpace W] [Fintype U] [Fintype I] [MeasurableSingletonClass I] [Fintype W] [MeasurableSingletonClass W] (N : ProbabilityTheory.Kernel I U) (α : ℝ) (C : I → ℝ) (L : ProbabilityTheory.Kernel U W) (w : W) (u : I) : ((noisySpeaker N α C L) w) {u} = channelMix N L u w ^ α * ENNReal.ofReal (Real.exp (-(α * C u))) / ∑ u' : I, channelMix N L u' w ^ α * ENNReal.ofReal (Real.exp (-(α * C u')))

instance BergenGoodman2015.instIsFiniteKernelNoisySpeaker {W : Type u_1} {I : Type u_2} {U : Type u_3} [MeasurableSpace I] [MeasurableSpace U] [MeasurableSpace W] [Fintype U] [Fintype I] [Fintype W] [MeasurableSingletonClass W] (N : ProbabilityTheory.Kernel I U) (α : ℝ) (C : I → ℝ) (L : ProbabilityTheory.Kernel U W) : ProbabilityTheory.IsFiniteKernel (noisySpeaker N α C L)

theorem BergenGoodman2015.noisySpeaker_real_singleton_lt_iff {W : Type u_1} {I : Type u_2} {U : Type u_3} [MeasurableSpace I] [MeasurableSpace U] [MeasurableSpace W] [Fintype U] [Fintype I] [MeasurableSingletonClass I] [Fintype W] [MeasurableSingletonClass W] {N : ProbabilityTheory.Kernel I U} {α : ℝ} (hα : 0 ≤ α) {C : I → ℝ} {L : ProbabilityTheory.Kernel U W} [ProbabilityTheory.IsFiniteKernel L] {w : W} (h0 : ∃ (u : I), channelMix N L u w ^ α * ENNReal.ofReal (Real.exp (-(α * C u))) ≠ 0) {u u' : I} : ((noisySpeaker N α C L) w).real {u} < ((noisySpeaker N α C L) w).real {u'} ↔ channelMix N L u w ^ α * ENNReal.ofReal (Real.exp (-(α * C u))) < channelMix N L u' w ^ α * ENNReal.ofReal (Real.exp (-(α * C u')))

Row preference of the speaker reduces to comparing the weighted channel-mixed listener values; the normalization cancels.

theorem BergenGoodman2015.ofDensity_noisyMeaning_id {W : Type u_1} {U : Type u_3} [MeasurableSpace U] [MeasurableSpace W] [Fintype U] [MeasurableSingletonClass U] (μ : MeasureTheory.Measure W) (ρ : MeasureTheory.Measure U) (m : U → W → ENNReal) {u : U} (h0 : ρ {u} ≠ 0) (htop : ρ {u} ≠ ⊤) : (ProbabilityTheory.Kernel.ofDensity μ (noisyMeaning ProbabilityTheory.Kernel.id ρ m)) u = (ProbabilityTheory.Kernel.ofDensity μ m) u

Without noise the literal listener is the noiseless one at every utterance of positive finite prior mass.

theorem BergenGoodman2015.channelMix_id {W : Type u_1} {U : Type u_3} [MeasurableSpace U] [MeasurableSpace W] [Fintype U] [MeasurableSingletonClass U] (L : ProbabilityTheory.Kernel U W) (u : U) (w : W) : channelMix ProbabilityTheory.Kernel.id L u w = (L u) {w}

theorem BergenGoodman2015.noisySpeaker_id {W : Type u_1} {U : Type u_3} [MeasurableSpace U] [MeasurableSpace W] [Fintype U] [MeasurableSingletonClass U] [Fintype W] [MeasurableSingletonClass W] (α : ℝ) (C : U → ℝ) (L : ProbabilityTheory.Kernel U W) [ProbabilityTheory.IsFiniteKernel L] : noisySpeaker ProbabilityTheory.Kernel.id α C L = RSA.speaker α C (⇑L) MeasureTheory.Measure.dirac

Without noise the speaker is the noiseless one.

theorem BergenGoodman2015.listener_id_comp_noisySpeaker {W : Type u_1} {U : Type u_3} [MeasurableSpace U] [MeasurableSpace W] [Fintype U] [MeasurableSingletonClass U] [Fintype W] [MeasurableSingletonClass W] (α : ℝ) (C : U → ℝ) (L : ProbabilityTheory.Kernel U W) [ProbabilityTheory.IsFiniteKernel L] (μ : MeasureTheory.Measure W) : RSA.listener μ ⇑(ProbabilityTheory.Kernel.id.comp (noisySpeaker ProbabilityTheory.Kernel.id α C L)) = RSA.listener μ ⇑(RSA.speaker α C (⇑L) MeasureTheory.Measure.dirac)

Without noise the pragmatic listener over the channel is the noiseless one.

Ellipsis

Three meanings and the full sentences expressing them; deletion strikes the predicate, leaving a subject fragment with no literal meaning.

inductive BergenGoodman2015.Ellipsis.Meaning : Type

Who went to the movies.

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

@[instance_reducible]

instance BergenGoodman2015.Ellipsis.instDecidableEqMeaning : DecidableEq Meaning

Equations

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

@[instance_reducible]

instance BergenGoodman2015.Ellipsis.instFintypeMeaning : Fintype Meaning

Equations

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

@[instance_reducible]

instance BergenGoodman2015.Ellipsis.instInhabitedMeaning : Inhabited Meaning

Equations

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

@[instance_reducible]

instance BergenGoodman2015.Ellipsis.instMeasurableSpaceMeaning : MeasurableSpace Meaning

Equations

• BergenGoodman2015.Ellipsis.instMeasurableSpaceMeaning = ⊤

inductive BergenGoodman2015.Ellipsis.Utterance : Type

The utterances are the full sentences and the fragments deletion leaves, a subject alone or the predicate.

• full (m : Meaning) : Utterance
• subject (m : Meaning) : Utterance
• predicate : Utterance

def BergenGoodman2015.Ellipsis.instDecidableEqUtterance.decEq (x✝ x✝¹ : Utterance) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• BergenGoodman2015.Ellipsis.instDecidableEqUtterance.decEq (BergenGoodman2015.Ellipsis.Utterance.full m) (BergenGoodman2015.Ellipsis.Utterance.subject m_1) = isFalse ⋯
• BergenGoodman2015.Ellipsis.instDecidableEqUtterance.decEq (BergenGoodman2015.Ellipsis.Utterance.full m) BergenGoodman2015.Ellipsis.Utterance.predicate = isFalse ⋯
• BergenGoodman2015.Ellipsis.instDecidableEqUtterance.decEq (BergenGoodman2015.Ellipsis.Utterance.subject m) (BergenGoodman2015.Ellipsis.Utterance.full m_1) = isFalse ⋯
• BergenGoodman2015.Ellipsis.instDecidableEqUtterance.decEq (BergenGoodman2015.Ellipsis.Utterance.subject m) BergenGoodman2015.Ellipsis.Utterance.predicate = isFalse ⋯
• BergenGoodman2015.Ellipsis.instDecidableEqUtterance.decEq BergenGoodman2015.Ellipsis.Utterance.predicate (BergenGoodman2015.Ellipsis.Utterance.full m) = isFalse ⋯
• BergenGoodman2015.Ellipsis.instDecidableEqUtterance.decEq BergenGoodman2015.Ellipsis.Utterance.predicate (BergenGoodman2015.Ellipsis.Utterance.subject m) = isFalse ⋯
• BergenGoodman2015.Ellipsis.instDecidableEqUtterance.decEq BergenGoodman2015.Ellipsis.Utterance.predicate BergenGoodman2015.Ellipsis.Utterance.predicate = isTrue ⋯

@[instance_reducible]

instance BergenGoodman2015.Ellipsis.instDecidableEqUtterance : DecidableEq Utterance

Equations

• BergenGoodman2015.Ellipsis.instDecidableEqUtterance = BergenGoodman2015.Ellipsis.instDecidableEqUtterance.decEq

@[instance_reducible]

instance BergenGoodman2015.Ellipsis.instFintypeUtterance : Fintype Utterance

Equations

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

@[instance_reducible]

instance BergenGoodman2015.Ellipsis.instMeasurableSpaceUtterance : MeasurableSpace Utterance

Equations

• BergenGoodman2015.Ellipsis.instMeasurableSpaceUtterance = ⊤

def BergenGoodman2015.Ellipsis.lit : Utterance → Set Meaning

Full sentences mean what they say; fragments have no literal meaning.

Equations

• BergenGoodman2015.Ellipsis.lit (BergenGoodman2015.Ellipsis.Utterance.full m) = {m}
• BergenGoodman2015.Ellipsis.lit x✝ = ∅

noncomputable def BergenGoodman2015.Ellipsis.rate (δ : ℝ) : Utterance → ℝ

Deletion strikes the predicate of a full sentence at rate δ.

Equations

• BergenGoodman2015.Ellipsis.rate δ (BergenGoodman2015.Ellipsis.Utterance.full m) = δ
• BergenGoodman2015.Ellipsis.rate δ x✝ = 0

def BergenGoodman2015.Ellipsis.slip : Utterance → Utterance

Deleting the predicate leaves the subject.

Equations

• BergenGoodman2015.Ellipsis.slip (BergenGoodman2015.Ellipsis.Utterance.full m) = BergenGoodman2015.Ellipsis.Utterance.subject m
• BergenGoodman2015.Ellipsis.slip x✝ = x✝

@[reducible, inline]

noncomputable abbrev BergenGoodman2015.Ellipsis.N (δ : ℝ) : ProbabilityTheory.Kernel Meaning Utterance

The deletion channel at rate δ, from the speaker's full sentences, indexed by the meaning they express, to the perceived utterances.

Equations

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

@[reducible, inline]

noncomputable abbrev BergenGoodman2015.Ellipsis.uttPrior : MeasureTheory.Measure Meaning

The speaker's full sentences are equally likely.

Equations

• BergenGoodman2015.Ellipsis.uttPrior = MeasureTheory.Measure.count

@[reducible, inline]

noncomputable abbrev BergenGoodman2015.Ellipsis.μ : MeasureTheory.Measure Meaning

The uniform meaning prior.

Equations

• BergenGoodman2015.Ellipsis.μ = MeasureTheory.Measure.count

@[reducible, inline]

noncomputable abbrev BergenGoodman2015.Ellipsis.lit' : Meaning → Meaning → ENNReal

The graded literal meaning of a full sentence.

Equations

• BergenGoodman2015.Ellipsis.lit' m = (BergenGoodman2015.Ellipsis.lit (BergenGoodman2015.Ellipsis.Utterance.full m)).indicator 1

@[reducible, inline]

noncomputable abbrev BergenGoodman2015.Ellipsis.L0 (δ : ℝ) : ProbabilityTheory.Kernel Utterance Meaning

The literal listener (eq. 6).

Equations

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

@[reducible, inline]

noncomputable abbrev BergenGoodman2015.Ellipsis.S1 (δ : ℝ) : ProbabilityTheory.Kernel Meaning Meaning

The speaker (eq. 7), choosing among the full sentences.

Equations

• BergenGoodman2015.Ellipsis.S1 δ = BergenGoodman2015.noisySpeaker (BergenGoodman2015.Ellipsis.N δ) 1 0 (BergenGoodman2015.Ellipsis.L0 δ)

@[reducible, inline]

noncomputable abbrev BergenGoodman2015.Ellipsis.L1 (δ : ℝ) : ProbabilityTheory.Kernel Utterance Meaning

The pragmatic listener (eq. 8).

Equations

• BergenGoodman2015.Ellipsis.L1 δ = RSA.listener BergenGoodman2015.Ellipsis.μ ⇑((BergenGoodman2015.Ellipsis.N δ).comp (BergenGoodman2015.Ellipsis.S1 δ))

theorem BergenGoodman2015.Ellipsis.noisyMeaning_subject {δ : ℝ} (m w : Meaning) : noisyMeaning (N δ) uttPrior lit' (Utterance.subject m) w = ENNReal.ofReal δ * {m}.indicator 1 w

Only the full sentence for m deletes to its subject fragment.

theorem BergenGoodman2015.Ellipsis.noisyMeaning_full {δ : ℝ} (m w : Meaning) : noisyMeaning (N δ) uttPrior lit' (Utterance.full m) w = ENNReal.ofReal (1 - δ) * {m}.indicator 1 w

Only the full sentence for m survives as itself.

theorem BergenGoodman2015.Ellipsis.L0_subject {δ : ℝ} (m : Meaning) (hδ : 0 < δ) : (L0 δ) (Utterance.subject m) = MeasureTheory.Measure.dirac m

A subject fragment is the point mass on the meaning whose full sentence deletes to it, at every positive deletion rate.

theorem BergenGoodman2015.Ellipsis.L0_full {δ : ℝ} (m : Meaning) (hδ : δ < 1) : (L0 δ) (Utterance.full m) = MeasureTheory.Measure.dirac m

A full sentence is interpreted literally, at every deletion rate below 1.

theorem BergenGoodman2015.Ellipsis.channelMix_full {δ : ℝ} (m : Meaning) (hδ₀ : 0 < δ) (hδ₁ : δ < 1) (m' : Meaning) : channelMix (N δ) (L0 δ) m' m = if m' = m then 1 else 0

The full sentence for m' is heard as itself or as its subject, so its channel-mixed listener at m is 1 when m' = m and 0 otherwise.

theorem BergenGoodman2015.Ellipsis.S1_apply {δ : ℝ} (m : Meaning) (hδ₀ : 0 < δ) (hδ₁ : δ < 1) : (S1 δ) m = MeasureTheory.Measure.dirac m

The speaker utters the full sentence for its meaning.

theorem BergenGoodman2015.Ellipsis.comp_apply_subject {δ : ℝ} (m : Meaning) (hδ₀ : 0 < δ) (hδ₁ : δ < 1) (w : Meaning) : (((N δ).comp (S1 δ)) w) {Utterance.subject m} = if w = m then ENNReal.ofReal δ else 0

The channelled speaker reaches the subject fragment for m only from m, with the deletion rate.

theorem BergenGoodman2015.Ellipsis.L1_subject {δ : ℝ} (m : Meaning) (hδ₀ : 0 < δ) (hδ₁ : δ < 1) : (L1 δ) (Utterance.subject m) = MeasureTheory.Measure.dirac m

The pragmatic listener also reads a subject fragment as the point mass on its source.

Prosody

Stress halves the rate at which a subject is misheard as the other (the paper's ε / n at n = 2); the conjunction is never misheard. A speaker who knows that only Bob went must keep the listener from hearing "Alice went", so stress is worth more to them.

inductive BergenGoodman2015.Prosody.Meaning : Type

Either one of Alice and Bob went alone, or both went.

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

@[instance_reducible]

instance BergenGoodman2015.Prosody.instDecidableEqMeaning : DecidableEq Meaning

Equations

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

@[instance_reducible]

instance BergenGoodman2015.Prosody.instFintypeMeaning : Fintype Meaning

Equations

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

@[instance_reducible]

instance BergenGoodman2015.Prosody.instInhabitedMeaning : Inhabited Meaning

Equations

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

@[instance_reducible]

instance BergenGoodman2015.Prosody.instMeasurableSpaceMeaning : MeasurableSpace Meaning

Equations

• BergenGoodman2015.Prosody.instMeasurableSpaceMeaning = ⊤

inductive BergenGoodman2015.Prosody.Utterance : Type

The subject sentences, stressed (capitals) or not, and the conjunction.

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

@[instance_reducible]

instance BergenGoodman2015.Prosody.instDecidableEqUtterance : DecidableEq Utterance

Equations

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

@[instance_reducible]

instance BergenGoodman2015.Prosody.instFintypeUtterance : Fintype Utterance

Equations

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

@[instance_reducible]

instance BergenGoodman2015.Prosody.instMeasurableSpaceUtterance : MeasurableSpace Utterance

Equations

• BergenGoodman2015.Prosody.instMeasurableSpaceUtterance = ⊤

def BergenGoodman2015.Prosody.lit : Utterance → Set Meaning

Literal meanings are lower-bounded, so "Alice went" is true whenever Alice went.

Equations

• BergenGoodman2015.Prosody.lit BergenGoodman2015.Prosody.Utterance.aliceWent = {BergenGoodman2015.Prosody.Meaning.onlyAlice, BergenGoodman2015.Prosody.Meaning.both}
• BergenGoodman2015.Prosody.lit BergenGoodman2015.Prosody.Utterance.ALICE_went = {BergenGoodman2015.Prosody.Meaning.onlyAlice, BergenGoodman2015.Prosody.Meaning.both}
• BergenGoodman2015.Prosody.lit BergenGoodman2015.Prosody.Utterance.bobWent = {BergenGoodman2015.Prosody.Meaning.onlyBob, BergenGoodman2015.Prosody.Meaning.both}
• BergenGoodman2015.Prosody.lit BergenGoodman2015.Prosody.Utterance.BOB_went = {BergenGoodman2015.Prosody.Meaning.onlyBob, BergenGoodman2015.Prosody.Meaning.both}
• BergenGoodman2015.Prosody.lit BergenGoodman2015.Prosody.Utterance.aliceAndBobWent = {BergenGoodman2015.Prosody.Meaning.both}

noncomputable def BergenGoodman2015.Prosody.rate (ε : ℝ) : Utterance → ℝ

Subjects are confused at rate ε, halved under stress; the conjunction is safe.

Equations

• BergenGoodman2015.Prosody.rate ε BergenGoodman2015.Prosody.Utterance.aliceWent = ε
• BergenGoodman2015.Prosody.rate ε BergenGoodman2015.Prosody.Utterance.bobWent = ε
• BergenGoodman2015.Prosody.rate ε BergenGoodman2015.Prosody.Utterance.ALICE_went = ε / 2
• BergenGoodman2015.Prosody.rate ε BergenGoodman2015.Prosody.Utterance.BOB_went = ε / 2
• BergenGoodman2015.Prosody.rate ε BergenGoodman2015.Prosody.Utterance.aliceAndBobWent = 0

def BergenGoodman2015.Prosody.slip : Utterance → Utterance

A subject is misheard as the other subject, with its prosody.

Equations

• BergenGoodman2015.Prosody.slip BergenGoodman2015.Prosody.Utterance.aliceWent = BergenGoodman2015.Prosody.Utterance.bobWent
• BergenGoodman2015.Prosody.slip BergenGoodman2015.Prosody.Utterance.bobWent = BergenGoodman2015.Prosody.Utterance.aliceWent
• BergenGoodman2015.Prosody.slip BergenGoodman2015.Prosody.Utterance.ALICE_went = BergenGoodman2015.Prosody.Utterance.BOB_went
• BergenGoodman2015.Prosody.slip BergenGoodman2015.Prosody.Utterance.BOB_went = BergenGoodman2015.Prosody.Utterance.ALICE_went
• BergenGoodman2015.Prosody.slip BergenGoodman2015.Prosody.Utterance.aliceAndBobWent = BergenGoodman2015.Prosody.Utterance.aliceAndBobWent

@[reducible, inline]

noncomputable abbrev BergenGoodman2015.Prosody.N (ε : ℝ) : ProbabilityTheory.Kernel Utterance Utterance

The subject-confusion channel at rate ε.

Equations

• BergenGoodman2015.Prosody.N ε = BergenGoodman2015.slipChannel (BergenGoodman2015.Prosody.rate ε) BergenGoodman2015.Prosody.slip

@[reducible, inline]

noncomputable abbrev BergenGoodman2015.Prosody.uttPrior : MeasureTheory.Measure Utterance

The uniform utterance prior.

Equations

• BergenGoodman2015.Prosody.uttPrior = MeasureTheory.Measure.count

@[reducible, inline]

noncomputable abbrev BergenGoodman2015.Prosody.μ : MeasureTheory.Measure Meaning

The uniform meaning prior.

Equations

• BergenGoodman2015.Prosody.μ = MeasureTheory.Measure.count

@[reducible, inline]

noncomputable abbrev BergenGoodman2015.Prosody.lit' : Utterance → Meaning → ENNReal

The graded literal meaning.

Equations

• BergenGoodman2015.Prosody.lit' u = (BergenGoodman2015.Prosody.lit u).indicator 1

@[reducible, inline]

noncomputable abbrev BergenGoodman2015.Prosody.L0 (ε : ℝ) : ProbabilityTheory.Kernel Utterance Meaning

The literal listener (eq. 6).

Equations

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

@[reducible, inline]

noncomputable abbrev BergenGoodman2015.Prosody.S1 (ε : ℝ) : ProbabilityTheory.Kernel Meaning Utterance

The knowledgeable speaker (eq. 7), over all five forms.

Equations

• BergenGoodman2015.Prosody.S1 ε = BergenGoodman2015.noisySpeaker (BergenGoodman2015.Prosody.N ε) 1 0 (BergenGoodman2015.Prosody.L0 ε)

theorem BergenGoodman2015.Prosody.rpow_mul_rpow_eq_exp_neg_binEntropy {r : ℝ} (hr₀ : 0 < r) (hr₁ : r < 1) : ((1 - r) / 2) ^ (1 - r) * (r / 2) ^ r = Real.exp (-Real.binEntropy r) / 2

By eq. 7, the exponentiated utility of a subject sentence at slip rate r for the meaning it is true of alone is exp (-binEntropy r) / 2.

theorem BergenGoodman2015.Prosody.channelMix_eq_exp_neg_binEntropy {ε : ℝ} (hε₀ : 0 < ε) (hε₁ : ε < 1) : channelMix (N ε) (L0 ε) Utterance.bobWent Meaning.onlyBob = ENNReal.ofReal (Real.exp (-Real.binEntropy ε) / 2) ∧ channelMix (N ε) (L0 ε) Utterance.BOB_went Meaning.onlyBob = ENNReal.ofReal (Real.exp (-Real.binEntropy (ε / 2)) / 2)

The knowledgeable speaker's channel-mixed listener for the two forms of "Bob went" is the entropy form of their rates.

theorem BergenGoodman2015.Prosody.S1_bobWent_lt_BOB_went {ε : ℝ} (hε₀ : 0 < ε) (hε : ε ≤ 1 / 2) : ((S1 ε) Meaning.onlyBob).real {Utterance.bobWent} < ((S1 ε) Meaning.onlyBob).real {Utterance.BOB_went}

A speaker who knows that only Bob went prefers "BOB went" to "Bob went", since halving the rate lowers its binary entropy (Fig. 2, right, at depth one).

def BergenGoodman2015.Prosody.uttOf (row : Datum) : Option Utterance

uttOf reads a row's stress feature as an utterance.

Equations

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

theorem BergenGoodman2015.Prosody.model_matches_stress_rows : ∃ (u_s : Utterance) (u_u : Utterance), uttOf Examples.stressed_subject = some u_s ∧ uttOf Examples.unstressed_subject = some u_u ∧ ((S1 (1 / 100)) Meaning.onlyBob).real {u_u} < ((S1 (1 / 100)) Meaning.onlyBob).real {u_s}

A speaker with the exhaustive meaning prefers the stressed row's form to the unstressed row's, at the paper's rate.