Cohn-Gordon, Goodman and Potts (2019): An Incremental Iterated Response Model of Pragmatics

Iterated response models compute pragmatic reasoning over complete utterances; the paper moves the reasoning inside the utterance. Utterances are word sequences from a closed set, an incremental semantics scores a prefix at a referent by the fraction of its complete extensions true of the referent among those true of some referent (§2.2), a word-level literal listener renormalizes that score (eq. 4), a word-level speaker best-responds at each prefix (eq. 5, with probability distributed evenly over words with viable continuations when no continuation is true), and the chain rule multiplies the word choices into an utterance-level speaker (eq. 7). On the Figure 1 reference game the architectures come apart: the global speaker prefers the fully informative red dress for the red dress while the incremental product prefers bare dress (Figures 1b, 1e), and upon hearing red the incremental listener already favours the red hat at 0.64, the anticipatory implicature (Figure 1d). The abstract two-letter game of Figure 3 separates the architectures even at equal global informativity. Any complete utterance true of its referent is weakly informative, in that the literal listener assigns the referent at least chance probability, which is the paper's certificate for greedy word-by-word unrolling (§2.4).

With a cost of one per word and none for the STOP token (§3.1), the global speaker prefers the bare noun in English and Spanish alike, but the incremental speaker is indifferent between dress and red dress while preferring vestido to vestido rojo: after red the English speaker is committed to the over-modified continuation, after vestido the Spanish speaker may stop, which is Rubio-Fernández's over-modification asymmetry between adjective–noun and noun–adjective languages. Hearing tall in Sedivy's display, the incremental pragmatic listener favours the tall cup over the tall pitcher at 0.6, since a speaker referring to the pitcher had no use for the modifier (§3.2); the implicature cancels, since after tall pitcher the listener excludes every referent but the pitcher.

Implementation notes

• The reference game carries an utterance-level Boolean semantics, as the paper's incremental semantics is "defined in terms of a global semantics and the set of available complete utterances" (§2.2); word-conjunctive semantics is a constructor, since Figure 3's semantics is not compositional.
• Word-level agents are the kernel pipeline at prefix-indexed graded meanings; the uniform prior and the viable-extension denominator cancel in the literal listener, so every cell is a ratio of extension counts, which decide evaluates.
• Chain-rule trajectory probabilities are real-valued products of speaker masses, so the §3.1 comparisons are real arithmetic in the content-word cost factor exp (-c), the paper's cost of one generalized to any positive cost.
• Kernels are noncomputable, so the greedy unroller is a per-referent table, certified to land in the utterance set and to be true of its target, which is all that §2.4's bound uses.

TODO

• §4's TUNA-corpus comparison (the share of two-word optima under each architecture) is an experiment over corpus trials, not formalizable content.
• The general §2.4 claim that greedy unrolling always terminates in a true complete utterance is argued informally in the paper; here it is certified for Figure 1.

References

• R. Cohn-Gordon, N. D. Goodman and C. Potts, An Incremental Iterated Response Model of Pragmatics (2019)
• P. Rubio-Fernández, How Redundant Are Redundant Color Adjectives? An Efficiency-Based Analysis of Color Overspecification (2016)
• J. C. Sedivy, Implicature During Real Time Conversation: A View from Language Processing Research (2007)

Reference games and the incremental semantics (§2.2)

structure CohnGordonEtAl2019.ReferenceGame (U W : Type) : Type

A reference game (Figure 1a) has a closed set of complete utterances over words U, an utterance-level Boolean semantics, and the referents on display.

• utterances : List (List U)

  The closed set of available complete utterances.

• sem : List U → W → Bool

  The global semantics ⟦·⟧ gives the truth of a complete utterance at a referent.

• worlds : List W

  The referents on display.

def CohnGordonEtAl2019.ReferenceGame.ofLexicon {U W : Type} (applies : U → W → Bool) (utts : List (List U)) (ws : List W) : ReferenceGame U W

A game whose semantics is word-conjunctive, from a lexicon of word extensions.

Equations

• CohnGordonEtAl2019.ReferenceGame.ofLexicon applies utts ws = { utterances := utts, sem := fun (u : List U) (r : W) => u.all fun (w : U) => applies w r, worlds := ws }

def CohnGordonEtAl2019.ReferenceGame.trueExts {U W : Type} [DecidableEq U] (g : ReferenceGame U W) (pfx : List U) (r : W) : ℕ

The number of complete extensions of pfx true of r.

Equations

• g.trueExts pfx r = (List.filter (fun (u : List U) => pfx.isPrefixOf u && g.sem u r) g.utterances).length

def CohnGordonEtAl2019.ReferenceGame.viableExts {U W : Type} [DecidableEq U] (g : ReferenceGame U W) (pfx : List U) : ℕ

The number of complete extensions of pfx true of some referent on display.

Equations

• g.viableExts pfx = (List.filter (fun (u : List U) => pfx.isPrefixOf u && g.worlds.any fun (r : W) => g.sem u r) g.utterances).length

theorem CohnGordonEtAl2019.ReferenceGame.trueExts_le_viableExts {U W : Type} [DecidableEq U] (g : ReferenceGame U W) (hw : ∀ (r : W), r ∈ g.worlds) (pfx : List U) (r : W) : g.trueExts pfx r ≤ g.viableExts pfx

