Documentation

Linglib.Comparisons.ExhaustivityLimit

RSA L1 at α → ∞ recovers Fox's exh @cite{fox-2007} #

This file proves the concrete connection between RSA pragmatic inference and Neo-Gricean exhaustification for the simplest non-trivial case: the Horn scale ⟨some, all⟩.

Setup. Two utterances (weak = "some", strong = "all") and two worlds (weakOnly = "some but not all", both = "all"). A belief-based RSA speaker S1 chooses utterances proportional to L0(w|u)^α, where L0 is the literal listener posterior under a uniform prior.

Main result (l1_weak_weakOnly_tendsto_one): The pragmatic listener L1, hearing "some", assigns probability converging to 1 to the "some but not all" world as α → ∞. This IS the scalar implicature: some ∧ ¬all.

Connection to Fox 2007 (§5): Fox's innocent-exclusion computation on the same scale yields exh(some) = some ∧ ¬all — true at weakOnly, false at both. The RSA limit concentrates on exactly the worlds where exh returns true.

The proof factors through two key steps:

  1. At the weakOnly world, "all" is false so S1(some|weakOnly) = 1 exactly (for any α > 0), since rpow(0, α) = 0.
  2. At the both world, "all" is strictly more informative (L0 = 1 vs 1/2), so rpow_luce_eq_softmax converts the rpow ratio to a softmax, and tendsto_softmax_infty_not_max gives S1(some|both) → 0.
source
inductive Comparisons.ExhaustivityLimit.ScaleU :
Type
Instances For
    source
    instance Comparisons.ExhaustivityLimit.instDecidableEqScaleU :
    DecidableEq ScaleU
    Equations
    source
    instance Comparisons.ExhaustivityLimit.instFintypeScaleU :
    Fintype ScaleU
    Equations
    • One or more equations did not get rendered due to their size.
    source
    inductive Comparisons.ExhaustivityLimit.ScaleW :
    Type
    Instances For
      source
      instance Comparisons.ExhaustivityLimit.instDecidableEqScaleW :
      DecidableEq ScaleW
      Equations
      source
      instance Comparisons.ExhaustivityLimit.instFintypeScaleW :
      Fintype ScaleW
      Equations
      • One or more equations did not get rendered due to their size.
      source
      instance Comparisons.ExhaustivityLimit.instNonemptyScaleU :
      Nonempty ScaleU
      source
      instance Comparisons.ExhaustivityLimit.instNonemptyScaleW :
      Nonempty ScaleW
      source
      def Comparisons.ExhaustivityLimit.meaning :
      ScaleU → ScaleW → Bool

      Literal meaning: weak is true everywhere, strong only at "both".

      Equations
      Instances For
        source
        noncomputable def Comparisons.ExhaustivityLimit.l0 :
        ScaleU → ScaleW → ℝ

        L0(w|u): uniform prior, so 1/|⟦u⟧| if true, 0 if false.

        Equations
        Instances For
          source
          noncomputable def Comparisons.ExhaustivityLimit.s1 (α : ℝ) (w : ScaleW) (u : ScaleU) :
          ℝ

          S1(u|w, α) = rpow(L0(w|u), α) / Σ_u' rpow(L0(w|u'), α).

          Equations
          Instances For
            source
            theorem Comparisons.ExhaustivityLimit.s1_weak_weakOnly (α : ℝ) (hα : 0 < α) :
            s1 α ScaleW.weakOnly ScaleU.weak = 1

            At weakOnly: s1(weak) = 1 for α > 0. "strong" is false, so rpow(0, α) = 0 — "weak" is the only live option.

            source
            theorem Comparisons.ExhaustivityLimit.s1_weak_both_tendsto_zero :
            Filter.Tendsto (fun (α : ℝ) => s1 α ScaleW.both ScaleU.weak) Filter.atTop (nhds 0)

            S1(weak | both, α) → 0 as α → ∞. "strong" (L0 = 1) is more informative than "weak" (L0 = 1/2), so the softmax speaker concentrates on "strong".

            source
            theorem Comparisons.ExhaustivityLimit.l1_weak_weakOnly_tendsto_one :
            Filter.Tendsto (fun (α : ℝ) => s1 α ScaleW.weakOnly ScaleU.weak / (s1 α ScaleW.weakOnly ScaleU.weak + s1 α ScaleW.both ScaleU.weak)) Filter.atTop (nhds 1)

            Scalar implicature limit: L1(weakOnly | weak, α) → 1 as α → ∞.

            The pragmatic listener hearing "some" concentrates on worlds where "all" is false. This IS the scalar implicature: some ∧ ¬all.

            source
            def Comparisons.ExhaustivityLimit.scaleDomain :
            List ScaleW
            Equations
            Instances For
              source
              def Comparisons.ExhaustivityLimit.weakMeaning :
              ScaleW → Bool
              Equations
              Instances For
                source
                def Comparisons.ExhaustivityLimit.strongMeaning :
                ScaleW → Bool
                Equations
                Instances For
                  source
                  def Comparisons.ExhaustivityLimit.scaleAlts :
                  List (ScaleW → Bool)
                  Equations
                  Instances For
                    source
                    theorem Comparisons.ExhaustivityLimit.scale_ie :
                    NeoGricean.Exhaustivity.Fox2007.ieIndices scaleDomain weakMeaning scaleAlts = [1]

                    Fox's innocent exclusion: "strong" is the only excludable alternative.

                    source
                    theorem Comparisons.ExhaustivityLimit.exh_weak (w : ScaleW) :
                    NeoGricean.Exhaustivity.Fox2007.exhB scaleDomain scaleAlts weakMeaning w = (weakMeaning w && !strongMeaning w)

                    exh(weak) = weak ∧ ¬strong.

                    source
                    theorem Comparisons.ExhaustivityLimit.exh_true_at_weakOnly :
                    NeoGricean.Exhaustivity.Fox2007.exhB scaleDomain scaleAlts weakMeaning ScaleW.weakOnly = true

                    The world where L1 concentrates is exactly where exh(weak) = true.

                    source
                    theorem Comparisons.ExhaustivityLimit.exh_false_at_both :
                    NeoGricean.Exhaustivity.Fox2007.exhB scaleDomain scaleAlts weakMeaning ScaleW.both = false

                    exh(weak) is false at the "both" world — L1 assigns probability 0 there.