Documentation

Studies.YoonEtAl2020

This file formalizes [YTGF20]'s Rational Speech Act model of polite speech, in which a speaker trades off three goals: to be informative, to be kind, and to appear informative and kind. In the experimental domain Ann rates Bob's poem on a scale of zero to three hearts and answers with one of four adjectives, plain or negated. The literal listener updates a uniform prior over states with the soft lexicon elicited in the norming experiment (meaning, l0); the first-order speaker maximizes a mixture of informational and social utility minus cost, φ · ln P_L0(s | w) + (1 − φ) · E_L0[V(s)] − C(w), (5) (util, speaker); the pragmatic listener infers the state and the speaker's goal weight jointly, (4) (listener); and the second-order polite speaker adds presentational utility, the log probability the pragmatic listener assigns to the projected goal weight, (3), inside the total utility (2) (s2Utility, s2Speaker, (1)).

The first-order predictions of Figure 2 are theorems over the free parameters. A speaker with no weight on informativity prefers "not terrible" to "terrible" exactly when the extra cost of negation is below its social gain (social_prefers_indirect_iff), and prefers "amazing" to "not amazing" at every cost (social_prefers_positive); a speaker with no weight on kindness prefers the direct form at both ends of the scale (informative_prefers_direct, informative_prefers_direct_positive), and never produces an utterance whose literal probability at the true state is zero (speaker_apply_eq_zero_of_meaning_eq_zero).

Implementation notes #

The lexicon is the acceptance count of each utterance at each state among the 49 participants in the released norming data (acceptance); the paper's Bayesian data analysis places a Beta posterior on each acceptance probability instead. An utterance with zero acceptance at a state has literal probability zero there, and its score is ⊥ for every speaker with some weight on informativity, since the pure-social speaker alone ignores the literal probability.
The listener's prior over the goal weight φ is uniform on the unit interval; it is discretized to five points (Phi) so that the joint prior is uniformOn.
Cost is the paper's cost of negation c (Figure 4): a plain utterance costs 1 and a negated one c, and it sits inside the utility scaled by α as in (2); the released model realizes it as an utterance prior instead.
Table 2's maximum a posteriori goal weights for the full model are recorded as data (tableTwo); the model comparison of Table 1 is outside the scope of the formalization.

References #

[YTGF20]

States, utterances, goals #

inductive YoonEtAl2020.HeartState :

The rating a poem deserves, in hearts.

Instances For

@[instance_reducible]

instance YoonEtAl2020.instDecidableEqHeartState :

DecidableEq HeartState

Equations

YoonEtAl2020.instDecidableEqHeartState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance YoonEtAl2020.instReprHeartState :

Repr HeartState

Equations

YoonEtAl2020.instReprHeartState = { reprPrec := YoonEtAl2020.instReprHeartState.repr }

def YoonEtAl2020.instReprHeartState.repr :

HeartState → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance YoonEtAl2020.instFintypeHeartState :

Fintype HeartState

Equations

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

@[instance_reducible]

instance YoonEtAl2020.instInhabitedHeartState :

Inhabited HeartState

Equations

YoonEtAl2020.instInhabitedHeartState = { default := YoonEtAl2020.instInhabitedHeartState.default }

@[instance_reducible]

instance YoonEtAl2020.instMeasurableSpaceHeartState :

MeasurableSpace HeartState

Equations

YoonEtAl2020.instMeasurableSpaceHeartState = ⊤

def YoonEtAl2020.HeartState.value :

HeartState → ℚ

The subjective value V(s) of a state, the number of hearts.

Equations

Instances For

inductive YoonEtAl2020.Adjective :

The four adjectives.

terrible : Adjective
bad : Adjective
good : Adjective
amazing : Adjective

Instances For

@[instance_reducible]

instance YoonEtAl2020.instDecidableEqAdjective :

DecidableEq Adjective

Equations

YoonEtAl2020.instDecidableEqAdjective x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def YoonEtAl2020.instReprAdjective.repr :

Adjective → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance YoonEtAl2020.instReprAdjective :

Equations

YoonEtAl2020.instReprAdjective = { reprPrec := YoonEtAl2020.instReprAdjective.repr }

@[instance_reducible]

instance YoonEtAl2020.instFintypeAdjective :

Fintype Adjective

Equations

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

@[instance_reducible]

instance YoonEtAl2020.instMeasurableSpaceAdjective :

MeasurableSpace Adjective

Equations

YoonEtAl2020.instMeasurableSpaceAdjective = ⊤

@[reducible, inline]

abbrev YoonEtAl2020.Utterance :

