Documentation

Linglib.Theories.Pragmatics.RSA.Core.Noise

Unified Noise Theory for RSA #

@cite{waldon-degen-2021} @cite{kursat-degen-2021} @cite{giles-etal-2026}

This module provides a unified treatment of noise in RSA models.

Noise Models in RSA #

Paper	Noise Type	Location
@cite{bergen-goodman-2015}	Channel	Transmission
@cite{degen-etal-2020}	Semantic	Perception
@cite{kursat-degen-2021}	Perceptual	Verification
@cite{giles-etal-2026}	Search efficiency	Psychophysics

Insight #

All four use the same underlying operation:

noiseChannel(match, mismatch, b) = match * b + mismatch * (1 - b)

Perceptual Grounding #

@cite{giles-etal-2026} provide experimental evidence for the perceptual grounding of noise parameters: discriminability (noise gap) is measured via psychophysical staircases, connecting the abstract match/mismatch parameters to observable perceptual thresholds. Their Exp 1 shows that overinformativeness tracks discriminability × sufficiency across both visual (colour) and auditory (material) modalities.

However, noise discrimination alone does not explain why colour is disproportionately overinformed relative to other privileged features like orientation (Exp 2). The residual colour privilege may reflect the optimality of colour naming systems (@cite{regier-etal-2007}, @cite{zaslavsky-etal-2019}): colour categories are partitioned to maximise perceptual discriminability, making colour inherently more search-efficient than attributes whose category boundaries are not perceptually optimised.

Current Status: Shallow Integration #

Currently, implementations import this module but don't deeply integrate:

Proofs still unfold definitions manually rather than using shared lemmas
No common typeclass that implementations instantiate
Theorems must be re-proven in each implementation

Future Work: Deep Integration #

Proper integration would involve:

1. Typeclass for Noisy Semantics #

class NoisySemantics (U W : Type) where
  φ : U → W → ℚ
  noiseParams : FeatureType → NoiseParams
  φ_decomposition : φ u w = Π features, noiseChannel (noiseParams f) (booleanMatch f u w)

2. Generic Theorems #

theorem discrimination_from_params [NoisySemantics U W] (f : FeatureType) :
    featureDiscrimination f = (noiseParams f).discrimination

3. Automatic Instantiation #

instance : NoisySemantics ReferringExpression Object := DegenSemantics
instance : NoisySemantics Utterance Meaning := BergenSemantics

-- Theorems apply to both automatically
#check @discrimination_from_params _ _ DegenSemantics

4. Information-Theoretic Measures #

The current "discrimination" measure (match - mismatch) is a proxy for informativeness but not actual mutual information I(X;Y). A proper treatment would compute channel capacity:

C = 1 - H(ε) -- for binary symmetric channel with error rate ε

def RSA.Noise.noiseChannel (onMatch onMismatch b : ℚ) :

The fundamental noise channel operation.

Transforms Boolean b ∈ {0, 1} into graded value in [mismatch, match].

Equations

RSA.Noise.noiseChannel onMatch onMismatch b = onMatch * b + onMismatch * (1 - b)

Instances For

def RSA.Noise.noiseGap (onMatch onMismatch : ℚ) :

The noise gap measures discrimination power.

Equations

RSA.Noise.noiseGap onMatch onMismatch = onMatch - onMismatch

Instances For

@[simp]

theorem RSA.Noise.noiseChannel_one (onMatch onMismatch : ℚ) :

noiseChannel onMatch onMismatch 1 = onMatch

@[simp]

theorem RSA.Noise.noiseChannel_zero (onMatch onMismatch : ℚ) :

noiseChannel onMatch onMismatch 0 = onMismatch

theorem RSA.Noise.noiseChannel_discrimination (onMatch onMismatch : ℚ) :

noiseChannel onMatch onMismatch 1 - noiseChannel onMatch onMismatch 0 = noiseGap onMatch onMismatch

def RSA.Noise.colorMatch :

Color parameters from @cite{degen-etal-2020}: low noise

Equations

RSA.Noise.colorMatch = 99 / 100

Instances For

def RSA.Noise.colorMismatch :

Equations

RSA.Noise.colorMismatch = 1 / 100

Instances For

def RSA.Noise.colorDiscrimination :

Equations

RSA.Noise.colorDiscrimination = RSA.Noise.colorMatch - RSA.Noise.colorMismatch

Instances For

def RSA.Noise.sizeMatch :

Size parameters from @cite{degen-etal-2020}: medium noise

Equations

RSA.Noise.sizeMatch = 8 / 10

Instances For

def RSA.Noise.sizeMismatch :

Equations

RSA.Noise.sizeMismatch = 2 / 10

Instances For

def RSA.Noise.sizeDiscrimination :

Equations

RSA.Noise.sizeDiscrimination = RSA.Noise.sizeMatch - RSA.Noise.sizeMismatch

Instances For

def RSA.Noise.materialMatch :

Material parameters (HYPOTHETICAL, not from any paper): high noise. @cite{kursat-degen-2021} establishes the ordering (material harder than color) but not specific channel parameters.

Equations

RSA.Noise.materialMatch = 7 / 10

Instances For

def RSA.Noise.materialMismatch :

Equations

RSA.Noise.materialMismatch = 3 / 10

Instances For

def RSA.Noise.materialDiscrimination :

Equations

RSA.Noise.materialDiscrimination = RSA.Noise.materialMatch - RSA.Noise.materialMismatch

