Degen, Hawkins, Graf, Kreiss and Goodman (2020): When Redundancy Is Useful: A Bayesian Approach to "Overinformative" Referring Expressions

Degen and colleagues' rational speech act model with a continuous semantics. A referring expression holds of an object to a degree in the unit interval. An adjective of semantic value x holds to degree x of the objects in its Boolean extension and to degree 1 − x of the others, and an expression of two adjectives multiplies their degrees. The literal listener normalizes the degrees over the objects of the context, and the speaker chooses an expression in proportion to the exponential of its utility, the log of the listener's probability of the intended object less the cost of the expression. An adjective that the Boolean semantics makes redundant then adds information, and adds more the less noisy it is.

Main statements

• overmodification_odds_lt_iff: among the three pins of the paper's first figure the speaker adds a redundant colour to a sufficient size more readily than a redundant size to a sufficient colour exactly when size is the noisier of the two, at every positive rationality and when the two redundant adjectives cost the same.
• color_overmodification_iff, size_overmodification_iff: without cost the redundant expression is preferred to the sufficient one exactly when the semantic value of the redundant adjective exceeds one half.
• boolean_no_preference: with Boolean values the redundant adjective adds nothing.

Implementation notes

• S1 is RSA.speaker, whose rationality α scales the whole utility. The paper weights informativeness and cost separately and notes that the two parameterizations are equivalent.
• The listener and the speaker take any graded meaning, so the typicality semantics of the paper's third experiment is the same model at another meaning, and S1_real_lt_iff is its preference for the term of greater utility.

TODO

• Tables 2 and 3 do not follow from Equation (1) at the stated values x_size = .8 and x_colour = .99. Their values match a listener proportional to the exponential of the meaning. The theorems follow the equations.
• The regression coefficients and the fitted parameters of the three experiments are not encoded.

References

• [DHG+20]
• [FG12]

Continuous semantics

def DegenEtAl2020.noisy (x : ℝ) (p : Prop) [Decidable p] : ℝ

An adjective of semantic value x holds to degree x of an object in its Boolean extension and to degree 1 − x of any other, (6).

Equations

• DegenEtAl2020.noisy x p = if p then x else 1 - x

theorem DegenEtAl2020.noisy_nonneg {x : ℝ} (h0 : 0 ≤ x) (h1 : x ≤ 1) (p : Prop) [Decidable p] : 0 ≤ noisy x p

The gain of a redundant adjective

noncomputable def DegenEtAl2020.gain (b : ℕ) (xs xr : ℝ) : ℝ

In a display where the target alone has the sufficient property, one competitor shares the redundant property with it and b distractors share neither, the redundant adjective multiplies the literal listener's probability of the target by this factor, where xs is the semantic value of the sufficient adjective and xr that of the redundant one.

Equations

• DegenEtAl2020.gain b xs xr = xr * (xs + (↑b + 1) * (1 - xs)) / (xr + ↑b * (1 - xs) * (1 - xr))

theorem DegenEtAl2020.gain_pos {b : ℕ} {xs xr : ℝ} (hs0 : 0 < xs) (hs1 : xs ≤ 1) (hr0 : 0 < xr) (hr1 : xr ≤ 1) : 0 < gain b xs xr

theorem DegenEtAl2020.div_div_eq_gain_one {xs xr : ℝ} (hs0 : 0 < xs) (hs1 : xs ≤ 1) (hr0 : 0 < xr) : xs * xr / (1 - xs + xs * xr) / (xs / (2 - xs)) = gain 1 xs xr

With one distractor the gain is the ratio of the listener's probabilities of the target under the redundant and under the sufficient expression.

theorem DegenEtAl2020.gain_one_left {b : ℕ} {xr : ℝ} (hr : xr ≠ 0) : gain b 1 xr = 1

Beside a Boolean sufficient adjective the redundant one adds nothing.

theorem DegenEtAl2020.one_lt_gain_iff {b : ℕ} {xs xr : ℝ} (hb : 0 < b) (hs1 : xs < 1) (hr0 : 0 < xr) (hr1 : xr ≤ 1) : 1 < gain b xs xr ↔ 1 / 2 < xr

Beside a sufficient adjective short of Boolean, the redundant one adds information exactly when its semantic value exceeds one half.