def CohnGordonEtAl2019.ReferenceGame.viable {U W : Type} (g : ReferenceGame U W) : List (List U)

The complete utterances true of some referent on display.

Equations

• g.viable = List.filter (fun (u : List U) => g.worlds.any fun (r : W) => g.sem u r) g.utterances

noncomputable def CohnGordonEtAl2019.ReferenceGame.incSem {U W : Type} [DecidableEq U] (g : ReferenceGame U W) (pfx : List U) (r : W) : ENNReal

The incremental semantics ⟦pfx⟧(r) (§2.2) is the string meaning of the prefix at the truth of the complete utterances, the fraction of the viable extensions of pfx that are true of r.

Equations

• g.incSem pfx r = ENNReal.ofReal (RSA.stringMeaning g.viable (fun (u : List U) (r : W) => if g.sem u r = true then 1 else 0) pfx r)

theorem CohnGordonEtAl2019.ReferenceGame.incSem_eq_div {U W : Type} [DecidableEq U] (g : ReferenceGame U W) {r : W} (hr : r ∈ g.worlds) (pfx : List U) : g.incSem pfx r = ↑(g.trueExts pfx r) / ↑(g.viableExts pfx)

The incremental semantics is the share of true extensions among the viable ones.

The global model (§2.1)

def CohnGordonEtAl2019.ReferenceGame.Complete {U W : Type} (g : ReferenceGame U W) : Type

The complete utterances of the game, as a type.

Equations

