Documentation

Linglib.Phenomena.Nonliteral.Irony.KaoEtAl2015PMF

@cite{kao-goodman-2015} on mathlib PMF — headline architectural theorem #

@cite{kao-goodman-2015}

"Let's talk (ironically) about the weather: Modeling verbal irony" Proceedings of the 37th Annual Meeting of the Cognitive Science Society (2015).

What this file is #

A headline-focused PMF formalisation of Kao & Goodman 2015's irony model — a minimal extension of the Kao 2014 hyperbole architecture that uses an additional arousal affect dimension.

The headline architectural insight #

The paper's central scientific claim:

"Adding the arousal dimension to affect is what enables ironic interpretation. Without arousal as a QUD, the model produces hyperbole but NOT irony."

The mechanism: arousal is symmetric across valence-opposite weather states (the U-curve). Both .terrible and .amazing weather have HIGH arousal; only .neutral has low arousal. So under the .arousal QUD, the equivalence class of .terrible includes .amazing — LITERALLY OPPOSITE in valence. The pragmatic listener can then rationally interpret "the weather is terrible" as "speaker means the weather is amazing, but feels strongly about it" — valence flip = irony.

Compare to Kao 2014 hyperbole, where the valence QUD connects worlds of the SAME valence (different states); irony requires the arousal QUD to connect worlds of OPPOSITE valence (arousal-symmetric states).

Headline theorem #

arousal_qud_creates_valence_opposite_equivalence — for any pair of weather states s, s' that are arousal-equivalent but valence-opposite, the arousal QUD's equivalence class connects them. This is the architectural mechanism that differentiates irony from hyperbole.

Specialised to the paper's central case:

terrible_amazing_arousal_equivalent — "terrible" and "amazing" are both high-arousal states, so under .arousal QUD the speaker's "terrible" utterance has positive qudProjL0 mass at the world (.amazing, .positive, .high) — enabling the ironic interpretation.

Substrate validation #

This file is the second irony-family migration (after Kao 2014 hyperbole). Both share the same qudProjL0 substrate. The architectural distinction is purely in the affect prior structure (which dimension is symmetric across worlds the speaker might want to flip) and in the QUD inventory (which dimensions get marginalised).

The substrate handles both papers without modification — the EReal softmax + posterior decomposition + qudProjL0_pos_iff_exists_qud_class lemmas all transfer directly. Only the priors and goal projection function change.

Scope #

The 6 paper findings (ironic_nonliteral, ironic_valence_flip, ironic_high_arousal, no_irony_without_arousal, literal_state, literal_no_flip) are described in §6 prose with discharge path sketched. Empirical-fit content; the architectural payoff is the headline above.

§0. Domain types #

source
inductive Phenomena.Nonliteral.Irony.KaoEtAl2015.PMF.Weather :
Type

Weather states (paper §"Computational Model"): 5 ordered values from terrible to amazing. Weather states double as utterance types — the speaker says "the weather is X" for X in this set.