theorem DegenEtAl2020.gain_lt_gain_iff {b : ℕ} {xs xr xr' : ℝ} (hb : 0 < b) (hs0 : 0 < xs) (hs1 : xs < 1) (hr0 : 0 < xr) (hr1 : xr ≤ 1) (hr0' : 0 < xr') (hr1' : xr' ≤ 1) : gain b xs xr < gain b xs xr' ↔ xr < xr'

Beside one sufficient adjective short of Boolean, the gain grows with the semantic value of the redundant adjective.

theorem DegenEtAl2020.gain_swap_lt_iff {b : ℕ} {x₁ x₂ : ℝ} (hb : 0 < b) (h₁0 : 0 < x₁) (h₁1 : x₁ ≤ 1) (h₂0 : 0 < x₂) (h₂1 : x₂ ≤ 1) : gain b x₂ x₁ < gain b x₁ x₂ ↔ x₁ < x₂

When two adjectives trade the sufficient and the redundant role, the gain is greater on the side where the redundant adjective is the less noisy of the two.

Listener and speaker

noncomputable def DegenEtAl2020.L0 {E : Type u_1} {U : Type u_2} [MeasurableSpace E] [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] (m : U → E → ℝ) : ProbabilityTheory.Kernel U E

The literal listener (1) normalizes the meaning of an expression over the objects at a uniform prior.

Equations

• DegenEtAl2020.L0 m = ProbabilityTheory.Kernel.ofDensity (ProbabilityTheory.uniformOn Set.univ) fun (u : U) (o : E) => ENNReal.ofReal (m u o)

instance DegenEtAl2020.instIsFiniteKernelL0 {E : Type u_1} {U : Type u_2} [MeasurableSpace E] [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] (m : U → E → ℝ) : ProbabilityTheory.IsFiniteKernel (L0 m)

noncomputable def DegenEtAl2020.S1 {E : Type u_1} {U : Type u_2} [Fintype E] [MeasurableSpace E] [MeasurableSingletonClass E] [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] (α : ℝ) (C : U → ℝ) (m : U → E → ℝ) : ProbabilityTheory.Kernel E U

The speaker of (3) and (4) at rationality α chooses an expression in proportion to the exponential of α times its utility, the log of the listener's probability of the object less the cost C.

Equations

• DegenEtAl2020.S1 α C m = RSA.speaker α C (⇑(DegenEtAl2020.L0 m)) MeasureTheory.Measure.dirac

instance DegenEtAl2020.instIsFiniteKernelS1 {E : Type u_1} {U : Type u_2} [Fintype E] [MeasurableSpace E] [MeasurableSingletonClass E] [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] (α : ℝ) (C : U → ℝ) (m : U → E → ℝ) : ProbabilityTheory.IsFiniteKernel (S1 α C m)

theorem DegenEtAl2020.S1_apply_singleton_of_equiv {E : Type u_1} {U : Type u_2} [Fintype E] [MeasurableSpace E] [MeasurableSingletonClass E] [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] {m : U → E → ℝ} {U' : Type u_3} [Fintype U'] [MeasurableSpace U'] [MeasurableSingletonClass U'] (τ : U ≃ U') (α : ℝ) (C : U' → ℝ) {m' : U' → E → ℝ} (h : ∀ (v : U), m' (τ v) = m v) (o : E) (u : U) : ((S1 α C m') o) {τ u} = ((S1 α (C ∘ ⇑τ) m) o) {u}

Relabelling the expressions carries the speaker along, with the cost relabelled with them.

