Potts, Lassiter, Levy and Frank (2016): Embedded Implicatures as Pragmatic Inferences under Compositional Lexical Uncertainty

Potts, Lassiter, Levy and Frank model embedded implicatures as pragmatic inference under compositional lexical uncertainty, in the context of their experiment (§6). Three players each hit none, some but not all, or all of their shots, a vertex of Aristotelian.Triangle, and a state is the multiset of outcomes (16). A message composes a quantifier over players with a quantifier over shots, the null message added (18), and the lexica are the neo-Gricean refinement set of some, itself or some but not all (14), (19d). The literal listener L0, the speaker S1 and the uncertainty listener L1, which inverts the speaker jointly over states and lexica (13), are compared with the fixed-lexicon listener L1fixed of (19b). Every ordering below holds at every rationality and every cost of the null message.

Main results

• one_some_local, no_some_local: under exactly one and no the uncertainty listener gives mass to the locally enriched states, which the fixed-lexicon model excludes, the low but non-negligible enrichment under a negative quantifier that Chemla and Spector report.
• one_some_literal_first, no_some_literal_first: the literal construals NNS and NNN still rank first.
• every_some_ordering, every_some_fixed: for every player hit some of his shots the uncertainty listener mirrors the human ordering, SSS first and AAA last among the true states, where the fixed-lexicon listener puts SAA first.

Implementation notes

The state and lexicon priors are flat (18). The null message is true at every state, so its cost adds the same weight to every row of the speaker, and the share of a statement is its informativity weight over the sum of the weights of the statements true at the state plus that constant; each ordering is an inequality between such fractions in the weights 4^{-α}, 3^{-α}, 2^{-α}, 1. The unconstrained refinement model (19c), whose lexica are the nonempty subsets of the denotation of some over sets of shots, and the fit to the response data are not formalized.

References

• [PLLF16]
• [CS11]

The context (§6, (16) and (18))

inductive PottsEtAl2016.World : Type

The states (16) are the multisets of three outcomes, each named by its outcomes.

• NNN : World
• NNS : World
• NNA : World
• NSS : World
• NSA : World
• NAA : World
• SSS : World
• SSA : World
• SAA : World
• AAA : World

@[instance_reducible]

instance PottsEtAl2016.instDecidableEqWorld : DecidableEq World

Equations

• PottsEtAl2016.instDecidableEqWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance PottsEtAl2016.instFintypeWorld : Fintype World

Equations

• PottsEtAl2016.instFintypeWorld = { elems := { val := ↑PottsEtAl2016.World.enumList, nodup := PottsEtAl2016.World.enumList_nodup }, complete := PottsEtAl2016.instFintypeWorld._proof_1 }

instance PottsEtAl2016.instNonemptyWorld : Nonempty World

@[instance_reducible]

instance PottsEtAl2016.instMeasurableSpaceWorld : MeasurableSpace World

Equations

• PottsEtAl2016.instMeasurableSpaceWorld = ⊤

def PottsEtAl2016.World.outcomes : World → Multiset Aristotelian.Triangle

The outcomes of a state.

Equations

• PottsEtAl2016.World.NNN.outcomes = {Aristotelian.Triangle.E, Aristotelian.Triangle.E, Aristotelian.Triangle.E}
• PottsEtAl2016.World.NNS.outcomes = {Aristotelian.Triangle.E, Aristotelian.Triangle.E, Aristotelian.Triangle.IO}
• PottsEtAl2016.World.NNA.outcomes = {Aristotelian.Triangle.E, Aristotelian.Triangle.E, Aristotelian.Triangle.A}
• PottsEtAl2016.World.NSS.outcomes = {Aristotelian.Triangle.E, Aristotelian.Triangle.IO, Aristotelian.Triangle.IO}
• PottsEtAl2016.World.NSA.outcomes = {Aristotelian.Triangle.E, Aristotelian.Triangle.IO, Aristotelian.Triangle.A}
• PottsEtAl2016.World.NAA.outcomes = {Aristotelian.Triangle.E, Aristotelian.Triangle.A, Aristotelian.Triangle.A}
• PottsEtAl2016.World.SSS.outcomes = {Aristotelian.Triangle.IO, Aristotelian.Triangle.IO, Aristotelian.Triangle.IO}
• PottsEtAl2016.World.SSA.outcomes = {Aristotelian.Triangle.IO, Aristotelian.Triangle.IO, Aristotelian.Triangle.A}
• PottsEtAl2016.World.SAA.outcomes = {Aristotelian.Triangle.IO, Aristotelian.Triangle.A, Aristotelian.Triangle.A}
• PottsEtAl2016.World.AAA.outcomes = {Aristotelian.Triangle.A, Aristotelian.Triangle.A, Aristotelian.Triangle.A}

