Communicative Efficiency and Pareto Optimality

@cite{xu-etal-2024} @cite{kemp-regier-2012} @cite{zaslavsky-kemp-regier-tishby-2018}

Domain-agnostic infrastructure for formalizing tradeoffs between competing communicative pressures via Pareto optimality. Many linguistic phenomena arise from the tension between two functional pressures — informativity vs. brevity, specificity vs. learnability, transparency vs. economy — and the resulting attested forms tend to be Pareto-efficient compromises.

Main definitions

• CostPair: two communicative costs (e.g., effort and information loss)
• dominates: strict Pareto dominance
• isParetoOptimal: non-dominated w.r.t. a set of alternatives
• weightedCost: linear scalarization with tradeoff parameter β
• efficiencyLoss: deviation from the Pareto frontier (Eq. 8 of @cite{xu-etal-2024})

structure Core.Efficiency.CostPair : Type

A pair of communicative costs. The framework is general: cost₁ and cost₂ can represent any two pressures in a functional tradeoff.

In @cite{xu-etal-2024}: cost₁ = speaker effort (word length), cost₂ = information loss (listener surprisal). In @cite{kemp-regier-2012}: cost₁ = complexity, cost₂ = informativeness loss. In @cite{zaslavsky-kemp-regier-tishby-2018}: cost₁ = I(W;U), cost₂ = D[p||q].

• cost₁ : ℚ
• cost₂ : ℚ

def Core.Efficiency.instReprCostPair.repr : CostPair → ℕ → Std.Format

Equations

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

instance Core.Efficiency.instReprCostPair : Repr CostPair

Equations

• Core.Efficiency.instReprCostPair = { reprPrec := Core.Efficiency.instReprCostPair.repr }

def Core.Efficiency.instDecidableEqCostPair.decEq (x✝ x✝¹ : CostPair) : Decidable (x✝ = x✝¹)

Equations

• Core.Efficiency.instDecidableEqCostPair.decEq { cost₁ := a, cost₂ := a_1 } { cost₁ := b, cost₂ := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance Core.Efficiency.instDecidableEqCostPair : DecidableEq CostPair

Equations

• Core.Efficiency.instDecidableEqCostPair = Core.Efficiency.instDecidableEqCostPair.decEq

def Core.Efficiency.instBEqCostPair.beq : CostPair → CostPair → Bool

Equations

• Core.Efficiency.instBEqCostPair.beq { cost₁ := a, cost₂ := a_1 } { cost₁ := b, cost₂ := b_1 } = (a == b && a_1 == b_1)
• Core.Efficiency.instBEqCostPair.beq x✝¹ x✝ = false

instance Core.Efficiency.instBEqCostPair : BEq CostPair

Equations

• Core.Efficiency.instBEqCostPair = { beq := Core.Efficiency.instBEqCostPair.beq }

def Core.Efficiency.dominates (a b : CostPair) : Prop

Pareto dominance: a dominates b iff a is at least as good on both dimensions and strictly better on at least one.

Equations

• Core.Efficiency.dominates a b = (a.cost₁ ≤ b.cost₁ ∧ a.cost₂ ≤ b.cost₂ ∧ (a.cost₁ < b.cost₁ ∨ a.cost₂ < b.cost₂))

theorem Core.Efficiency.dominates_irrefl (a : CostPair) : ¬dominates a a

theorem Core.Efficiency.dominates_trans {a b c : CostPair} (hab : dominates a b) (hbc : dominates b c) : dominates a c

def Core.Efficiency.isParetoOptimal (x : CostPair) (alternatives : List CostPair) : Prop

A cost pair is Pareto optimal if no alternative dominates it.

Equations

• Core.Efficiency.isParetoOptimal x alternatives = ∀ (y : Core.Efficiency.CostPair), y ∈ alternatives → ¬Core.Efficiency.dominates y x

def Core.Efficiency.weightedCost (c : CostPair) (β : ℚ) : ℚ

Weighted cost: linear scalarization of two costs. L_β = cost₂ + β · cost₁. β = 0 considers only cost₂; large β emphasizes cost₁.

Equations

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

def Core.Efficiency.efficiencyLossAt (attested optimal : CostPair) (β : ℚ) : ℚ

Efficiency loss at a specific β: deviation from the optimal encoding.

Equations

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

def Core.Efficiency.efficiencyLoss (attested : CostPair) (optimalAt : ℚ → CostPair) (βs : List ℚ) : ℚ

Overall efficiency loss: minimum deviation across β values. ε = min_β (L_β[attested] − L_β[optimal_β]) (Eq. 8, @cite{xu-etal-2024}).

Equations

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

theorem Core.Efficiency.efficiencyLossAt_self (c : CostPair) (β : ℚ) : efficiencyLossAt c c β = 0

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