Documentation

Linglib.Theories.Pragmatics.RSA.Core.RankingBridge

Ranking Functions as RSA Limits #

@cite{spohn-1988} @cite{goldszmidt-pearl-1996} @cite{frank-goodman-2012}

As the rationality parameter α → ∞, softmax-based probabilistic inference converges to ranking-based default reasoning. This file makes the connection precise.

Key results #

  1. rankToScore: Every ranking function κ induces scores s(w) = -κ(w).
  2. softmax_concentrates_unique: softmax(s, α) → point mass on the unique rank-0 world as α → ∞.
  3. minRank_worlds_satisfy: Under ranking entailment, all minimum-rank φ-worlds satisfy σ — connecting to the softmax limit.
  4. condProb_tendsto_one: Conditional Softmax Limit Theorem — P_α(σ|φ) → 1 as α → ∞ whenever κ ⊨ φ → σ. This is the central result: RSA with infinite rationality = ranking entailment.

Mathematical background #

@cite{spohn-1988} §7 observes that rankings are ordinal probabilities: κ(w) = n corresponds to P(w) ∝ ε^n for infinitesimal ε. The finite analogue replaces ε^n with exp(-n·α) for large α:

softmax(-κ, α)(w) = exp(-α · κ(w)) / Σ_v exp(-α · κ(v))

As α → ∞, this concentrates on rank-0 (most normal) worlds — exactly the worlds that survive ranking-based default reasoning.

This makes System Z's κ^z ranking (@cite{goldszmidt-pearl-1996}) the "infinite rationality" limit of RSA pragmatic inference (@cite{frank-goodman-2012}). Qualitative default reasoning and quantitative Bayesian pragmatics are not rival frameworks but endpoints of the same rationality continuum.

Convert a ranking function to softmax scores.

s(w) = -(κ(w) : ℝ). Lower rank → higher score → more plausible.

This is the finite analogue of @cite{spohn-1988} §7's P(w) ∝ ε^{κ(w)}: here exp(α · s(w)) = exp(-α · κ(w)) plays the role of ε^{κ(w)} with ε = exp(-α).

