Waldon and Degen (2021): Modeling Cross-Linguistic Production of Referring Expressions

Waldon and Degen's continuous-incremental rational speech act model of redundant modification, which joins two earlier models. From Cohn-Gordon, Goodman and Potts it takes word-by-word production: an incomplete string means the average of the complete utterances that continue it, the speaker chooses each word against a listener who hears the string so far, and the probability of an utterance is the product of its word choices. From Degen and colleagues it takes the continuous semantics, on which an adjective of semantic value v holds to degree v of the pins it is true of and to degree 1 − v of the others. The incremental model with Boolean meanings is the case of both values one.

English puts both adjectives before the noun, and the paper's postnominal Spanish puts both after it, colour first. The Spanish alternatives are then the mirror image of the English ones, with size and colour exchanged, so the Spanish speaker in a scene is the English speaker in the counterpart of the scene with the two semantic values exchanged.

Main statements

• spanish_cs_production_eq_english_ss, spanish_ss_production_eq_english_cs: for the small blue pin, pin blue small in one scene of Spanish is as likely as small blue pin in the other scene of English with the semantic values exchanged. With equal values, and so with Boolean meanings, redundant size in Spanish is as likely as redundant colour in English, and redundant colour in Spanish as redundant size in English.
• english_step_eq_sigmoid: after small, the English speaker adds the redundant blue with a probability that is a logistic function of the log of the gain of the redundant adjective, less its cost.
• spanish_size_step_lt_english_color_step_iff: the Spanish speaker adds the redundant size after pin blue less readily than the English speaker adds the redundant colour after small exactly when size is noisier than colour.
• meaning_perm: the meaning of an utterance does not depend on the order of its words, so a speaker who chooses among whole utterances cannot tell the two languages apart.

Implementation notes

• The word-level speaker step is the speaker of Degen and colleagues at the string meaning, so the redundancy step is their comparison of the redundant with the sufficient expression.
• A scene lists three pins in the order of the paper's first figure, with the target last.
• The costs are any that give a word and its counterpart the same cost. The paper charges each adjective 0.1 and the noun and the stop token nothing.

TODO

• The paper prints the utility of the incremental speaker without the logarithm. The transition probabilities of its third figure are those of the speaker with the logarithm, which is the one formalized.
• The utterance probabilities at the simulated values, the split and conjunctive Spanish idiolects, and the comparison over parameter values are not encoded.

References

• [WD21]
• [CGGP19]
• [DHG+20]
• [FG12]

Words and their meanings

inductive WaldonDegen2021.Word : Type

The words of the reference game, with a stop token that closes an utterance.

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

@[instance_reducible]

instance WaldonDegen2021.instDecidableEqWord : DecidableEq Word

Equations

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

@[instance_reducible]

instance WaldonDegen2021.instFintypeWord : Fintype Word

Equations

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

@[instance_reducible]

instance WaldonDegen2021.instMeasurableSpaceWord : MeasurableSpace Word

Equations

• WaldonDegen2021.instMeasurableSpaceWord = ⊤

instance WaldonDegen2021.instDiscreteMeasurableSpaceWord : DiscreteMeasurableSpace Word

def WaldonDegen2021.Word.Holds : Word → DegenEtAl2020.Size × DegenEtAl2020.Color → Prop

A word is true of a pin of a given size and colour. The noun and the stop token are true of every pin.

Equations

• WaldonDegen2021.Word.big.Holds x✝ = (x✝.1 = DegenEtAl2020.Size.big)
• WaldonDegen2021.Word.small.Holds x✝ = (x✝.1 = DegenEtAl2020.Size.small)
• WaldonDegen2021.Word.blue.Holds x✝ = (x✝.2 = DegenEtAl2020.Color.blue)
• WaldonDegen2021.Word.red.Holds x✝ = (x✝.2 = DegenEtAl2020.Color.red)
• WaldonDegen2021.Word.pin.Holds x✝ = True
• WaldonDegen2021.Word.stop.Holds x✝ = True

@[instance_reducible]

instance WaldonDegen2021.instDecidableHolds (w : Word) (r : DegenEtAl2020.Size × DegenEtAl2020.Color) : Decidable (w.Holds r)

Equations

