[CGGP19] — Incremental Iterated Response Model

Cohn-Gordon, R., Goodman, N. D., & Potts, C. (2019). An Incremental Iterated Response Model of Pragmatics. Proceedings of the Society for Computation in Linguistics (SCiL) 2, 81–90.

The Model

The incremental RSA model extends the standard RSA framework to word-by-word production. The speaker produces referring expressions incrementally, choosing each word to maximize the listener's posterior probability for the target:

S1^WORD(wₖ | [w₁,...,wₖ₋₁], r) ∝ L0(r | w₁,...,wₖ)^α

The full utterance probability factors via the chain rule:

S1^UTT-IP(w₁,...,wₙ | r) = ∏ₖ S1^WORD(wₖ | [w₁,...,wₖ₋₁], r)

L0 uses extension-based incremental semantics (§2.2): given prefix c,

⟦c⟧(w) = |{u ∈ U : c ⊑ u ∧ ⟦u⟧(w) = 1}| / |{u ∈ U : c ⊑ u ∧ ∃w'. ⟦u⟧(w') = 1}|

where U is the set of complete utterances and ⊑ is the prefix relation.

Formalization via the IncrementalSemantics bundle

Each scene in this file is a single value of IncrementalSemantics U W (defined below), specifying just the lexicon (wordApplies), the closed set of complete utterances, and the world set. The file derives the chain-rule speaker (α = 1, no cost, uniform priors) and extension-based L0 from the bundle, so the three scenes (Figure 1, the [Sed07] reference game, the [rubio-fernandez-2016] display) share machinery rather than duplicating it.

The bundle exposes a single deep theorem, l0Utt_ge_inv_card, proving the §2.4 weakly-informative bound generically: any complete utterance true of r ∈ worlds yields a literal posterior at least 1 / worlds.length. The Figure 1 application (greedyUnroll_weakly_informative) below discharges only the r ∈ worlds and uttSem utt r = true premises; the bound follows.

Main results

