IncrementalSemantics — Cohn-Gordon's bundle for word-by-word RSA

[CGGP19]

A scene-specific incremental RSA model factors into three pieces:

• wordApplies : U → W → Bool — word-level Boolean truth
• completeUtterances : List (List U) — closed set of full utterances
• worlds : List W — referents to normalize over

From these three pieces every other ingredient — utterance-level truth, extension-based incremental semantics ⟦pfx⟧(r), the chain-rule speaker, the literal-listener categorical L0^UTT, and the study-level chain — is derived rather than re-stipulated per study.

This consolidates what was previously triplicated across CommonGround's Figure 1 scene, the [Sed07] reference-game scene, and the [rubio-fernandez-2016] display: each becomes a single IncrementalSemantics value; studies derive their exact-ℚ chains from it.

The deep theorem (§2.4)

l0Utt_ge_inv_card proves Cohn-Gordon's weakly-informative bound generically over the bundle: any complete utterance true of r ∈ worlds yields a literal-listener posterior of at least 1 / worlds.length for r. The bound follows from filter-monotonicity (numerator ≥ 1 since r is in the filter; total ≤ worlds.length since filtering can only shrink). Concrete scenes inherit the bound by instantiating the bundle.

structure RSA.IncrementalSemantics (U W : Type) [DecidableEq U] : Type

Bundle of scene-specific data for an incremental RSA model.

The three fields jointly determine the entire model: incrementalSem derives the extension-based meaning function ([CGGP19] §2.2) and l0Utt projects the literal listener over complete utterances; studies build their No-Brevity chains (s1Score = L0, α = 1, no cost) from these.

• wordApplies : U → W → Bool

  Word-level Boolean truth: does word u apply to world w?

• completeUtterances : List (List U)

  Closed set of complete utterances available in the scene.

• worlds : List W

  Referents to normalize over (e.g. the visual display).

def RSA.IncrementalSemantics.uttSem {U W : Type} [DecidableEq U] (sem : IncrementalSemantics U W) (utt : List U) (r : W) : Bool

Utterance-level Boolean semantics: conjunction of word applicability.

Equations

• sem.uttSem utt r = utt.all fun (w : U) => sem.wordApplies w r

def RSA.IncrementalSemantics.trueExtCount {U W : Type} [DecidableEq U] (sem : IncrementalSemantics U W) (pfx : List U) (r : W) : ℕ

Number of complete utterances extending pfx that are true of r.

Equations

• sem.trueExtCount pfx r = (List.filter (fun (u : List U) => pfx.isPrefixOf u && sem.uttSem u r) sem.completeUtterances).length

def RSA.IncrementalSemantics.viableExtCount {U W : Type} [DecidableEq U] (sem : IncrementalSemantics U W) (pfx : List U) : ℕ

Number of complete utterances extending pfx that are true of at least one referent in sem.worlds.

Equations

• sem.viableExtCount pfx = (List.filter (fun (u : List U) => pfx.isPrefixOf u && sem.worlds.any fun (r : W) => sem.uttSem u r) sem.completeUtterances).length

noncomputable def RSA.IncrementalSemantics.incrementalSem {U W : Type} [DecidableEq U] (sem : IncrementalSemantics U W) (pfx : List U) (r : W) : ℝ

Extension-based incremental semantics ([CGGP19] §2.2):

⟦pfx⟧(r) = trueExtCount(pfx, r) / viableExtCount(pfx)

Equations

• sem.incrementalSem pfx r = ↑(sem.trueExtCount pfx r) / ↑(sem.viableExtCount pfx)

theorem RSA.IncrementalSemantics.incrementalSem_nonneg {U W : Type} [DecidableEq U] (sem : IncrementalSemantics U W) (pfx : List U) (r : W) : 0 ≤ sem.incrementalSem pfx r

noncomputable def RSA.IncrementalSemantics.l0Utt {U W : Type} [DecidableEq U] (sem : IncrementalSemantics U W) (utt : List U) (r : W) : ℝ

Literal listener over complete utterances: L0^UTT(r | utt) = ⟦utt⟧(r) / Σ_{r'} ⟦utt⟧(r'). For complete utt with no proper extensions, ⟦utt⟧ collapses to Boolean truth, so this is uniform-prior Bayes over worlds.

Equations

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

theorem RSA.IncrementalSemantics.l0Utt_nonneg {U W : Type} [DecidableEq U] (sem : IncrementalSemantics U W) (utt : List U) (r : W) : 0 ≤ sem.l0Utt utt r

theorem RSA.IncrementalSemantics.l0Utt_ge_inv_card {U W : Type} [DecidableEq U] (sem : IncrementalSemantics U W) (utt : List U) (r : W) (hr : r ∈ sem.worlds) (htrue : sem.uttSem utt r = true) : sem.l0Utt utt r ≥ 1 / ↑sem.worlds.length

Cohn-Gordon §2.4 weakly-informative bound (generic).

For any complete utterance utt that is true of r (with r ∈ worlds), the literal listener assigns posterior at least 1 / worlds.length to r. The proof is purely combinatorial: the numerator is 1 (since utt is true of r), and the total counts referents satisfying utt, which is at most worlds.length and at least 1 (since r is in the filter).

Cohn-Gordon use this bound to certify that greedy unrolling — even without a global view of the utterance space — never produces an utterance arbitrarily worse than uniform. Studies that build a greedy unroller for a specific scene need only prove that the output is in completeUtterances and is true of the target; the bound then follows.