An utterance is an adjective, plain or negated, as in it was X or it wasn't X.

Equations

YoonEtAl2020.Utterance = (YoonEtAl2020.Adjective × Bool)

Instances For

inductive YoonEtAl2020.GoalCondition :

The speaker's goal condition in the production experiment.

informative : GoalCondition
kind : GoalCondition
both : GoalCondition

Instances For

@[instance_reducible]

instance YoonEtAl2020.instDecidableEqGoalCondition :

DecidableEq GoalCondition

Equations

YoonEtAl2020.instDecidableEqGoalCondition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def YoonEtAl2020.instReprGoalCondition.repr :

GoalCondition → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance YoonEtAl2020.instReprGoalCondition :

Repr GoalCondition

Equations

YoonEtAl2020.instReprGoalCondition = { reprPrec := YoonEtAl2020.instReprGoalCondition.repr }

inductive YoonEtAl2020.Phi :

The first-order speaker's goal weight φ, the weight on informativity against kindness, discretized to five points.

p0 : Phi
p25 : Phi
p50 : Phi
p75 : Phi
p100 : Phi

Instances For

@[instance_reducible]

instance YoonEtAl2020.instDecidableEqPhi :

DecidableEq Phi

Equations

YoonEtAl2020.instDecidableEqPhi x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance YoonEtAl2020.instReprPhi :

Repr Phi

Equations

YoonEtAl2020.instReprPhi = { reprPrec := YoonEtAl2020.instReprPhi.repr }

def YoonEtAl2020.instReprPhi.repr :

Phi → ℕ → Std.Format

Equations

YoonEtAl2020.instReprPhi.repr YoonEtAl2020.Phi.p0 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "YoonEtAl2020.Phi.p0")).group prec✝
YoonEtAl2020.instReprPhi.repr YoonEtAl2020.Phi.p25 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "YoonEtAl2020.Phi.p25")).group prec✝
YoonEtAl2020.instReprPhi.repr YoonEtAl2020.Phi.p50 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "YoonEtAl2020.Phi.p50")).group prec✝
YoonEtAl2020.instReprPhi.repr YoonEtAl2020.Phi.p75 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "YoonEtAl2020.Phi.p75")).group prec✝
YoonEtAl2020.instReprPhi.repr YoonEtAl2020.Phi.p100 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "YoonEtAl2020.Phi.p100")).group prec✝

Instances For

@[instance_reducible]

instance YoonEtAl2020.instFintypePhi :

Fintype Phi

Equations

YoonEtAl2020.instFintypePhi = { elems := { val := ↑YoonEtAl2020.Phi.enumList, nodup := YoonEtAl2020.Phi.enumList_nodup }, complete := YoonEtAl2020.instFintypePhi._proof_1 }

@[instance_reducible]

instance YoonEtAl2020.instInhabitedPhi :

Inhabited Phi

Equations

YoonEtAl2020.instInhabitedPhi = { default := YoonEtAl2020.instInhabitedPhi.default }

@[instance_reducible]

instance YoonEtAl2020.instMeasurableSpacePhi :

MeasurableSpace Phi

Equations

YoonEtAl2020.instMeasurableSpacePhi = ⊤

def YoonEtAl2020.Phi.val :

Phi → ℚ

The value of each goal weight.

Equations

Instances For

The soft lexicon #

def YoonEtAl2020.acceptance :

Adjective → Bool → HeartState → ℕ

The number of the 49 norming participants who accepted the utterance at the state (Figure 2, top left), from the released norming data.

Equations

Instances For

def YoonEtAl2020.meaning (u : Utterance) (s : HeartState) :

ℚ

The soft literal meaning 𝓛(s) of an utterance is its acceptance proportion at the state.

Equations

YoonEtAl2020.meaning u s = ↑(YoonEtAl2020.acceptance u.1 u.2 s) / 49

Instances For

theorem YoonEtAl2020.meaning_bounded (u : Utterance) (s : HeartState) :

0 ≤ meaning u s ∧ meaning u s ≤ 1

The lexicon is soft, with values in [0, 1].

def YoonEtAl2020.cost (c : ℝ) (u : Utterance) :

ℝ

A plain adjective costs 1, and a negated one the cost of negation c.

Equations

YoonEtAl2020.cost c u = if u.2 = true then c else 1

Instances For

The literal listener #

With a uniform state prior, P_L0(s | w) = 𝓛(s) / Σ_s' 𝓛(s').

def YoonEtAl2020.semMass (u : Utterance) :

ℚ

The lexicon mass of an utterance, the literal listener's normalizer.