• adj_first_for_target / noun_after_adj / noun_only_for_r2 / adj_only_for_r3: the Figure 1c word-by-word speaker rows.
• uniform_after_red_for_r2: the §2.2 dead-end fallback (Figure 1c's R2 row: 0, ½, ½ over words with viable continuations).
• listener_anticipation: hearing "red", L1 favours R3 at 7/11 (Figure 1d) — the anticipatory implicature.
• incremental_prefers_bare_noun: the chain-rule product prefers bare "dress" (3/7) over "red dress" (8/21) for R1 (Figure 1e), diverging from global_prefers_red_dress — the paper's central architectural wedge.
• sedivy_contrast_inference / cgSedivyLooks_satisfy_contrast_reduces_competitor: the §3.2 contrastive-inference reanalysis, discharging the visual-world paradigm contract under the Bayesian posterior linking hypothesis.

Implementation notes

Extension counts are natural numbers, so the chain is exact ℚ≥0 with PMF agents via PMF.ofScores. The §2.2 dead-end fallback distributes over words with viable continuations, gated to scene referents (out-of-scene referents keep their zero row). Utterance-level probabilities are chain-rule products of s1 values (eq. 7).

IncrementalSemantics bundle

A scene-specific incremental RSA model factors into three pieces — wordApplies : U → W → Bool, completeUtterances : List (List U), and worlds : List W. Utterance-level truth, extension-based incremental semantics ⟦pfx⟧(r), the chain-rule speaker, and the literal-listener categorical L0^UTT are all derived from those three pieces. The bundle exposes l0Utt_ge_inv_card (§2.4 weakly-informative bound) generically.

structure CohnGordonEtAl2019.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 (§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 CohnGordonEtAl2019.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 CohnGordonEtAl2019.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 CohnGordonEtAl2019.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 CohnGordonEtAl2019.IncrementalSemantics.incrementalSem {U W : Type} [DecidableEq U] (sem : IncrementalSemantics U W) (pfx : List U) (r : W) : ℝ

Extension-based incremental semantics (§2.2):

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

Equations

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

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

noncomputable def CohnGordonEtAl2019.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 CohnGordonEtAl2019.IncrementalSemantics.l0Utt_nonneg {U W : Type} [DecidableEq U] (sem : IncrementalSemantics U W) (utt : List U) (r : W) : 0 ≤ sem.l0Utt utt r

theorem CohnGordonEtAl2019.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

§2.4 weakly-informative bound (generic).

For any complete utterance utt 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.

Cohn-Gordon et al. 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.

Domain Types (Figure 1a)

inductive CohnGordonEtAl2019.Word : Type

Words available to the incremental speaker (Figure 1a).

• red : Word
• dress : Word
• object : Word

@[instance_reducible]

instance CohnGordonEtAl2019.instDecidableEqWord : DecidableEq Word

Equations

• CohnGordonEtAl2019.instDecidableEqWord x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CohnGordonEtAl2019.instFintypeWord : Fintype Word

Equations

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

def CohnGordonEtAl2019.instReprWord.repr : Word → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance CohnGordonEtAl2019.instReprWord : Repr Word

Equations

• CohnGordonEtAl2019.instReprWord = { reprPrec := CohnGordonEtAl2019.instReprWord.repr }

instance CohnGordonEtAl2019.instNonemptyWord : Nonempty Word

inductive CohnGordonEtAl2019.Referent : Type

Referents in the reference game scene (Figure 1a).

Scene: {red dress (R1), blue dress (R2), red hat (R3)}

• redDress : Referent
• blueDress : Referent
• redHat : Referent

@[instance_reducible]

instance CohnGordonEtAl2019.instDecidableEqReferent : DecidableEq Referent

Equations

• CohnGordonEtAl2019.instDecidableEqReferent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CohnGordonEtAl2019.instFintypeReferent : Fintype Referent

Equations

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

@[instance_reducible]

instance CohnGordonEtAl2019.instReprReferent : Repr Referent

Equations

• CohnGordonEtAl2019.instReprReferent = { reprPrec := CohnGordonEtAl2019.instReprReferent.repr }

def CohnGordonEtAl2019.instReprReferent.repr : Referent → ℕ → Std.Format

Equations

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

instance CohnGordonEtAl2019.instNonemptyReferent : Nonempty Referent

The Figure 1 bundle

def CohnGordonEtAl2019.figureOne : IncrementalSemantics Word Referent

The Figure 1 reference scene as an IncrementalSemantics bundle: three words ("red", "dress", "object"), three complete utterances ("dress", "red dress", "red object"), three referents (R1, R2, R3).

Equations

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

The kernel face over the bundle

def CohnGordonEtAl2019.incSemScore {U W : Type} [DecidableEq U] (sem : IncrementalSemantics U W) (pfx : List U) (r : W) : ℚ≥0

ℚ extension semantics ⟦pfx⟧(r) (§2.2), mirroring IncrementalSemantics.incrementalSem.

Equations

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

def CohnGordonEtAl2019.l0Score {U W : Type} [DecidableEq U] [Fintype W] (sem : IncrementalSemantics U W) (ctx : List U) (u : U) (r : W) : ℚ≥0

Word-level literal listener value (eq. 4).

Equations

• CohnGordonEtAl2019.l0Score sem ctx u r = CohnGordonEtAl2019.incSemScore sem (ctx ++ [u]) r / ∑ r' : W, CohnGordonEtAl2019.incSemScore sem (ctx ++ [u]) r'

def CohnGordonEtAl2019.s1Score {U W : Type} [DecidableEq U] [Fintype W] [DecidableEq W] [Fintype U] (sem : IncrementalSemantics U W) (ctx : List U) (r : W) (u : U) : ℚ≥0

Word-level speaker score at context ctx (eq. 5, zero cost, α = 1). At dead-end cells — no word makes the referent reachable — probability is "evenly distributed" over the words with viable continuations (§2.2, Figure 1c's R2 row: 0, ½, ½).

Equations

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

def CohnGordonEtAl2019.s1Post {U W : Type} [DecidableEq U] [Fintype W] [DecidableEq W] [Fintype U] (sem : IncrementalSemantics U W) (ctx : List U) (r : W) : U → ℚ≥0

Normalized incremental speaker.

Equations

• CohnGordonEtAl2019.s1Post sem ctx r = PMF.normalizeScores (CohnGordonEtAl2019.s1Score sem ctx r)

noncomputable def CohnGordonEtAl2019.s1 {U W : Type} [DecidableEq U] [Fintype W] [DecidableEq W] [Fintype U] [Nonempty U] (sem : IncrementalSemantics U W) (ctx : List U) (r : W) : PMF U

Word-by-word speaker at context ctx (eq. 5).

Equations

• CohnGordonEtAl2019.s1 sem ctx r = PMF.ofScores PMF.Fallback.uniform (CohnGordonEtAl2019.s1Score sem ctx r)

noncomputable def CohnGordonEtAl2019.l1 {U W : Type} [DecidableEq U] [Fintype W] [DecidableEq W] [Fintype U] [Nonempty W] (sem : IncrementalSemantics U W) (u : U) : PMF W

Pragmatic listener upon the first word (eq. 6, uniform priors).

Equations

• CohnGordonEtAl2019.l1 sem u = PMF.ofScores PMF.Fallback.uniform fun (r : W) => CohnGordonEtAl2019.s1Post sem [] r u

The incremental chain

Predictions

Figure 1c: the word-by-word speaker

theorem CohnGordonEtAl2019.adj_first_for_target : (s1 figureOne [] Referent.redDress) Word.dress < (s1 figureOne [] Referent.redDress) Word.red

For R1 the speaker leads with "red" (4/7 > 3/7): both red referents stay viable, while "dress" dilutes L0 over the two dresses.

theorem CohnGordonEtAl2019.noun_after_adj : (s1 figureOne [Word.red] Referent.redDress) Word.object < (s1 figureOne [Word.red] Referent.redDress) Word.dress

After "red", the speaker completes with "dress" (2/3 > 1/3): "red dress" is unique to R1, "red object" ambiguous with R3.

theorem CohnGordonEtAl2019.noun_only_for_r2 : (s1 figureOne [] Referent.blueDress) Word.red < (s1 figureOne [] Referent.blueDress) Word.dress

For R2 (blue dress) the speaker must start with "dress": no extension of "red" is true of R2.

theorem CohnGordonEtAl2019.adj_only_for_r3 : (s1 figureOne [] Referent.redHat) Word.dress < (s1 figureOne [] Referent.redHat) Word.red

For R3 (red hat) the speaker must start with "red": "dress" is false of R3.

theorem CohnGordonEtAl2019.uniform_after_red_for_r2 (w : Word) (hw : w ≠ Word.red) : (s1 figureOne [Word.red] Referent.blueDress) Word.dress = (s1 figureOne [Word.red] Referent.blueDress) w

The §2.2 dead end: after "red" for R2 nothing is true, and "probability is evenly distributed over all choices of word" — S1 is uniform (½, ½) over the viable continuations.

Figure 1d: the pragmatic listener

theorem CohnGordonEtAl2019.listener_anticipation : (l1 figureOne Word.red) Referent.redDress < (l1 figureOne Word.red) Referent.redHat

The anticipatory implicature: hearing "red", L1 favours R3 over R1 (7/11 > 4/11) — "red" is R3's only option, while R1's speaker had alternatives. The §3.2 [STCC99] bridge below builds on this; the authors cite [Sed07] for the effect.

Figure 1e: utterance-level probabilities

theorem CohnGordonEtAl2019.incremental_prefers_bare_noun : (s1 figureOne [] Referent.redDress) Word.red * (s1 figureOne [Word.red] Referent.redDress) Word.dress < (s1 figureOne [] Referent.redDress) Word.dress

The architectural wedge (Figure 1e): the chain-rule product prefers bare "dress" (3/7) over "red dress" (4/7 · 2/3 = 8/21) for R1, while the global model prefers the more informative "red dress".

§2.4 Weakly-Informative Greedy Unrolling

§2.4's weakly informative bound — greedy unrolling reaches a complete utterance whose literal posterior for the target is at least 1/|W| — is proved generically as IncrementalSemantics.l0Utt_ge_inv_card above; here we define the Figure 1 unroller and discharge its premises.

def CohnGordonEtAl2019.greedyUnroll : Referent → List Word

Greedy unrolling for Figure 1's scene: at each step pick the word maximizing L0(r | ctx ++ [w]); stop when ctx is a complete utterance. Tabulated by case for the three Figure 1 referents.

Equations

• CohnGordonEtAl2019.greedyUnroll CohnGordonEtAl2019.Referent.redDress = [CohnGordonEtAl2019.Word.red, CohnGordonEtAl2019.Word.dress]
• CohnGordonEtAl2019.greedyUnroll CohnGordonEtAl2019.Referent.blueDress = [CohnGordonEtAl2019.Word.dress]
• CohnGordonEtAl2019.greedyUnroll CohnGordonEtAl2019.Referent.redHat = [CohnGordonEtAl2019.Word.red, CohnGordonEtAl2019.Word.object]

theorem CohnGordonEtAl2019.greedyUnroll_weakly_informative (r : Referent) : figureOne.l0Utt (greedyUnroll r) r ≥ 1 / 3

§2.4 weakly informative bound, instantiated for Figure 1.

Each of the three greedy outputs is a complete utterance true of its target referent, so the generic l0Utt_ge_inv_card above immediately gives the 1/|worlds| = 1/3 bound. The actual values for this scene are 1, 1/2, 1/2 — the bound is loose here by design: it certifies architectural sanity, not optimality.

Global RSA Model + Divergence (§2.4)

The global RSA model treats each complete utterance as an atomic option, normalizing over the whole utterance space rather than chaining word-by-word. The divergence between global and incremental predictions for R1 is a central result of [CGGP19] §2.4: the global model prefers the more-informative "red dress" over the bare "dress" (standard RSA Q-implicature), but the incremental model prefers "dress" because chain-rule products penalize longer trajectories (Finding 7, incremental_prefers_bare_noun).

inductive CohnGordonEtAl2019.Utterance : Type

The three complete utterances of Figure 1, treated as atomic options for the global RSA model.

• dress : Utterance
• redDress : Utterance
• redObject : Utterance

@[instance_reducible]

instance CohnGordonEtAl2019.instDecidableEqUtterance : DecidableEq Utterance

Equations

• CohnGordonEtAl2019.instDecidableEqUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CohnGordonEtAl2019.instFintypeUtterance : Fintype Utterance

Equations

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

def CohnGordonEtAl2019.instReprUtterance.repr : Utterance → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance CohnGordonEtAl2019.instReprUtterance : Repr Utterance

Equations

• CohnGordonEtAl2019.instReprUtterance = { reprPrec := CohnGordonEtAl2019.instReprUtterance.repr }

instance CohnGordonEtAl2019.instNonemptyUtterance : Nonempty Utterance

def CohnGordonEtAl2019.uttApplies : Utterance → Referent → Bool

Boolean truth of a complete utterance for a referent.

Equations

• CohnGordonEtAl2019.uttApplies CohnGordonEtAl2019.Utterance.dress CohnGordonEtAl2019.Referent.redDress = true
• CohnGordonEtAl2019.uttApplies CohnGordonEtAl2019.Utterance.dress CohnGordonEtAl2019.Referent.blueDress = true
• CohnGordonEtAl2019.uttApplies CohnGordonEtAl2019.Utterance.redDress CohnGordonEtAl2019.Referent.redDress = true
• CohnGordonEtAl2019.uttApplies CohnGordonEtAl2019.Utterance.redObject CohnGordonEtAl2019.Referent.redDress = true
• CohnGordonEtAl2019.uttApplies CohnGordonEtAl2019.Utterance.redObject CohnGordonEtAl2019.Referent.redHat = true
• CohnGordonEtAl2019.uttApplies x✝¹ x✝ = false

def CohnGordonEtAl2019.globalL0Score (u : Utterance) (r : Referent) : ℚ≥0

Global literal listener value (eq. 1): indicator over referents.

Equations

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

noncomputable def CohnGordonEtAl2019.globalS1 (r : Referent) : PMF Utterance

Global speaker (eq. 2 at zero cost, α = 1): renormalizes L0 over the three atomic utterances.

Equations

• CohnGordonEtAl2019.globalS1 r = PMF.ofScores PMF.Fallback.uniform fun (u : CohnGordonEtAl2019.Utterance) => CohnGordonEtAl2019.globalL0Score u r

theorem CohnGordonEtAl2019.global_prefers_red_dress : (globalS1 Referent.redDress) Utterance.dress < (globalS1 Referent.redDress) Utterance.redDress

Divergence from incremental (§2.4): the global RSA prefers the fully-modified "red dress" over the bare "dress" for R1, because "red dress" uniquely identifies R1 while "dress" leaves R1/R2 ambiguous. Compare Finding 7 (incremental_prefers_bare_noun), where the incremental trajectory probability has the opposite preference: chain-rule products discount longer trajectories enough to flip the ordering. This is the central empirical wedge between the two architectures the paper articulates.

The §3.2 contrastive-inference bridge

§3.2 reanalyses [Sed07]'s review (the effect is [STCC99]'s) in incremental RSA: hearing bare "tall", L1 prefers the tall cup over the tall pitcher — extensionally both fit, but a pitcher-referring speaker had no use for "tall". Both contrast cells are formalized: the paper's four-referent sedivyBundle and a no-contrast companion (SedivyScene_NoContrast.bundle, dropping the absent short cup's word); the shared Referent type lets one Cell-typed LookProportion read off both.

inductive CohnGordonEtAl2019.SedivyScene.Word : Type

Sedivy scene words: scalar adjectives (tall, short) and category nouns (cup, pitcher, key).

• tall : Word
• short : Word
• cup : Word
• pitcher : Word
• key : Word

@[instance_reducible]

instance CohnGordonEtAl2019.SedivyScene.instDecidableEqWord : DecidableEq Word

Equations

• CohnGordonEtAl2019.SedivyScene.instDecidableEqWord x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CohnGordonEtAl2019.SedivyScene.instFintypeWord : Fintype Word

Equations

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

def CohnGordonEtAl2019.SedivyScene.instReprWord.repr : Word → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance CohnGordonEtAl2019.SedivyScene.instReprWord : Repr Word

Equations

• CohnGordonEtAl2019.SedivyScene.instReprWord = { reprPrec := CohnGordonEtAl2019.SedivyScene.instReprWord.repr }

instance CohnGordonEtAl2019.SedivyScene.instNonemptyWord : Nonempty Word

inductive CohnGordonEtAl2019.SedivyScene.Referent : Type

Sedivy scene referents: the four objects in the visual display.

• tallCup : Referent
• shortCup : Referent
• tallPitcher : Referent
• key : Referent

@[instance_reducible]

instance CohnGordonEtAl2019.SedivyScene.instDecidableEqReferent : DecidableEq Referent

Equations

• CohnGordonEtAl2019.SedivyScene.instDecidableEqReferent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CohnGordonEtAl2019.SedivyScene.instFintypeReferent : Fintype Referent

Equations

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

@[instance_reducible]

instance CohnGordonEtAl2019.SedivyScene.instReprReferent : Repr Referent

Equations

• CohnGordonEtAl2019.SedivyScene.instReprReferent = { reprPrec := CohnGordonEtAl2019.SedivyScene.instReprReferent.repr }

def CohnGordonEtAl2019.SedivyScene.instReprReferent.repr : Referent → ℕ → Std.Format

Equations

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

instance CohnGordonEtAl2019.SedivyScene.instNonemptyReferent : Nonempty Referent

def CohnGordonEtAl2019.SedivyScene.sedivyBundle : IncrementalSemantics Word Referent

The Sedivy scene as an IncrementalSemantics bundle: 5 words, 6 complete utterances (3 adj+noun phrases + 3 bare nouns; the bare-noun option is essential — without it "tall" is no longer diagnostic of the cup), 4 referents.

Equations

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

No-contrast companion scene

No-contrast variant of the Sedivy scene, sharing SedivyScene.Referent but with a smaller word inventory. Empirically this is the no-contrast cell of [STCC99]'s 2 × 2 × 2 design: the same-category contrast object (the short cup) is removed from the visual display.

The companion bundle drops .short from Word and the [short, cup] utterance from completeUtterances. Justification: with no shortCup in the display, a cooperative speaker has no scene-anchored use for .short, and the paper's IncrementalSemantics is a scene-specific production model rather than a lexicon-wide one. (The listener's standing mental lexicon still contains short; the bundle here is a model of speaker production for this scene, not of mental inventories.)

