Documentation

Linglib.Phenomena.Nonliteral.Irony.Studies.SpinosoDiPiano2025PMF

@cite{spinoso-di-piano-etal-2025} — (RSA)² on mathlib PMF #

@cite{spinoso-di-piano-etal-2025} @cite{kao-goodman-2015}

(RSA)²: A Rhetorical-Strategy-Aware Rational Speech Act Framework for Figurative Language Understanding (ACL 2025).

What this file is #

A headline-focused PMF formalisation of the (RSA)² model's central architectural claim. The paper's deepest result (worth a Lean theorem):

For non-midpoint utterances, the entire (RSA)² model's behavior reduces to a single prior comparison.

We formalise this as irony_iff_prior_favors_antonym:

L1(u)(opposite u) > L1(u)(literal u) ↔ wp(opposite u) > wp(literal u)

This explains WHY (RSA)² agrees with @cite{kao-goodman-2015} (affect-aware RSA) on cross-context predictions: both reduce to the world-prior asymmetry, but (RSA)² achieves this WITHOUT modeling affect dimensions or QUD projection. Affect is unnecessary for irony.

(RSA)² in three lines #

The paper's key generalisation: replace RSA's literal indicator 𝟙_{m ∈ ⟦u⟧} with a rhetorical strategy function f_r(c, m, u) parameterised by strategy r ∈ R:

In our binary irony fragment, R = {literal, ironic}; f_literal is the standard indicator and f_ironic(u, w) = 𝟙_{w = opposite(meaning(u))}.

Why the binary-strategy fragment reduces to a prior comparison #

For non-midpoint u (where u.toWeather ≠ opposite u.toWeather):

So posterior mixedS1 worldPrior u puts all its mass on those two worlds, with relative ratio determined by worldPrior — exactly the content of the headline theorem.

Connection to QUD-RSA (Appendix A.3) #

The paper proves QUD-RSA (RSA.QUD.proj in our substrate, used by Kao metaphor / hyperbole / irony) is a strict special case of (RSA)² (Lemma 1: every QUD-RSA instance arises from a specific f_r; Lemma 2: not all (RSA)² instances arise from any QUD-RSA instance). This file formalises the (RSA)² side; RSA/QUD.lean formalises the QUD-RSA side.

Scope #

The 10 numerical predictions from the paper (ironic_reading, literal_reading, infer_ironic, ...) are corollaries of the headline theorem at specific worldPrior values. They are paper-finding content (empirical-fit) — out of scope for this architectural migration.

§0. Domain types #

source
inductive SpinosoDiPiano2025.PMF.Weather :
Type

Weather scale: 5-point ordered set from terrible to amazing. Mirrors @cite{kao-goodman-2015}'s weather scale.