• WaldonDegen2021.instDecidableHolds WaldonDegen2021.Word.big x✝ = WaldonDegen2021.instDecidableHolds._aux_1 x✝
• WaldonDegen2021.instDecidableHolds WaldonDegen2021.Word.small x✝ = WaldonDegen2021.instDecidableHolds._aux_3 x✝
• WaldonDegen2021.instDecidableHolds WaldonDegen2021.Word.blue x✝ = WaldonDegen2021.instDecidableHolds._aux_5 x✝
• WaldonDegen2021.instDecidableHolds WaldonDegen2021.Word.red x✝ = WaldonDegen2021.instDecidableHolds._aux_7 x✝
• WaldonDegen2021.instDecidableHolds WaldonDegen2021.Word.pin x✝ = { decide := true, reflects_decide := ⋯ }
• WaldonDegen2021.instDecidableHolds WaldonDegen2021.Word.stop x✝ = { decide := true, reflects_decide := ⋯ }

def WaldonDegen2021.value (vs vc : ℝ) : Word → ℝ

The semantic value of a word is vs for a size adjective, vc for a colour adjective, and one for the noun and the stop token.

Equations

• WaldonDegen2021.value vs vc WaldonDegen2021.Word.big = vs
• WaldonDegen2021.value vs vc WaldonDegen2021.Word.small = vs
• WaldonDegen2021.value vs vc WaldonDegen2021.Word.blue = vc
• WaldonDegen2021.value vs vc WaldonDegen2021.Word.red = vc
• WaldonDegen2021.value vs vc WaldonDegen2021.Word.pin = 1
• WaldonDegen2021.value vs vc WaldonDegen2021.Word.stop = 1

def WaldonDegen2021.lexicon (vs vc : ℝ) (w : Word) (r : DegenEtAl2020.Size × DegenEtAl2020.Color) : ℝ

In the continuous lexicon a word holds of a pin it is true of to the degree of its semantic value, and of any other pin to the complementary degree.

Equations

• WaldonDegen2021.lexicon vs vc w r = DegenEtAl2020.noisy (WaldonDegen2021.value vs vc w) (w.Holds r)

Languages and scenes

def WaldonDegen2021.english : List (List Word)

English puts size, then colour, before the noun.

Equations

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

def WaldonDegen2021.spanish : List (List Word)

Postnominal Spanish puts colour, then size, after the noun.

Equations

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

@[reducible, inline]

abbrev WaldonDegen2021.Scene : Type

A scene shows three pins, of which the third is the target.

Equations

• WaldonDegen2021.Scene = (Fin 3 → DegenEtAl2020.Size × DegenEtAl2020.Color)

@[reducible, inline]

abbrev WaldonDegen2021.target : Fin 3

The target of every prediction is the small blue pin, the third of each scene.

Equations

• WaldonDegen2021.target = 2

def WaldonDegen2021.ss : Scene

In the size-sufficient scene the target is the only small pin.

Equations

• WaldonDegen2021.ss 0 = (DegenEtAl2020.Size.big, DegenEtAl2020.Color.blue)
• WaldonDegen2021.ss 1 = (DegenEtAl2020.Size.big, DegenEtAl2020.Color.red)
• WaldonDegen2021.ss 2 = (DegenEtAl2020.Size.small, DegenEtAl2020.Color.blue)

def WaldonDegen2021.cs : Scene

In the colour-sufficient scene the target is the only blue pin.

Equations

• WaldonDegen2021.cs 0 = (DegenEtAl2020.Size.small, DegenEtAl2020.Color.red)
• WaldonDegen2021.cs 1 = (DegenEtAl2020.Size.big, DegenEtAl2020.Color.red)
• WaldonDegen2021.cs 2 = (DegenEtAl2020.Size.small, DegenEtAl2020.Color.blue)

def WaldonDegen2021.alternatives (L : List (List Word)) (s : Scene) : List (List Word)

The alternatives of a language in a scene are its utterances true of one of the pins.

Equations

• WaldonDegen2021.alternatives L s = List.filter (fun (u : List WaldonDegen2021.Word) => decide (∃ (i : Fin 3), ∀ w ∈ u, w.Holds (s i))) L

def WaldonDegen2021.meaning (vs vc : ℝ) (s : Scene) (u : List Word) (i : Fin 3) : ℝ

The continuous meaning of an utterance at a pin of the scene is the product of the degrees to which its words hold of the pin.

Equations

• WaldonDegen2021.meaning vs vc s u i = RSA.prodMeaning (WaldonDegen2021.lexicon vs vc) u (s i)

theorem WaldonDegen2021.meaning_nonneg {vs vc : ℝ} (hs0 : 0 ≤ vs) (hs1 : vs ≤ 1) (hc0 : 0 ≤ vc) (hc1 : vc ≤ 1) (s : Scene) (u : List Word) (i : Fin 3) : 0 ≤ meaning vs vc s u i

