He, Kaiser and Iskarous (2025): Modeling sentence polarity asymmetries

This file formalizes the rational speech act models of He, Kaiser and Iskarous for a speaker who says of a whole that it has a part, that it lacks it, or nothing. Setting.speaker is the standard speaker of (1)–(4) on the kernel pipeline of RSA.speaker, under the Boolean meaning of (2) or the fuzzy meaning fuzzy of (11)–(13), whose positive sentence holds at its state to a sigmoid degree of that state's prior. Setting.wonkyListener is the wonky-world listener of (14)–(16), who infers the state together with the world, normal at the measured prior or wonky at the uniform one, with Setting.wonkiness its posterior probability of the wonky world and the expected typicality of (17) the marginal of the state over the worlds; the funky model of (18)–(22) is the same listener under the fuzzy meaning.

Under the Boolean meaning the likelihood of each polarity is a logistic function of the cost saved by silence and the log prior of its state (Setting.likelihood_boolean): it falls as the prior rises, and at equal priors the positive polarity is the likelier exactly when it is the cheaper, the two coinciding at equal costs. The fuzzy positive sentence informs the literal listener exactly when its degree exceeds one half, which the sigmoid degree does above a threshold prior; below it the speaker prefers silence to the positive sentence, where the Boolean speaker prefers the sentence at every prior below the exponential of the cost saved. The wonky listener's wonkiness rises above its prior exactly when the described state's prior exceeds one half, whatever the costs, and its expected typicality moves the state's prior toward one half by the wonkiness.

Implementation notes

• The sigmoid of (13) in the wonky world takes that world's prior of the positive state, one half; the paper does not say which prior it takes there.
• The wonkiness of the Boolean wonky listener depends on the polarity only through the cost (Setting.wonkiness_boolean), so the polarities coincide at equal costs; the paper's costs differ, and its remark that the model does not differentiate the polarities holds of the direction of the wonkiness update, not of its size.

TODO

• The best-fit predictions of Figures 4, 5 and 7 and the mean squared errors of §4.2 and §5.2.
• The funky listener's typicality difference between the polarities (§6.2).

References

• [HKI25]
• [FG12]
• [DTG15]
• [CWS23]
• [DHG+20]
• [Hor89]

States, utterances and meanings

inductive HeKaiserIskarous2025.State : Type

In one state the whole has the part, in the other it lacks it.

• pos : State
• neg : State

@[instance_reducible]

instance HeKaiserIskarous2025.instDecidableEqState : DecidableEq State

Equations

• HeKaiserIskarous2025.instDecidableEqState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HeKaiserIskarous2025.instFintypeState : Fintype State

Equations

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

instance HeKaiserIskarous2025.instNonemptyState : Nonempty State

@[instance_reducible]

instance HeKaiserIskarous2025.instMeasurableSpaceState : MeasurableSpace State

Equations

• HeKaiserIskarous2025.instMeasurableSpaceState = ⊤

inductive HeKaiserIskarous2025.Utterance : Type

The speaker says the positive sentence, its negation, or nothing.

• pos : Utterance
• neg : Utterance
• null : Utterance

@[instance_reducible]

instance HeKaiserIskarous2025.instDecidableEqUtterance : DecidableEq Utterance

Equations

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

@[instance_reducible]

instance HeKaiserIskarous2025.instFintypeUtterance : Fintype Utterance

Equations

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

instance HeKaiserIskarous2025.instNonemptyUtterance : Nonempty Utterance

@[instance_reducible]

instance HeKaiserIskarous2025.instMeasurableSpaceUtterance : MeasurableSpace Utterance

Equations

• HeKaiserIskarous2025.instMeasurableSpaceUtterance = ⊤

def HeKaiserIskarous2025.State.utterance : State → Utterance

A state is described by the sentence of its polarity.

Equations

• HeKaiserIskarous2025.State.pos.utterance = HeKaiserIskarous2025.Utterance.pos
• HeKaiserIskarous2025.State.neg.utterance = HeKaiserIskarous2025.Utterance.neg

theorem HeKaiserIskarous2025.sum_state {β : Type u_1} [AddCommMonoid β] (f : State → β) : ∑ st : State, f st = f State.pos + f State.neg

@[reducible, inline]

abbrev HeKaiserIskarous2025.Meaning : Type

A graded meaning gives the degree to which an utterance holds at a state.

Equations

• HeKaiserIskarous2025.Meaning = (HeKaiserIskarous2025.Utterance → HeKaiserIskarous2025.State → ℝ)

def HeKaiserIskarous2025.boolean : Meaning