• g.Complete = { u : List U // u ∈ g.utterances }

@[instance_reducible]

instance CohnGordonEtAl2019.ReferenceGame.instFintypeComplete {U W : Type} [DecidableEq U] (g : ReferenceGame U W) : Fintype g.Complete

Equations

• g.instFintypeComplete = Fintype.subtype g.utterances.toFinset ⋯

@[instance_reducible]

instance CohnGordonEtAl2019.ReferenceGame.instMeasurableSpaceComplete {U W : Type} (g : ReferenceGame U W) : MeasurableSpace g.Complete

Equations

• g.instMeasurableSpaceComplete = ⊤

instance CohnGordonEtAl2019.ReferenceGame.instDiscreteMeasurableSpaceComplete {U W : Type} (g : ReferenceGame U W) : DiscreteMeasurableSpace g.Complete

@[instance_reducible]

instance CohnGordonEtAl2019.ReferenceGame.instDecidableEqComplete {U W : Type} [DecidableEq U] (g : ReferenceGame U W) : DecidableEq g.Complete

Equations

• g.instDecidableEqComplete = Subtype.instDecidableEq

noncomputable def CohnGordonEtAl2019.ReferenceGame.globalL0 {U W : Type} [DecidableEq U] (g : ReferenceGame U W) [MeasurableSpace W] : ProbabilityTheory.Kernel g.Complete W

The global literal listener (eq. 1) conditions the uniform prior on the utterance's truth.

Equations

• g.globalL0 = ProbabilityTheory.Kernel.ofDensity (ProbabilityTheory.uniformOn Set.univ) fun (u : g.Complete) (r : W) => if g.sem (↑u) r = true then 1 else 0

instance CohnGordonEtAl2019.ReferenceGame.instIsFiniteKernelCompleteGlobalL0 {U W : Type} [DecidableEq U] (g : ReferenceGame U W) [MeasurableSpace W] : ProbabilityTheory.IsFiniteKernel g.globalL0

noncomputable def CohnGordonEtAl2019.ReferenceGame.globalS1 {U W : Type} [DecidableEq U] (g : ReferenceGame U W) [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] (cost : g.Complete → ℝ) : ProbabilityTheory.Kernel W g.Complete

The global pragmatic speaker (eq. 2).

Equations

• g.globalS1 cost = RSA.speaker 1 cost (⇑g.globalL0) MeasureTheory.Measure.dirac

def CohnGordonEtAl2019.ReferenceGame.uttCost {U : Type} (cost : U → ℝ) (u : List U) : ℝ

An utterance costs the sum of its words' costs (§3.1).

Equations

• CohnGordonEtAl2019.ReferenceGame.uttCost cost u = (List.map cost u).sum

theorem CohnGordonEtAl2019.ReferenceGame.globalL0_apply {U W : Type} [DecidableEq U] (g : ReferenceGame U W) [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] (u : g.Complete) (r : W) : (g.globalL0 u) {r} = (if g.sem (↑u) r = true then 1 else 0) / ↑{r' : W | g.sem (↑u) r' = true}.card

theorem CohnGordonEtAl2019.ReferenceGame.globalL0_ge_inv_card {U W : Type} [DecidableEq U] (g : ReferenceGame U W) [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] {u : g.Complete} {r : W} (htrue : g.sem (↑u) r = true) : (↑(Fintype.card W))⁻¹ ≤ (g.globalL0 u) {r}

A complete utterance true of a referent gives the literal listener at least chance probability of it, the weak informativity of §2.4.

The word-level pipeline (eqs. 4–6)

noncomputable def CohnGordonEtAl2019.ReferenceGame.l0 {U W : Type} [DecidableEq U] (g : ReferenceGame U W) [MeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] (ctx : List U) : ProbabilityTheory.Kernel U W

The incremental literal listener at context ctx (eq. 4) reweights the uniform prior by ⟦ctx ++ [u]⟧.

Equations

• g.l0 ctx = ProbabilityTheory.Kernel.ofDensity (ProbabilityTheory.uniformOn Set.univ) fun (u : U) => g.incSem (ctx ++ [u])

instance CohnGordonEtAl2019.ReferenceGame.instIsFiniteKernelL0 {U W : Type} [DecidableEq U] (g : ReferenceGame U W) [MeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] (ctx : List U) : ProbabilityTheory.IsFiniteKernel (g.l0 ctx)

theorem CohnGordonEtAl2019.ReferenceGame.l0_apply {U W : Type} [DecidableEq U] (g : ReferenceGame U W) [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] (hw : ∀ (r : W), r ∈ g.worlds) (ctx : List U) (u : U) (r : W) : ((g.l0 ctx) u) {r} = ↑(g.trueExts (ctx ++ [u]) r) / ↑(∑ r' : W, g.trueExts (ctx ++ [u]) r')

The uniform prior and the viable-extension denominator cancel in the listener, so each cell is the referent's share of the true-extension counts.

def CohnGordonEtAl2019.ReferenceGame.DeadEnd {U W : Type} [DecidableEq U] (g : ReferenceGame U W) (ctx : List U) (r : W) : Prop

A context ctx is a dead end for r (§2.2) when no continuation of it is true of r.

Equations

• g.DeadEnd ctx r = ∀ (u : U), g.trueExts (ctx ++ [u]) r = 0

@[instance_reducible]

instance CohnGordonEtAl2019.ReferenceGame.instDecidableDeadEnd {U W : Type} [DecidableEq U] (g : ReferenceGame U W) [Fintype U] (ctx : List U) (r : W) : Decidable (g.DeadEnd ctx r)

Equations

• g.instDecidableDeadEnd ctx r = { decide := decide (∀ a ∈ Finset.univ, (fun (u : U) => g.trueExts (ctx ++ [u]) r = 0) a), reflects_decide := ⋯ }

noncomputable def CohnGordonEtAl2019.ReferenceGame.s1 {U W : Type} [DecidableEq U] (g : ReferenceGame U W) [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] (cost : U → ℝ) (ctx : List U) : ProbabilityTheory.Kernel W U

The word-level speaker at context ctx (eq. 5) is the best response to the incremental literal listener. At a dead end, probability is distributed evenly over the words with viable continuations.

Equations

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

theorem CohnGordonEtAl2019.ReferenceGame.s1_apply {U W : Type} [DecidableEq U] (g : ReferenceGame U W) [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] {ctx : List U} {r : W} (hnd : ¬g.DeadEnd ctx r) (cost : U → ℝ) : (g.s1 cost ctx) r = (RSA.speaker 1 cost (⇑(g.l0 ctx)) MeasureTheory.Measure.dirac) r

theorem CohnGordonEtAl2019.ReferenceGame.s1_apply_deadEnd {U W : Type} [DecidableEq U] (g : ReferenceGame U W) [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] {ctx : List U} {r : W} (hd : g.DeadEnd ctx r) (cost : U → ℝ) : (g.s1 cost ctx) r = ProbabilityTheory.uniformOn ↑{u : U | 0 < g.viableExts (ctx ++ [u])}

instance CohnGordonEtAl2019.ReferenceGame.instIsFiniteKernelS1 {U W : Type} [DecidableEq U] (g : ReferenceGame U W) [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] (cost : U → ℝ) (ctx : List U) : ProbabilityTheory.IsFiniteKernel (g.s1 cost ctx)

noncomputable def CohnGordonEtAl2019.ReferenceGame.l1 {U W : Type} [DecidableEq U] (g : ReferenceGame U W) [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] (cost : U → ℝ) (ctx : List U) : ProbabilityTheory.Kernel U W

The incremental pragmatic listener at context ctx (eq. 6) inverts the word-level speaker against the uniform prior.

Equations

• g.l1 cost ctx = RSA.listener (ProbabilityTheory.uniformOn Set.univ) ⇑(g.s1 cost ctx)

instance CohnGordonEtAl2019.ReferenceGame.instIsFiniteKernelL1 {U W : Type} [DecidableEq U] (g : ReferenceGame U W) [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] (cost : U → ℝ) (ctx : List U) : ProbabilityTheory.IsFiniteKernel (g.l1 cost ctx)

noncomputable def CohnGordonEtAl2019.ReferenceGame.s1Utt {U W : Type} [DecidableEq U] (g : ReferenceGame U W) [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] (cost : U → ℝ) (r : W) (u : List U) : ℝ

The utterance-level incremental speaker (eq. 7) is the chain-rule product of the word-level speaker's choices along the utterance.

Equations

• g.s1Utt cost r u = RSA.chain (g.s1 cost) r [] u

theorem CohnGordonEtAl2019.ReferenceGame.s1_real_singleton {U W : Type} [DecidableEq U] (g : ReferenceGame U W) [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] {ctx : List U} {r : W} (hnd : ¬g.DeadEnd ctx r) {cost : U → ℝ} (u : U) : ((g.s1 cost ctx) r).real {u} = (((g.l0 ctx) u) {r}).toReal * Real.exp (-cost u) / ∑ u' : U, (((g.l0 ctx) u') {r}).toReal * Real.exp (-cost u')

On reals, the speaker's share is the weighted listener value over the row sum.

Evaluation lemmas

theorem CohnGordonEtAl2019.ReferenceGame.l0_apply_ne_zero {U W : Type} [DecidableEq U] (g : ReferenceGame U W) [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] (hw : ∀ (r : W), r ∈ g.worlds) {ctx : List U} {u : U} {r : W} (ht : g.trueExts (ctx ++ [u]) r ≠ 0) : ((g.l0 ctx) u) {r} ≠ 0

theorem CohnGordonEtAl2019.ReferenceGame.l0_apply_eq_zero {U W : Type} [DecidableEq U] (g : ReferenceGame U W) [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] (hw : ∀ (r : W), r ∈ g.worlds) {ctx : List U} {u : U} {r : W} (ht : g.trueExts (ctx ++ [u]) r = 0) : ((g.l0 ctx) u) {r} = 0

theorem CohnGordonEtAl2019.ReferenceGame.l0_real {U W : Type} [DecidableEq U] (g : ReferenceGame U W) [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] (hw : ∀ (r : W), r ∈ g.worlds) (ctx : List U) (u : U) (r : W) : (((g.l0 ctx) u) {r}).toReal = ↑(g.trueExts (ctx ++ [u]) r) / ↑(∑ r' : W, g.trueExts (ctx ++ [u]) r')

On reals, a listener cell is the referent's share of the true-extension counts.

theorem CohnGordonEtAl2019.ReferenceGame.s1_real_lt_iff {U W : Type} [DecidableEq U] (g : ReferenceGame U W) [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] {ctx : List U} {r : W} (hnd : ¬g.DeadEnd ctx r) {cost : U → ℝ} {u₀ : U} (h0 : ((g.l0 ctx) u₀) {r} ≠ 0) {u u' : U} : ((g.s1 cost ctx) r).real {u} < ((g.s1 cost ctx) r).real {u'} ↔ ((g.l0 ctx) u) {r} * ENNReal.ofReal (Real.exp (-cost u)) < ((g.l0 ctx) u') {r} * ENNReal.ofReal (Real.exp (-cost u'))

