Communicative efficiency

This file defines the scalarization of a pair of communicative costs by a tradeoff parameter and the deviation of an attested encoding from the efficient frontier.

Many linguistic phenomena arise from a tension between two functional pressures, and attested forms tend to be efficient compromises between them. A CostPair records the two costs. In the work of Xu and colleagues they are speaker effort, measured by word length, and information loss, measured by listener surprisal. For Kemp and Regier they are complexity and loss of informativeness, and for Zaslavsky and colleagues they are the complexity I(W;U) and the distortion D[p‖q] of an information bottleneck. The weighted cost L_β = cost₂ + β · cost₁ trades one against the other, and the efficiency loss of an attested pair is its least deviation, over a list of values of β, from the pair that is optimal at that β.

Main definitions

• CostPair: a pair of costs, such as effort and information loss.
• weightedCost: the linear scalarization L_β = cost₂ + β · cost₁.
• efficiencyLossAt: the deviation from the optimal pair at one β.
• efficiencyLoss: the least deviation across a list of values of β.

Main results

• frontier_antitone: optimal pairs move along the frontier as β grows, with smaller cost₁ and larger cost₂.
• efficiencyLoss_nonneg: the efficiency loss against optimal pairs is nonnegative.

References

• A. Xu, C. Kemp, L. Frermann and Y. Xu, Word reuse and combination support efficient communication of emerging concepts (2024)
• C. Kemp and T. Regier, Kinship categories across languages reflect general communicative principles (2012)
• N. Zaslavsky, C. Kemp, T. Regier and N. Tishby, Efficient compression in color naming and its evolution (2018)

structure Pragmatics.Efficiency.CostPair : Type

A pair of communicative costs, which can stand for any two pressures in a functional tradeoff.

• cost₁ : ℝ
• cost₂ : ℝ

def Pragmatics.Efficiency.weightedCost (c : CostPair) (β : ℝ) : ℝ

The weighted cost is the linear scalarization L_β = cost₂ + β · cost₁ of the two costs. At β = 0 only cost₂ counts, and a large β emphasizes cost₁.

Equations

• Pragmatics.Efficiency.weightedCost c β = c.cost₂ + β * c.cost₁

def Pragmatics.Efficiency.efficiencyLossAt (attested optimal : CostPair) (β : ℝ) : ℝ

The efficiency loss at β is the deviation of the attested pair from the optimal one.

Equations

• Pragmatics.Efficiency.efficiencyLossAt attested optimal β = Pragmatics.Efficiency.weightedCost attested β - Pragmatics.Efficiency.weightedCost optimal β

noncomputable def Pragmatics.Efficiency.efficiencyLoss (attested : CostPair) (optimalAt : ℝ → CostPair) (βs : List ℝ) : ℝ

The overall efficiency loss is the least deviation across the listed values of β, ε = min_β (L_β[attested] − L_β[optimal_β]).

Equations

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

@[simp]

theorem Pragmatics.Efficiency.efficiencyLossAt_self (c : CostPair) (β : ℝ) : efficiencyLossAt c c β = 0

theorem Pragmatics.Efficiency.weightedCost_mono_β (c : CostPair) {β₁ β₂ : ℝ} (hβ : β₁ ≤ β₂) (hc : 0 ≤ c.cost₁) : weightedCost c β₁ ≤ weightedCost c β₂

theorem Pragmatics.Efficiency.frontier_antitone {a b : CostPair} {β₁ β₂ : ℝ} (hβ₁ : 0 ≤ β₁) (hβ : β₁ < β₂) (h₁ : weightedCost a β₁ ≤ weightedCost b β₁) (h₂ : weightedCost b β₂ ≤ weightedCost a β₂) : b.cost₁ ≤ a.cost₁ ∧ a.cost₂ ≤ b.cost₂

Optimal cost pairs move along the frontier as the tradeoff parameter grows, so the pair optimal at the larger β has the smaller cost₁ and the larger cost₂.

theorem Pragmatics.Efficiency.efficiencyLossAt_nonneg {attested optimal : CostPair} {β : ℝ} (h : weightedCost optimal β ≤ weightedCost attested β) : 0 ≤ efficiencyLossAt attested optimal β

The deviation from an encoding optimal at β is nonnegative.

theorem Pragmatics.Efficiency.efficiencyLoss_nonneg {attested : CostPair} {optimalAt : ℝ → CostPair} {βs : List ℝ} (h : ∀ β ∈ βs, weightedCost (optimalAt β) β ≤ weightedCost attested β) : 0 ≤ efficiencyLoss attested optimalAt βs

The efficiency loss against encodings optimal at each listed β is nonnegative.