Under the Boolean meaning of (2), each sentence holds at its state alone and silence everywhere.

Equations

• HeKaiserIskarous2025.boolean HeKaiserIskarous2025.Utterance.pos HeKaiserIskarous2025.State.pos = 1
• HeKaiserIskarous2025.boolean HeKaiserIskarous2025.Utterance.pos HeKaiserIskarous2025.State.neg = 0
• HeKaiserIskarous2025.boolean HeKaiserIskarous2025.Utterance.neg HeKaiserIskarous2025.State.neg = 1
• HeKaiserIskarous2025.boolean HeKaiserIskarous2025.Utterance.neg HeKaiserIskarous2025.State.pos = 0
• HeKaiserIskarous2025.boolean HeKaiserIskarous2025.Utterance.null x✝ = 1

def HeKaiserIskarous2025.fuzzy (n σ : ℝ) : Meaning

Under the fuzzy meaning of (11) and (12), the negative sentence holds at its state to the degree n and the positive sentence to the degree σ, each to the complementary degree at the other state, and silence holds everywhere.

Equations

• HeKaiserIskarous2025.fuzzy n σ HeKaiserIskarous2025.Utterance.pos HeKaiserIskarous2025.State.pos = σ
• HeKaiserIskarous2025.fuzzy n σ HeKaiserIskarous2025.Utterance.pos HeKaiserIskarous2025.State.neg = 1 - σ
• HeKaiserIskarous2025.fuzzy n σ HeKaiserIskarous2025.Utterance.neg HeKaiserIskarous2025.State.neg = n
• HeKaiserIskarous2025.fuzzy n σ HeKaiserIskarous2025.Utterance.neg HeKaiserIskarous2025.State.pos = 1 - n
• HeKaiserIskarous2025.fuzzy n σ HeKaiserIskarous2025.Utterance.null x✝ = 1

theorem HeKaiserIskarous2025.boolean_nonneg (u : Utterance) (st : State) : 0 ≤ boolean u st

theorem HeKaiserIskarous2025.fuzzy_nonneg {n σ : ℝ} (hn0 : 0 ≤ n) (hn1 : n ≤ 1) (hσ0 : 0 ≤ σ) (hσ1 : σ ≤ 1) (u : Utterance) (st : State) : 0 ≤ fuzzy n σ u st

theorem HeKaiserIskarous2025.fuzzy_one_one : fuzzy 1 1 = boolean

The Boolean meaning is the fuzzy meaning of full degrees.

structure HeKaiserIskarous2025.Sigmoid : Type

The sigmoid of (13) has a height, a steepness, a midpoint and an offset.

• L : ℝ

  The height.

• k : ℝ

  The steepness.

• x0 : ℝ

  The midpoint.

• c : ℝ

  The offset.

noncomputable def HeKaiserIskarous2025.Sigmoid.eval (θ : Sigmoid) (x : ℝ) : ℝ

The sigmoid of (13) gives the degree of the positive sentence at its state as a function of that state's prior.

Equations

• θ.eval x = θ.L * (θ.k * (x - θ.x0)).sigmoid + θ.c

noncomputable def HeKaiserIskarous2025.Sigmoid.threshold (θ : Sigmoid) : ℝ

The prior below which the sigmoid degree is below one half.

Equations

• θ.threshold = θ.x0 + Real.log ((1 / 2 - θ.c) / (θ.L + θ.c - 1 / 2)) / θ.k

theorem HeKaiserIskarous2025.Sigmoid.eval_lt_half_iff (θ : Sigmoid) (hk : 0 < θ.k) (hL : 0 < θ.L) (hc : θ.c < 1 / 2) (hLc : 1 / 2 < θ.L + θ.c) (x : ℝ) : θ.eval x < 1 / 2 ↔ x < θ.threshold

A rising sigmoid whose range straddles one half is below one half exactly below its threshold prior.

noncomputable def HeKaiserIskarous2025.bestFit : Sigmoid

The best-fit sigmoid of §4.2.

Equations

• HeKaiserIskarous2025.bestFit = { L := 7 / 10, k := 6, x0 := 7 / 20, c := 3 / 10 }

noncomputable def HeKaiserIskarous2025.bestFitNeg : ℝ

The best-fit degree of the negative sentence at its state, §4.2.

Equations

• HeKaiserIskarous2025.bestFitNeg = 4 / 5

theorem HeKaiserIskarous2025.bestFit_threshold : bestFit.threshold = 7 / 20 - Real.log (5 / 2) / 6

