@cite{waldon-degen-2021} — Continuous-Incremental RSA (CI-RSA)

@cite{cohn-gordon-goodman-potts-2019} @cite{degen-etal-2020}

Waldon, B. & Degen, J. (2021). Modeling cross-linguistic production of referring expressions. Proceedings of the Society for Computation in Linguistics (SCiL) 4, 206–215.

The Model

CI-RSA synthesizes two RSA extensions:

1. Incremental RSA (@cite{cohn-gordon-goodman-potts-2019}): Word-by-word production via the chain rule S1(u|r) = ∏ₖ S1(wₖ | [w₁,...,wₖ₋₁], r)
2. Continuous semantics (@cite{degen-etal-2020}): Noisy adjective reliability L^C(r, i) = v^i if i true of r, else 1 - v^i

The incremental meaning function averages continuous semantics over grammatical completions of the current prefix:

X^C(c, i, r) = Σ_{u ⊒ c+i} ⟦u⟧^C(r) / |{u : u ⊒ c+i}|

The utterance set is scene-filtered: only utterances Boolean-true of at least one scene member are included (Figure 1).

Formalization

This builds on RSAConfig's sequential infrastructure (following @cite{cohn-gordon-goodman-potts-2019}), adding:

• Continuous (ℚ-valued) meaning instead of Boolean extension-counting
• rpow-based s1Score with α = 7
• Scene-parameterized configs for cross-condition comparisons

The three predictions are trajectory probability comparisons across different RSAConfig instances (language × scene).

Predictions

#	Prediction	Status
1	English color/size asymmetry: SS > CS	rsa_predict
2	Cross-linguistic: English SS > Spanish SS	rsa_predict
3	Spanish flip: CS > SS for redundant size	rsa_predict
4	Overall: English total > Spanish total	rsa_predict

Connections

• Noise theory: lexContinuousQ instantiates the unified noise channel from RSA.Core.Noise. See lexContinuous_as_noiseChannel.
• Incremental RSA: Extends @cite{cohn-gordon-goodman-potts-2019} with continuous semantics and cross-linguistic word order variation.

inductive WaldonDegen2021.Word : Type

Words available to the incremental speaker: two color adjectives, two size adjectives, a noun ("pin"), and an explicit stop token. The stop token models the speaker's choice to end the utterance; without it, postnominal word orders lack a way to represent the stopping decision after the noun (cf. English where "pin" naturally terminates utterances).

• blue : Word
• red : Word
• big : Word
• small : Word
• pin : Word
• stop : Word

@[implicit_reducible]

instance WaldonDegen2021.instDecidableEqWord : DecidableEq Word

Equations

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

@[implicit_reducible]

instance WaldonDegen2021.instFintypeWord : Fintype Word

Equations

• WaldonDegen2021.instFintypeWord = { elems := { val := ↑WaldonDegen2021.Word.enumList, nodup := WaldonDegen2021.Word.enumList_nodup }, complete := WaldonDegen2021.instFintypeWord._proof_1 }

@[implicit_reducible]

instance WaldonDegen2021.instReprWord : Repr Word

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• WaldonDegen2021.instReprWord.repr WaldonDegen2021.Word.blue prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "WaldonDegen2021.Word.blue")).group prec✝
• WaldonDegen2021.instReprWord.repr WaldonDegen2021.Word.red prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "WaldonDegen2021.Word.red")).group prec✝
• WaldonDegen2021.instReprWord.repr WaldonDegen2021.Word.big prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "WaldonDegen2021.Word.big")).group prec✝
• WaldonDegen2021.instReprWord.repr WaldonDegen2021.Word.pin prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "WaldonDegen2021.Word.pin")).group prec✝
• WaldonDegen2021.instReprWord.repr WaldonDegen2021.Word.stop prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "WaldonDegen2021.Word.stop")).group prec✝

inductive WaldonDegen2021.Referent : Type

Referents in the 2×2 reference game: big/small × blue/red.

• bigBlue : Referent
• bigRed : Referent
• smallBlue : Referent
• smallRed : Referent

@[implicit_reducible]

instance WaldonDegen2021.instDecidableEqReferent : DecidableEq Referent

Equations

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

@[implicit_reducible]

instance WaldonDegen2021.instFintypeReferent : Fintype Referent