Why the fresh Word type rather than a {sedivyBundle with worlds := …} update? Keeping .short in the lexicon while removing all of its referents leaves incrementalSem [.short] _ = 0/0, which mathlib treats as 0 but which kernel evaluation of the ℚ face cannot reduce. The fresh type sidesteps the divide-by-zero pattern at the cost of mild bundle duplication.

inductive CohnGordonEtAl2019.SedivyScene_NoContrast.Word : Type

• tall : Word
• cup : Word
• pitcher : Word
• key : Word

@[instance_reducible]

instance CohnGordonEtAl2019.SedivyScene_NoContrast.instDecidableEqWord : DecidableEq Word

Equations

• CohnGordonEtAl2019.SedivyScene_NoContrast.instDecidableEqWord x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CohnGordonEtAl2019.SedivyScene_NoContrast.instFintypeWord : Fintype Word

Equations

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

@[instance_reducible]

instance CohnGordonEtAl2019.SedivyScene_NoContrast.instReprWord : Repr Word

Equations

• CohnGordonEtAl2019.SedivyScene_NoContrast.instReprWord = { reprPrec := CohnGordonEtAl2019.SedivyScene_NoContrast.instReprWord.repr }

def CohnGordonEtAl2019.SedivyScene_NoContrast.instReprWord.repr : Word → ℕ → Std.Format