Row preference of the incremental speaker compares weighted listener cells.

theorem CohnGordonEtAl2019.ReferenceGame.s1_apply_ne_zero {U W : Type} [DecidableEq U] (g : ReferenceGame U W) [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] (hw : ∀ (r : W), r ∈ g.worlds) {ctx : List U} {r : W} {u : U} (hnd : ¬g.DeadEnd ctx r) {cost : U → ℝ} (ht : g.trueExts (ctx ++ [u]) r ≠ 0) : ((g.s1 cost ctx) r) {u} ≠ 0

theorem CohnGordonEtAl2019.ReferenceGame.s1_apply_eq_zero {U W : Type} [DecidableEq U] (g : ReferenceGame U W) [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] (hw : ∀ (r : W), r ∈ g.worlds) {ctx : List U} {r : W} {u : U} (hnd : ¬g.DeadEnd ctx r) (cost : U → ℝ) (ht : g.trueExts (ctx ++ [u]) r = 0) : ((g.s1 cost ctx) r) {u} = 0

A word with no true continuation is never chosen off a dead end.

theorem CohnGordonEtAl2019.ReferenceGame.s1_apply_eq_one {U W : Type} [DecidableEq U] (g : ReferenceGame U W) [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] (hw : ∀ (r : W), r ∈ g.worlds) {ctx : List U} {r : W} {u : U} (hnd : ¬g.DeadEnd ctx r) {cost : U → ℝ} (ht : g.trueExts (ctx ++ [u]) r ≠ 0) (hother : ∀ (u' : U), u' ≠ u → g.trueExts (ctx ++ [u']) r = 0) : ((g.s1 cost ctx) r) {u} = 1

A referent whose only true continuation is u is signalled with certainty.

theorem CohnGordonEtAl2019.ReferenceGame.l1_real_lt_iff {U W : Type} [DecidableEq U] (g : ReferenceGame U W) [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] {cost : U → ℝ} {ctx : List U} {u : U} {r r' : W} : ((g.l1 cost ctx) u).real {r} < ((g.l1 cost ctx) u).real {r'} ↔ ((g.s1 cost ctx) r).real {u} < ((g.s1 cost ctx) r').real {u}

Listener preference upon a word compares the speaker's masses, since the uniform prior cancels.

theorem CohnGordonEtAl2019.ReferenceGame.l1_real_singleton {U W : Type} [DecidableEq U] (g : ReferenceGame U W) [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] {cost : U → ℝ} {ctx : List U} {u : U} (r : W) : ((g.l1 cost ctx) u).real {r} = ((g.s1 cost ctx) r).real {u} / ∑ r' : W, ((g.s1 cost ctx) r').real {u}

Exact Bayes for the incremental listener.

theorem CohnGordonEtAl2019.ReferenceGame.s1_real_counts {U W : Type} [DecidableEq U] (g : ReferenceGame U W) [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] (hw : ∀ (r : W), r ∈ g.worlds) {ctx : List U} {r : W} (hnd : ¬g.DeadEnd ctx r) (u : U) : ((g.s1 0 ctx) r).real {u} = ↑(g.trueExts (ctx ++ [u]) r) / ↑(∑ r' : W, g.trueExts (ctx ++ [u]) r') / ∑ u' : U, ↑(g.trueExts (ctx ++ [u']) r) / ↑(∑ r' : W, g.trueExts (ctx ++ [u']) r')

At no cost, the speaker's share is a double ratio of extension counts.

Figure 1: the reference game