Equations

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

@[implicit_reducible]

instance WaldonDegen2021.instReprReferent : Repr Referent

Equations

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

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

Equations

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

def WaldonDegen2021.wordApplies : Word → Referent → Bool

Whether a word is veridically true of a referent.

Equations

• WaldonDegen2021.wordApplies WaldonDegen2021.Word.blue WaldonDegen2021.Referent.bigBlue = true
• WaldonDegen2021.wordApplies WaldonDegen2021.Word.blue WaldonDegen2021.Referent.smallBlue = true
• WaldonDegen2021.wordApplies WaldonDegen2021.Word.red WaldonDegen2021.Referent.bigRed = true
• WaldonDegen2021.wordApplies WaldonDegen2021.Word.red WaldonDegen2021.Referent.smallRed = true
• WaldonDegen2021.wordApplies WaldonDegen2021.Word.big WaldonDegen2021.Referent.bigBlue = true
• WaldonDegen2021.wordApplies WaldonDegen2021.Word.big WaldonDegen2021.Referent.bigRed = true
• WaldonDegen2021.wordApplies WaldonDegen2021.Word.small WaldonDegen2021.Referent.smallBlue = true
• WaldonDegen2021.wordApplies WaldonDegen2021.Word.small WaldonDegen2021.Referent.smallRed = true
• WaldonDegen2021.wordApplies WaldonDegen2021.Word.pin x✝ = true
• WaldonDegen2021.wordApplies WaldonDegen2021.Word.stop x✝ = true
• WaldonDegen2021.wordApplies x✝¹ x✝ = false

def WaldonDegen2021.semanticValueQ : Word → ℚ

Semantic reliability values v^i. Color adjectives are more reliable than size adjectives: v^color = 19/20 (0.95), v^size = 4/5 (0.8).

Equations

• WaldonDegen2021.semanticValueQ WaldonDegen2021.Word.blue = 19 / 20
• WaldonDegen2021.semanticValueQ WaldonDegen2021.Word.red = 19 / 20
• WaldonDegen2021.semanticValueQ WaldonDegen2021.Word.big = 4 / 5
• WaldonDegen2021.semanticValueQ WaldonDegen2021.Word.small = 4 / 5
• WaldonDegen2021.semanticValueQ WaldonDegen2021.Word.pin = 1
• WaldonDegen2021.semanticValueQ WaldonDegen2021.Word.stop = 1

def WaldonDegen2021.lexContinuousQ (r : Referent) (w : Word) : ℚ

Continuous lexical interpretation L^C(r, i). Returns v^i if true, (1 - v^i) if false.

Equations

• WaldonDegen2021.lexContinuousQ r w = if WaldonDegen2021.wordApplies w r = true then WaldonDegen2021.semanticValueQ w else 1 - WaldonDegen2021.semanticValueQ w

def WaldonDegen2021.uttContinuousQ (r : Referent) (u : List Word) : ℚ

Continuous utterance meaning ⟦u⟧^C(r) = ∏_{w ∈ u} L^C(r, w).

Equations

• WaldonDegen2021.uttContinuousQ r u = List.foldl (fun (acc : ℚ) (w : WaldonDegen2021.Word) => acc * WaldonDegen2021.lexContinuousQ r w) 1 u

def WaldonDegen2021.uttBoolTrue (u : List Word) (r : Referent) : Bool

Boolean utterance truth: conjunction of word applicability.

Equations

• WaldonDegen2021.uttBoolTrue u r = u.all fun (w : WaldonDegen2021.Word) => WaldonDegen2021.wordApplies w r

def WaldonDegen2021.allUttsEng : List (List Word)

All grammatical English (prenominal) utterances, each terminated by .stop. In English the noun always comes last before stop, so "pin" naturally precedes the stopping decision.

Equations

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

def WaldonDegen2021.allUttsSpn : List (List Word)

All grammatical Spanish (postnominal) utterances, each terminated by .stop. The stop token is critical here: after [pin, blue], the S1 chooses between .stop (2-word non-redundant) and .small (continuing to the 3-word redundant utterance). Without .stop, the model forces continuation whenever valid extensions exist.

Equations

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

def WaldonDegen2021.sceneFilter (utts : List (List Word)) (scene : Referent → Bool) : List (List Word)

