@cite{goodman-stuhlmuller-2013} on mathlib PMF #
@cite{goodman-stuhlmuller-2013}
PMF reformulation of GS2013 using PMF.hypergeometric as the observation
kernel primitive. The model is parameterized over a : Access throughout —
there is no per-.a1/.a2/.a3 substrate; each downstream operator
(speakerBelief, qualityOk, s1Score, S1g, marginalSpeaker, L1)
takes (a, k) where k : Fin (a.toNat + 1) is the observed count.
PMF stack (one definition each, parameterized) #
worldPrior : PMF WorldState— uniform on 4 statesobsKernel a w : PMF (Fin (a.toNat + 1))—PMF.hypergeometric 3 w.toNat a.toNatspeakerBelief a k : PMF WorldState—PMF.posterior (obsKernel a) worldPrior kS1g m α a k h : PMF U— softmax-of-expected-log over the speaker's beliefmarginalSpeaker m α a w hCov : PMF U—(obsKernel a w).bind (S1g a)L1 m α a u hMarg : PMF WorldState—PMF.posterior (marginalSpeaker a) worldPrior u
Silence-extended findings #
All 11 paper findings are stated against the silence-extended utterance
space WithSilence U — the cover hypothesis cover_silent is universal
because silence is qOk at every observation. This dissolves the
(access, word) ∉ {sensible} defects that block formalization without
silence (paper p. 180 "sensible situations").
§1. Substrate: world states, utterance enums, meaning functions, access #
World states: how many of 3 objects have the property.
- s0 : WorldState
- s1 : WorldState
- s2 : WorldState
- s3 : WorldState
Instances For
Equations
- Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.PMF.instDecidableEqWorldState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.PMF.WorldState.s0.toNat = 0
- Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.PMF.WorldState.s1.toNat = 1
- Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.PMF.WorldState.s2.toNat = 2
- Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.PMF.WorldState.s3.toNat = 3
Instances For
Equations
- Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.PMF.instDecidableEqQUtt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.PMF.qMeaning Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.PMF.QUtt.none_ x✝ = (x✝.toNat == 0)
- Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.PMF.qMeaning Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.PMF.QUtt.some_ x✝ = decide (x✝.toNat ≥ 1)
- Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.PMF.qMeaning Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.PMF.QUtt.all x✝ = (x✝.toNat == 3)
Instances For
Equations
- Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.PMF.instDecidableEqNumUtt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.PMF.lbMeaning Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.PMF.NumUtt.one x✝ = decide (x✝.toNat ≥ 1)
- Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.PMF.lbMeaning Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.PMF.NumUtt.two x✝ = decide (x✝.toNat ≥ 2)
- Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.PMF.lbMeaning Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.PMF.NumUtt.three x✝ = decide (x✝.toNat ≥ 3)
Instances For
Speaker access = number of objects (out of 3) the speaker observes.
A Fin 4 indexed at 0..3. The paper restricts to {1, 2, 3}; access=0
(speaker observes nothing) is well-defined but unused.
Carrying this as Fin 4 instead of a custom Access enum eliminates the
Access.toNat indirection — a.val is just the access value and
Fin (a.val + 1) reduces in type position when a is concrete.
Equations
Instances For
Access value 1 (speaker observes 1 of 3 objects).
Instances For
Access value 2 (speaker observes 2 of 3 objects).
Instances For
Access value 3 — full access (speaker observes all 3 objects).
Instances For
§2. World prior — uniform on WorldState #
Equations
Instances For
The uniform world prior assigns ENNReal.ofReal (1/4) to every world.
§3. Hypergeometric observation kernel #
obsKernel a w : PMF (Fin (a.toNat + 1)) is the hypergeometric distribution
over count outcomes when the speaker observes a.toNat of the 3 objects, of
which w.toNat have the property. Built directly from PMF.hypergeometric.
Equations
Instances For
Closed-form observation kernel value: C(K, k) · C(N-K, n-k) / C(N, n).
§4. Speaker belief — PMF.posterior of obsKernel #
Speaker's posterior over worlds given a count observation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
§5. obsCompatible — combinatorial feasibility #
A world s is compatible with observing k.val successes out of a.toNat
draws iff the hypergeometric numerator at (K=s.toNat, k=k.val) is non-zero.
Equations
Instances For
§6. qualityOk — utterance quality filter #
An utterance u is quality-OK at observation (a, k) iff u is true at
every world compatible with (a, k).
Equations
- One or more equations did not get rendered due to their size.
Instances For
§7. lexReal — uniform-on-extension literal probability #
Equations
- Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.PMF.lexReal meaning u s = if meaning u s = true then (↑(RSA.extensionOf meaning u).card)⁻¹ else 0
Instances For
§8. beliefReal — toReal projection of speakerBelief #
Equations
Instances For
§9. s1Score — softmaxBelief instance #
Equations
- One or more equations did not get rendered due to their size.
Instances For
§10. S1g — speaker conditional on observation #
Equations
- Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.PMF.S1g meaning α a k h0 = PMF.normalize (fun (x : U) => Phenomena.ScalarImplicatures.GoodmanStuhlmuller2013.PMF.s1Score meaning α a k x) h0 ⋯
Instances For
§11. marginalSpeaker — PMF.bind over the obs kernel #
Since we use PMF.bind (not bindOnSupport), we need S1g defined at every
k, not just kernel-supported ones. The cover hypothesis hCov therefore
quantifies over all k : Fin (a.toNat + 1). With WithSilence, this is
automatic via cover_silent (silence is qOk everywhere).
Equations
- One or more equations did not get rendered due to their size.
Instances For
§12. L1 — Bayesian inversion of the marginal speaker #
Equations
- One or more equations did not get rendered due to their size.
Instances For
§13. cover_silent — silence is universally qOk #
liftMeaning m none = true at every world, so silence passes qualityOk at
every observation. The cover hypothesis is universally satisfiable.
§14. obsKernel value lemmas (per (a, w, k)) #
Closed-form values for obsKernel a w k at each combination — derived from
obsKernel_apply by unfolding the Nat.choose arithmetic. These are the
numerical foundations for the marginalSpeaker / findings layer below.
§15. marginalSpeaker collapse — .a3 (concentrated kernel) #
At full access, obsKernel .a3 w puts all mass on a single k = w.toNat,
so marginalSpeaker = (obsKernel .a3 w).bind (S1g .a3 _) collapses to a
single S1g evaluation at the diagonal k. Polymorphic over w —
replaces what was previously 4 per-world specializations.
§17. Extension cardinalities for silence-extended models #
Per-(meaning, utterance) extension cardinalities, locally tagged for
pmf_eval_simps so the universal s1Score_liftMeaning_apply_eq_ite
(§17b) reduces to concrete ofReal((card)⁻¹) values.
§17a. Generic s1Score lemmas (work for any (a, k)) #
When qOk u passes, liftMeaning-lifted utterances have a uniform lex
value on the belief support (because: qOk ⇒ m u s = true at all
compatible s ⊇ belief support ⇒ lex u s = 1/(card extension)).
softmaxBelief_uniform_on_support then collapses s1Score = ENNReal.ofReal (1/c).
§17b. Universal pmf_eval-friendly if-form for s1Score (liftMeaning _) #
The universal s1Score_uniform_apply is hypothesis-laden (h_qok, h_card, h_pos)
so simp can't use it. s1Score_liftMeaning_apply_eq_ite below is parameterized
over the meaning function m and has no free preconditions — the qOk branch is
encoded as a decidable if, and extension nonemptiness is proved universally
via the witnessWorld helper.
This collapses what previously required two paper-tagged lemmas (one per meaning)
into one polymorphic lemma. The local attribute [pmf_eval_simps] keeps the
tag file-scoped so it does not pollute the substrate set with a private paper
lemma (audit hygiene rule).
pmf_eval smoke tests for the if-form variants #
§19a. s1Score evaluations for .a1 #
At (.a1, k=0): compatible worlds = {s0, s1, s2}. Only silence is qOk; all other quantifiers / numerals are false at s0 ⇒ qOk fails ⇒ score 0.
At (.a1, k=1): compatible worlds = {s1, s2, s3}. Silence and some_/one
are qOk; none_, all, two, three fail.
§19c. S1g per-(a1, k, target-utt) #
Computed via S1g = normalize (s1Score), with the score and the partition
function from §19a/b.
§19d. marginalSpeaker collapse — .a1 #
For each (.a1, w), expand bind = ∑ k : Fin 2, obsKernel * S1g.
§19g. S1g per-(a2, k, target-utt) #
§20. Findings (silence-extended) #
The 11 paper findings restated against WithSilence + liftMeaning so the
cover hypothesis is automatically satisfied via cover_silent.
Status: illustrations, not corollaries of a single structural theorem #
The 11 cells below are computational evaluations of the model at specific (meaning, access, world-pair, utterance) tuples. They demonstrate that the model produces the predictions plotted in Fig. 2 (A, B).
They are NOT corollaries of a single information-theoretic cancellation
theorem. The structural theorem that IS provable
(RSA.mutualInfoStateObs_bind_noise_le in
Linglib/Theories/Pragmatics/RSA/Cancellation.lean) only gives obs-level
MI cancellation: MI(state; obs_n) ≤ MI(state; obs_i). The per-(world-pair)
orderings these cells encode are utterance-level claims that depend on the
specific lex shape, not just on kernel informativity — see Cancellation.lean
§3 for why utterance-level MI cancellation isn't a clean DPI corollary.
Demoted to examples rather than named theorems: they're computational
illustrations of model behavior, not load-bearing claims. Anyone wanting to
prove a structural property about the model should use the obs-level
cancellation theorem in Cancellation.lean.
Finding 4: at full access, two favors s2 > s3 (upper-bounded reading).
.a1 minimal-access findings #
Each shows marginalSpeaker (smaller-state) ≤ marginalSpeaker (larger-state),
so ¬ L1 (smaller) > L1 (larger). Proof: at (.a1, k=0) the target utterance
has S1g = 0 (qOk fails); at (.a1, k=1) it has S1g = 4/7. So the comparison
reduces to obsKernel(smaller)(k=1) ≤ obsKernel(larger)(k=1).
Finding 3: at partial access, some does NOT favor s2 > s3 (equality).
Finding 5: at partial access, "two" does NOT favor s2 > s3 (weakened).
Finding 10 (HEADLINE): at partial access, "one" favors s1 > s3.
Finding 11: at partial access, "one" does NOT favor s1 > s2.