theorem WaldonDegen2021.meaning_perm {vs vc : ℝ} (s : Scene) {u u' : List Word} (h : u.Perm u') : meaning vs vc s u = meaning vs vc s u'

The meaning of an utterance does not depend on the order of its words.

theorem WaldonDegen2021.meaning_one_one (s : Scene) (u : List Word) (i : Fin 3) : meaning 1 1 s u i = if ∀ w ∈ u, w.Holds (s i) then 1 else 0

With both semantic values one the continuous meaning is truth, so the incremental model with Boolean meanings is the continuous one at these values.

The incremental speaker

noncomputable def WaldonDegen2021.step (α : ℝ) (cost : Word → ℝ) (vs vc : ℝ) (L : List (List Word)) (s : Scene) (ctx : List Word) : ProbabilityTheory.Kernel (Fin 3) Word

At a context the incremental speaker is the speaker of Degen and colleagues against a listener who interprets the context extended by the next word as a string.

Equations

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

noncomputable def WaldonDegen2021.production (α : ℝ) (cost : Word → ℝ) (vs vc : ℝ) (L : List (List Word)) (s : Scene) (u : List Word) : ℝ

The probability of an utterance for the target is the product of its word choices.

Equations

• WaldonDegen2021.production α cost vs vc L s u = RSA.chain (WaldonDegen2021.step α cost vs vc L s) WaldonDegen2021.target [] u

Spanish as the mirror image of English

def WaldonDegen2021.mirror : Word → Word

The counterpart of a word exchanges size with colour, and the noun, which closes the adjectives of an English utterance, with the stop token, which closes those of a Spanish one.

Equations

• WaldonDegen2021.mirror WaldonDegen2021.Word.small = WaldonDegen2021.Word.blue
• WaldonDegen2021.mirror WaldonDegen2021.Word.blue = WaldonDegen2021.Word.small
• WaldonDegen2021.mirror WaldonDegen2021.Word.big = WaldonDegen2021.Word.red
• WaldonDegen2021.mirror WaldonDegen2021.Word.red = WaldonDegen2021.Word.big
• WaldonDegen2021.mirror WaldonDegen2021.Word.pin = WaldonDegen2021.Word.stop
• WaldonDegen2021.mirror WaldonDegen2021.Word.stop = WaldonDegen2021.Word.pin

theorem WaldonDegen2021.mirror_mirror (w : Word) : mirror (mirror w) = w

def WaldonDegen2021.swap : DegenEtAl2020.Size × DegenEtAl2020.Color → DegenEtAl2020.Size × DegenEtAl2020.Color

The counterpart of a pin exchanges its size with its colour, small with blue and big with red.

Equations

• WaldonDegen2021.swap (DegenEtAl2020.Size.small, DegenEtAl2020.Color.blue) = (DegenEtAl2020.Size.small, DegenEtAl2020.Color.blue)
• WaldonDegen2021.swap (DegenEtAl2020.Size.big, DegenEtAl2020.Color.blue) = (DegenEtAl2020.Size.small, DegenEtAl2020.Color.red)
• WaldonDegen2021.swap (DegenEtAl2020.Size.small, DegenEtAl2020.Color.red) = (DegenEtAl2020.Size.big, DegenEtAl2020.Color.blue)
• WaldonDegen2021.swap (DegenEtAl2020.Size.big, DegenEtAl2020.Color.red) = (DegenEtAl2020.Size.big, DegenEtAl2020.Color.red)

def WaldonDegen2021.mirrorUtterance (u : List Word) : List Word

The Spanish counterpart of an English utterance puts the noun first and the counterparts of the adjectives after it.

Equations

• WaldonDegen2021.mirrorUtterance u = WaldonDegen2021.Word.pin :: List.map WaldonDegen2021.mirror u.dropLast.dropLast ++ [WaldonDegen2021.Word.stop]

theorem WaldonDegen2021.cs_eq_swap_ss (i : Fin 3) : cs i = swap (ss i)

Each scene is the counterpart of the other.

theorem WaldonDegen2021.ss_eq_swap_cs (i : Fin 3) : ss i = swap (cs i)

theorem WaldonDegen2021.alternatives_spanish_cs : (alternatives spanish cs).Perm (List.map mirrorUtterance (alternatives english ss))