Equations

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

instance CohnGordonEtAl2019.SedivyScene_NoContrast.instNonemptyWord : Nonempty Word

def CohnGordonEtAl2019.SedivyScene_NoContrast.bundle : IncrementalSemantics Word SedivyScene.Referent

Equations

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

theorem CohnGordonEtAl2019.sedivy_contrast_inference : (l1 SedivyScene.sedivyBundle SedivyScene.Word.tall) SedivyScene.Referent.tallPitcher < (l1 SedivyScene.sedivyBundle SedivyScene.Word.tall) SedivyScene.Referent.tallCup

Cohn-Gordon §3.2 prediction: after hearing "tall", L1 favours the tall cup over the tall pitcher (3/5 vs 2/5). The mechanism is the contrastive inference: a speaker referring to the pitcher would use "pitcher" alone (S1(pitcher | tallPitcher) = 2/3); the only referent for which "tall" is the speaker's preferred first word is the tall cup, where "cup" alone leaves shortCup ambiguous.

This formalises [Sed07]'s anticipatory contrast effect within the incremental RSA framework (and indirectly captures the [STCC99] empirical pattern Sedivy 2007 reviews). The paradigm-level statement (Sedivy Pattern 2, VisualWorld.ContrastReducesCompetitorLooks) requires a contrast vs no-contrast comparison; this theorem captures the contrast-condition direction only.