Instances For

def RSA.Noise.orientationMatch :

Orientation parameters: high discrimination (like colour). @cite{giles-etal-2026} Exp 2 confirms ≥99% labelling accuracy for orientation (vertical vs horizontal), comparable to colour. Orientation is a privileged visual feature (@cite{wolfe-horowitz-2017}) capable of producing pop-out effects and guiding pre-attentive search.

Despite equal discrimination, colour is overinformed more than orientation — this dissociation is the key finding of Exp 2.

Equations

RSA.Noise.orientationMatch = 99 / 100

Instances For

def RSA.Noise.orientationMismatch :

Equations

RSA.Noise.orientationMismatch = 1 / 100

Instances For

def RSA.Noise.orientationDiscrimination :

Equations

RSA.Noise.orientationDiscrimination = RSA.Noise.orientationMatch - RSA.Noise.orientationMismatch

Instances For

theorem RSA.Noise.color_gt_size :

colorDiscrimination > sizeDiscrimination

Color has higher discrimination than size

theorem RSA.Noise.size_gt_material :

sizeDiscrimination > materialDiscrimination

Size has higher discrimination than material

theorem RSA.Noise.color_eq_orientation :

colorDiscrimination = orientationDiscrimination

Colour and orientation have equal discrimination.

theorem RSA.Noise.discrimination_ordering :

colorDiscrimination > sizeDiscrimination ∧ sizeDiscrimination > materialDiscrimination

Full ordering: color = orientation > size > material

theorem RSA.Noise.discrimination_ordering_full :

colorDiscrimination = orientationDiscrimination ∧ colorDiscrimination > sizeDiscrimination ∧ sizeDiscrimination > materialDiscrimination

The full ordering including orientation.

inductive RSA.Noise.PerceptualDifficulty :

Perceptual difficulty levels

Instances For

instance RSA.Noise.instDecidableEqPerceptualDifficulty :

DecidableEq PerceptualDifficulty

Equations

RSA.Noise.instDecidableEqPerceptualDifficulty x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def RSA.Noise.instBEqPerceptualDifficulty.beq :

PerceptualDifficulty → PerceptualDifficulty → Bool

Equations

RSA.Noise.instBEqPerceptualDifficulty.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance RSA.Noise.instBEqPerceptualDifficulty :

BEq PerceptualDifficulty

Equations

RSA.Noise.instBEqPerceptualDifficulty = { beq := RSA.Noise.instBEqPerceptualDifficulty.beq }

instance RSA.Noise.instReprPerceptualDifficulty :

Repr PerceptualDifficulty

Equations

RSA.Noise.instReprPerceptualDifficulty = { reprPrec := RSA.Noise.instReprPerceptualDifficulty.repr }

def RSA.Noise.instReprPerceptualDifficulty.repr :

PerceptualDifficulty → ℕ → Std.Format

Equations

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

Instances For

def RSA.Noise.difficultyToDiscrimination :

PerceptualDifficulty → ℚ

Map difficulty to discrimination

Equations

Instances For

theorem RSA.Noise.easier_higher_discrimination :

difficultyToDiscrimination PerceptualDifficulty.easy > difficultyToDiscrimination PerceptualDifficulty.hard

Easier perception → higher discrimination

theorem RSA.Noise.noise_model_predicts_no_colour_orientation_difference :

colorDiscrimination = orientationDiscrimination

The noise model predicts that attributes with equal discrimination should be overinformed at equal rates. Colour and orientation have equal noise discrimination (0.98), so the noise model predicts no preference between them.

@cite{giles-etal-2026} Exp 2 falsifies this prediction: colour is overinformed significantly more than orientation (β = −0.97, 95% CI = [−1.20, −0.75]) even when controlling for:

Perceptual discriminability (both ≥99% labelling accuracy)
Contextual distinctiveness (both equally salient)
Production effort (button-click equalises effort)
Word frequency (low-frequency colour terms tested)

This means the noise model is necessary but not sufficient: discriminability drives overinformativeness (Exp 1), but something additional about colour — plausibly the perceptual optimality of colour category boundaries (@cite{regier-etal-2007}) — produces a residual privilege.

theorem RSA.Noise.product_discrimination_monotone (match₁ mismatch₁ match₂ mismatch₂ sizeMatch sizeMismatch : ℚ) (h_gap : match₁ - mismatch₁ ≥ match₂ - mismatch₂) (h_match_mono : match₁ ≥ match₂) (h_size_nonneg : sizeMatch ≥ 0 ∧ sizeMismatch ≥ 0) (h_size_order : sizeMatch ≥ sizeMismatch) :

match₁ * sizeMatch - mismatch₁ * sizeMismatch ≥ match₂ * sizeMatch - mismatch₂ * sizeMismatch

Product discrimination is monotone: when match scores are individually at least as large AND the gap is at least as large, the weighted product is at least as large.

The gap condition alone is insufficient — counterexample: match₁=0, match₂=10, mismatch₁=0, mismatch₂=11, sizeMatch=100, sizeMismatch=1. Gap: 0 ≥ -1 ✓, but 0·100-0·1=0 < 10·100-11·1=989.

def Core.PropertyDomain.noiseDiscrimination :

PropertyDomain → Option ℚ

Map a PropertyDomain to its established noise discrimination value. Returns none for domains without empirically grounded noise params.

Equations

Instances For