Equations

YoonEtAl2020.semMass u = ∑ s : YoonEtAl2020.HeartState, YoonEtAl2020.meaning u s

Instances For

def YoonEtAl2020.l0 (u : Utterance) (s : HeartState) :

ℚ

P_L0(s | u), the literal listener's posterior under the uniform prior.

Equations

YoonEtAl2020.l0 u s = YoonEtAl2020.meaning u s / YoonEtAl2020.semMass u

Instances For

def YoonEtAl2020.ev (u : Utterance) :

ℚ

E_{P_L0(· | u)}[V(s)], the social utility of u, which does not depend on the true state.

Equations

YoonEtAl2020.ev u = ∑ s : YoonEtAl2020.HeartState, YoonEtAl2020.l0 u s * s.value

Instances For

The first-order speaker #

noncomputable def YoonEtAl2020.util (α c : ℝ) (p : HeartState × Phi) (u : Utterance) :

EReal

The first-order utility U(w; s; φ) = φ · ln P_L0(s | w) + (1 − φ) · E_L0[V(s)] − C(w), scaled by the optimality α, as an extended-real score over the situations (s, φ). An utterance of literal probability zero at s scores ⊥ for every φ ≠ 0.

Equations

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

Instances For

theorem YoonEtAl2020.util_ne_top (α c : ℝ) (p : HeartState × Phi) (u : Utterance) :

util α c p u ≠ ⊤

theorem YoonEtAl2020.util_exists_ne_bot (α c : ℝ) (p : HeartState × Phi) :

∃ (u : Utterance), util α c p u ≠ ⊥

Every situation has an applicable utterance, the adjective accepted at its state.

noncomputable def YoonEtAl2020.speaker (α c : ℝ) :

ProbabilityTheory.Kernel (HeartState × Phi) Utterance

The first-order speaker (5) is the score speaker of util.

Equations

YoonEtAl2020.speaker α c = ProbabilityTheory.Kernel.softmax (YoonEtAl2020.util α c)

Instances For

instance YoonEtAl2020.instIsFiniteKernelProdHeartStatePhiUtteranceSpeaker (α c : ℝ) :

ProbabilityTheory.IsFiniteKernel (speaker α c)