noncomputable def CohnGordonEtAl2019.cgSedivyLooks : VisualWorld.LookProportion SedivyEtAl1999.Cell ENNReal

Cell-typed look projection for the Sedivy paradigm under the incremental-RSA model.

Linking hypothesis (load-bearing, editorial)

The incremental RSA model produces a posterior over referents, L1 : Word → Referent → ℝ. Visual-world data are fixation proportions. Mapping the former to the latter requires a linking hypothesis. This file makes the simplest one explicit:

Bayesian posterior linking hypothesis — the proportion of looks to an object equals the listener's posterior probability of that object being the referent at the same point in the unfolding utterance.

[CGGP19] do not state this assumption; they discuss the contrastive-inference effect at the level of L1 posteriors and treat empirical contact with [Sed07]'s look data informally. The Bayesian linking hypothesis used here is the strongest natural choice given a single normalised posterior. A weaker alternative would be a Luce-choice rule over a monotone-in-posterior activation; that weakening preserves the qualitative inequality patterns this file proves. If a second linking hypothesis enters the codebase, the paradigm contract should grow a typed LinkingHypothesis API and the bridge theorem statement should mention which hypothesis is in force.

Construction

cgSedivyLooks role c selects the appropriate scene config based on c.contrast (incRSA_sedivy for the contrast cell; SedivyScene_NoContrast.incRSA_sedivy_noContrast for the no-contrast cell) and reads off L1 .tall · at the referent corresponding to role. Other factors of the cell (typicality, task) are ignored — the incremental RSA model has no internal representation of typicality or task, so the projection is constant in those factors.

