Silence as a null alternative

[BLG16]

WithSilence U := Option U is the standard wrapper that adds a "silence" element to any utterance type: none is silence, some u a paper-utterance. liftMeaning gives silence universal extension — true at every world — following the null utterance of [BLG16], which is true in every world so that the speaker always has an honest option.

Deviation from the source: [BLG16] disfavor their null utterance by cost (it is the most expensive alternative), and observe that a sufficiently cheap null utterance is used in the fully ignorant knowledge state. This costless rendering disfavors silence by informativity alone: universal extension gives it the smallest literal-listener value (1/card W under the extensionOf-based literal listener), so the softmax speaker prefers any honest informative utterance, and silence absorbs all probability exactly where none exists. That dissolves the "no qOk witness" defect that would otherwise make some observation cells vacuous in PMF formalizations of [GS13]-style models (whose own utterance sets have no null utterance).

Main definitions

• WithSilence U — Option U, where none = silence.
• liftMeaning m — extends m : U → W → Bool to WithSilence U → W → Bool, with silence true at every world.
• extensionOf_liftMeaning_none — silence's extension is the whole world space.

Per-paper specialisations

The "cover hypothesis is universally satisfied because silence is always qOk" theorem is paper-specific (because qOk depends on the paper's observation type and compatibility predicate). Each consumer paper proves its own cover_silent as a 1-line application of liftMeaning_none.

@[reducible, inline]

abbrev RSA.WithSilence (U : Type u_3) : Type u_3

Silence-extended utterance type. some u is a paper-utterance; none is the "say nothing" alternative.

Definitionally Option U so it inherits all standard instances (DecidableEq, Fintype, Repr, Inhabited) without manual derivation.

Equations

• RSA.WithSilence U = Option U

def RSA.liftMeaning {U : Type u_1} {W : Type u_2} (m : U → W → Bool) : WithSilence U → W → Bool

Lift a meaning function to handle silence. Silence is "vacuously honest" — true at every world (commits to nothing).

Equations

• RSA.liftMeaning m (some u) x✝ = m u x✝
• RSA.liftMeaning m none x✝ = true

@[simp]

theorem RSA.liftMeaning_some {U : Type u_1} {W : Type u_2} (m : U → W → Bool) (u : U) (w : W) : liftMeaning m (some u) w = m u w

@[simp]

theorem RSA.liftMeaning_none {U : Type u_1} {W : Type u_2} (m : U → W → Bool) (w : W) : liftMeaning m none w = true

Costed silence

[BLG16] disfavor the null utterance by cost: the speaker utility is informativity minus cost, so the softmax weight factors as L0 ^ α · exp (−α·c) — a per-utterance cost factor, the slot RSA.S1Belief already carries. liftCostFactor extends a content-utterance cost factor to WithSilence U with a designated silence weight κ: silence maximally expensive (κ minimal) recovers the regime of [BLG16], where silence is a never-preferred honesty fallback; silence free with costly speech gives the decision-to-speak regime of [RHKF22], where whether the speaker talks is itself informative.

def RSA.liftCostFactor {U : Type u_1} (κ : ENNReal) (c : U → ENNReal) : WithSilence U → ENNReal

Extend a cost factor to WithSilence U, with silence weighted κ.

Equations

• RSA.liftCostFactor κ c (some u) = c u
• RSA.liftCostFactor κ c none = κ

@[simp]

theorem RSA.liftCostFactor_some {U : Type u_1} (κ : ENNReal) (c : U → ENNReal) (u : U) : liftCostFactor κ c (some u) = c u

@[simp]

theorem RSA.liftCostFactor_none {U : Type u_1} (κ : ENNReal) (c : U → ENNReal) : liftCostFactor κ c none = κ

The extension of silence

Universal truth makes silence's extension the whole world space — the largest possible, hence the smallest uniform literal-listener value.

@[simp]

theorem RSA.extensionOf_liftMeaning_none {U : Type u_1} {W : Type u_2} [Fintype W] (m : U → W → Bool) : extensionOf (liftMeaning m) none = Finset.univ

theorem RSA.card_extensionOf_liftMeaning_none {U : Type u_1} {W : Type u_2} [Fintype W] (m : U → W → Bool) : (extensionOf (liftMeaning m) none).card = Fintype.card W

theorem RSA.extensionOf_liftMeaning_some_subset {U : Type u_1} {W : Type u_2} [Fintype W] (m : U → W → Bool) (u : U) : extensionOf (liftMeaning m) (some u) ⊆ extensionOf (liftMeaning m) none

Every paper-utterance's extension is contained in silence's.