Giles, Rubio-Fernandez and Mollica (2026): Search Efficiency Drives Reference Production Across Modalities, But Colour Is Special

This file formalizes the search-efficiency view of overinformative reference as [GRFM26] test it across attributes and sensory modalities. On that view ([RF19], [JERF22]) a speaker adds a redundant modifier when it speeds the listener's search for the referent, and a description guides search along the most discriminable attribute it mentions (Display.efficiency); so a redundant attribute exerts a pressure to overinform exactly when it is more discriminable than the attribute that already singles out the target (Display.Pressure, Display.pressure_iff). The three display types of the first experiment, built from the two calibration points the psychophysical staircases deliver, come out as the paper predicts: pressure when the sufficient attribute is hard and the redundant one easy, none when both are easy or the redundant one is hard (predicted_sHighRLow, predicted_baseline). The rival strategy of mentioning every highly discriminable attribute ([FC22]) cannot tell the baseline from the critical display (highRedundant_predicted_baseline), and the baseline contrast decides between the two (rows_baseline_refutes_highRedundant).

Any strategy that reads only the display predicts no difference between two redundant attributes at matched discriminability (predictedBy_self). The data contradict this twice: redundant colour is used more than redundant material in the first experiment and more than redundant orientation in the second, where attentional guidance, production effort and term frequency are controlled (rows_colour_special), while low- and high-frequency colour terms do not differ (rows_frequency_predicted).

Implementation notes

• Discriminability is the two-point scale the adaptive staircases produce for each participant and attribute (Discriminability); the model is stated for any linear order so that graded measures fit it too.
• A row is one non-reference level of one predictor of the paper's regressions (Tables 1 and 2); its observed direction against the reference level is the side of zero its 95% credible interval lies on (Row.observed), and the coefficients stay in the data rows.
• In the second experiment the sufficient attribute is the shape noun, which was never at a category boundary, so both attributes count as highly discriminable there.
• The paper's speculations about why colour is privileged, optimised category partitions and learned strategy selection, are not modelled; nor are display density and contextual distinctiveness, which the second experiment varied without finding an effect.

References

• [GRFM26]
• [RF19]
• [JERF22]
• [FC22]
• [KD21]
• [DHG+20]
• [WH17]

Displays and the predictions of a production strategy

structure GilesEtAl2026.Display (D : Type u_2) : Type u_2

A display as the speaker's choice sees it: the perceptual discriminability of the attribute that alone singles out the target and that of the redundant attribute.

• sufficient : D

  Discriminability of the sufficient attribute.

• redundant : D

  Discriminability of the redundant attribute.