The threshold prior of the best-fit sigmoid, about 0.197.

Priors and costs

structure HeKaiserIskarous2025.Setting : Type

A model is fixed by the prior probability of the positive state, the rationality α, and the costs.

• p : ℝ

  The prior probability of the positive state.

• α : ℝ

  The rationality.

• cost : Utterance → ℝ

  The cost of an utterance.

• p_pos : 0 < self.p

  The positive state is possible.

• p_lt_one : self.p < 1

  The negative state is possible.

• α_pos : 0 < self.α

  The rationality is positive.

noncomputable def HeKaiserIskarous2025.markednessCost : Utterance → ℝ

In §3.2 silence is free, the positive sentence costs one and its negation two, the marked form being the costlier.

Equations

• HeKaiserIskarous2025.markednessCost HeKaiserIskarous2025.Utterance.pos = 1
• HeKaiserIskarous2025.markednessCost HeKaiserIskarous2025.Utterance.neg = 2
• HeKaiserIskarous2025.markednessCost HeKaiserIskarous2025.Utterance.null = 0

def HeKaiserIskarous2025.Setting.statePrior (s : Setting) : State → ℝ

The prior probability of a state.

Equations

• s.statePrior HeKaiserIskarous2025.State.pos = s.p
• s.statePrior HeKaiserIskarous2025.State.neg = 1 - s.p

theorem HeKaiserIskarous2025.Setting.statePrior_pos (s : Setting) (st : State) : 0 < s.statePrior st

noncomputable def HeKaiserIskarous2025.Setting.prior (s : Setting) : MeasureTheory.Measure State

The measured prior over states.

Equations

• s.prior = ∑ st : HeKaiserIskarous2025.State, ENNReal.ofReal (s.statePrior st) • MeasureTheory.Measure.dirac st

theorem HeKaiserIskarous2025.Setting.prior_apply_singleton (s : Setting) (st : State) : s.prior {st} = ENNReal.ofReal (s.statePrior st)

theorem HeKaiserIskarous2025.Setting.prior_real_singleton (s : Setting) (st : State) : s.prior.real {st} = s.statePrior st

theorem HeKaiserIskarous2025.Setting.prior_ne_zero (s : Setting) (st : State) : s.prior {st} ≠ 0

instance HeKaiserIskarous2025.Setting.instIsProbabilityMeasureStatePrior (s : Setting) : MeasureTheory.IsProbabilityMeasure s.prior

The literal listener and the speaker, (1) to (3)

noncomputable def HeKaiserIskarous2025.L0 (P : MeasureTheory.Measure State) (m : Meaning) : ProbabilityTheory.Kernel Utterance State

The literal listener of (1) reweights the prior by the meaning.

Equations

• HeKaiserIskarous2025.L0 P m = ProbabilityTheory.Kernel.ofDensity P fun (u : HeKaiserIskarous2025.Utterance) (st : HeKaiserIskarous2025.State) => ENNReal.ofReal (m u st)

instance HeKaiserIskarous2025.instIsFiniteKernelUtteranceStateL0 (P : MeasureTheory.Measure State) (m : Meaning) : ProbabilityTheory.IsFiniteKernel (L0 P m)

theorem HeKaiserIskarous2025.L0_ne_top (P : MeasureTheory.Measure State) (m : Meaning) (u : Utterance) (st : State) : ((L0 P m) u) {st} ≠ ⊤

theorem HeKaiserIskarous2025.L0_eq_zero (P : MeasureTheory.Measure State) (m : Meaning) {u : Utterance} {st : State} (h : m u st = 0) : ((L0 P m) u) {st} = 0

theorem HeKaiserIskarous2025.L0_ne_zero (P : MeasureTheory.Measure State) (m : Meaning) [MeasureTheory.IsFiniteMeasure P] {u : Utterance} {st : State} (h : 0 < m u st) (hst : P {st} ≠ 0) : ((L0 P m) u) {st} ≠ 0