Instances For
    source
    @[implicit_reducible]
    instance SpinosoDiPiano2025.PMF.instDecidableEqWeather :
    DecidableEq Weather
    Equations
    source
    @[implicit_reducible]
    instance SpinosoDiPiano2025.PMF.instReprWeather :
    Repr Weather
    Equations
    source
    def SpinosoDiPiano2025.PMF.instReprWeather.repr :
    Weather → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance SpinosoDiPiano2025.PMF.instFintypeWeather :
      Fintype Weather
      Equations
      • One or more equations did not get rendered due to their size.
      source
      inductive SpinosoDiPiano2025.PMF.Utterance :
      Type

      Utterance type: weather descriptions used as speech acts. Structurally isomorphic to Weather but distinct for type discipline (utterance space vs meaning space).

      Instances For
        source
        @[implicit_reducible]
        instance SpinosoDiPiano2025.PMF.instDecidableEqUtterance :
        DecidableEq Utterance
        Equations
        source
        @[implicit_reducible]
        instance SpinosoDiPiano2025.PMF.instReprUtterance :
        Repr Utterance
        Equations
        source
        def SpinosoDiPiano2025.PMF.instReprUtterance.repr :
        Utterance → ℕ → Std.Format
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[implicit_reducible]
          instance SpinosoDiPiano2025.PMF.instFintypeUtterance :
          Fintype Utterance
          Equations
          • One or more equations did not get rendered due to their size.
          source
          inductive SpinosoDiPiano2025.PMF.Strategy :
          Type

          The two rhetorical strategies in the paper's binary fragment.

          Instances For
            source
            @[implicit_reducible]
            instance SpinosoDiPiano2025.PMF.instDecidableEqStrategy :
            DecidableEq Strategy
            Equations
            source
            @[implicit_reducible]
            instance SpinosoDiPiano2025.PMF.instReprStrategy :
            Repr Strategy
            Equations
            source
            def SpinosoDiPiano2025.PMF.instReprStrategy.repr :
            Strategy → ℕ → Std.Format
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[implicit_reducible]
              instance SpinosoDiPiano2025.PMF.instFintypeStrategy :
              Fintype Strategy
              Equations
              • One or more equations did not get rendered due to their size.
              source
              instance SpinosoDiPiano2025.PMF.instNonemptyWeather :
              Nonempty Weather
              source
              instance SpinosoDiPiano2025.PMF.instNonemptyUtterance :
              Nonempty Utterance
              source
              instance SpinosoDiPiano2025.PMF.instNonemptyStrategy :
              Nonempty Strategy
              source
              def SpinosoDiPiano2025.PMF.Utterance.toWeather :
              Utterance → Weather

              The Utterance ↔ Weather bijection: each utterance has a unique literal weather meaning.

              Equations
              Instances For
                source
                def SpinosoDiPiano2025.PMF.Utterance.fromWeather :
                Weather → Utterance

                Inverse of Utterance.toWeather.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem SpinosoDiPiano2025.PMF.Utterance.toWeather_fromWeather (w : Weather) :
                  (fromWeather w).toWeather = w
                  source
                  @[simp]
                  theorem SpinosoDiPiano2025.PMF.Utterance.fromWeather_toWeather (u : Utterance) :
                  fromWeather u.toWeather = u

                  §1. Evaluative antonym (involutive) #

                  source
                  def SpinosoDiPiano2025.PMF.opposite :
                  Weather → Weather

                  The evaluative antonym on the weather scale: flip endpoints, fix the midpoint. This IS the ironic interpretation function: "amazing" ironically conveys "terrible" because they are evaluative antonyms.

                  Equations
                  Instances For
                    source
                    theorem SpinosoDiPiano2025.PMF.opposite_involutive (w : Weather) :
                    opposite (opposite w) = w

                    §2. Per-strategy speakers (deterministic kernels) #

                    In the binary-strategy fragment with indicator meanings, each strategy maps a world to a unique utterance:

                    Because Utterance ≅ Weather (via toWeather), these are well-defined total functions, and the per-strategy speaker collapses to PMF.pure.

                    source
                    noncomputable def SpinosoDiPiano2025.PMF.literalSpeaker (w : Weather) :
                    PMF Utterance

                    The literal speaker: at world w, deterministically emit the utterance whose literal meaning is w.

                    Equations
                    Instances For
                      source
                      noncomputable def SpinosoDiPiano2025.PMF.ironicSpeaker (w : Weather) :
                      PMF Utterance

                      The ironic speaker: at world w, deterministically emit the utterance whose ironic meaning is w (i.e., whose literal meaning is opposite w).

                      Equations
                      Instances For
                        source
                        noncomputable def SpinosoDiPiano2025.PMF.speakerByStrategy :
                        Strategy → Weather → PMF Utterance

                        The per-strategy speaker dispatch.

                        Equations
                        Instances For

                          §3. Strategy-marginalised speaker (Eq. 7) #

                          source
                          noncomputable def SpinosoDiPiano2025.PMF.strategyPrior :
                          PMF Strategy

                          Uniform strategy prior — paper's default for the binary fragment.

                          Equations
                          Instances For
                            source
                            theorem SpinosoDiPiano2025.PMF.strategyPrior_apply (s : Strategy) :
                            strategyPrior s = (↑(Fintype.card Strategy))⁻¹
                            source
                            theorem SpinosoDiPiano2025.PMF.strategyPrior_eq_half (s : Strategy) :
                            strategyPrior s = 1 / 2
                            source
                            noncomputable def SpinosoDiPiano2025.PMF.mixedS1 (w : Weather) :
                            PMF Utterance

                            The strategy-marginalised speaker (Eq. 7's mixture): at world w, sample a strategy then emit an utterance. This is the L1 likelihood.

                            Equations
                            Instances For

                              §4. Computing mixedS1 at the matching worlds #

                              The two architectural lemmas the headline theorem hinges on.

                              source
                              theorem SpinosoDiPiano2025.PMF.mixedS1_at_literal_world (u : Utterance) (hne : u.toWeather ≠ opposite u.toWeather) :
                              (mixedS1 u.toWeather) u = 1 / 2

                              mixedS1 at u.toWeather (the literal-matching world) for u: only the literal strategy contributes (the ironic strategy emits a DIFFERENT utterance there, namely Utterance.fromWeather (opposite u.toWeather), which differs from u because the world is non-midpoint).

                              source
                              theorem SpinosoDiPiano2025.PMF.mixedS1_at_ironic_world (u : Utterance) (hne : u.toWeather ≠ opposite u.toWeather) :
                              (mixedS1 (opposite u.toWeather)) u = 1 / 2

                              mixedS1 at opposite u.toWeather (the ironic-matching world) for u: only the ironic strategy contributes. Symmetric to mixedS1_at_literal_world, hinging on opposite_involutive.

                              §5. The L1 posterior #

                              source
                              noncomputable def SpinosoDiPiano2025.PMF.L1 (worldPrior : PMF Weather) (u : Utterance) (h_marg : PMF.marginal mixedS1 worldPrior u ≠ 0) :
                              PMF Weather

                              Pragmatic listener L1: posterior over worlds given an utterance.

                              Equations
                              Instances For

                                §6. Architectural payoff — irony reduces to prior comparison #

                                source
                                theorem SpinosoDiPiano2025.PMF.irony_iff_prior_favors_antonym (worldPrior : PMF Weather) (u : Utterance) (hne : u.toWeather ≠ opposite u.toWeather) (h_marg : PMF.marginal mixedS1 worldPrior u ≠ 0) :
                                (L1 worldPrior u h_marg) u.toWeather < (L1 worldPrior u h_marg) (opposite u.toWeather) ↔ worldPrior u.toWeather < worldPrior (opposite u.toWeather)

                                Headline theorem (Spinoso–Di Piano et al. 2025): For any non-midpoint utterance u, the L1 posterior orders the two candidate weather states strictly by the world prior at those states.

                                This is the paper's core architectural insight, formalised: the entire (RSA)² model behavior — for non-midpoint utterances — reduces to a single prior comparison. Affect dimensions and QUD projection are unnecessary for irony; context (the world prior) alone determines whether an utterance is interpreted ironically.

                                The shared 1/2 factor (the strategy-prior weight on each strategy) cancels via posterior_lt_iff_score_lt + mul_lt_mul_iff_right.