Incremental RSA: prefix meanings

Incremental RSA ([CGGP19]) runs the pipeline word by word, so the literal listener needs the meaning of an utterance prefix. With the graded lexical semantics of [DHG+20] each word contributes a value in a commutative monoid and the prefix meaning is their product, treating words as independent constraints — the composition of [WD21] (ℚ-valued) and [SW23] (ℚ≥0-valued), an instance of the probabilistic turn surveyed in [erk-2022].

Main definitions

• RSA.prodMeaning lex us w: the product over the tokens us of the per-word values lex u w.

Main results

• RSA.prodMeaning_perm: the prefix meaning is independent of token order — the listener-level sanity check of [SW23].
• RSA.prodMeaning_nonneg: nonnegativity from a nonnegative lexicon.

References

• R. Cohn-Gordon, N. D. Goodman, C. Potts, An incremental iterated response model of pragmatics
• J. Degen et al., When redundancy is useful: a Bayesian approach to "overinformative" referring expressions
• B. Waldon, J. Degen, Modeling cross-linguistic production of referring expressions
• F. Schlotterbeck, H. Wang, An incremental RSA model for adjective ordering preferences in referential visual context

def RSA.prodMeaning {U : Type u_1} {W : Type u_2} {R : Type u_3} [CommMonoid R] (lex : U → W → R) (us : List U) (w : W) : R

The prefix meaning: the per-word lexicon composed multiplicatively over a token list, prodMeaning lex us w = (us.map (lex · w)).prod.

Equations

• RSA.prodMeaning lex us w = (List.map (fun (x : U) => lex x w) us).prod

@[simp]

theorem RSA.prodMeaning_nil {U : Type u_1} {W : Type u_2} {R : Type u_3} [CommMonoid R] (lex : U → W → R) (w : W) : prodMeaning lex [] w = 1

@[simp]

theorem RSA.prodMeaning_cons {U : Type u_1} {W : Type u_2} {R : Type u_3} [CommMonoid R] (lex : U → W → R) (u : U) (us : List U) (w : W) : prodMeaning lex (u :: us) w = lex u w * prodMeaning lex us w

theorem RSA.prodMeaning_perm {U : Type u_1} {W : Type u_2} {R : Type u_3} [CommMonoid R] {lex : U → W → R} {us us' : List U} (h : us.Perm us') (w : W) : prodMeaning lex us w = prodMeaning lex us' w

Any permutation of the token list yields the same meaning.

theorem RSA.prodMeaning_nonneg {U : Type u_1} {W : Type u_2} {R : Type u_3} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulMono R] {lex : U → W → R} (h : ∀ (u : U) (w : W), 0 ≤ lex u w) (us : List U) (w : W) : 0 ≤ prodMeaning lex us w