Scene-filtered utterances: only those Boolean-true of at least one scene member (Figure 1). This yields 7 utterances per scene.

Equations

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

def WaldonDegen2021.wordCostQ : Word → ℚ

Per-word production cost (Section 4): each adjective incurs cost 0.1. Pin and stop have zero cost (noun and utterance boundary).

Equations

• WaldonDegen2021.wordCostQ WaldonDegen2021.Word.pin = 0
• WaldonDegen2021.wordCostQ WaldonDegen2021.Word.stop = 0
• WaldonDegen2021.wordCostQ x✝ = 1 / 10

def WaldonDegen2021.continuousMeaningQ (utts : List (List Word)) (scene : Referent → Bool) (pfx : List Word) (r : Referent) : ℚ

Incremental continuous meaning: average continuous semantics over all grammatical completions of prefix.

X^C(c, i, r) = Σ_{u ⊒ c+i} ⟦u⟧^C(r) / |{u : u ⊒ c+i}|

Equations

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

noncomputable def WaldonDegen2021.continuousMeaning (utts : List (List Word)) (scene : Referent → Bool) (pfx : List Word) (r : Referent) : ℝ

Real-valued continuous meaning (for RSAConfig).

Equations

• WaldonDegen2021.continuousMeaning utts scene pfx r = ↑(WaldonDegen2021.continuousMeaningQ utts scene pfx r)

def WaldonDegen2021.ssScene : Referent → Bool

Size-sufficient scene: {big_blue, big_red, small_blue}. Target small_blue is uniquely identified by size alone.

Equations

• WaldonDegen2021.ssScene WaldonDegen2021.Referent.bigBlue = true
• WaldonDegen2021.ssScene WaldonDegen2021.Referent.bigRed = true
• WaldonDegen2021.ssScene WaldonDegen2021.Referent.smallBlue = true
• WaldonDegen2021.ssScene x✝ = false

def WaldonDegen2021.csScene : Referent → Bool

Color-sufficient scene: {small_red, big_red, small_blue}. Target small_blue is uniquely identified by color alone.

Equations

• WaldonDegen2021.csScene WaldonDegen2021.Referent.smallRed = true
• WaldonDegen2021.csScene WaldonDegen2021.Referent.bigRed = true
• WaldonDegen2021.csScene WaldonDegen2021.Referent.smallBlue = true
• WaldonDegen2021.csScene x✝ = false

noncomputable def WaldonDegen2021.mkCIRSA (utts : List (List Word)) (scene : Referent → Bool) : RSA.RSAConfig Word Referent

CI-RSA configuration parameterized by utterance set and scene.

• L0 uses extension-based continuous meaning, returning 0 for referents outside the scene
• S1 uses rpow-based scoring with α = 7 and per-word cost C(i)
• S1(i|c,r) ∝ L0(r|c,i)^α · exp(−α · C(i)) (Section 4)

Note: v^color = 0.95 here, matching the paper's fitted values. This differs from the @cite{degen-etal-2020} value of v^color = 0.99 used in RSA.Core.Noise, because the two papers fit different experimental datasets.

Equations

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

noncomputable def WaldonDegen2021.englishSS : RSA.RSAConfig Word Referent

English (prenominal) CI-RSA in size-sufficient scene.

Equations

• WaldonDegen2021.englishSS = WaldonDegen2021.mkCIRSA WaldonDegen2021.allUttsEng WaldonDegen2021.ssScene

noncomputable def WaldonDegen2021.englishCS : RSA.RSAConfig Word Referent

English (prenominal) CI-RSA in color-sufficient scene.

Equations

• WaldonDegen2021.englishCS = WaldonDegen2021.mkCIRSA WaldonDegen2021.allUttsEng WaldonDegen2021.csScene

noncomputable def WaldonDegen2021.spanishSS : RSA.RSAConfig Word Referent

Spanish (postnominal) CI-RSA in size-sufficient scene.

Equations

• WaldonDegen2021.spanishSS = WaldonDegen2021.mkCIRSA WaldonDegen2021.allUttsSpn WaldonDegen2021.ssScene

noncomputable def WaldonDegen2021.spanishCS : RSA.RSAConfig Word Referent

Spanish (postnominal) CI-RSA in color-sufficient scene.

Equations