theorem HeKaiserIskarous2025.L0_real (P : MeasureTheory.Measure State) (m : Meaning) [MeasureTheory.IsFiniteMeasure P] (hm : ∀ (u : Utterance) (st : State), 0 ≤ m u st) (u : Utterance) (st : State) : (((L0 P m) u) {st}).toReal = m u st * P.real {st} / ∑ st' : State, m u st' * P.real {st'}

On reals, the literal listener at a state is the prior weighted by the meaning, normalized over the row.

noncomputable def HeKaiserIskarous2025.speaker (P : MeasureTheory.Measure State) (m : Meaning) (s : Setting) : ProbabilityTheory.Kernel State Utterance

The speaker of (3) is the softmax of the literal listener's log probability less the cost, scaled by the rationality.

Equations

• HeKaiserIskarous2025.speaker P m s = RSA.speaker s.α s.cost (⇑(HeKaiserIskarous2025.L0 P m)) MeasureTheory.Measure.dirac

instance HeKaiserIskarous2025.instIsFiniteKernelStateUtteranceSpeaker (P : MeasureTheory.Measure State) (m : Meaning) (s : Setting) : ProbabilityTheory.IsFiniteKernel (speaker P m s)

theorem HeKaiserIskarous2025.speaker_eq_zero (P : MeasureTheory.Measure State) (m : Meaning) (s : Setting) {u : Utterance} {st : State} (h : m u st = 0) : ((speaker P m s) st) {u} = 0

An utterance not holding at a state is never used there.

theorem HeKaiserIskarous2025.speaker_real_eq_zero (P : MeasureTheory.Measure State) (m : Meaning) (s : Setting) {u : Utterance} {st : State} (h : m u st = 0) : ((speaker P m s) st).real {u} = 0

theorem HeKaiserIskarous2025.speaker_ne_zero (P : MeasureTheory.Measure State) (m : Meaning) (s : Setting) [MeasureTheory.IsFiniteMeasure P] {u : Utterance} {st : State} (h : 0 < m u st) (hst : P {st} ≠ 0) : ((speaker P m s) st) {u} ≠ 0

An utterance holding at a state is used there.

theorem HeKaiserIskarous2025.speaker_real_pos (P : MeasureTheory.Measure State) (m : Meaning) (s : Setting) [MeasureTheory.IsFiniteMeasure P] {u : Utterance} {st : State} (h : 0 < m u st) (hst : P {st} ≠ 0) : 0 < ((speaker P m s) st).real {u}

theorem HeKaiserIskarous2025.speaker_real_lt_iff (P : MeasureTheory.Measure State) (m : Meaning) (s : Setting) [MeasureTheory.IsFiniteMeasure P] {u v : Utterance} {st : State} (hu : 0 < m u st) (hv : 0 < m v st) (hst : P {st} ≠ 0) : ((speaker P m s) st).real {u} < ((speaker P m s) st).real {v} ↔ Real.log (((L0 P m) u) {st}).toReal - s.cost u < Real.log (((L0 P m) v) {st}).toReal - s.cost v

Between two utterances holding at a state, the speaker prefers the one of higher utility.

theorem HeKaiserIskarous2025.speaker_real_of_pair (P : MeasureTheory.Measure State) (m : Meaning) (s : Setting) [MeasureTheory.IsFiniteMeasure P] (hm : ∀ (u : Utterance) (st : State), 0 ≤ m u st) {u v : Utterance} {st : State} (huv : u ≠ v) (hu : 0 < m u st) (hv : 0 < m v st) (hsupp : ∀ (x : Utterance), 0 < m x st → x = u ∨ x = v) (hst : P {st} ≠ 0) : ((speaker P m s) st).real {u} = (s.α * (Real.log (((L0 P m) u) {st}).toReal - s.cost u - (Real.log (((L0 P m) v) {st}).toReal - s.cost v))).sigmoid

When exactly two utterances hold at a state, the speaker's use of one is the logistic function of the scaled utility difference.

Closed forms under the Boolean meaning

theorem HeKaiserIskarous2025.L0_null_real (P : MeasureTheory.Measure State) [MeasureTheory.IsProbabilityMeasure P] (m : Meaning) (hm : ∀ (u : Utterance) (st : State), 0 ≤ m u st) (hnull : ∀ (st : State), m Utterance.null st = 1) (st : State) : (((L0 P m) Utterance.null) {st}).toReal = P.real {st}

Silence leaves the literal listener at the prior, under any meaning where it holds everywhere.

theorem HeKaiserIskarous2025.L0_boolean_utterance_real (P : MeasureTheory.Measure State) [MeasureTheory.IsProbabilityMeasure P] (hP : ∀ (st : State), P {st} ≠ 0) (st : State) : (((L0 P boolean) st.utterance) {st}).toReal = 1

The sentence of a state puts the Boolean literal listener at that state.

theorem HeKaiserIskarous2025.speaker_boolean_real (P : MeasureTheory.Measure State) [MeasureTheory.IsProbabilityMeasure P] (hP : ∀ (st : State), P {st} ≠ 0) (s : Setting) (st : State) : ((speaker P boolean s) st).real {st.utterance} = (s.α * (s.cost Utterance.null - s.cost st.utterance - Real.log (P.real {st}))).sigmoid

The Boolean speaker uses a state's sentence at that state with the logistic function of the cost saved by silence less the log prior of the state, scaled by the rationality.

The standard model (§3.2) and the fuzzy model (§4)

@[reducible, inline]

noncomputable abbrev HeKaiserIskarous2025.Setting.speaker (s : Setting) (m : Meaning) : ProbabilityTheory.Kernel State Utterance

The speaker under the measured prior.

Equations

• s.speaker m = HeKaiserIskarous2025.speaker s.prior m s

noncomputable def HeKaiserIskarous2025.Setting.likelihood (s : Setting) (m : Meaning) (st : State) : ℝ

The utterance likelihood of a polarity is the speaker's use of a state's sentence at that state.

Equations

• s.likelihood m st = ((s.speaker m) st).real {st.utterance}

theorem HeKaiserIskarous2025.Setting.likelihood_boolean (s : Setting) (st : State) : s.likelihood boolean st = (s.α * (s.cost Utterance.null - s.cost st.utterance - Real.log (s.statePrior st))).sigmoid

Under the Boolean meaning, the likelihood of a polarity is the logistic function of the cost saved by silence less the log prior of its state, scaled by the rationality.

theorem HeKaiserIskarous2025.Setting.likelihood_boolean_lt (s : Setting) {s' : Setting} (hα : s.α = s'.α) (hc : s.cost = s'.cost) {st : State} (h : s.statePrior st < s'.statePrior st) : s'.likelihood boolean st < s.likelihood boolean st

The Boolean likelihood of a polarity falls as its state's prior rises, the main effect of the state prior.

theorem HeKaiserIskarous2025.Setting.likelihood_boolean_neg_lt_pos_iff (s : Setting) {s' : Setting} (hα : s.α = s'.α) (hc : s.cost = s'.cost) (hp : s'.statePrior State.neg = s.statePrior State.pos) : s'.likelihood boolean State.neg < s.likelihood boolean State.pos ↔ s.cost Utterance.pos < s.cost Utterance.neg

At equal state priors, rationality and costs, the negative polarity is the less likely exactly when its sentence is the costlier, the main effect of polarity.

theorem HeKaiserIskarous2025.Setting.likelihood_boolean_neg_eq_pos (s : Setting) {s' : Setting} (hα : s.α = s'.α) (hc : s.cost = s'.cost) (hp : s'.statePrior State.neg = s.statePrior State.pos) (hcost : s.cost Utterance.pos = s.cost Utterance.neg) : s'.likelihood boolean State.neg = s.likelihood boolean State.pos

At equal costs the two polarities are equally likely at equal state priors (the paper's second simulation).

theorem HeKaiserIskarous2025.Setting.speaker_boolean_pos_lt_null_iff (s : Setting) : ((s.speaker boolean) State.pos).real {Utterance.pos} < ((s.speaker boolean) State.pos).real {Utterance.null} ↔ Real.exp (s.cost Utterance.null - s.cost Utterance.pos) < s.p

The Boolean speaker prefers silence to the positive sentence at the positive state exactly when the state's prior exceeds the exponential of the cost saved by silence.

theorem HeKaiserIskarous2025.Setting.statePrior_lt_L0_real_iff (s : Setting) {m : Meaning} (hm : ∀ (u : Utterance) (st : State), 0 ≤ m u st) {u : Utterance} (hsum : m u State.pos + m u State.neg = 1) (st : State) : s.statePrior st < (((L0 s.prior m) u) {st}).toReal ↔ 1 / 2 < m u st

An utterance holding at a state and its complement to degrees summing to one informs the literal listener about the state exactly when its degree there exceeds one half.

theorem HeKaiserIskarous2025.Setting.p_lt_L0_fuzzy_pos_iff (s : Setting) {n σ : ℝ} (hn0 : 0 ≤ n) (hn1 : n ≤ 1) (hσ0 : 0 ≤ σ) (hσ1 : σ ≤ 1) : s.p < (((L0 s.prior (fuzzy n σ)) Utterance.pos) {State.pos}).toReal ↔ 1 / 2 < σ

The fuzzy positive sentence informs the literal listener about the positive state exactly when its degree there exceeds one half.

theorem HeKaiserIskarous2025.Setting.one_sub_p_lt_L0_fuzzy_neg_iff (s : Setting) {n σ : ℝ} (hn0 : 0 ≤ n) (hn1 : n ≤ 1) (hσ0 : 0 ≤ σ) (hσ1 : σ ≤ 1) : 1 - s.p < (((L0 s.prior (fuzzy n σ)) Utterance.neg) {State.neg}).toReal ↔ 1 / 2 < n

The fuzzy negative sentence informs the literal listener about the negative state exactly when its degree there exceeds one half, at every prior.

theorem HeKaiserIskarous2025.Setting.speaker_fuzzy_pos_lt_null (s : Setting) {n σ : ℝ} (hn0 : 0 ≤ n) (hn1 : n ≤ 1) (hσ0 : 0 < σ) (hσ : σ ≤ 1 / 2) (hc : s.cost Utterance.null < s.cost Utterance.pos) : ((s.speaker (fuzzy n σ)) State.pos).real {Utterance.pos} < ((s.speaker (fuzzy n σ)) State.pos).real {Utterance.null}

At the positive state, the fuzzy speaker prefers silence to a positive sentence of degree at most one half whenever the sentence costs more than silence.

noncomputable def HeKaiserIskarous2025.Setting.fuzzyMeaning (s : Setting) (θ : Sigmoid) (n : ℝ) : Meaning

The fuzzy meaning of §4.1 gives the negative sentence degree n and the positive sentence the sigmoid degree at the measured prior of the positive state.

Equations

• s.fuzzyMeaning θ n = HeKaiserIskarous2025.fuzzy n (θ.eval s.p)

theorem HeKaiserIskarous2025.Setting.speaker_fuzzyMeaning_pos_lt_null (s : Setting) (θ : Sigmoid) {n : ℝ} (hn0 : 0 ≤ n) (hn1 : n ≤ 1) (hk : 0 < θ.k) (hL : 0 < θ.L) (hc0 : 0 ≤ θ.c) (hc : θ.c < 1 / 2) (hLc : 1 / 2 < θ.L + θ.c) (hp : s.p < θ.threshold) (hcost : s.cost Utterance.null < s.cost Utterance.pos) : ((s.speaker (s.fuzzyMeaning θ n)) State.pos).real {Utterance.pos} < ((s.speaker (s.fuzzyMeaning θ n)) State.pos).real {Utterance.null}

Below the threshold prior, the fuzzy speaker prefers silence to the positive sentence at the positive state, since the sigmoid degree disincentivizes the communication of low-prior positive states (§4.1).

The wonky-world listener (§5) and the funky listener (§6)

inductive HeKaiserIskarous2025.World : Type

The complex prior of (5) has two worlds, the normal world with the measured prior and the wonky world with the uniform one.

• normal : World
• wonky : World

@[instance_reducible]

instance HeKaiserIskarous2025.instDecidableEqWorld : DecidableEq World

Equations

• HeKaiserIskarous2025.instDecidableEqWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HeKaiserIskarous2025.instFintypeWorld : Fintype World

Equations

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

instance HeKaiserIskarous2025.instNonemptyWorld : Nonempty World

@[instance_reducible]

instance HeKaiserIskarous2025.instMeasurableSpaceWorld : MeasurableSpace World

Equations

• HeKaiserIskarous2025.instMeasurableSpaceWorld = ⊤

theorem HeKaiserIskarous2025.sum_world {β : Type u_1} [AddCommMonoid β] (f : World → β) : ∑ w : World, f w = f World.normal + f World.wonky

def HeKaiserIskarous2025.wonkinessWeight (ω : ℝ) : World → ℝ

Under a wonkiness ω the wonky world has weight ω and the normal world 1 - ω.

Equations

• HeKaiserIskarous2025.wonkinessWeight ω HeKaiserIskarous2025.World.normal = 1 - ω
• HeKaiserIskarous2025.wonkinessWeight ω HeKaiserIskarous2025.World.wonky = ω

noncomputable def HeKaiserIskarous2025.wonkinessPrior (ω : ℝ) : MeasureTheory.Measure World

The prior over worlds.

Equations

• HeKaiserIskarous2025.wonkinessPrior ω = ∑ w : HeKaiserIskarous2025.World, ENNReal.ofReal (HeKaiserIskarous2025.wonkinessWeight ω w) • MeasureTheory.Measure.dirac w

theorem HeKaiserIskarous2025.wonkinessPrior_apply_singleton (ω : ℝ) (w : World) : (wonkinessPrior ω) {w} = ENNReal.ofReal (wonkinessWeight ω w)

instance HeKaiserIskarous2025.instIsFiniteMeasureWorldWonkinessPrior (ω : ℝ) : MeasureTheory.IsFiniteMeasure (wonkinessPrior ω)

noncomputable def HeKaiserIskarous2025.Setting.worldPrior (s : Setting) : World → MeasureTheory.Measure State

The prior over states is the measured one in the normal world and uniform in the wonky one.

Equations

• s.worldPrior HeKaiserIskarous2025.World.normal = s.prior
• s.worldPrior HeKaiserIskarous2025.World.wonky = ProbabilityTheory.uniformOn Set.univ

instance HeKaiserIskarous2025.Setting.instIsProbabilityMeasureStateWorldPrior (s : Setting) (w : World) : MeasureTheory.IsProbabilityMeasure (s.worldPrior w)

theorem HeKaiserIskarous2025.Setting.worldPrior_ne_zero (s : Setting) (w : World) (st : State) : (s.worldPrior w) {st} ≠ 0

theorem HeKaiserIskarous2025.Setting.worldPrior_real_normal (s : Setting) (st : State) : (s.worldPrior World.normal).real {st} = s.statePrior st

theorem HeKaiserIskarous2025.Setting.worldPrior_real_wonky (s : Setting) (st : State) : (s.worldPrior World.wonky).real {st} = 1 / 2

noncomputable def HeKaiserIskarous2025.Setting.wonkySpeaker (s : Setting) (m : World → Meaning) (p : State × World) : MeasureTheory.Measure Utterance

In each world, the wonky speaker of (14) and (15) is the speaker under that world's prior and meaning, the world riding in the state.

Equations

• s.wonkySpeaker m p = (HeKaiserIskarous2025.speaker (s.worldPrior p.2) (m p.2) s) p.1

theorem HeKaiserIskarous2025.Setting.wonkySpeaker_apply (s : Setting) (m : World → Meaning) (st : State) (w : World) : s.wonkySpeaker m (st, w) = (HeKaiserIskarous2025.speaker (s.worldPrior w) (m w) s) st

instance HeKaiserIskarous2025.Setting.instIsFiniteMeasureUtteranceWonkySpeaker (s : Setting) (m : World → Meaning) (p : State × World) : MeasureTheory.IsFiniteMeasure (s.wonkySpeaker m p)

noncomputable def HeKaiserIskarous2025.Setting.wonkyJoint (s : Setting) (ω : ℝ) : MeasureTheory.Measure (State × World)

The prior of (16) is the measured prior over states, independent of the wonkiness.

Equations

• s.wonkyJoint ω = s.prior.prod (HeKaiserIskarous2025.wonkinessPrior ω)

instance HeKaiserIskarous2025.Setting.instIsFiniteMeasureProdStateWorldWonkyJoint (s : Setting) (ω : ℝ) : MeasureTheory.IsFiniteMeasure (s.wonkyJoint ω)

theorem HeKaiserIskarous2025.Setting.wonkyJoint_apply_singleton (s : Setting) (ω : ℝ) (st : State) (w : World) : (s.wonkyJoint ω) {(st, w)} = ENNReal.ofReal (s.statePrior st) * ENNReal.ofReal (wonkinessWeight ω w)

theorem HeKaiserIskarous2025.Setting.wonkyJoint_real_singleton (s : Setting) {ω : ℝ} (hω0 : 0 ≤ ω) (hω1 : ω ≤ 1) (st : State) (w : World) : (s.wonkyJoint ω).real {(st, w)} = s.statePrior st * wonkinessWeight ω w

noncomputable def HeKaiserIskarous2025.Setting.wonkyListener (s : Setting) (m : World → Meaning) (ω : ℝ) : ProbabilityTheory.Kernel Utterance (State × World)

The wonky listener of (16) inverts the wonky speaker over states and worlds against the prior of (16).

Equations

• s.wonkyListener m ω = RSA.listener (s.wonkyJoint ω) (s.wonkySpeaker m)

theorem HeKaiserIskarous2025.Setting.isProbabilityMeasure_wonkyListener_boolean (s : Setting) {ω : ℝ} (hω0 : 0 < ω) (st : State) : MeasureTheory.IsProbabilityMeasure ((s.wonkyListener (fun (x : World) => boolean) ω) st.utterance)

The Boolean wonky listener is a probability measure after a state's sentence.

noncomputable def HeKaiserIskarous2025.Setting.wonkiness (s : Setting) (m : World → Meaning) (ω : ℝ) (st : State) : ℝ

The posterior wonkiness after the sentence of a state.

Equations

• s.wonkiness m ω st = ((s.wonkyListener m ω) st.utterance).snd.real {HeKaiserIskarous2025.World.wonky}

noncomputable def HeKaiserIskarous2025.Setting.expectedTypicality (s : Setting) (m : World → Meaning) (ω : ℝ) (st : State) : ℝ

The expected typicality of (17) weighs the prior of a state in each world by the posterior over worlds after the state's sentence.

Equations

• s.expectedTypicality m ω st = ∑ w : HeKaiserIskarous2025.World, ((s.wonkyListener m ω) st.utterance).snd.real {w} * (s.worldPrior w).real {st}

theorem HeKaiserIskarous2025.Setting.expectedTypicality_eq (s : Setting) (m : World → Meaning) (ω : ℝ) (st : State) [MeasureTheory.IsProbabilityMeasure ((s.wonkyListener m ω) st.utterance)] : s.expectedTypicality m ω st = s.statePrior st + s.wonkiness m ω st * (1 / 2 - s.statePrior st)

The expected typicality moves the state's prior toward one half by the wonkiness.

theorem HeKaiserIskarous2025.Setting.wonkiness_boolean (s : Setting) {ω : ℝ} (hω0 : 0 < ω) (hω1 : ω < 1) (st : State) : s.wonkiness (fun (x : World) => boolean) ω st = ω * ((HeKaiserIskarous2025.speaker (s.worldPrior World.wonky) boolean s) st).real {st.utterance} / (ω * ((HeKaiserIskarous2025.speaker (s.worldPrior World.wonky) boolean s) st).real {st.utterance} + (1 - ω) * ((HeKaiserIskarous2025.speaker (s.worldPrior World.normal) boolean s) st).real {st.utterance})

After a state's sentence, the posterior wonkiness of the Boolean wonky listener is the wonkiness-weighted share of the wonky speaker's use of the sentence against the normal speaker's.

theorem HeKaiserIskarous2025.Setting.wonkiness_boolean_pos (s : Setting) {ω : ℝ} (hω0 : 0 < ω) (hω1 : ω < 1) (st : State) : 0 < s.wonkiness (fun (x : World) => boolean) ω st

theorem HeKaiserIskarous2025.Setting.lt_wonkiness_iff (s : Setting) {ω : ℝ} (hω0 : 0 < ω) (hω1 : ω < 1) (st : State) : ω < s.wonkiness (fun (x : World) => boolean) ω st ↔ 1 / 2 < s.statePrior st

The wonky listener's wonkiness rises above its prior after a state's sentence exactly when that state's prior exceeds one half, whatever the costs (§5.3, Figure 6).

theorem HeKaiserIskarous2025.Setting.statePrior_lt_expectedTypicality_iff (s : Setting) {ω : ℝ} (hω0 : 0 < ω) (hω1 : ω < 1) (st : State) : s.statePrior st < s.expectedTypicality (fun (x : World) => boolean) ω st ↔ s.statePrior st < 1 / 2

After a state's sentence, the Boolean wonky listener's expected typicality of the state exceeds its prior exactly when the prior is below one half, giving typicality and atypicality inferences in both polarities (§5.3, Figure 5).

theorem HeKaiserIskarous2025.Setting.wonkiness_boolean_neg_eq_pos (s : Setting) {s' : Setting} {ω : ℝ} (hω0 : 0 < ω) (hω1 : ω < 1) (hα : s.α = s'.α) (hc : s.cost = s'.cost) (hp : s'.statePrior State.neg = s.statePrior State.pos) (hcost : s.cost Utterance.pos = s.cost Utterance.neg) : s'.wonkiness (fun (x : World) => boolean) ω State.neg = s.wonkiness (fun (x : World) => boolean) ω State.pos

The wonkiness after a sentence depends on its polarity only through its cost, so at equal state priors, rationality and costs the two polarities update it alike.

noncomputable def HeKaiserIskarous2025.Setting.funkyMeaning (s : Setting) (θ : Sigmoid) (n : ℝ) (w : World) : Meaning

In a world, the funky listener of (18) to (20) uses the fuzzy meaning at that world's prior of the positive state.

Equations

• s.funkyMeaning θ n w = HeKaiserIskarous2025.fuzzy n (θ.eval ((s.worldPrior w).real {HeKaiserIskarous2025.State.pos}))

theorem HeKaiserIskarous2025.Setting.wonkySpeaker_funkyMeaning_normal (s : Setting) (θ : Sigmoid) (n : ℝ) (st : State) : s.wonkySpeaker (s.funkyMeaning θ n) (st, World.normal) = (s.speaker (s.fuzzyMeaning θ n)) st

In the normal world the funky speaker is the fuzzy speaker, so the two models agree on utterance likelihood (§6.2).