inductive CohnGordonEtAl2019.Word : Type

The words of 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.

@[instance_reducible]

instance CohnGordonEtAl2019.instReprWord : Repr Word

Equations

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

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

Equations

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

instance CohnGordonEtAl2019.instNonemptyWord : Nonempty Word

@[instance_reducible]

instance CohnGordonEtAl2019.instMeasurableSpaceWord : MeasurableSpace Word

Equations

• CohnGordonEtAl2019.instMeasurableSpaceWord = ⊤

instance CohnGordonEtAl2019.instDiscreteMeasurableSpaceWord : DiscreteMeasurableSpace Word

inductive CohnGordonEtAl2019.Referent : Type

The referents of Figure 1a are the red dress R1, the blue dress R2, and the 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

@[instance_reducible]

instance CohnGordonEtAl2019.instMeasurableSpaceReferent : MeasurableSpace Referent

Equations

• CohnGordonEtAl2019.instMeasurableSpaceReferent = ⊤

instance CohnGordonEtAl2019.instDiscreteMeasurableSpaceReferent : DiscreteMeasurableSpace Referent

def CohnGordonEtAl2019.figureOne : ReferenceGame Word Referent

Figure 1a has three utterances with word-conjunctive semantics over three referents.

Equations

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

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

For R1 the speaker leads with red, keeping both red referents viable, while dress dilutes the listener over the two dresses (Figure 1c).

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

For R1 after red the speaker completes with dress, unique to R1 (Figure 1c).

theorem CohnGordonEtAl2019.noun_only_for_r2 : ((figureOne.s1 0 []) Referent.blueDress) {Word.dress} = 1

The blue dress R2 forces dress as the first word (Figure 1c).

theorem CohnGordonEtAl2019.adj_only_for_r3 : ((figureOne.s1 0 []) Referent.redHat) {Word.red} = 1

The red hat R3 forces red as the first word (Figure 1c).

theorem CohnGordonEtAl2019.uniform_after_red_for_r2 : ((figureOne.s1 0 [Word.red]) Referent.blueDress).real {Word.dress} = 1 / 2 ∧ ((figureOne.s1 0 [Word.red]) Referent.blueDress).real {Word.object} = 1 / 2 ∧ ((figureOne.s1 0 [Word.red]) Referent.blueDress).real {Word.red} = 0

For R2 after red, the dead end of §2.2, no continuation is true of the blue dress, and probability distributes evenly over the words with viable continuations (Figure 1c).

Figure 1d: the anticipatory implicature

theorem CohnGordonEtAl2019.s1_figureOne_values : ((figureOne.s1 0 []) Referent.redDress).real {Word.red} = 4 / 7 ∧ ((figureOne.s1 0 []) Referent.redDress).real {Word.dress} = 3 / 7 ∧ ((figureOne.s1 0 [Word.red]) Referent.redDress).real {Word.dress} = 2 / 3 ∧ ((figureOne.s1 0 []) Referent.redHat).real {Word.red} = 1

The four speaker cells behind Figures 1c–1e, at no cost, in closed form.

theorem CohnGordonEtAl2019.listener_anticipation : ((figureOne.l1 0 []) Word.red).real {Referent.redDress} < ((figureOne.l1 0 []) Word.red).real {Referent.redHat}

Upon hearing red, the incremental listener favours the red hat over the red dress, since red is the hat's only opening while the dress's speaker had alternatives. This is the anticipatory implicature of Figure 1d.

theorem CohnGordonEtAl2019.listener_anticipation_value : ((figureOne.l1 0 []) Word.red).real {Referent.redHat} = 7 / 11

Exactly, L1(R3 | red) = 1 / (4/7 + 0 + 1) = 7/11 ≈ 0.64, the paper's 0.64 (Figure 1d).

Figure 1e: the chain-rule wedge

theorem CohnGordonEtAl2019.incremental_prefers_bare_noun : figureOne.s1Utt 0 Referent.redDress [Word.red, Word.dress] < figureOne.s1Utt 0 Referent.redDress [Word.dress]

For R1 the chain-rule utterance-level speaker (eq. 7) prefers bare dress (3/7) to red dress (4/7 · 2/3 = 8/21) (Figure 1e). This is the architectural wedge against Figure 1b, where the global speaker prefers red dress.

The global model on Figure 1 (§2.1, Figure 1b)

theorem CohnGordonEtAl2019.fig1_mem_dress : [Word.dress] ∈ figureOne.utterances

theorem CohnGordonEtAl2019.fig1_mem_redDress : [Word.red, Word.dress] ∈ figureOne.utterances

theorem CohnGordonEtAl2019.global_prefers_red_dress : ((figureOne.globalS1 0) Referent.redDress).real {⟨[Word.dress], fig1_mem_dress⟩} < ((figureOne.globalS1 0) Referent.redDress).real {⟨[Word.red, Word.dress], fig1_mem_redDress⟩}

For the red dress the global pragmatic speaker prefers red dress (1/2) to bare dress (1/4), the preference the chain rule reverses (Figure 1b).

§2.4: greedy unrolling and weak informativity

def CohnGordonEtAl2019.greedyUnroll : Referent → List Word

The greedy unrolling of Figure 1 (§2.3) takes the word-by-word argmax trajectory per referent.

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_complete (r : Referent) : greedyUnroll r ∈ figureOne.utterances

Greedy unrolling lands in the utterance set.