theorem DegenEtAl2020.L0_apply {E : Type u_1} {U : Type u_2} [Fintype E] [MeasurableSpace E] [MeasurableSingletonClass E] [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] {m : U → E → ℝ} {u : U} [Nonempty E] (hm : ∀ (o' : E), 0 ≤ m u o') (hpos : 0 < ∑ o' : E, m u o') (o : E) : ((L0 m) u) {o} = ENNReal.ofReal (m u o / ∑ o' : E, m u o')

The listener's probability of an object is the share of its degree in the row.

theorem DegenEtAl2020.L0_real_singleton {E : Type u_1} {U : Type u_2} [Fintype E] [MeasurableSpace E] [MeasurableSingletonClass E] [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] {m : U → E → ℝ} {u : U} [Nonempty E] (hm : ∀ (o' : E), 0 ≤ m u o') (hpos : 0 < ∑ o' : E, m u o') (o : E) : ((L0 m) u).real {o} = m u o / ∑ o' : E, m u o'

theorem DegenEtAl2020.S1_real_div {E : Type u_1} {U : Type u_2} [Fintype E] [MeasurableSpace E] [MeasurableSingletonClass E] [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] {m : U → E → ℝ} {α : ℝ} {C : U → ℝ} {u u' : U} {o : E} [Nonempty E] (hα : 0 ≤ α) (hm : ∀ (v : U) (o' : E), 0 ≤ m v o') (hu : 0 < m u o) (hu' : 0 < m u' o) : ((S1 α C m) o).real {u'} / ((S1 α C m) o).real {u} = ((m u' o / ∑ o' : E, m u' o') / (m u o / ∑ o' : E, m u o')) ^ α * Real.exp (-(α * (C u' - C u)))

The odds of one expression against another for an object are the ratio of the listener's probabilities of the object to the power α, discounted by the difference in cost.

theorem DegenEtAl2020.S1_real_lt_iff {E : Type u_1} {U : Type u_2} [Fintype E] [MeasurableSpace E] [MeasurableSingletonClass E] [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] {m : U → E → ℝ} {α : ℝ} {C : U → ℝ} {u u' : U} {o : E} [Nonempty E] (hα : 0 < α) (hm : ∀ (v : U) (o' : E), 0 ≤ m v o') (hu : 0 < m u o) (hu' : 0 < m u' o) : ((S1 α C m) o).real {u} < ((S1 α C m) o).real {u'} ↔ Real.log (m u o / ∑ o' : E, m u o') - C u < Real.log (m u' o / ∑ o' : E, m u' o') - C u'

The speaker prefers the expression of greater utility.

theorem DegenEtAl2020.S1_real_of_pair {E : Type u_1} {U : Type u_2} [Fintype E] [MeasurableSpace E] [MeasurableSingletonClass E] [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] {m : U → E → ℝ} {α : ℝ} {C : U → ℝ} {u u' : U} {o : E} [Nonempty E] (hα : 0 < α) (huu' : u ≠ u') (hm : ∀ (v : U) (o' : E), 0 ≤ m v o') (hu : 0 < m u o) (hu' : 0 < m u' o) (hsupp : ∀ (v : U), 0 < m v o → v = u ∨ v = u') : ((S1 α C m) o).real {u} = (α * (Real.log (m u o / ∑ o' : E, m u o') - C u - (Real.log (m u' o / ∑ o' : E, m u' o') - C u'))).sigmoid

When two expressions alone hold of an object to a positive degree, the probability of one is the logistic function of its advantage in utility over the other, scaled by the rationality.

theorem DegenEtAl2020.S1_real_eq_one {E : Type u_1} {U : Type u_2} [Fintype E] [MeasurableSpace E] [MeasurableSingletonClass E] [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] {m : U → E → ℝ} {α : ℝ} {C : U → ℝ} {u : U} {o : E} [Nonempty E] (hα : 0 < α) (hm : ∀ (v : U) (o' : E), 0 ≤ m v o') (hu : 0 < m u o) (hother : ∀ (v : U), v ≠ u → m v o = 0) : ((S1 α C m) o).real {u} = 1

An expression that alone holds of an object to a positive degree is produced for it with certainty.

theorem DegenEtAl2020.distinguishes_L0_iff {E : Type u_1} {U : Type u_2} [Fintype E] [MeasurableSpace E] [MeasurableSingletonClass E] [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] {m : U → E → ℝ} {u : U} [Nonempty E] (hm : ∀ (o' : E), 0 ≤ m u o') (hpos : 0 < ∑ o' : E, m u o') (D : Finset E) (r : E) : Reference.Distinguishes (fun (u : U) (o : E) => ((L0 m) u) {o}) D r u ↔ Reference.Distinguishes m D r u

A description distinguishes an object under the literal listener, so that the object is the listener's best guess, exactly when it does under the meaning.

The pins of the first figure

inductive DegenEtAl2020.Size : Type

The sizes of the pins.

• big : Size
• small : Size

@[instance_reducible]

instance DegenEtAl2020.instDecidableEqSize : DecidableEq Size

Equations

• DegenEtAl2020.instDecidableEqSize x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DegenEtAl2020.instReprSize.repr : Size → ℕ → Std.Format

Equations

• DegenEtAl2020.instReprSize.repr DegenEtAl2020.Size.big prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DegenEtAl2020.Size.big")).group prec✝
• DegenEtAl2020.instReprSize.repr DegenEtAl2020.Size.small prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DegenEtAl2020.Size.small")).group prec✝

@[instance_reducible]

instance DegenEtAl2020.instReprSize : Repr Size

Equations

• DegenEtAl2020.instReprSize = { reprPrec := DegenEtAl2020.instReprSize.repr }

inductive DegenEtAl2020.Color : Type

The colours of the pins.

• blue : Color
• red : Color

@[instance_reducible]

instance DegenEtAl2020.instDecidableEqColor : DecidableEq Color

Equations

• DegenEtAl2020.instDecidableEqColor x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DegenEtAl2020.instReprColor : Repr Color

Equations

• DegenEtAl2020.instReprColor = { reprPrec := DegenEtAl2020.instReprColor.repr }

def DegenEtAl2020.instReprColor.repr : Color → ℕ → Std.Format

Equations

• DegenEtAl2020.instReprColor.repr DegenEtAl2020.Color.blue prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DegenEtAl2020.Color.blue")).group prec✝
• DegenEtAl2020.instReprColor.repr DegenEtAl2020.Color.red prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DegenEtAl2020.Color.red")).group prec✝

inductive DegenEtAl2020.Pin : Type

The size-sufficient context has three pins, the target small blue pin, a big blue one and a big red one.

• bigBlue : Pin
• bigRed : Pin
• smallBlue : Pin

@[instance_reducible]

instance DegenEtAl2020.instDecidableEqPin : DecidableEq Pin

Equations

• DegenEtAl2020.instDecidableEqPin x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DegenEtAl2020.instReprPin.repr : Pin → ℕ → Std.Format

Equations

• DegenEtAl2020.instReprPin.repr DegenEtAl2020.Pin.bigBlue prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DegenEtAl2020.Pin.bigBlue")).group prec✝
• DegenEtAl2020.instReprPin.repr DegenEtAl2020.Pin.bigRed prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DegenEtAl2020.Pin.bigRed")).group prec✝
• DegenEtAl2020.instReprPin.repr DegenEtAl2020.Pin.smallBlue prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DegenEtAl2020.Pin.smallBlue")).group prec✝

@[instance_reducible]

instance DegenEtAl2020.instReprPin : Repr Pin

Equations

• DegenEtAl2020.instReprPin = { reprPrec := DegenEtAl2020.instReprPin.repr }

@[instance_reducible]

instance DegenEtAl2020.instInhabitedPin : Inhabited Pin

Equations

• DegenEtAl2020.instInhabitedPin = { default := DegenEtAl2020.instInhabitedPin.default }

@[instance_reducible]

instance DegenEtAl2020.instFintypePin : Fintype Pin

Equations

• DegenEtAl2020.instFintypePin = { elems := { val := ↑DegenEtAl2020.Pin.enumList, nodup := DegenEtAl2020.Pin.enumList_nodup }, complete := DegenEtAl2020.instFintypePin._proof_1 }

@[instance_reducible]

instance DegenEtAl2020.instMeasurableSpacePin : MeasurableSpace Pin

Equations

• DegenEtAl2020.instMeasurableSpacePin = ⊤

instance DegenEtAl2020.instDiscreteMeasurableSpacePin : DiscreteMeasurableSpace Pin

def DegenEtAl2020.Pin.size : Pin → Size

The size of a pin.

Equations

• DegenEtAl2020.Pin.bigBlue.size = DegenEtAl2020.Size.big
• DegenEtAl2020.Pin.bigRed.size = DegenEtAl2020.Size.big
• DegenEtAl2020.Pin.smallBlue.size = DegenEtAl2020.Size.small

def DegenEtAl2020.Pin.color : Pin → Color

The colour of a pin.

Equations

• DegenEtAl2020.Pin.bigBlue.color = DegenEtAl2020.Color.blue
• DegenEtAl2020.Pin.smallBlue.color = DegenEtAl2020.Color.blue
• DegenEtAl2020.Pin.bigRed.color = DegenEtAl2020.Color.red

inductive DegenEtAl2020.Utterance : Type

The seven referring expressions name a size, a colour, or both, each followed by pin.

• big : Utterance
• small : Utterance
• blue : Utterance
• red : Utterance
• bigBlue : Utterance
• bigRed : Utterance
• smallBlue : Utterance

@[instance_reducible]

instance DegenEtAl2020.instDecidableEqUtterance : DecidableEq Utterance

Equations

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

def DegenEtAl2020.instReprUtterance.repr : Utterance → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DegenEtAl2020.instReprUtterance : Repr Utterance

Equations

• DegenEtAl2020.instReprUtterance = { reprPrec := DegenEtAl2020.instReprUtterance.repr }

@[instance_reducible]

instance DegenEtAl2020.instInhabitedUtterance : Inhabited Utterance

Equations

• DegenEtAl2020.instInhabitedUtterance = { default := DegenEtAl2020.instInhabitedUtterance.default }

@[instance_reducible]

instance DegenEtAl2020.instFintypeUtterance : Fintype Utterance

Equations

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

@[instance_reducible]

instance DegenEtAl2020.instMeasurableSpaceUtterance : MeasurableSpace Utterance

Equations

• DegenEtAl2020.instMeasurableSpaceUtterance = ⊤

instance DegenEtAl2020.instDiscreteMeasurableSpaceUtterance : DiscreteMeasurableSpace Utterance

def DegenEtAl2020.Utterance.size : Utterance → Option Size

The size an expression names, if any.

Equations

• DegenEtAl2020.Utterance.big.size = some DegenEtAl2020.Size.big
• DegenEtAl2020.Utterance.bigBlue.size = some DegenEtAl2020.Size.big
• DegenEtAl2020.Utterance.bigRed.size = some DegenEtAl2020.Size.big
• DegenEtAl2020.Utterance.small.size = some DegenEtAl2020.Size.small
• DegenEtAl2020.Utterance.smallBlue.size = some DegenEtAl2020.Size.small
• DegenEtAl2020.Utterance.blue.size = none
• DegenEtAl2020.Utterance.red.size = none

def DegenEtAl2020.Utterance.color : Utterance → Option Color

The colour an expression names, if any.

Equations

• DegenEtAl2020.Utterance.blue.color = some DegenEtAl2020.Color.blue
• DegenEtAl2020.Utterance.bigBlue.color = some DegenEtAl2020.Color.blue
• DegenEtAl2020.Utterance.smallBlue.color = some DegenEtAl2020.Color.blue
• DegenEtAl2020.Utterance.red.color = some DegenEtAl2020.Color.red
• DegenEtAl2020.Utterance.bigRed.color = some DegenEtAl2020.Color.red
• DegenEtAl2020.Utterance.big.color = none
• DegenEtAl2020.Utterance.small.color = none

def DegenEtAl2020.meaning (xs xc : ℝ) (u : Utterance) (o : Pin) : ℝ

The meaning of an expression is the product, over the adjectives it contains, of the degree to which each holds of the pin, (5) and (6), with semantic value xs for size and xc for colour.

Equations

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

theorem DegenEtAl2020.meaning_nonneg {xs xc : ℝ} (hs0 : 0 ≤ xs) (hs1 : xs ≤ 1) (hc0 : 0 ≤ xc) (hc1 : xc ≤ 1) (u : Utterance) (o : Pin) : 0 ≤ meaning xs xc u o

theorem DegenEtAl2020.gain_smallBlue {xs xc : ℝ} (hs0 : 0 < xs) (hs1 : xs ≤ 1) (hc0 : 0 < xc) : (meaning xs xc Utterance.smallBlue Pin.smallBlue / ∑ o : Pin, meaning xs xc Utterance.smallBlue o) / (meaning xs xc Utterance.small Pin.smallBlue / ∑ o : Pin, meaning xs xc Utterance.small o) = gain 1 xs xc

Adding the redundant colour to the sufficient size multiplies the listener's probability of the small blue pin by the gain of the display.

theorem DegenEtAl2020.gain_bigRed {xs xc : ℝ} (hs0 : 0 < xs) (hc0 : 0 < xc) (hc1 : xc ≤ 1) : (meaning xs xc Utterance.bigRed Pin.bigRed / ∑ o : Pin, meaning xs xc Utterance.bigRed o) / (meaning xs xc Utterance.red Pin.bigRed / ∑ o : Pin, meaning xs xc Utterance.red o) = gain 1 xc xs

Adding the redundant size to the sufficient colour multiplies the listener's probability of the big red pin by the gain of the display with the two semantic values exchanged.

theorem DegenEtAl2020.color_overmodification_iff {xs xc α : ℝ} (hα : 0 < α) (hs0 : 0 < xs) (hs1 : xs < 1) (hc0 : 0 < xc) (hc1 : xc ≤ 1) : ((S1 α 0 (meaning xs xc)) Pin.smallBlue).real {Utterance.small} < ((S1 α 0 (meaning xs xc)) Pin.smallBlue).real {Utterance.smallBlue} ↔ 1 / 2 < xc

For the small blue pin and without cost, the redundant small blue is preferred to the sufficient small exactly when the semantic value of colour exceeds one half, whatever that of size short of Boolean.

theorem DegenEtAl2020.size_overmodification_iff {xs xc α : ℝ} (hα : 0 < α) (hs0 : 0 < xs) (hs1 : xs ≤ 1) (hc0 : 0 < xc) (hc1 : xc < 1) : ((S1 α 0 (meaning xs xc)) Pin.bigRed).real {Utterance.red} < ((S1 α 0 (meaning xs xc)) Pin.bigRed).real {Utterance.bigRed} ↔ 1 / 2 < xs

For the big red pin and without cost, the redundant big red is preferred to the sufficient red exactly when the semantic value of size exceeds one half, whatever that of colour short of Boolean.

theorem DegenEtAl2020.overmodification_odds_lt_iff {xs xc α : ℝ} {C : Utterance → ℝ} (hα : 0 < α) (hs0 : 0 < xs) (hs1 : xs ≤ 1) (hc0 : 0 < xc) (hc1 : xc ≤ 1) (hC : C Utterance.smallBlue - C Utterance.small = C Utterance.bigRed - C Utterance.red) : ((S1 α C (meaning xs xc)) Pin.bigRed).real {Utterance.bigRed} / ((S1 α C (meaning xs xc)) Pin.bigRed).real {Utterance.red} < ((S1 α C (meaning xs xc)) Pin.smallBlue).real {Utterance.smallBlue} / ((S1 α C (meaning xs xc)) Pin.smallBlue).real {Utterance.small} ↔ xs < xc

The odds of the redundant small blue against small for the small blue pin exceed the odds of the redundant big red against red for the big red pin exactly when size is noisier than colour, at every positive rationality and when the two redundant adjectives cost the same. This is the paper's asymmetry, more redundant use of colour than of size.

theorem DegenEtAl2020.small_distinguishes_iff {xs xc : ℝ} : Reference.Distinguishes (meaning xs xc) {Pin.bigBlue, Pin.bigRed} Pin.smallBlue Utterance.small ↔ 1 / 2 < xs

The sufficient small distinguishes the small blue pin from the big ones, so that the listener's best guess is the target, exactly when the semantic value of size beats chance.

theorem DegenEtAl2020.smallBlue_distinguishes_iff {xs xc : ℝ} (hc : 0 < xc) : Reference.Distinguishes (meaning xs xc) {Pin.bigBlue, Pin.bigRed} Pin.smallBlue Utterance.smallBlue ↔ 1 / 2 < xs ∧ 1 < xs + xc

The redundant small blue distinguishes the pin exactly when the semantic value of size beats chance and the two values together exceed one, so a noisy colour can cost the identification that the sufficient description had. With Boolean values both descriptions distinguish.

theorem DegenEtAl2020.boolean_no_preference (α : ℝ) : ((S1 α 0 (meaning 1 1)) Pin.smallBlue).real {Utterance.small} = ((S1 α 0 (meaning 1 1)) Pin.smallBlue).real {Utterance.smallBlue}

With Boolean values the redundant modifier adds nothing, since small and small blue both identify the small blue pin with certainty and are produced alike.