Communicative Efficiency: β-scalarization and Frontier Deviation

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

A CostPair is a 2-component cost profile (effort, information loss). Many linguistic phenomena arise from a tension between two functional pressures, and attested forms tend to be Pareto-efficient compromises.

Pareto dominance lives in Core.Constraint.Pareto. This file does not redefine it. CostPair.toProfile projects a cost pair into Core.Constraint.Profile ℝ 2, where paretoFeaturePreorder answers "is a Pareto-dominated by b?" via the substrate.

What this file does contribute is the β-scalarization (weightedCost) and the frontier-deviation primitives (efficiencyLossAt, efficiencyLoss) specific to the Xu-et-al / Kemp-Regier / Zaslavsky efficient-communication framework. These are not generic preorder operations.

Main definitions

• CostPair: 2-component cost (effort, information loss)
• CostPair.toProfile: bridge to Profile ℝ 2 for substrate-side Pareto
• weightedCost: linear scalarization L_β = cost₂ + β · cost₁
• efficiencyLossAt: per-β deviation from optimal
• efficiencyLoss: minimum deviation across a list of β values (corresponds to ε in @cite{xu-etal-2024} eq. 8)

structure Pragmatics.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 Pragmatics.Efficiency.CostPair.toProfile (c : CostPair) : Core.Constraint.Profile ℝ 2

Bridge a CostPair into the substrate Core.Constraint.Profile ℝ 2. Pareto dominance and optimality on cost pairs come for free via Core.Constraint.paretoFeaturePreorder composed with this function; no per-file dominates / isParetoOptimal redefinition is needed.

Equations

• c.toProfile 0 = c.cost₁
• c.toProfile 1 = c.cost₂

@[simp]

theorem Pragmatics.Efficiency.CostPair.toProfile_zero (c : CostPair) : c.toProfile 0 = c.cost₁

@[simp]

theorem Pragmatics.Efficiency.CostPair.toProfile_one (c : CostPair) : c.toProfile 1 = c.cost₂

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

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

Equations

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

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

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

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 ℝ) : ℝ

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

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 β₂