theorem CohnGordonEtAl2019.greedyUnroll_true (r : Referent) : figureOne.sem (greedyUnroll r) r = true

Greedy unrolling produces a true utterance.

theorem CohnGordonEtAl2019.greedyUnroll_weakly_informative (r : Referent) : (↑(Fintype.card Referent))⁻¹ ≤ (figureOne.globalL0 ⟨greedyUnroll r, ⋯⟩) {r}

In Figure 1 the global literal listener gives the target of each greedy output at least chance probability, the weak informativity of §2.4.

Figure 3: the abstract two-letter game

Four utterances AA, AB, BA, BB over two worlds; every pair is true except (AB, W1). The global speaker is indifferent among W1's three true utterances, while the chain rule prefers AA: choosing A first costs informativity (AB is false of W1), but the second letter is then forced, and 2/5 · 1 beats 3/5 · 1/2.

inductive CohnGordonEtAl2019.Letter : Type

The two letters.

• A : Letter
• B : Letter

@[instance_reducible]

instance CohnGordonEtAl2019.instDecidableEqLetter : DecidableEq Letter

Equations

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

@[instance_reducible]

instance CohnGordonEtAl2019.instFintypeLetter : Fintype Letter

Equations

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

def CohnGordonEtAl2019.instReprLetter.repr : Letter → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance CohnGordonEtAl2019.instReprLetter : Repr Letter

Equations

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

instance CohnGordonEtAl2019.instNonemptyLetter : Nonempty Letter

@[instance_reducible]

instance CohnGordonEtAl2019.instMeasurableSpaceLetter : MeasurableSpace Letter

Equations

• CohnGordonEtAl2019.instMeasurableSpaceLetter = ⊤

instance CohnGordonEtAl2019.instDiscreteMeasurableSpaceLetter : DiscreteMeasurableSpace Letter

inductive CohnGordonEtAl2019.AbstractWorld : Type

The two worlds.

• W1 : AbstractWorld
• W2 : AbstractWorld

@[instance_reducible]

instance CohnGordonEtAl2019.instDecidableEqAbstractWorld : DecidableEq AbstractWorld

Equations

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

@[instance_reducible]

instance CohnGordonEtAl2019.instFintypeAbstractWorld : Fintype AbstractWorld

Equations

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

@[instance_reducible]

instance CohnGordonEtAl2019.instReprAbstractWorld : Repr AbstractWorld

Equations

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

def CohnGordonEtAl2019.instReprAbstractWorld.repr : AbstractWorld → ℕ → Std.Format

Equations

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

instance CohnGordonEtAl2019.instNonemptyAbstractWorld : Nonempty AbstractWorld

@[instance_reducible]

instance CohnGordonEtAl2019.instMeasurableSpaceAbstractWorld : MeasurableSpace AbstractWorld

Equations

• CohnGordonEtAl2019.instMeasurableSpaceAbstractWorld = ⊤

instance CohnGordonEtAl2019.instDiscreteMeasurableSpaceAbstractWorld : DiscreteMeasurableSpace AbstractWorld

def CohnGordonEtAl2019.figureThree : ReferenceGame Letter AbstractWorld

In Figure 3's game the semantics is a table, not word-conjunctive.

Equations

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

theorem CohnGordonEtAl2019.figureThree_incremental_prefers_AA : figureThree.s1Utt 0 AbstractWorld.W1 [Letter.B, Letter.A] < figureThree.s1Utt 0 AbstractWorld.W1 [Letter.A, Letter.A]

For W1 the chain rule strictly prefers AA (0.4) to BA (0.3) (Figure 3, red).

theorem CohnGordonEtAl2019.fig3_mem_AA : [Letter.A, Letter.A] ∈ figureThree.utterances

theorem CohnGordonEtAl2019.fig3_mem_BA : [Letter.B, Letter.A] ∈ figureThree.utterances

theorem CohnGordonEtAl2019.figureThree_global_indifferent : ((figureThree.globalS1 0) AbstractWorld.W1) {⟨[Letter.A, Letter.A], fig3_mem_AA⟩} = ((figureThree.globalS1 0) AbstractWorld.W1) {⟨[Letter.B, Letter.A], fig3_mem_BA⟩}

For W1 the global speaker is indifferent between AA and BA (Figure 3, green), which are both true and equally informative, so only the chain rule separates them.

§3.1: over-modification and the STOP token

English: a red dress R1 and a blue hat R2, utterances dress, red dress, hat, blue hat, each closed by STOP. Every content word carries the same cost c and STOP is free. The incremental speaker is indifferent between dress and red dress at every c: the first choice weighs dress and red equally, and each continuation is then forced. Spanish puts the noun first, so vestido alone opens R1's utterances; the choice between STOP and rojo is then cost-driven, and any dispreference for longer utterances (0 < c) yields the paper's preference for the bare noun — at c = 1, 0.73 against 0.27.

inductive CohnGordonEtAl2019.English.Word : Type

English puts the adjective before the noun, and STOP closes the utterance.

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

@[instance_reducible]

instance CohnGordonEtAl2019.English.instDecidableEqWord : DecidableEq Word

Equations

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

@[instance_reducible]

instance CohnGordonEtAl2019.English.instFintypeWord : Fintype Word

Equations

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

@[instance_reducible]

instance CohnGordonEtAl2019.English.instReprWord : Repr Word

Equations

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

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

Equations

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

