@cite{kao-etal-2014-metaphor} on mathlib `PMF` #

@cite{kao-etal-2014-metaphor}

"Formalizing the Pragmatics of Metaphor Understanding" Proceedings of the Annual Meeting of the Cognitive Science Society 36, 719-724.

Model (verified against paper) #

L0 (Eq. before 1): L0(c, f⃗ | u) = P(f⃗|c) if c = u, else 0
Speaker utility (Eq. 1): U(u | g, f⃗) = log Σ_{c, f⃗' : g(f⃗') = g(f⃗)} L0(c, f⃗' | u)
Speaker (Eq. 2): S1(u | g, f⃗) ∝ exp(λ · U(u | g, f⃗))
Pragmatic listener: L1(c, f⃗ | u) ∝ P(c) · P(f⃗|c) · Σ_g P(g) · S1(u | g, f⃗)

Parameters (paper §"Model Evaluation"):

λ = 3 (speaker rationality)
P(whale) = 0.01, P(person) = 0.99 (category prior)
Vague QUD: uniform P(g) = 1/3
Specific QUD (f₁): P(g₁) = 0.6, P(g₂) = P(g₃) = 0.2

Softmax-of-log at the root, not rpow workaround #

The speaker utility U = log Σ L0 returns -∞ when the QUD-projected L0 marginal is 0. Mathlib's Real.log 0 = 0 would silently break this — exp(λ · 0) = 1 would give nonzero weight to impossible utterances.

The substrate fix: PMF.softmax takes score : α → EReal, with EReal.exp(⊥) = 0 correctly handling impossible utterances. The Kao S1 is then PMF.softmax (fun u => (α : EReal) * ENNReal.log (qudProjL0 g u f⃗)) — directly the paper's formula with no rpow workaround. Mathematically equivalent to (qudProjL0)^λ (via ENNReal.rpow_eq_exp_mul_log) when qudProjL0 > 0, but the EReal form makes the boundary case explicit.

For Kao's empirical priors (Experiment 1b), all featurePriorℕ entries are strictly positive (min = 379), so all QUD-marginals are positive and the boundary doesn't bite numerically. The substrate handles the general case correctly anyway — RSA papers with sparser literal-listener support inherit the right behaviour.

Joint posterior over `(World × Goal)` #

Kao's L1 jointly infers the speaker's category-and-features and marginalises over goal. PMF-natively: posterior of World × Goal projected to the World-marginal — exactly PMF.posterior_fst_apply from Core/Probability/JointPosterior.lean.

This file uses the equivalent kernel-form: World → PMF Cat defined as goalPrior.bind ∘ s1, folding the goal-marginalisation into the kernel. The two formulations agree by associativity of bind.

@cite{kao-etal-2014-metaphor} on mathlib PMF #

Model (verified against paper) #

Softmax-of-log at the root, not rpow workaround #

Joint posterior over (World × Goal) #

§0. Domain types #

§1. Empirical priors (Experiment 1b counts ×10000) #

§2. PMF construction #

§3. Literal listener L0 #

§4. QUD projection #

§5. Speaker S1 (softmax of log-utility, Eq. 1-2) #

§6. Goal-marginalised speaker #

§7. Pragmatic listener L1 #

§8. Standard goal priors #

§9. Empirical findings (paper §"Model Evaluation") #

§9a. Architectural theorems (parametric in priors) #

§9b. Kao-specific corollaries (paper findings at empirical priors) #

§10. Cross-paper engagement #

@cite{kao-etal-2014-metaphor} on mathlib `PMF` #

Joint posterior over `(World × Goal)` #