inductive PottsEtAl2016.ShotQ : Type

The quantifiers over a player's shots are every, no and some.

• every : ShotQ
• no : ShotQ
• some_ : ShotQ

@[instance_reducible]

instance PottsEtAl2016.instDecidableEqShotQ : DecidableEq ShotQ

Equations

• PottsEtAl2016.instDecidableEqShotQ x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance PottsEtAl2016.instFintypeShotQ : Fintype ShotQ

Equations

• PottsEtAl2016.instFintypeShotQ = { elems := { val := ↑PottsEtAl2016.ShotQ.enumList, nodup := PottsEtAl2016.ShotQ.enumList_nodup }, complete := PottsEtAl2016.instFintypeShotQ._proof_1 }

inductive PottsEtAl2016.PlayerQ : Type

The quantifiers over the players are every, exactly one and no.

• every : PlayerQ
• exactlyOne : PlayerQ
• no : PlayerQ

@[instance_reducible]

instance PottsEtAl2016.instDecidableEqPlayerQ : DecidableEq PlayerQ

Equations

• PottsEtAl2016.instDecidableEqPlayerQ x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance PottsEtAl2016.instFintypePlayerQ : Fintype PlayerQ

Equations

• PottsEtAl2016.instFintypePlayerQ = { elems := { val := ↑PottsEtAl2016.PlayerQ.enumList, nodup := PottsEtAl2016.PlayerQ.enumList_nodup }, complete := PottsEtAl2016.instFintypePlayerQ._proof_1 }

inductive PottsEtAl2016.Lex : Type

The lexica of the neo-Gricean refinement set (14), (19d) read some as itself or as some but not all.

• weak : Lex
• strong : Lex

@[instance_reducible]

instance PottsEtAl2016.instDecidableEqLex : DecidableEq Lex

Equations

• PottsEtAl2016.instDecidableEqLex x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance PottsEtAl2016.instFintypeLex : Fintype Lex

Equations

• PottsEtAl2016.instFintypeLex = { elems := { val := ↑PottsEtAl2016.Lex.enumList, nodup := PottsEtAl2016.Lex.enumList_nodup }, complete := PottsEtAl2016.instFintypeLex._proof_1 }

instance PottsEtAl2016.instNonemptyLex : Nonempty Lex

@[instance_reducible]

instance PottsEtAl2016.instMeasurableSpaceLex : MeasurableSpace Lex

Equations

• PottsEtAl2016.instMeasurableSpaceLex = ⊤

def PottsEtAl2016.Lex.someDen : Lex → Finset Aristotelian.Triangle

Under a lexicon some covers the outcomes with any hit, or those with some but not all.

Equations

• PottsEtAl2016.Lex.weak.someDen = {Aristotelian.Triangle.IO, Aristotelian.Triangle.A}
• PottsEtAl2016.Lex.strong.someDen = {Aristotelian.Triangle.IO}

theorem PottsEtAl2016.lex_refines (l : Lex) : l.someDen.Nonempty ∧ l.someDen ⊆ Lex.weak.someDen

The refinement condition (11) holds, each lexicon reading some as a nonempty part of its base denotation, which the base lexicon is.

def PottsEtAl2016.ShotQ.Holds (l : Lex) : ShotQ → Aristotelian.Triangle → Prop

Whether an outcome satisfies the quantifier over shots under a lexicon.

Equations

• PottsEtAl2016.ShotQ.Holds l PottsEtAl2016.ShotQ.every x✝ = (x✝ = ⊤)
• PottsEtAl2016.ShotQ.Holds l PottsEtAl2016.ShotQ.no x✝ = (x✝ = ⊥)
• PottsEtAl2016.ShotQ.Holds l PottsEtAl2016.ShotQ.some_ x✝ = (x✝ ∈ l.someDen)

@[instance_reducible]

instance PottsEtAl2016.instDecidablePredTriangleHolds (l : Lex) (s : ShotQ) : DecidablePred (ShotQ.Holds l s)

Equations

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

def PottsEtAl2016.PlayerQ.Holds : PlayerQ → ℕ → Prop

Whether a number of players satisfies the quantifier over players.

Equations