Cells in the contrast condition cover four roles; cells in the no-contrast condition omit .contrastingObject (no shortCup is on display) and so collapse to 0 for that role.

Equations

• One or more equations did not get rendered due to their size.
• CohnGordonEtAl2019.cgSedivyLooks role✝ c = 0

theorem CohnGordonEtAl2019.cgSedivyLooks_satisfy_contrast_reduces_competitor : VisualWorld.ContrastReducesCompetitorLooks cgSedivyLooks

Paradigm Pattern 2 verified for Cohn-Gordon's incremental RSA: swapping the contrast factor from contrast to noContrast strictly increases looks to the cross-category competitor (the tall pitcher), under the Bayesian posterior linking hypothesis stated on cgSedivyLooks.

Mechanism: in the contrast scene, L1(.tall, tallPitcher) = 2/5 because a speaker referring to the pitcher would prefer "pitcher" alone (the shortCup distractor pulls "tall" toward the cup). In the no-contrast scene there is no shortCup, "tall" is uninformative between the two extant scale-pole objects, and L1(.tall, tallPitcher) = 1/2.

Discharges SedivyEtAl1999.SatisfiesSedivyPattern.contrast_reduces_competitor_looks for this model. The proof reduces — via the HasContrastCondition lens applied to a destructured cell — to the per-cell L1 inequality, kernel-verified on the exact-ℚ face.