instance CohnGordonEtAl2019.English.instNonemptyWord : Nonempty Word

@[instance_reducible]

instance CohnGordonEtAl2019.English.instMeasurableSpaceWord : MeasurableSpace Word

Equations

• CohnGordonEtAl2019.English.instMeasurableSpaceWord = ⊤

instance CohnGordonEtAl2019.English.instDiscreteMeasurableSpaceWord : DiscreteMeasurableSpace Word

inductive CohnGordonEtAl2019.English.Referent : Type

The two referents are a red dress and a blue hat.

• redDress : Referent
• blueHat : Referent

@[instance_reducible]

instance CohnGordonEtAl2019.English.instDecidableEqReferent : DecidableEq Referent

Equations

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

@[instance_reducible]

instance CohnGordonEtAl2019.English.instFintypeReferent : Fintype Referent

Equations

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

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

Equations

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

@[instance_reducible]

instance CohnGordonEtAl2019.English.instReprReferent : Repr Referent

Equations

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

instance CohnGordonEtAl2019.English.instNonemptyReferent : Nonempty Referent

@[instance_reducible]

instance CohnGordonEtAl2019.English.instMeasurableSpaceReferent : MeasurableSpace Referent

Equations

• CohnGordonEtAl2019.English.instMeasurableSpaceReferent = ⊤

instance CohnGordonEtAl2019.English.instDiscreteMeasurableSpaceReferent : DiscreteMeasurableSpace Referent

def CohnGordonEtAl2019.English.game : ReferenceGame Word Referent

The English game has adjective–noun order and STOP-terminated utterances.

Equations

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

theorem CohnGordonEtAl2019.English.sem_append_stop (u : List Word) (r : Referent) : game.sem (u ++ [Word.stop]) r = game.sem u r

STOP is semantically inert, since appending it changes no utterance's truth value.

theorem CohnGordonEtAl2019.English.utterances_stop_terminated (u : List Word) : u ∈ game.utterances → u.getLast? = some Word.stop

Every complete utterance is STOP-terminated.

def CohnGordonEtAl2019.English.cost (c : ℝ) : Word → ℝ

Under the cost of §3.1 every content word costs c and STOP nothing.

Equations

• CohnGordonEtAl2019.English.cost c u = if u = CohnGordonEtAl2019.English.Word.stop then 0 else c

theorem CohnGordonEtAl2019.English.incremental_indifferent (c : ℝ) : game.s1Utt (cost c) Referent.redDress [Word.dress, Word.stop] = game.s1Utt (cost c) Referent.redDress [Word.red, Word.dress, Word.stop]

In English (§3.1) the incremental speaker is indifferent between bare dress and over-modified red dress at every content-word cost, the paper's 0.5/0.5. The first word decides on informativity alone, where dress and red tie, and after red the over-modifying dress is forced.

theorem CohnGordonEtAl2019.English.mem_dress : [Word.dress, Word.stop] ∈ game.utterances

theorem CohnGordonEtAl2019.English.mem_redDress : [Word.red, Word.dress, Word.stop] ∈ game.utterances

theorem CohnGordonEtAl2019.English.global_prefers_bare_noun {c : ℝ} (hc : 0 < c) : ((game.globalS1 fun (u : game.Complete) => ReferenceGame.uttCost (cost c) ↑u) Referent.redDress).real {⟨[Word.red, Word.dress, Word.stop], mem_redDress⟩} < ((game.globalS1 fun (u : game.Complete) => ReferenceGame.uttCost (cost c) ↑u) Referent.redDress).real {⟨[Word.dress, Word.stop], mem_dress⟩}

Globally both English utterances identify the red dress (§3.1), so with any dispreference for length the global speaker prefers bare dress, the paper's 0.73 against 0.27 at c = 1, in contrast with the incremental speaker's indifference.

inductive CohnGordonEtAl2019.Spanish.Word : Type

Spanish puts the noun before the adjective, and STOP closes the utterance.

• vestido : Word
• rojo : Word
• sombrero : Word
• azul : Word
• stop : Word

@[instance_reducible]

instance CohnGordonEtAl2019.Spanish.instDecidableEqWord : DecidableEq Word

Equations

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

@[instance_reducible]

instance CohnGordonEtAl2019.Spanish.instFintypeWord : Fintype Word

Equations

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

@[instance_reducible]

instance CohnGordonEtAl2019.Spanish.instReprWord : Repr Word

Equations

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

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

Equations

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

instance CohnGordonEtAl2019.Spanish.instNonemptyWord : Nonempty Word

@[instance_reducible]

instance CohnGordonEtAl2019.Spanish.instMeasurableSpaceWord : MeasurableSpace Word

Equations

• CohnGordonEtAl2019.Spanish.instMeasurableSpaceWord = ⊤

instance CohnGordonEtAl2019.Spanish.instDiscreteMeasurableSpaceWord : DiscreteMeasurableSpace Word

def CohnGordonEtAl2019.Spanish.game : ReferenceGame Word English.Referent

The Spanish game over the same referents has noun–adjective order and STOP-terminated utterances.

Equations

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

def CohnGordonEtAl2019.Spanish.cost (c : ℝ) : Word → ℝ

The §3.1 cost, as in English.

Equations

• CohnGordonEtAl2019.Spanish.cost c u = if u = CohnGordonEtAl2019.Spanish.Word.stop then 0 else c