• PottsEtAl2016.PlayerQ.every.Holds x✝ = (x✝ = 3)
• PottsEtAl2016.PlayerQ.exactlyOne.Holds x✝ = (x✝ = 1)
• PottsEtAl2016.PlayerQ.no.Holds x✝ = (x✝ = 0)

@[instance_reducible]

instance PottsEtAl2016.instDecidablePredNatHolds (q : PlayerQ) : DecidablePred q.Holds

Equations

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

@[reducible, inline]

abbrev PottsEtAl2016.Stmt : Type

A statement (18c) applies a quantifier over players to a quantifier over shots.

Equations

• PottsEtAl2016.Stmt = (PottsEtAl2016.PlayerQ × PottsEtAl2016.ShotQ)

def PottsEtAl2016.Stmt.Truth (l : Lex) (s : Stmt) (w : World) : Prop

A statement is true at a state under a lexicon when its quantifier over players holds of the number of players whose outcome satisfies its quantifier over shots.

Equations

• PottsEtAl2016.Stmt.Truth l s w = s.1.Holds (Multiset.countP (PottsEtAl2016.ShotQ.Holds l s.2) w.outcomes)

@[instance_reducible]

instance PottsEtAl2016.instDecidablePredWorldTruth (l : Lex) (s : Stmt) : DecidablePred (Stmt.Truth l s)

Equations

• PottsEtAl2016.instDecidablePredWorldTruth l s w = PottsEtAl2016.instDecidablePredWorldTruth._aux_1 l s w

def PottsEtAl2016.stmtSem (l : Lex) (s : Stmt) : Finset World

The extension of a statement under a lexicon.

Equations

• PottsEtAl2016.stmtSem l s = Finset.filter (PottsEtAl2016.Stmt.Truth l s) Finset.univ

@[reducible, inline]

abbrev PottsEtAl2016.Msg : Type

The messages (18c) are the statements and the null message of (12a).

Equations

• PottsEtAl2016.Msg = Option PottsEtAl2016.Stmt

@[instance_reducible]

instance PottsEtAl2016.instMeasurableSpaceMsg : MeasurableSpace Msg

Equations

• PottsEtAl2016.instMeasurableSpaceMsg = ⊤

def PottsEtAl2016.sem (l : Lex) (m : Msg) : Finset World

The extension of a message under a lexicon, the null message true at every state.

Equations

• PottsEtAl2016.sem l m = Option.elim m Finset.univ (PottsEtAl2016.stmtSem l)

@[reducible, inline]

abbrev PottsEtAl2016.everySome : Stmt

Every player hit some of his shots.

Equations

• PottsEtAl2016.everySome = (PottsEtAl2016.PlayerQ.every, PottsEtAl2016.ShotQ.some_)

@[reducible, inline]

abbrev PottsEtAl2016.oneSome : Stmt

Exactly one player hit some of his shots.

Equations

• PottsEtAl2016.oneSome = (PottsEtAl2016.PlayerQ.exactlyOne, PottsEtAl2016.ShotQ.some_)

@[reducible, inline]

abbrev PottsEtAl2016.noSome : Stmt

No player hit some of his shots.

Equations

• PottsEtAl2016.noSome = (PottsEtAl2016.PlayerQ.no, PottsEtAl2016.ShotQ.some_)

theorem PottsEtAl2016.refinement_facts : (∀ (q : PlayerQ), stmtSem Lex.weak (q, ShotQ.every) = stmtSem Lex.strong (q, ShotQ.every) ∧ stmtSem Lex.weak (q, ShotQ.no) = stmtSem Lex.strong (q, ShotQ.no)) ∧ stmtSem Lex.strong everySome ⊂ stmtSem Lex.weak everySome ∧ stmtSem Lex.weak noSome ⊂ stmtSem Lex.strong noSome ∧ stmtSem Lex.weak oneSome = {World.NNS, World.NNA} ∧ stmtSem Lex.strong oneSome = {World.NNS, World.NSA, World.SAA}

The lexica agree off some, and the refinement narrows the extension of some under every while widening it under no, the source of the asymmetry; under exactly one the refinement admits the locally enriched states NSA and SAA.

The model (13), (18), (19)

def PottsEtAl2016.cost (k : ℝ) (m : Msg) : ℝ

The cost (18d) is k for the null message and 0 for every statement.

Equations

• PottsEtAl2016.cost k m = Option.elim m k fun (x : PottsEtAl2016.Stmt) => 0

noncomputable def PottsEtAl2016.L0 (l : Lex) : ProbabilityTheory.Kernel Msg World