• WaldonDegen2021.spanishCS = WaldonDegen2021.mkCIRSA WaldonDegen2021.allUttsSpn WaldonDegen2021.csScene

theorem WaldonDegen2021.ss_eng_has_7_utts : (sceneFilter allUttsEng ssScene).length = 7

theorem WaldonDegen2021.cs_eng_has_7_utts : (sceneFilter allUttsEng csScene).length = 7

theorem WaldonDegen2021.ss_spn_has_7_utts : (sceneFilter allUttsSpn ssScene).length = 7

theorem WaldonDegen2021.cs_spn_has_7_utts : (sceneFilter allUttsSpn csScene).length = 7

theorem WaldonDegen2021.prediction1_english_asymmetry : englishSS.trajectoryProb () Referent.smallBlue [Word.small, Word.blue, Word.pin, Word.stop] > englishCS.trajectoryProb () Referent.smallBlue [Word.small, Word.blue, Word.pin, Word.stop]

theorem WaldonDegen2021.prediction2_cross_linguistic : englishSS.trajectoryProb () Referent.smallBlue [Word.small, Word.blue, Word.pin, Word.stop] > spanishSS.trajectoryProb () Referent.smallBlue [Word.pin, Word.blue, Word.small, Word.stop]

theorem WaldonDegen2021.prediction3_spanish_flip : spanishCS.trajectoryProb () Referent.smallBlue [Word.pin, Word.blue, Word.small, Word.stop] > spanishSS.trajectoryProb () Referent.smallBlue [Word.pin, Word.blue, Word.small, Word.stop]

theorem WaldonDegen2021.color_more_reliable_than_size : semanticValueQ Word.blue > semanticValueQ Word.big ∧ semanticValueQ Word.red > semanticValueQ Word.small

Color adjectives have higher reliability than size adjectives. This asymmetry drives the redundant modification predictions.

theorem WaldonDegen2021.semantic_values_positive (w : Word) : semanticValueQ w > 0

All semantic values are positive (required for valid probability).

theorem WaldonDegen2021.lexContinuous_as_noiseChannel (r : Referent) (w : Word) : lexContinuousQ r w = RSA.Noise.noiseChannel (semanticValueQ w) (1 - semanticValueQ w) (if wordApplies w r = true then 1 else 0)

lexContinuousQ is an instance of the unified noise channel from RSA.Core.Noise. The continuous lexical semantics L^C(r, i) is exactly the noise channel with onMatch = v^i, onMismatch = 1 - v^i, b = 1 if item i is true of referent r, 0 otherwise.

This connects @cite{waldon-degen-2021} to the @cite{degen-etal-2020} parameterization where mismatch = 1 - match.

def WaldonDegen2021.noisyLex : RSA.NoisyLex Word Referent

lexContinuousQ packaged as a RSA.NoisyLex bundle. The bundle is the substrate this study and @cite{schlotterbeck-wang-2023} share — each provides its own lex and reliability parameters; the PoE prefix-product machinery (RSA.prefixMeaning and friends) is reused.

Equations

• WaldonDegen2021.noisyLex = { lex := fun (w : WaldonDegen2021.Word) (r : WaldonDegen2021.Referent) => WaldonDegen2021.lexContinuousQ r w, lex_nonneg := WaldonDegen2021.noisyLex._proof_1 }

theorem WaldonDegen2021.uttContinuousQ_eq_prefixMeaning (r : Referent) (u : List Word) : uttContinuousQ r u = noisyLex.prefixMeaning u r

uttContinuousQ is the NoisyLex.prefixMeaning of the bundled lex (modulo argument order). Substrate-bridge analogue of S&W's prefix_meaning_product for the W&D extension-averaging context.

Uses the polymorphic RSA.prefixMeaning_eq_foldl_mul from Sequential.lean — no need for a study-local foldl helper.

theorem WaldonDegen2021.prediction4_overall_redundancy : englishSS.trajectoryProb () Referent.smallBlue [Word.small, Word.blue, Word.pin, Word.stop] + englishCS.trajectoryProb () Referent.smallBlue [Word.small, Word.blue, Word.pin, Word.stop] > spanishSS.trajectoryProb () Referent.smallBlue [Word.pin, Word.blue, Word.small, Word.stop] + spanishCS.trajectoryProb () Referent.smallBlue [Word.pin, Word.blue, Word.small, Word.stop]