theorem CohnGordonEtAl2019.Spanish.incremental_prefers_bare_noun {c : ℝ} (hc : 0 < c) : game.s1Utt (cost c) English.Referent.redDress [Word.vestido, Word.rojo, Word.stop] < game.s1Utt (cost c) English.Referent.redDress [Word.vestido, Word.stop]

In Spanish (§3.1), with any dispreference for longer utterances (0 < c), the incremental speaker prefers bare vestido to vestido rojo, at c = 1 the paper's 0.73 against 0.27. The noun alone already settles the referent, so the second step is a pure cost choice between STOP and rojo.

§3.2: the anticipatory implicature in Sedivy's display

A tall cup, a short cup, a tall pitcher and a key; utterances tall cup, short cup, tall pitcher, cup, pitcher, key. Upon hearing tall the incremental pragmatic listener favours the tall cup at 3/5 against the tall pitcher at 2/5: a speaker meaning the pitcher had pitcher alone, so tall was a third of her choices, while the cup's speaker, whose bare cup is ambiguous with the short cup, uses tall half the time. The §3.1 cost is common to every content word, so it cancels within each row, and the scene is evaluated at zero cost. The implicature cancels: were the next word pitcher, the listener who has updated on tall excludes every referent but the pitcher.

inductive CohnGordonEtAl2019.Sedivy.Word : Type

The scene's words are the two scalar adjectives and three category nouns.

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

@[instance_reducible]

instance CohnGordonEtAl2019.Sedivy.instDecidableEqWord : DecidableEq Word

Equations

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

@[instance_reducible]

instance CohnGordonEtAl2019.Sedivy.instFintypeWord : Fintype Word

Equations

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

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

Equations

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

@[instance_reducible]

instance CohnGordonEtAl2019.Sedivy.instReprWord : Repr Word

Equations

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

instance CohnGordonEtAl2019.Sedivy.instNonemptyWord : Nonempty Word

@[instance_reducible]

instance CohnGordonEtAl2019.Sedivy.instMeasurableSpaceWord : MeasurableSpace Word

Equations

• CohnGordonEtAl2019.Sedivy.instMeasurableSpaceWord = ⊤

instance CohnGordonEtAl2019.Sedivy.instDiscreteMeasurableSpaceWord : DiscreteMeasurableSpace Word

inductive CohnGordonEtAl2019.Sedivy.Referent : Type

The four objects on display.

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

@[instance_reducible]

instance CohnGordonEtAl2019.Sedivy.instDecidableEqReferent : DecidableEq Referent

Equations

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

@[instance_reducible]

instance CohnGordonEtAl2019.Sedivy.instFintypeReferent : Fintype Referent

Equations

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

@[instance_reducible]

instance CohnGordonEtAl2019.Sedivy.instReprReferent : Repr Referent

Equations

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

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

Equations

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

instance CohnGordonEtAl2019.Sedivy.instNonemptyReferent : Nonempty Referent

@[instance_reducible]

instance CohnGordonEtAl2019.Sedivy.instMeasurableSpaceReferent : MeasurableSpace Referent

Equations

• CohnGordonEtAl2019.Sedivy.instMeasurableSpaceReferent = ⊤

instance CohnGordonEtAl2019.Sedivy.instDiscreteMeasurableSpaceReferent : DiscreteMeasurableSpace Referent

def CohnGordonEtAl2019.Sedivy.game : ReferenceGame Word Referent

Sedivy's display is a reference game with six utterances and word-conjunctive semantics.

Equations

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

theorem CohnGordonEtAl2019.Sedivy.s1_tall_values : ((game.s1 0 []) Referent.tallCup).real {Word.tall} = 1 / 2 ∧ ((game.s1 0 []) Referent.tallPitcher).real {Word.tall} = 1 / 3 ∧ ((game.s1 0 []) Referent.shortCup).real {Word.tall} = 0 ∧ ((game.s1 0 []) Referent.key).real {Word.tall} = 0

The speaker uses tall as a first word half the time for the tall cup, a third of the time for the tall pitcher, and never for the others.

theorem CohnGordonEtAl2019.Sedivy.listener_prefers_tall_cup : ((game.l1 0 []) Word.tall).real {Referent.tallPitcher} < ((game.l1 0 []) Word.tall).real {Referent.tallCup}

Upon hearing tall, the incremental listener favours the tall cup over the tall pitcher, the anticipatory contrastive inference of §3.2.

theorem CohnGordonEtAl2019.Sedivy.listener_tall_values : ((game.l1 0 []) Word.tall).real {Referent.tallCup} = 3 / 5 ∧ ((game.l1 0 []) Word.tall).real {Referent.tallPitcher} = 2 / 5

Exactly, the listener puts 3/5 on the tall cup and 2/5 on the pitcher, the paper's 0.6 and 0.4 (§3.2).

noncomputable def CohnGordonEtAl2019.Sedivy.afterTallPitcher : MeasureTheory.Measure Referent

The listener who has heard tall and then hears pitcher takes the posterior of the word-level speaker at context tall against the updated prior.

Equations

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

theorem CohnGordonEtAl2019.Sedivy.afterTallPitcher_eq_one : afterTallPitcher {Referent.tallPitcher} = 1

The implicature cancels, since after tall pitcher every referent but the pitcher is excluded. The tall cup's speaker never continues tall with pitcher, and the other two referents already had no posterior mass.