The literal listener (13a) conditions a flat prior on the message's extension.

Equations

• PottsEtAl2016.L0 l = RSA.listener (ProbabilityTheory.uniformOn Set.univ) (RSA.truthful fun (m : PottsEtAl2016.Msg) => ↑(PottsEtAl2016.sem l m))

instance PottsEtAl2016.instIsFiniteKernelMsgWorldL0 (l : Lex) : ProbabilityTheory.IsFiniteKernel (L0 l)

noncomputable def PottsEtAl2016.S1 (α k : ℝ) (l : Lex) : ProbabilityTheory.Kernel World Msg

The speaker (13b).

Equations

• PottsEtAl2016.S1 α k l = RSA.speaker α (PottsEtAl2016.cost k) (⇑(PottsEtAl2016.L0 l)) MeasureTheory.Measure.dirac

instance PottsEtAl2016.instIsFiniteKernelWorldMsgS1 (α k : ℝ) (l : Lex) : ProbabilityTheory.IsFiniteKernel (S1 α k l)

noncomputable def PottsEtAl2016.L1 (α k : ℝ) : ProbabilityTheory.Kernel Msg (World × Lex)

The uncertainty listener (13c) inverts the lexicon-indexed speaker against flat priors over states and lexica; its state marginal is the paper's listener.

Equations

• PottsEtAl2016.L1 α k = RSA.listener (ProbabilityTheory.uniformOn Set.univ) fun (p : PottsEtAl2016.World × PottsEtAl2016.Lex) => (PottsEtAl2016.S1 α k p.2) p.1

noncomputable def PottsEtAl2016.L1fixed (α k : ℝ) : ProbabilityTheory.Kernel Msg World

The fixed-lexicon pragmatic listener (19b) inverts the base lexicon's speaker at a flat prior.

Equations

• PottsEtAl2016.L1fixed α k = RSA.listener (ProbabilityTheory.uniformOn Set.univ) ⇑(PottsEtAl2016.S1 α k PottsEtAl2016.Lex.weak)

theorem PottsEtAl2016.L1_fst_real_lt_iff {α k : ℝ} (m : Msg) (w₁ w₂ : World) : ((L1 α k) m).fst.real {w₁} < ((L1 α k) m).fst.real {w₂} ↔ ∑ l : Lex, ((S1 α k l) w₁).real {m} < ∑ l : Lex, ((S1 α k l) w₂).real {m}

State preference of the uncertainty listener is the pooled speaker preference.

theorem PottsEtAl2016.L1fixed_real_lt_iff {α k : ℝ} (m : Msg) (w₁ w₂ : World) : ((L1fixed α k) m).real {w₁} < ((L1fixed α k) m).real {w₂} ↔ ((S1 α k Lex.weak) w₁).real {m} < ((S1 α k Lex.weak) w₂).real {m}

State preference of the fixed-lexicon listener is the base-lexicon speaker's preference.

Support: local enrichment (§6.3)

theorem PottsEtAl2016.L1_fst_ne_zero_iff {α : ℝ} (hα : 0 < α) {k : ℝ} (m : Msg) (w : World) : ((L1 α k) m).fst {w} ≠ 0 ↔ ∃ (l : Lex), w ∈ sem l m

The uncertainty listener assigns mass to a state exactly when some lexicon makes the message true there.

theorem PottsEtAl2016.L1fixed_ne_zero_iff {α : ℝ} (hα : 0 < α) {k : ℝ} (m : Msg) (w : World) : ((L1fixed α k) m) {w} ≠ 0 ↔ w ∈ sem Lex.weak m

The fixed-lexicon listener assigns mass to a state exactly when the base lexicon makes the message true there.

theorem PottsEtAl2016.one_some_local {α : ℝ} (hα : 0 < α) {k : ℝ} (w : World) : w ∈ {World.NSA, World.SAA} → ((L1 α k) (some oneSome)).fst {w} ≠ 0 ∧ ((L1fixed α k) (some oneSome)) {w} = 0

Hearing exactly one player hit some of his shots, the uncertainty listener gives mass to the locally enriched states NSA and SAA, false on the literal construal, and the fixed-lexicon listener none.

theorem PottsEtAl2016.no_some_local {α : ℝ} (hα : 0 < α) {k : ℝ} (w : World) : w ∈ {World.NNA, World.NAA, World.AAA} → ((L1 α k) (some noSome)).fst {w} ≠ 0 ∧ ((L1fixed α k) (some noSome)) {w} = 0