Rubio-Fernández §3.1 Bridge (English Over-Modification, STOP token)

[CGGP19] §3.1 reanalyses [rubio-fernandez-2016]'s finding that English speakers over-modify (saying "the red dress" when "the dress" suffices in a display with one dress). The mechanism: an explicit STOP token marks the end of the utterance, so trajectories of different lengths ([dress, STOP] vs [red, dress, STOP]) become directly comparable under the chain rule. Without STOP, the chain rule penalizes longer trajectories monotonically (Finding 7); with STOP and a per-word cost the over-modification preference can emerge in the right cost regime.

This formalisation establishes the model's lexicon and complete- utterance set with STOP, and proves the structural invariants (every complete utterance ends in STOP; STOP does not apply mid-utterance). The cost-dependent comparison theorem S1^UTT-IP(red dress, STOP | R1) > S1^UTT-IP(dress, STOP | R1) is left as future work — formalising it requires Real.exp over a cost schedule and a quantitative argument that does not reduce via kernel comparison.

inductive CohnGordonEtAl2019.RubioFernandezScene.Word : Type

English lexicon for the Rubio-Fernández display: type nouns and colour adjectives, plus a stop token marking utterance termination.

• dress : Word
• hat : Word
• red : Word
• blue : Word
• stop : Word

@[instance_reducible]

instance CohnGordonEtAl2019.RubioFernandezScene.instDecidableEqWord : DecidableEq Word

Equations

• CohnGordonEtAl2019.RubioFernandezScene.instDecidableEqWord x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CohnGordonEtAl2019.RubioFernandezScene.instFintypeWord : Fintype Word

Equations

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

def CohnGordonEtAl2019.RubioFernandezScene.instReprWord.repr : Word → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance CohnGordonEtAl2019.RubioFernandezScene.instReprWord : Repr Word

Equations

• CohnGordonEtAl2019.RubioFernandezScene.instReprWord = { reprPrec := CohnGordonEtAl2019.RubioFernandezScene.instReprWord.repr }

inductive CohnGordonEtAl2019.RubioFernandezScene.Referent : Type

Display referents: a red dress and a blue hat, the canonical minimal pair from [rubio-fernandez-2016]'s display.

• redDress : Referent
• blueHat : Referent

@[instance_reducible]

instance CohnGordonEtAl2019.RubioFernandezScene.instDecidableEqReferent : DecidableEq Referent

Equations

• CohnGordonEtAl2019.RubioFernandezScene.instDecidableEqReferent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CohnGordonEtAl2019.RubioFernandezScene.instFintypeReferent : Fintype Referent

Equations

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

@[instance_reducible]

instance CohnGordonEtAl2019.RubioFernandezScene.instReprReferent : Repr Referent

Equations

• CohnGordonEtAl2019.RubioFernandezScene.instReprReferent = { reprPrec := CohnGordonEtAl2019.RubioFernandezScene.instReprReferent.repr }

def CohnGordonEtAl2019.RubioFernandezScene.instReprReferent.repr : Referent → ℕ → Std.Format

Equations

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

def CohnGordonEtAl2019.RubioFernandezScene.rfBundle : IncrementalSemantics Word Referent

The Rubio-Fernández scene as an IncrementalSemantics bundle: five words including stop, four complete utterances all ending in stop, two referents. stop does not apply to any referent — it is a structural marker, not a content word.

Equations

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

theorem CohnGordonEtAl2019.RubioFernandezScene.completeUtterances_terminate_in_stop (u : List Word) : u ∈ rfBundle.completeUtterances → u.getLast? = some Word.stop

Every complete utterance terminates with stop. This is the structural invariant the STOP machinery enforces.

theorem CohnGordonEtAl2019.RubioFernandezScene.stop_never_applies (r : Referent) : rfBundle.wordApplies Word.stop r = false

stop never applies to any referent — it is a structural marker, not a content word. This is what makes a STOP-augmented utterance u ++ [.stop] veridically equivalent to the underlying content sequence u.