def GilesEtAl2026.instDecidableEqDisplay.decEq {D✝ : Type u_2} [DecidableEq D✝] (x✝ x✝¹ : Display D✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance GilesEtAl2026.instDecidableEqDisplay {D✝ : Type u_2} [DecidableEq D✝] : DecidableEq (Display D✝)

Equations

• GilesEtAl2026.instDecidableEqDisplay = GilesEtAl2026.instDecidableEqDisplay.decEq

inductive GilesEtAl2026.Description : Type

The speaker's options: the sufficient attribute alone, or both attributes.

• minimal : Description
• overinformative : Description

@[instance_reducible]

instance GilesEtAl2026.instDecidableEqDescription : DecidableEq Description

Equations

• GilesEtAl2026.instDecidableEqDescription x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive GilesEtAl2026.Direction : Type

The direction of a level against its reference level.

• lower : Direction
• higher : Direction
• null : Direction

@[instance_reducible]

instance GilesEtAl2026.instDecidableEqDirection : DecidableEq Direction

Equations

• GilesEtAl2026.instDecidableEqDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance GilesEtAl2026.instReprDirection : Repr Direction

Equations

• GilesEtAl2026.instReprDirection = { reprPrec := GilesEtAl2026.instReprDirection.repr }

def GilesEtAl2026.instReprDirection.repr : Direction → ℕ → Std.Format

Equations

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

def GilesEtAl2026.predictedBy {D : Type u_1} (P : Display D → Prop) [DecidablePred P] (level ref : Display D) : Direction

The direction a production strategy predicts for a level against its reference, given the condition P under which the strategy overinforms.

Equations

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

theorem GilesEtAl2026.predictedBy_eq_null {D : Type u_1} {P : Display D → Prop} [DecidablePred P] {level ref : Display D} (h : P level ↔ P ref) : predictedBy P level ref = Direction.null

theorem GilesEtAl2026.predictedBy_eq_lower {D : Type u_1} {P : Display D → Prop} [DecidablePred P] {level ref : Display D} (hl : ¬P level) (hr : P ref) : predictedBy P level ref = Direction.lower

theorem GilesEtAl2026.predictedBy_self {D : Type u_1} (P : Display D → Prop) [DecidablePred P] (d : Display D) : predictedBy P d d = Direction.null

A strategy that reads only the display predicts no difference between two conditions with the same display, in particular between two redundant attributes at matched discriminability.

Search efficiency

def GilesEtAl2026.Display.efficiency {D : Type u_1} [LinearOrder D] (d : Display D) : Description → D

A description guides the listener's search along the most discriminable attribute it mentions.

Equations

• d.efficiency GilesEtAl2026.Description.minimal = d.sufficient
• d.efficiency GilesEtAl2026.Description.overinformative = max d.sufficient d.redundant

def GilesEtAl2026.Display.Pressure {D : Type u_1} [LinearOrder D] (d : Display D) : Prop

The search-efficiency pressure to overinform: the redundant attribute makes the description easier to search with.

Equations

• d.Pressure = (d.efficiency GilesEtAl2026.Description.minimal < d.efficiency GilesEtAl2026.Description.overinformative)

@[instance_reducible]

instance GilesEtAl2026.instDecidablePressure {D : Type u_1} [LinearOrder D] (d : Display D) : Decidable d.Pressure

Equations

• GilesEtAl2026.instDecidablePressure d = GilesEtAl2026.instDecidablePressure._aux_1 d

theorem GilesEtAl2026.Display.pressure_iff {D : Type u_1} [LinearOrder D] (d : Display D) : d.Pressure ↔ d.sufficient < d.redundant

def GilesEtAl2026.Display.HighRedundant {D : Type u_1} [LinearOrder D] (θ : D) (d : Display D) : Prop

The rival strategy's condition for overinforming: the redundant attribute reaches the threshold θ of high discriminability, whether or not it is needed.

Equations

• GilesEtAl2026.Display.HighRedundant θ d = (θ ≤ d.redundant)

@[instance_reducible]

instance GilesEtAl2026.instDecidableHighRedundant {D : Type u_1} [LinearOrder D] (θ : D) (d : Display D) : Decidable (Display.HighRedundant θ d)

Equations

• GilesEtAl2026.instDecidableHighRedundant θ d = GilesEtAl2026.instDecidableHighRedundant._aux_1 θ d

The display types of the first experiment

inductive GilesEtAl2026.DisplayType : Type

The display types of the first experiment: the sufficient attribute of high and the redundant one of low discriminability, the reverse, and both high.

• sHighRLow : DisplayType
• sLowRHigh : DisplayType
• baseline : DisplayType

@[instance_reducible]

instance GilesEtAl2026.instDecidableEqDisplayType : DecidableEq DisplayType

Equations

• GilesEtAl2026.instDecidableEqDisplayType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def GilesEtAl2026.instReprDisplayType.repr : DisplayType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance GilesEtAl2026.instReprDisplayType : Repr DisplayType

Equations

• GilesEtAl2026.instReprDisplayType = { reprPrec := GilesEtAl2026.instReprDisplayType.repr }

def GilesEtAl2026.DisplayType.display {D : Type u_1} (lo hi : D) : DisplayType → Display D

The display of a type, from the low and the high calibration point.

Equations

• GilesEtAl2026.DisplayType.display lo hi GilesEtAl2026.DisplayType.sHighRLow = { sufficient := hi, redundant := lo }
• GilesEtAl2026.DisplayType.display lo hi GilesEtAl2026.DisplayType.sLowRHigh = { sufficient := lo, redundant := hi }
• GilesEtAl2026.DisplayType.display lo hi GilesEtAl2026.DisplayType.baseline = { sufficient := hi, redundant := hi }

theorem GilesEtAl2026.pressure_sLowRHigh {D : Type u_1} [LinearOrder D] {lo hi : D} (h : lo < hi) : (DisplayType.display lo hi DisplayType.sLowRHigh).Pressure

theorem GilesEtAl2026.not_pressure_sHighRLow {D : Type u_1} [LinearOrder D] {lo hi : D} (h : lo < hi) : ¬(DisplayType.display lo hi DisplayType.sHighRLow).Pressure

theorem GilesEtAl2026.not_pressure_baseline {D : Type u_1} [LinearOrder D] {lo hi : D} : ¬(DisplayType.display lo hi DisplayType.baseline).Pressure

theorem GilesEtAl2026.predicted_sHighRLow {D : Type u_1} [LinearOrder D] {lo hi : D} (h : lo < hi) : predictedBy Display.Pressure (DisplayType.display lo hi DisplayType.sHighRLow) (DisplayType.display lo hi DisplayType.sLowRHigh) = Direction.lower

Against the critical display, the view predicts less overinformativeness when the sufficient attribute is easy and the redundant one hard.

theorem GilesEtAl2026.predicted_baseline {D : Type u_1} [LinearOrder D] {lo hi : D} (h : lo < hi) : predictedBy Display.Pressure (DisplayType.display lo hi DisplayType.baseline) (DisplayType.display lo hi DisplayType.sLowRHigh) = Direction.lower

Against the critical display, the view predicts less overinformativeness when both attributes are easy: speakers do not simply mention every easy attribute.

theorem GilesEtAl2026.highRedundant_predicted_baseline {D : Type u_1} [LinearOrder D] {lo hi : D} : predictedBy (Display.HighRedundant hi) (DisplayType.display lo hi DisplayType.baseline) (DisplayType.display lo hi DisplayType.sLowRHigh) = Direction.null

The rival strategy predicts no difference between the baseline and the critical display.

The regressions

inductive GilesEtAl2026.Discriminability : Type

The calibration points the adaptive staircases deliver for each participant and attribute: a stimulus the participant categorizes consistently and one at the participant's category boundary.

• low : Discriminability
• high : Discriminability

@[instance_reducible]

instance GilesEtAl2026.instDecidableEqDiscriminability : DecidableEq Discriminability

Equations

• GilesEtAl2026.instDecidableEqDiscriminability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance GilesEtAl2026.instReprDiscriminability : Repr Discriminability

Equations

• GilesEtAl2026.instReprDiscriminability = { reprPrec := GilesEtAl2026.instReprDiscriminability.repr }

def GilesEtAl2026.instReprDiscriminability.repr : Discriminability → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance GilesEtAl2026.instLinearOrderDiscriminability : LinearOrder Discriminability

Equations

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

theorem GilesEtAl2026.Discriminability.low_lt_high : low < high

inductive GilesEtAl2026.Predictor : Type

The predictors of the two regressions.

• displayType : Predictor
• attribute : Predictor
• frequency : Predictor

@[instance_reducible]

instance GilesEtAl2026.instDecidableEqPredictor : DecidableEq Predictor

Equations

• GilesEtAl2026.instDecidableEqPredictor x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance GilesEtAl2026.instReprPredictor : Repr Predictor

Equations

• GilesEtAl2026.instReprPredictor = { reprPrec := GilesEtAl2026.instReprPredictor.repr }

def GilesEtAl2026.instReprPredictor.repr : Predictor → ℕ → Std.Format

Equations

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

structure GilesEtAl2026.Row : Type

A non-reference level of a predictor: the displays of the level and of the reference level, and the 95% credible interval of its coefficient in hundredths of a logit.

• experiment : ℕ
• predictor : Predictor
• level : Display Discriminability
• reference : Display Discriminability
• ci : ℤ × ℤ

def GilesEtAl2026.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance GilesEtAl2026.instDecidableEqRow : DecidableEq Row

Equations

• GilesEtAl2026.instDecidableEqRow = GilesEtAl2026.instDecidableEqRow.decEq

def GilesEtAl2026.discriminability : List (String × Discriminability)

Equations

• GilesEtAl2026.discriminability = [("low", GilesEtAl2026.Discriminability.low), ("high", GilesEtAl2026.Discriminability.high)]

def GilesEtAl2026.Row.ofDatum (ex : Datum) : Option Row

Equations

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

def GilesEtAl2026.Row.observed (r : Row) : Direction

The observed direction of a level against its reference: the side of zero its credible interval lies on, null when the interval includes zero.

Equations

• r.observed = if r.ci.2 < 0 then GilesEtAl2026.Direction.lower else if 0 < r.ci.1 then GilesEtAl2026.Direction.higher else GilesEtAl2026.Direction.null

def GilesEtAl2026.Row.predicted (r : Row) : Direction

The direction the search-efficiency view predicts for the level.

Equations

• r.predicted = GilesEtAl2026.predictedBy GilesEtAl2026.Display.Pressure r.level r.reference

def GilesEtAl2026.rows : List Row

The five coefficients of Tables 1 and 2.

Equations

• GilesEtAl2026.rows = List.filterMap GilesEtAl2026.Row.ofDatum GilesEtAl2026.Examples.all

theorem GilesEtAl2026.rows_displayType_predicted (r : Row) : r ∈ rows → r.predictor = Predictor.displayType → r.observed = r.predicted

Both display-type contrasts of the first experiment go the way the view predicts.

theorem GilesEtAl2026.rows_baseline_refutes_highRedundant (r : Row) : r ∈ rows → r.predictor = Predictor.displayType → r.level = DisplayType.display Discriminability.low Discriminability.high DisplayType.baseline → r.observed ≠ predictedBy (Display.HighRedundant Discriminability.high) r.level r.reference

The baseline contrast refutes the strategy of mentioning every highly discriminable attribute, which predicts no difference from the critical display.

theorem GilesEtAl2026.rows_attribute_level_eq_reference (r : Row) : r ∈ rows → r.predictor = Predictor.attribute → r.level = r.reference

theorem GilesEtAl2026.rows_attribute_observed_lower (r : Row) : r ∈ rows → r.predictor = Predictor.attribute → r.observed = Direction.lower

theorem GilesEtAl2026.rows_colour_special (P : Display Discriminability → Prop) [DecidablePred P] (r : Row) : r ∈ rows → r.predictor = Predictor.attribute → predictedBy P r.level r.reference = Direction.null ∧ r.observed = Direction.lower

Colour is special: no strategy that reads only the display distinguishes the redundant attributes of either experiment, yet redundant material and redundant orientation are both used less than redundant colour.

theorem GilesEtAl2026.rows_frequency_predicted (r : Row) : r ∈ rows → r.predictor = Predictor.frequency → r.observed = r.predicted

Low- and high-frequency colour terms do not differ, as the view predicts for one attribute at one discriminability.