Instances For
    source
    @[implicit_reducible]
    instance Phenomena.Nonliteral.Irony.KaoEtAl2015.PMF.instDecidableEqWeather :
    DecidableEq Weather
    Equations
    source
    @[implicit_reducible]
    instance Phenomena.Nonliteral.Irony.KaoEtAl2015.PMF.instReprWeather :
    Repr Weather
    Equations
    source
    def Phenomena.Nonliteral.Irony.KaoEtAl2015.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 Phenomena.Nonliteral.Irony.KaoEtAl2015.PMF.instFintypeWeather :
      Fintype Weather
      Equations
      • One or more equations did not get rendered due to their size.
      source
      inductive Phenomena.Nonliteral.Irony.KaoEtAl2015.PMF.Goal :
      Type

      Communicative goals / QUDs. Three dimensions:

      • .state: literal state (price-equivalent in hyperbole)
      • .valence: positive vs negative emotional valence (hyperbole's affect)
      • .arousal: high vs low emotional arousal — the irony-enabling dimension

      The paper's central claim is that adding .arousal to the QUD inventory is what enables ironic interpretation. Without it, the model produces hyperbole but not valence-flipped irony.

      Instances For
        source
        @[implicit_reducible]
        instance Phenomena.Nonliteral.Irony.KaoEtAl2015.PMF.instDecidableEqGoal :
        DecidableEq Goal
        Equations
        source
        def Phenomena.Nonliteral.Irony.KaoEtAl2015.PMF.instReprGoal.repr :
        Goal → ℕ → Std.Format
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[implicit_reducible]
          instance Phenomena.Nonliteral.Irony.KaoEtAl2015.PMF.instReprGoal :
          Repr Goal
          Equations
          source
          @[implicit_reducible]
          instance Phenomena.Nonliteral.Irony.KaoEtAl2015.PMF.instFintypeGoal :
          Fintype Goal
          Equations
          • One or more equations did not get rendered due to their size.
          source
          @[reducible, inline]
          abbrev Phenomena.Nonliteral.Irony.KaoEtAl2015.PMF.World :
          Type

          World: weather state × valence × arousal.

          • .1: weather state
          • .2.1: valence (true = positive, false = negative)
          • .2.2: arousal (true = high, false = low)
          Equations
          Instances For
            source
            instance Phenomena.Nonliteral.Irony.KaoEtAl2015.PMF.instNonemptyWorld :
            Nonempty World

            §1. Affect priors (Experiment 1, derived from Russell 1980 PCA) #

            Valence follows an S-curve across weather states (positive valence rises monotonically: terrible → amazing).

            Arousal follows a symmetric U-curve (high at both extremes): both .terrible and .amazing weather have high arousal; .neutral has the lowest. This U-curve is what creates the arousal-equivalence between valence-opposite states — the architectural mechanism for irony.

            source
            def Phenomena.Nonliteral.Irony.KaoEtAl2015.PMF.positiveValencePercent :
            Weather → ℕ

            P(positive valence | weather state), ×100 (integer percent). S-curve: terrible 1%, bad 15%, neutral 50%, good 85%, amazing 99%.

            Equations
            Instances For
              source
              def Phenomena.Nonliteral.Irony.KaoEtAl2015.PMF.highArousalPercent :
              Weather → ℕ

              P(high arousal | weather state), ×100 (integer percent). U-curve: terrible 90%, bad 40%, neutral 10%, good 40%, amazing 90%. Symmetric across valence — the irony-enabling structure.

              Equations
              Instances For
                source
                def Phenomena.Nonliteral.Irony.KaoEtAl2015.PMF.affectPriorℕ (st : Weather) (positive high : Bool) :
                ℕ

                Affect prior P(valence, arousal | state) as integer counts ×10000 (from the product of valence and arousal probabilities, treating them as conditionally independent given state).

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  §2. Literal listener L0 (Eq. analogous to Hyperbole Eq. 9) #

                  L0(s, A | u) = P(A | s) if s = u, else 0. Same form as Hyperbole.

                  source
                  noncomputable def Phenomena.Nonliteral.Irony.KaoEtAl2015.PMF.L0Weight (u : Weather) (w : World) :
                  ENNReal

                  L0 weight at world (s, valence, arousal) given utterance u: the affect prior at (s, valence, arousal), gated by s = u.

                  Equations
                  Instances For
                    source
                    @[simp]
                    theorem Phenomena.Nonliteral.Irony.KaoEtAl2015.PMF.L0Weight_of_match (u : Weather) (w : World) (h : w.1 = u) :
                    L0Weight u w = ↑(affectPriorℕ w.1 w.2.1 w.2.2) / 10000
                    source
                    @[simp]
                    theorem Phenomena.Nonliteral.Irony.KaoEtAl2015.PMF.L0Weight_of_mismatch (u : Weather) (w : World) (h : w.1 ≠ u) :
                    L0Weight u w = 0
                    source
                    theorem Phenomena.Nonliteral.Irony.KaoEtAl2015.PMF.L0Weight_ne_zero_of_match_and_affect (u : Weather) (w : World) (h_match : w.1 = u) (h_affect : affectPriorℕ w.1 w.2.1 w.2.2 ≠ 0) :
                    L0Weight u w ≠ 0

                    L0 weight is non-zero iff the utterance matches the world's weather AND the affect prior at that world is non-zero.

                    §3. QUD projection — the architectural pivot #

                    The QUD projection function project g w returns a value such that two worlds are QUD-equivalent under g iff they project to the same value.

                    The three projections:

                    The architectural insight: under .arousal, valence-opposite states with matching arousal are EQUIVALENT. E.g., .terrible and .amazing (both high arousal) are arousal-equivalent — the irony-enabling pair.

                    source
                    def Phenomena.Nonliteral.Irony.KaoEtAl2015.PMF.project (g : Goal) (w : World) :
                    ℕ

                    The QUD projection. Encoded as ℕ for pattern-matching simplicity.

                    Equations
                    Instances For
                      source
                      def Phenomena.Nonliteral.Irony.KaoEtAl2015.PMF.project.weatherIdx :
                      Weather → ℕ
                      Equations
                      Instances For
                        source
                        noncomputable def Phenomena.Nonliteral.Irony.KaoEtAl2015.PMF.qudProjL0 (g : Goal) (u : Weather) (w : World) :
                        ENNReal

                        QUD-projected L0: sum of L0Weight u w' over worlds w' in the QUD-equivalence class of w under goal g.

                        Built from the parametric RSA.QUD.proj substrate — same primitive as Kao 2014 hyperbole, with the irony-vs-hyperbole distinction living entirely in the prior structure (arousal U-curve) and the QUD inventory (arousal as a goal).

                        Equations
                        Instances For
                          source
                          theorem Phenomena.Nonliteral.Irony.KaoEtAl2015.PMF.qudProjL0_pos_iff_exists_qud_class_member (g : Goal) (u : Weather) (w : World) :
                          0 < qudProjL0 g u w ↔ ∃ w' ∈ {w' : World | project g w' = project g w}, 0 < L0Weight u w'

                          Headline support theorem: qudProjL0 is positive iff some world in the QUD-equivalence class has positive L0 weight. Direct instance of the parametric RSA.QUD.proj_pos_iff_exists_class_member.

                          §4. The irony-vs-hyperbole architectural distinction #

                          Both Kao 2014 (hyperbole) and Kao 2015 (irony) use qudProjL0 to enable nonliteral interpretation. They differ in which QUDs create which equivalence classes:

                          The headline theorem captures the irony-enabling structure.

                          source
                          theorem Phenomena.Nonliteral.Irony.KaoEtAl2015.PMF.arousal_QUD_equivalence_iff (w w' : World) :
                          project Goal.arousal w = project Goal.arousal w' ↔ w.2.2 = w'.2.2

                          Architectural theorem: under the .arousal QUD, two worlds with matching arousal are QUD-equivalent — even if they have OPPOSITE valences or DIFFERENT weather states.

                          source
                          theorem Phenomena.Nonliteral.Irony.KaoEtAl2015.PMF.terrible_amazing_arousal_equivalent :
                          project Goal.arousal (Weather.terrible, false, true) = project Goal.arousal (Weather.amazing, true, true)

                          Headline lemma: .terrible and .amazing are arousal-equivalent (both high arousal). This is the irony-enabling pair: opposite valence, matched arousal.

                          source
                          theorem Phenomena.Nonliteral.Irony.KaoEtAl2015.PMF.irony_emerges_at_arousal_QUD :
                          0 < qudProjL0 Goal.arousal Weather.terrible (Weather.amazing, true, true)

                          The architectural mechanism for irony (analogue of Kao Hyperbole's hyperbole_emerges_at_valence_goal).

                          Saying "the weather is terrible" while the actual world is (.amazing, positive, high) is LITERALLY FALSE (L0Weight .terrible (.amazing, ...) = 0) but has positive QUD-projection mass under the .arousal goal — because the literally-true world (.terrible, _, .high) is arousal-equivalent.

                          This is the architectural condition for the speaker to rationally produce "terrible" when actually meaning "amazing" — i.e., for verbal irony.

                          §5. Why arousal — and not just any QUD — enables irony #

                          The previous theorem demonstrates that arousal QUD enables valence-flipped interpretation. But why doesn't, say, the .state QUD do the same?

                          Answer: under .state, every world is in its own equivalence class (or at most equivalence classes pairing identical states). So the only literally-true world arousal-equivalent to (.amazing, _, _) under .state is (.amazing, ?, ?) itself — no other state shares the equivalence class. Hence "terrible" cannot be informatively used to mean "amazing" under .state.

                          It's specifically the arousal-symmetric prior structure (high arousal at both extremes) that creates the valence-flipped equivalence class.

                          source
                          theorem Phenomena.Nonliteral.Irony.KaoEtAl2015.PMF.no_irony_under_state_QUD :
                          qudProjL0 Goal.state Weather.terrible (Weather.amazing, true, true) = 0

                          No irony under .state QUD: under the state QUD, the equivalence class of (.amazing, _, _) is exactly {w | w.1 = .amazing} — only .amazing-state worlds. So saying "terrible" gives qudProjL0 = 0 at any .amazing-state world (no literally-true .amazing world is state-equivalent to a literally-true .terrible world).

                          §6. Paper findings (sorried — empirical-fit content) #

                          The 6 paper findings (paper §"Behavioral Experiments" + Table 1):

                          1. ironic_nonliteral: pleasantCfg.L1 .terrible (¬terrible) > L1 .terrible
                          2. ironic_valence_flip: pleasantCfg.L1 .terrible (positive) > L1 .terrible (negative) ← THE central irony finding
                          3. ironic_high_arousal: pleasantCfg.L1 .terrible (high) > L1 .terrible (low)
                          4. no_irony_without_arousal: when arousal goal removed, valence flip disappears
                          5. literal_state: terribleCfg.L1 .terrible (.terrible) > L1 .terrible (¬terrible)
                          6. literal_no_flip: terribleCfg.L1 .terrible (negative) > L1 .terrible (positive)

                          Each follows the substrate pattern: structural decomposition via PMF.posterior_toOuterMeasure_lt_iff_finset_score_lt + numerical comparison at the empirical priors. Findings 2 + 4 establish the paper's central mechanistic claim (arousal QUD enables valence flip); findings 2 + 6 demonstrate context-dependence (same utterance, opposite inference in different weather contexts).

                          Future work: discharge via the substrate pattern. The architectural content (irony emerges from arousal-symmetric prior + arousal QUD) is captured in §4 above.