Hearing no player hit some of his shots, the uncertainty listener gives mass to the locally enriched states NNA, NAA and AAA, and the fixed-lexicon listener none.

Preference orderings (§6.2, §6.3)

theorem PottsEtAl2016.S1_real {α : ℝ} (hα : 0 < α) {k : ℝ} (l : Lex) (w : World) (s : Stmt) : ((S1 α k l) w).real {some s} = (if w ∈ stmtSem l s then (↑(stmtSem l s).card)⁻¹ ^ α else 0) / ((∑ s' : Stmt, if w ∈ stmtSem l s' then (↑(stmtSem l s').card)⁻¹ ^ α else 0) + Real.exp (-(α * k)) * 10⁻¹ ^ α)

The speaker's share of a statement is its informativity weight over the weights of the statements true at the state plus the null message's weight.

The weights and the sums

def PottsEtAl2016.Lex.equivFin : Lex ≃ Fin 2

The two lexica as Fin 2, for sums over the family.

Equations

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

def PottsEtAl2016.PlayerQ.equivFin : PlayerQ ≃ Fin 3

The quantifiers over players as Fin 3.

Equations

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

def PottsEtAl2016.ShotQ.equivFin : ShotQ ≃ Fin 3

The quantifiers over shots as Fin 3.

Equations

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

theorem PottsEtAl2016.Lex.sum_univ {M : Type u_1} [AddCommMonoid M] (f : Lex → M) : ∑ l : Lex, f l = f weak + f strong

theorem PottsEtAl2016.PlayerQ.sum_univ {M : Type u_1} [AddCommMonoid M] (f : PlayerQ → M) : ∑ q : PlayerQ, f q = f every + f exactlyOne + f no

theorem PottsEtAl2016.ShotQ.sum_univ {M : Type u_1} [AddCommMonoid M] (f : ShotQ → M) : ∑ s : ShotQ, f s = f every + f no + f some_

theorem PottsEtAl2016.every_some_ordering {α : ℝ} (hα : 0 < α) {k : ℝ} : ((L1 α k) (some everySome)).fst.real {World.SSA} < ((L1 α k) (some everySome)).fst.real {World.SSS} ∧ ((L1 α k) (some everySome)).fst.real {World.SAA} < ((L1 α k) (some everySome)).fst.real {World.SSS} ∧ ((L1 α k) (some everySome)).fst.real {World.AAA} < ((L1 α k) (some everySome)).fst.real {World.SSA} ∧ ((L1 α k) (some everySome)).fst.real {World.AAA} < ((L1 α k) (some everySome)).fst.real {World.SAA}

Hearing every player hit some of his shots, the uncertainty listener ranks the locally enriched SSS above the other true states and AAA below the two remaining ones, the ordering of the human responses.

theorem PottsEtAl2016.every_some_fixed {α : ℝ} (hα : 0 < α) {k : ℝ} : ((L1fixed α k) (some everySome)).real {World.SSS} < ((L1fixed α k) (some everySome)).real {World.SAA}

The fixed-lexicon listener instead puts SAA above SSS.

theorem PottsEtAl2016.one_some_literal_first {α : ℝ} (hα : 0 < α) {k : ℝ} : ((L1 α k) (some oneSome)).fst.real {World.NNA} < ((L1 α k) (some oneSome)).fst.real {World.NNS} ∧ ((L1 α k) (some oneSome)).fst.real {World.NSA} < ((L1 α k) (some oneSome)).fst.real {World.NNS} ∧ ((L1 α k) (some oneSome)).fst.real {World.SAA} < ((L1 α k) (some oneSome)).fst.real {World.NNS}

Hearing exactly one player hit some of his shots, the uncertainty listener still prefers the literal construal NNS most, above NNA and above the locally enriched NSA and SAA.

theorem PottsEtAl2016.no_some_literal_first {α : ℝ} (hα : 0 < α) {k : ℝ} : ((L1 α k) (some noSome)).fst.real {World.NNA} < ((L1 α k) (some noSome)).fst.real {World.NNN} ∧ ((L1 α k) (some noSome)).fst.real {World.NAA} < ((L1 α k) (some noSome)).fst.real {World.NNN} ∧ ((L1 α k) (some noSome)).fst.real {World.AAA} < ((L1 α k) (some noSome)).fst.real {World.NNN}

Hearing no player hit some of his shots, the uncertainty listener still prefers the literal construal NNN most, above the locally enriched NNA, NAA and AAA.