[SW23] — incremental RSA for adjective ordering

[CGGP19] [DHG+20] [WD21]

Schlotterbeck, F. & Wang, H. (2023). An incremental RSA model for adjective ordering preferences in referential visual context. SCiL 6, 121–132.

Scope. This file formalizes the symmetric-PoE sanity-check slice of the paper, not its main asymmetric model: the order-independence of the incremental listener under symmetric per-class semantics, plus discrimination-driven ordering preferences at the speaker level as chain-rule trajectory products (per-step normalized; the paper's S1^inc normalizes once globally, and the two agree at the literal layer). Not formalized: asymmetric per-class semantics, the P_Lang grammaticality filter, and the size-first utterance-prior bias. The paper's α is the utterance-level softmax temperature; its β (word-level) is 1 in all reported simulations, matching the exponent-free chain here.

Main results

• meaning_perm: the PoE prefix meaning is order-independent, for every lexicon — the paper's listener-level sanity check.
• size_first_when_size_discriminates / color_first_when_color_reliable: the trajectory preference tracks discriminatory power (Scene A) and flips to the more reliable dimension under equal discrimination (Scene B); ordering_preference_flips conjoins them.
• big_more_informative_A / blue_more_informative_B: the first-word preferences driving the flip.
• both_orderings_identify_target_A/_B: after both adjectives the target carries the highest meaning among scene members.

Implementation notes

The chain is exact ℚ≥0: lex is the Bernoulli-channel form of [DHG+20]'s continuous semantics (reliability if the word truly applies, the complementary noise floor otherwise), prefix meanings are List products, l0Score/s1Score normalize via PMF.normalizeScores, and the PMF speaker is PMF.ofScores. Trajectories are Fin-indexed products of speaker values, so ordering predictions close by PMF.prod_ofScores_lt with one kernel certificate each.

inductive SchlotterbeckWang2023.Referent : Type

Referents in the reference game.

• bigBlue : Referent
• bigGreen : Referent
• smallBlue : Referent
• smallGreen : Referent
• smallRed : Referent

@[implicit_reducible]

instance SchlotterbeckWang2023.instDecidableEqReferent : DecidableEq Referent

Equations

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

@[implicit_reducible]

instance SchlotterbeckWang2023.instFintypeReferent : Fintype Referent

Equations

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

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

Equations

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

@[implicit_reducible]

instance SchlotterbeckWang2023.instReprReferent : Repr Referent

Equations

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

instance SchlotterbeckWang2023.instNonemptyReferent : Nonempty Referent

inductive SchlotterbeckWang2023.Word : Type

Words available to the speaker: size adjectives, color adjectives, noun.

• big : Word
• small : Word
• blue : Word
• green : Word
• red : Word
• sticker : Word

@[implicit_reducible]

instance SchlotterbeckWang2023.instDecidableEqWord : DecidableEq Word

Equations

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

@[implicit_reducible]

instance SchlotterbeckWang2023.instFintypeWord : Fintype Word

Equations

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

@[implicit_reducible]

instance SchlotterbeckWang2023.instReprWord : Repr Word

Equations

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

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

Equations

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

instance SchlotterbeckWang2023.instNonemptyWord : Nonempty Word

def SchlotterbeckWang2023.wordApplies : Word → Referent → Bool

Whether a word is veridically true of a referent.

Equations

• SchlotterbeckWang2023.wordApplies SchlotterbeckWang2023.Word.big SchlotterbeckWang2023.Referent.bigBlue = true
• SchlotterbeckWang2023.wordApplies SchlotterbeckWang2023.Word.big SchlotterbeckWang2023.Referent.bigGreen = true
• SchlotterbeckWang2023.wordApplies SchlotterbeckWang2023.Word.small SchlotterbeckWang2023.Referent.smallBlue = true
• SchlotterbeckWang2023.wordApplies SchlotterbeckWang2023.Word.small SchlotterbeckWang2023.Referent.smallGreen = true
• SchlotterbeckWang2023.wordApplies SchlotterbeckWang2023.Word.small SchlotterbeckWang2023.Referent.smallRed = true
• SchlotterbeckWang2023.wordApplies SchlotterbeckWang2023.Word.blue SchlotterbeckWang2023.Referent.bigBlue = true
• SchlotterbeckWang2023.wordApplies SchlotterbeckWang2023.Word.blue SchlotterbeckWang2023.Referent.smallBlue = true
• SchlotterbeckWang2023.wordApplies SchlotterbeckWang2023.Word.green SchlotterbeckWang2023.Referent.bigGreen = true
• SchlotterbeckWang2023.wordApplies SchlotterbeckWang2023.Word.green SchlotterbeckWang2023.Referent.smallGreen = true
• SchlotterbeckWang2023.wordApplies SchlotterbeckWang2023.Word.red SchlotterbeckWang2023.Referent.smallRed = true
• SchlotterbeckWang2023.wordApplies SchlotterbeckWang2023.Word.sticker x✝ = true
• SchlotterbeckWang2023.wordApplies x✝¹ x✝ = false

def SchlotterbeckWang2023.rel (sRel cRel : ℚ≥0) : Word → ℚ≥0

Per-class perceptual reliability: size words use sRel, color words use cRel, the noun applies universally.

Equations

• SchlotterbeckWang2023.rel sRel cRel SchlotterbeckWang2023.Word.big = sRel
• SchlotterbeckWang2023.rel sRel cRel SchlotterbeckWang2023.Word.small = sRel
• SchlotterbeckWang2023.rel sRel cRel SchlotterbeckWang2023.Word.blue = cRel
• SchlotterbeckWang2023.rel sRel cRel SchlotterbeckWang2023.Word.green = cRel
• SchlotterbeckWang2023.rel sRel cRel SchlotterbeckWang2023.Word.red = cRel
• SchlotterbeckWang2023.rel sRel cRel SchlotterbeckWang2023.Word.sticker = 1

def SchlotterbeckWang2023.lex (sRel cRel : ℚ≥0) (w : Word) (r : Referent) : ℚ≥0

Noisy word meaning: reliability if the word truly applies, the complementary noise floor otherwise — the Bernoulli-channel form of [DHG+20]'s continuous semantics.

Equations

• SchlotterbeckWang2023.lex sRel cRel w r = if SchlotterbeckWang2023.wordApplies w r = true then SchlotterbeckWang2023.rel sRel cRel w else 1 - SchlotterbeckWang2023.rel sRel cRel w

def SchlotterbeckWang2023.meaning (lex : Word → Referent → ℚ≥0) (us : List Word) (r : Referent) : ℚ≥0

PoE prefix meaning: the product of per-word noisy meanings.

Equations

• SchlotterbeckWang2023.meaning lex us r = (List.map (fun (x : SchlotterbeckWang2023.Word) => lex x r) us).prod

theorem SchlotterbeckWang2023.meaning_perm (lex : Word → Referent → ℚ≥0) {us vs : List Word} (h : us.Perm vs) (r : Referent) : meaning lex us r = meaning lex vs r

The listener-level sanity check: the PoE prefix meaning is order-independent, for every lexicon and reliability setting.

Scenes

def SchlotterbeckWang2023.sceneA : Referent → Bool

Scene A: size discriminates. Objects {big-blue, small-blue, small-green, small-red}, so "big" uniquely identifies the target.

Equations

• SchlotterbeckWang2023.sceneA SchlotterbeckWang2023.Referent.bigBlue = true
• SchlotterbeckWang2023.sceneA SchlotterbeckWang2023.Referent.smallBlue = true
• SchlotterbeckWang2023.sceneA SchlotterbeckWang2023.Referent.smallGreen = true
• SchlotterbeckWang2023.sceneA SchlotterbeckWang2023.Referent.smallRed = true
• SchlotterbeckWang2023.sceneA x✝ = false

def SchlotterbeckWang2023.sceneB : Referent → Bool

Scene B: equal discrimination. Objects {big-blue, big-green, small-blue, small-green}; "big" and "blue" each narrow to two.

Equations

• SchlotterbeckWang2023.sceneB SchlotterbeckWang2023.Referent.bigBlue = true
• SchlotterbeckWang2023.sceneB SchlotterbeckWang2023.Referent.bigGreen = true
• SchlotterbeckWang2023.sceneB SchlotterbeckWang2023.Referent.smallBlue = true
• SchlotterbeckWang2023.sceneB SchlotterbeckWang2023.Referent.smallGreen = true
• SchlotterbeckWang2023.sceneB x✝ = false

def SchlotterbeckWang2023.target : Referent

The target referent in both scenes.

Equations

• SchlotterbeckWang2023.target = SchlotterbeckWang2023.Referent.bigBlue

def SchlotterbeckWang2023.lexA : Word → Referent → ℚ≥0

Scene A lexicon: size more reliable (99/100 vs 95/100).

Equations

• SchlotterbeckWang2023.lexA = SchlotterbeckWang2023.lex (99 / 100) (95 / 100)

def SchlotterbeckWang2023.lexB : Word → Referent → ℚ≥0

Scene B lexicon: color more reliable (95/100 vs 80/100).

Equations

• SchlotterbeckWang2023.lexB = SchlotterbeckWang2023.lex (80 / 100) (95 / 100)

The incremental chain

def SchlotterbeckWang2023.l0Score (lex : Word → Referent → ℚ≥0) (scene : Referent → Bool) (ctx : List Word) (u : Word) : Referent → ℚ≥0

Literal listener over scene referents at each prefix extension.

Equations

• SchlotterbeckWang2023.l0Score lex scene ctx u = PMF.normalizeScores fun (r : SchlotterbeckWang2023.Referent) => if scene r = true then SchlotterbeckWang2023.meaning lex (ctx ++ [u]) r else 0

def SchlotterbeckWang2023.s1Score (lex : Word → Referent → ℚ≥0) (scene : Referent → Bool) (ctx : List Word) (r : Referent) : Word → ℚ≥0

Word-level speaker (β = 1, no cost): renormalized literal posteriors.

Equations

• SchlotterbeckWang2023.s1Score lex scene ctx r = PMF.normalizeScores fun (u : SchlotterbeckWang2023.Word) => SchlotterbeckWang2023.l0Score lex scene ctx u r

noncomputable def SchlotterbeckWang2023.s1 (lex : Word → Referent → ℚ≥0) (scene : Referent → Bool) (ctx : List Word) (r : Referent) : PMF Word

Word-by-word speaker at context ctx.

Equations

• SchlotterbeckWang2023.s1 lex scene ctx r = PMF.ofScores PMF.Fallback.uniform (SchlotterbeckWang2023.s1Score lex scene ctx r)

noncomputable def SchlotterbeckWang2023.s1Traj (lex : Word → Referent → ℚ≥0) (scene : Referent → Bool) (r : Referent) (us : List Word) : ENNReal

Trajectory probability of an utterance: the chain-rule product of per-step speaker values along its prefixes.

Equations

• SchlotterbeckWang2023.s1Traj lex scene r us = ∏ i : Fin us.length, (SchlotterbeckWang2023.s1 lex scene (List.take (↑i) us) r) (us.get i)

def SchlotterbeckWang2023.s1TrajScore (lex : Word → Referent → ℚ≥0) (scene : Referent → Bool) (r : Referent) (us : List Word) : ℚ≥0

ℚ≥0 shadow of s1Traj.

Equations

• SchlotterbeckWang2023.s1TrajScore lex scene r us = ∏ i : Fin us.length, PMF.scoresWith PMF.Fallback.uniform (SchlotterbeckWang2023.s1Score lex scene (List.take (↑i) us) r) (us.get i)

theorem SchlotterbeckWang2023.s1Traj_lt {lex₁ lex₂ : Word → Referent → ℚ≥0} {sc₁ sc₂ : Referent → Bool} {r₁ r₂ : Referent} {us vs : List Word} (h : s1TrajScore lex₁ sc₁ r₁ us < s1TrajScore lex₂ sc₂ r₂ vs) : s1Traj lex₁ sc₁ r₁ us < s1Traj lex₂ sc₂ r₂ vs

Predictions

def SchlotterbeckWang2023.sizeFirst : List Word

Size-first and color-first orderings for the big-blue target.

Equations

• SchlotterbeckWang2023.sizeFirst = [SchlotterbeckWang2023.Word.big, SchlotterbeckWang2023.Word.blue, SchlotterbeckWang2023.Word.sticker]

def SchlotterbeckWang2023.colorFirst : List Word

See sizeFirst.

Equations

• SchlotterbeckWang2023.colorFirst = [SchlotterbeckWang2023.Word.blue, SchlotterbeckWang2023.Word.big, SchlotterbeckWang2023.Word.sticker]

theorem SchlotterbeckWang2023.size_first_when_size_discriminates : s1Traj lexA sceneA target colorFirst < s1Traj lexA sceneA target sizeFirst

When size has the higher discriminatory power (Scene A), the incremental speaker prefers the size-first ordering.

theorem SchlotterbeckWang2023.color_first_when_color_reliable : s1Traj lexB sceneB target sizeFirst < s1Traj lexB sceneB target colorFirst

Under equal discrimination with color more reliable (Scene B), the preference flips to color-first.

theorem SchlotterbeckWang2023.ordering_preference_flips : s1Traj lexA sceneA target colorFirst < s1Traj lexA sceneA target sizeFirst ∧ s1Traj lexB sceneB target sizeFirst < s1Traj lexB sceneB target colorFirst

The ordering preference tracks the scene's discriminatory structure, not a fixed ordering rule.

theorem SchlotterbeckWang2023.big_more_informative_A : (s1 lexA sceneA [] target) Word.blue < (s1 lexA sceneA [] target) Word.big

In Scene A, "big" is the more informative first word for the target.

theorem SchlotterbeckWang2023.blue_more_informative_B : (s1 lexB sceneB [] target) Word.big < (s1 lexB sceneB [] target) Word.blue

In Scene B, "blue" is the more informative first word.

theorem SchlotterbeckWang2023.both_orderings_identify_target_A (r : Referent) (hr : sceneA r = true) (hne : r ≠ target) : meaning lexA [Word.big, Word.blue] r < meaning lexA [Word.big, Word.blue] target

After both adjectives, the target carries the highest meaning among Scene A members.

theorem SchlotterbeckWang2023.both_orderings_identify_target_B (r : Referent) (hr : sceneB r = true) (hne : r ≠ target) : meaning lexB [Word.big, Word.blue] r < meaning lexB [Word.big, Word.blue] target

After both adjectives, the target carries the highest meaning among Scene B members.

theorem SchlotterbeckWang2023.lex_as_noiseChannel {sRel cRel : ℚ≥0} (hs : sRel ≤ 1) (hc : cRel ≤ 1) (w : Word) (r : Referent) : ↑(lex sRel cRel w r) = RSA.Noise.noiseChannel (↑(rel sRel cRel w)) (1 - ↑(rel sRel cRel w)) (if wordApplies w r = true then 1 else 0)

lex is the unified noise channel of RSA.Noise at onMatch = reliability, onMismatch = its complement — the [DHG+20] parameterization.