The Spanish alternatives in the colour-sufficient scene are the counterparts of the English alternatives in the size-sufficient scene.

theorem WaldonDegen2021.alternatives_spanish_ss : (alternatives spanish ss).Perm (List.map mirrorUtterance (alternatives english cs))

The Spanish alternatives in the size-sufficient scene are the counterparts of the English alternatives in the colour-sufficient scene.

theorem WaldonDegen2021.lexicon_mirror {vs vc : ℝ} (w : Word) (r : DegenEtAl2020.Size × DegenEtAl2020.Color) : lexicon vs vc (mirror w) (swap r) = lexicon vc vs w r

theorem WaldonDegen2021.meaning_mirror {vs vc : ℝ} {s s' : Scene} (hs : ∀ (i : Fin 3), s' i = swap (s i)) {u : List Word} (hu : u ∈ english) (i : Fin 3) : meaning vs vc s' (mirrorUtterance u) i = meaning vc vs s u i

An English utterance means at a pin, with the semantic values exchanged, what its Spanish counterpart means at the counterpart of the pin.

theorem WaldonDegen2021.spanish_cs_production_eq_english_ss {vs vc α : ℝ} {cost : Word → ℝ} (hα : 0 < α) (hcost : ∀ (w : Word), cost (mirror w) = cost w) (hs0 : 0 < vs) (hs1 : vs ≤ 1) (hc0 : 0 < vc) (hc1 : vc ≤ 1) : production α cost vs vc spanish cs [Word.pin, Word.blue, Word.small, Word.stop] = production α cost vc vs english ss [Word.small, Word.blue, Word.pin, Word.stop]

For the small blue pin, pin blue small in the colour-sufficient scene of Spanish is as likely as small blue pin in the size-sufficient scene of English with the semantic values of size and colour exchanged. With equal values, and so with Boolean meanings, redundant size in Spanish is as likely as redundant colour in English.

theorem WaldonDegen2021.spanish_ss_production_eq_english_cs {vs vc α : ℝ} {cost : Word → ℝ} (hα : 0 < α) (hcost : ∀ (w : Word), cost (mirror w) = cost w) (hs0 : 0 < vs) (hs1 : vs ≤ 1) (hc0 : 0 < vc) (hc1 : vc ≤ 1) : production α cost vs vc spanish ss [Word.pin, Word.blue, Word.small, Word.stop] = production α cost vc vs english cs [Word.small, Word.blue, Word.pin, Word.stop]

For the small blue pin, pin blue small in the size-sufficient scene of Spanish is as likely as small blue pin in the colour-sufficient scene of English with the semantic values exchanged. With equal values redundant colour in Spanish is as likely as redundant size in English.

The redundancy step

theorem WaldonDegen2021.english_step_eq_sigmoid {vs vc α : ℝ} {cost : Word → ℝ} (hα : 0 < α) (hs0 : 0 < vs) (hs1 : vs ≤ 1) (hc0 : 0 < vc) (hc1 : vc ≤ 1) : ((step α cost vs vc english ss [Word.small]) target).real {Word.blue} = (α * (Real.log (DegenEtAl2020.gain 1 vs vc) - (cost Word.blue - cost Word.pin))).sigmoid

After small, the English speaker in the size-sufficient scene adds the redundant blue with a probability that is a logistic function of the log of the gain of the redundant adjective, less its cost over the noun's.

theorem WaldonDegen2021.boolean_english_step {α : ℝ} {cost : Word → ℝ} (hα : 0 < α) : ((step α cost 1 1 english ss [Word.small]) target).real {Word.blue} = (-(α * (cost Word.blue - cost Word.pin))).sigmoid

With Boolean meanings the redundant adjective adds no information, and the speaker adds it only as far as its cost allows.

theorem WaldonDegen2021.spanish_size_step_lt_english_color_step_iff {vs vc α : ℝ} {cost : Word → ℝ} (hα : 0 < α) (hcost : ∀ (w : Word), cost (mirror w) = cost w) (hs0 : 0 < vs) (hs1 : vs ≤ 1) (hc0 : 0 < vc) (hc1 : vc ≤ 1) : ((step α cost vs vc spanish cs [Word.pin, Word.blue]) target).real {Word.small} < ((step α cost vs vc english ss [Word.small]) target).real {Word.blue} ↔ vs < vc

The Spanish speaker adds the redundant size after pin blue less readily than the English speaker adds the redundant colour after small exactly when size is noisier than colour. With equal values, and so with Boolean meanings, the two steps are equally likely.