theorem YoonEtAl2020.speaker_real_singleton_lt_iff (α c : ℝ) (p : HeartState × Phi) (u u' : Utterance) :

((speaker α c) p).real {u} < ((speaker α c) p).real {u'} ↔ util α c p u < util α c p u'

Speaker preference at a situation is utility comparison.

theorem YoonEtAl2020.speaker_apply_eq_zero_of_meaning_eq_zero (α c : ℝ) {s : HeartState} {φ : Phi} {u : Utterance} (h0 : meaning u s = 0) (hφ : φ ≠ Phi.p0) :

((speaker α c) (s, φ)) {u} = 0

An utterance of literal probability zero at the true state is never produced by a speaker with some weight on informativity.

First-order predictions (Figure 2, top right) #

theorem YoonEtAl2020.social_lt_iff {α : ℝ} (hα : 0 < α) (c : ℝ) (s : HeartState) (u u' : Utterance) :

((speaker α c) (s, Phi.p0)).real {u} < ((speaker α c) (s, Phi.p0)).real {u'} ↔ ↑(ev u) - cost c u < ↑(ev u') - cost c u'

The pure-social speaker compares social utility net of cost, at every state.

theorem YoonEtAl2020.social_prefers_indirect_iff {α : ℝ} (hα : 0 < α) (c : ℝ) (s : HeartState) :

((speaker α c) (s, Phi.p0)).real {(Adjective.terrible, false)} < ((speaker α c) (s, Phi.p0)).real {(Adjective.terrible, true)} ↔ c - 1 < ↑(ev (Adjective.terrible, true)) - ↑(ev (Adjective.terrible, false))

The pure-social speaker prefers the indirect "not terrible" to "terrible" exactly when the extra cost of negation is below the social gain of the negation.

theorem YoonEtAl2020.social_prefers_positive {α c : ℝ} (hα : 0 < α) (hc : 1 ≤ c) (s : HeartState) :

((speaker α c) (s, Phi.p0)).real {(Adjective.amazing, true)} < ((speaker α c) (s, Phi.p0)).real {(Adjective.amazing, false)}

The pure-social speaker prefers "amazing" to "not amazing", since the direct form is both kinder and no costlier.

theorem YoonEtAl2020.informative_prefers_direct {α c : ℝ} (hα : 0 < α) (hc : 1 ≤ c) :

((speaker α c) (HeartState.h0, Phi.p100)).real {(Adjective.terrible, true)} < ((speaker α c) (HeartState.h0, Phi.p100)).real {(Adjective.terrible, false)}

The pure-informative speaker prefers the direct "terrible" at zero hearts, since the literal listener puts far more of the mass of "terrible" than of "not terrible" on that state, and the direct form is no costlier.

theorem YoonEtAl2020.informative_prefers_direct_positive (α c : ℝ) :

((speaker α c) (HeartState.h3, Phi.p100)).real {(Adjective.amazing, true)} < ((speaker α c) (HeartState.h3, Phi.p100)).real {(Adjective.amazing, false)}

The pure-informative speaker prefers the direct "amazing" at three hearts, where "not amazing" is never accepted, so its score is ⊥.

The pragmatic listener, (4) #

noncomputable def YoonEtAl2020.prior :

MeasureTheory.Measure (HeartState × Phi)

The uniform joint prior over states and goal weights.

Equations

YoonEtAl2020.prior = ProbabilityTheory.uniformOn Set.univ

Instances For

instance YoonEtAl2020.instIsProbabilityMeasureProdHeartStatePhiPrior :

MeasureTheory.IsProbabilityMeasure prior

theorem YoonEtAl2020.prior_ne_zero (p : HeartState × Phi) :

prior {p} ≠ 0

theorem YoonEtAl2020.comp_speaker_ne_zero (α c : ℝ) (u : Utterance) :

(prior.bind ⇑(speaker α c)) {u} ≠ 0

Every utterance is accepted by someone at zero hearts, so every utterance is heard with positive probability.

noncomputable def YoonEtAl2020.listener (α c : ℝ) :

ProbabilityTheory.Kernel Utterance (HeartState × Phi)

The pragmatic listener (4) infers the state and the goal weight (s, φ) from the utterance. Its first marginal is P_L1(s | w) and its second P_L1(φ | w), the probability inside (3).

Equations

YoonEtAl2020.listener α c = RSA.listener YoonEtAl2020.prior ⇑(YoonEtAl2020.speaker α c)

Instances For

The second-order polite speaker, (1)–(3) #

structure YoonEtAl2020.S2Weights :

The weights ω on the informational, social and presentational utilities.

wInf : ℚ
wSoc : ℚ
wPres : ℚ

Instances For

def YoonEtAl2020.tableTwo :

GoalCondition → S2Weights

Table 2 gives the maximum a posteriori goal weights of the full model in each goal condition.

Equations

YoonEtAl2020.tableTwo YoonEtAl2020.GoalCondition.both = { wInf := 36 / 100, wSoc := 11 / 100, wPres := 54 / 100 }
YoonEtAl2020.tableTwo YoonEtAl2020.GoalCondition.informative = { wInf := 36 / 100, wSoc := 2 / 100, wPres := 62 / 100 }
YoonEtAl2020.tableTwo YoonEtAl2020.GoalCondition.kind = { wInf := 25 / 100, wSoc := 31 / 100, wPres := 44 / 100 }

Instances For

def YoonEtAl2020.tableTwoPhi :

GoalCondition → ℚ

Table 2 gives the maximum a posteriori projected goal weight φ of the full model in each goal condition.

Equations

YoonEtAl2020.tableTwoPhi YoonEtAl2020.GoalCondition.both = 36 / 100
YoonEtAl2020.tableTwoPhi YoonEtAl2020.GoalCondition.informative = 49 / 100
YoonEtAl2020.tableTwoPhi YoonEtAl2020.GoalCondition.kind = 37 / 100

Instances For

noncomputable def YoonEtAl2020.s2Utility (α c : ℝ) (W : S2Weights) (phiHat : Phi) (s : HeartState) (u : Utterance) :

ℝ

The total utility (2), with the presentational utility (3), is ω_inf · ln P_L1(s | w) + ω_soc · E_{P_L1(· | w)}[V] + ω_pres · ln P_L1(phiHat | w) − C(w), for the projected goal weight phiHat.

Equations

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

Instances For

noncomputable def YoonEtAl2020.s2Speaker (α c : ℝ) (W : S2Weights) (phiHat : Phi) :

ProbabilityTheory.Kernel HeartState Utterance

The second-order speaker (1) is the score speaker of the total utility scaled by α.

Equations

YoonEtAl2020.s2Speaker α c W phiHat = ProbabilityTheory.Kernel.softmax fun (s : YoonEtAl2020.HeartState) (u : YoonEtAl2020.Utterance) => ↑(α * YoonEtAl2020.s2Utility α c W phiHat s u)

Instances For