Equations
Instances For

    rankToScore reverses the ordering: higher rank ↔ lower score.

    Rank-0 worlds achieve the maximum score (0).

    Rank-0 worlds maximize the score.

    theorem Theories.Pragmatics.RSA.RankingBridge.softmax_concentrates_unique {W : Type u_1} [Fintype W] [DecidableEq W] [Nonempty W] (κ : Core.Logic.Ranking.RankingFunction W) (w₀ : W) (h_zero : κ.rank w₀ = 0) (h_unique : ∀ (v : W), v w₀0 < κ.rank v) (w : W) :
    Filter.Tendsto (fun (α : ) => Core.softmax (rankToScore κ) α w) Filter.atTop (nhds (if w = w₀ then 1 else 0))

    When κ has a unique rank-0 world, softmax(rankToScore κ, α) concentrates on it as α → ∞.

    This is the core convergence result: the probabilistic distribution approaches a point mass on the most normal world, recovering the ranking-based notion of normality.

    Proof: Apply Softmax.tendsto_softmax_infty_unique_max with scores s = rankToScore κ. The unique rank-0 world maximizes s (since s(w) = -κ(w) and κ(w₀) = 0 < κ(v) for v ≠ w₀).

    theorem Theories.Pragmatics.RSA.RankingBridge.entropy_vanishes_unique {W : Type u_1} [Fintype W] [DecidableEq W] [Nonempty W] (κ : Core.Logic.Ranking.RankingFunction W) (w₀ : W) (h_zero : κ.rank w₀ = 0) (h_unique : ∀ (v : W), v w₀0 < κ.rank v) :

    Entropy of softmax(rankToScore κ, α) → 0 as α → ∞ (unique rank-0 case). The distribution becomes maximally concentrated.

    noncomputable def Theories.Pragmatics.RSA.RankingBridge.minRankBool {W : Type u_1} [Fintype W] (κ : Core.Logic.Ranking.RankingFunction W) (φ : WBool) ( : ∃ (w : W), φ w = true) :

    The minimum rank among worlds satisfying a Bool predicate.

    Equations
    Instances For
      theorem Theories.Pragmatics.RSA.RankingBridge.rankEntails_iff_minRank_lt {W : Type u_1} [Fintype W] (κ : Core.Logic.Ranking.RankingFunction W) (φ σ : WBool) (hφσ : ∃ (w : W), (φ w && σ w) = true) :
      Core.Logic.SystemZ.rankEntails κ φ σ ∀ (w : W), (φ w && !σ w) = trueminRankBool κ (fun (v : W) => φ v && σ v) hφσ < κ.rank w

      rankEntails is equivalent to: every φ∧¬σ world has strictly higher rank than some φ∧σ world.

      When φ∧σ is non-empty, this is the same as: the minimum rank among φ∧σ worlds is strictly less than the rank of every φ∧¬σ world. When φ∧¬σ is empty, rankEntails holds vacuously.

      theorem Theories.Pragmatics.RSA.RankingBridge.minRank_worlds_satisfy {W : Type u_1} [Fintype W] (κ : Core.Logic.Ranking.RankingFunction W) (φ σ : WBool) (h : Core.Logic.SystemZ.rankEntails κ φ σ) ( : ∃ (w : W), φ w = true) (w : W) :
      φ w = trueκ.rank w = minRankBool κ φ σ w = true

      Under ranking entailment, all minimum-rank φ-worlds satisfy σ.

      This is the key lemma connecting ranking entailment to softmax concentration: as α → ∞, softmax concentrates on minimum-rank worlds. If all minimum-rank φ-worlds satisfy σ, then the limiting conditional probability P(σ|φ) = 1.

      Proof: If a minimum-rank φ-world w fails σ, then rankEntails gives a φ∧σ world v with κ(v) < κ(w), contradicting w having the minimum rank among φ-worlds.

      The theorems above establish the formal bridge between RSA and ranking-based default reasoning:

      ```
      α = 0          α finite           α → ∞
      uniform ←——— softmax(s, α) ———→ hardmax
      no inference   RSA pragmatics     ranking entailment
      ```
      
      At α = 0, the listener has no rationality assumption and
      the posterior is uniform (`Softmax.tendsto_softmax_zero`).
      At finite α, the listener performs soft Bayesian inference
      (standard RSA). As α → ∞, the posterior concentrates on
      the most normal worlds (`softmax_concentrates_unique`),
      and inference becomes ranking entailment.
      
      This justifies two practices:
      1. RSA modelers can use System Z rankings as the "skeleton"
         of their prior, softened by finite α for gradient predictions.
      2. Default reasoning theorists can view their qualitative
         inferences as the limiting case of probabilistic pragmatics. 
      

      The exponential prior induced by a ranking function.

      P(w) = exp(-κ(w)). This is the natural prior for connecting ranking functions to Bayesian inference: rank-0 worlds get maximal prior probability, and the prior ordering on worlds matches the ranking ordering.

      @cite{spohn-1988} §7 uses P(w) ∝ ε^{κ(w)} with ε infinitesimal; here we use the concrete parameterization exp(-κ(w)).

      Equations
      Instances For

        The exponential prior is always positive.

        The exponential prior is non-negative.

        Rank-0 worlds maximize the exponential prior.

        The exponential prior preserves the rank ordering: lower rank ↔ higher prior.

        An RSAConfig with worldPrior = rankToPrior κ and boolean meaning computes L1 posteriors that concentrate on the minimum-rank worlds in the support of the utterance as α → ∞.

        Specifically, for an utterance u with boolean denotation ⟦u⟧:
        - L1(w|u) ∝ rankToPrior(κ, w) · S1(u|w)
        - As α → ∞, S1 concentrates on the most informative true utterance
        - The prior rankToPrior(κ, ·) breaks ties among equally informative
          utterances in favor of lower-rank worlds
        - The net effect: L1 concentrates on minimum-rank ⟦u⟧-worlds
        
        This is exactly what `rankEntails κ ⟦u⟧ σ` characterizes: the
        most normal worlds satisfying the utterance also satisfy σ.
        
        The conditional limit theorem `condProb_tendsto_one` (§7)
        formalizes this precisely: P_α(σ|φ) → 1 as α → ∞ whenever
        κ ⊨ φ → σ. 
        

        The softmax distribution with ranking scores is exactly the exponential prior (up to normalization).

        softmax(rankToScore κ, 1)(w) = exp(-κ(w)) / Σ_v exp(-κ(v)) = rankToPrior(κ, w) / Σ_v rankToPrior(κ, v)

        At α = 1, softmax with ranking scores IS the normalized exponential prior. At other α, it's a tempered version: softmax(rankToScore κ, α)(w) = exp(-α·κ(w)) / Σ_v exp(-α·κ(v)).

        @cite{spohn-1988} §7 observes that ranking functions are the ordinal analogue of probability measures. This is not an analogy — it is an exact algebraic identity via the tropical semiring.

        The **tropical semiring** `Tropical ℕ` has:
        - Addition = min (the rank of a disjunction)
        - Multiplication = + (the rank of a conjunction under independence)
        
        The map ε^{·} (for 0 < ε < 1) is a homomorphism from the tropical
        semiring to (ℝ₊, max, ×):
        - ε^{a * b} = ε^{a + b} = ε^a · ε^b  (tropical × → real ×)
        - ε^{a + b} = ε^{min(a,b)} = max(ε^a, ε^b)  (tropical + → real max)
        
        The only "approximation" is that real addition (Σ) approximates max
        in the ε → 0 limit. This is the dequantization: as ε → 0 (α → ∞),
        the sum Σ_w ε^{κ(w)} is dominated by its largest term max_w ε^{κ(w)},
        and probabilistic inference degenerates to tropical (ranking) algebra. 
        

        The exponential map sends tropical multiplication (= underlying +) to real multiplication: ε^{a ×_trop b} = ε^{a + b} = ε^a · ε^b.

        This is exact, not approximate. It formalizes @cite{spohn-1988} §7's observation that ranking independence (κ(A∩B) = κ(A) + κ(B)) corresponds to probabilistic independence (P(A∩B) = P(A)·P(B)).

        theorem Theories.Pragmatics.RSA.RankingBridge.exp_tropical_add (ε : ) ( : 0 < ε) (hε1 : ε 1) (a b : Tropical ) :

        The exponential map sends tropical addition (= min) to real max: ε^{a +_trop b} = ε^{min(a,b)} = max(ε^a, ε^b) for 0 < ε ≤ 1.

        This formalizes @cite{spohn-1988} §7's observation that ranking disjunction (κ(A∪B) = min(κ(A), κ(B))) corresponds to the dominant term in P(A∪B) = P(A) + P(B) − P(A∩B).

        theorem Theories.Pragmatics.RSA.RankingBridge.independent_iff_tropical_mul {W : Type u_1} [Fintype W] (κ : Core.Logic.Ranking.RankingFunction W) (φ ψ : WProp) [DecidablePred φ] [DecidablePred ψ] [DecidablePred fun (w : W) => φ w ψ w] ( : ∃ (w : W), φ w) ( : ∃ (w : W), ψ w) (hφψ : ∃ (w : W), φ w ψ w) :
        κ.independent φ ψ hφψ Tropical.trop (κ.rankProp (fun (w : W) => φ w ψ w) hφψ) = Tropical.trop (κ.rankProp φ ) * Tropical.trop (κ.rankProp ψ )

        Ranking independence is tropical multiplicativity.

        κ(φ ∧ ψ) = κ(φ) + κ(ψ) ↔ trop(κ(φ∧ψ)) = trop(κ(φ)) ×_trop trop(κ(ψ))

        This is not an analogy: "P(A∩B) = P(A)·P(B)" and "κ(A∩B) = κ(A)+κ(B)" are literally the same equation in two semirings.

        The softmax distribution is the tropical-to-probabilistic functor applied to ranking values, with ε = exp(-α).

        softmax(-κ, α)(w) = exp(-α·κ(w)) / Σ_v exp(-α·κ(v)) = ε^{κ(w)} / Σ_v ε^{κ(v)} where ε = exp(-α)

        As ε → 0 (α → ∞), the normalizing sum Σ_v ε^{κ(v)} is dominated by its largest term ε^{min_v κ(v)} = ε^0 = 1 (for rank-0 worlds). In this limit, the probabilistic sum degenerates to the tropical sum, and Bayesian inference becomes ranking-based reasoning.

        The conditional limit theorem: as α → ∞, the conditional probability P_α(σ|φ) → 1 whenever ranking entailment κ ⊨ φ → σ holds.

        This completes the RSA–ranking bridge:
        - §2 shows the *prior* concentrates on rank-0 worlds
        - §7 shows the *posterior* (conditioned on φ) concentrates on σ-worlds
        
        The proof uses exponential decay of non-minimal-rank worlds:
        under ranking entailment, every φ∧¬σ world has rank strictly above
        the minimum-rank φ∧σ world, so its softmax weight decays
        exponentially faster, driving P(σ|φ) → 1. 
        
        theorem Theories.Pragmatics.RSA.RankingBridge.rankEntails_exists_sat {W : Type u_1} [Fintype W] (κ : Core.Logic.Ranking.RankingFunction W) (φ σ : WBool) (h : Core.Logic.SystemZ.rankEntails κ φ σ) ( : ∃ (w : W), φ w = true) :
        ∃ (w : W), (φ w && σ w) = true

        rankEntails implies the existence of a φ∧σ witness.

        noncomputable def Theories.Pragmatics.RSA.RankingBridge.condProb {W : Type u_1} [Fintype W] (s : W) (α : ) (φ σ : WBool) :

        Conditional probability of σ given φ under scores s at rationality α. P_α(σ|φ) = Σ_{w: φ∧σ} exp(α·s(w)) / Σ_{w: φ} exp(α·s(w))

        Equations
        Instances For
          theorem Theories.Pragmatics.RSA.RankingBridge.condProb_tendsto_one {W : Type u_1} [Fintype W] [DecidableEq W] (κ : Core.Logic.Ranking.RankingFunction W) (φ σ : WBool) (h : Core.Logic.SystemZ.rankEntails κ φ σ) ( : ∃ (w : W), φ w = true) :
          Filter.Tendsto (fun (α : ) => condProb (rankToScore κ) α φ σ) Filter.atTop (nhds 1)

          Conditional Softmax Limit Theorem. Under ranking entailment κ ⊨ φ → σ, the conditional probability P_α(σ|φ) converges to 1 as α → ∞.

          This is the central theorem connecting RSA to default reasoning: an RSA listener with ranking-derived scores and infinite rationality draws exactly the conclusions that ranking entailment sanctions.