Lexical Uncertainty Extension to RSA

Architecture

Lexical uncertainty posits that speakers and listeners have uncertainty about the semantic content of utterances. Rather than a fixed lexicon, there is a set of possible lexica Λ, and pragmatic inference involves reasoning about which lexicon is in use.

Innovation

The marginalization over lexica happens at L₁, not L₀:

• L₀ is still parameterized by a specific lexicon L
• S₁ believes L₀ uses lexicon L (and is certain about it)
• L₁ is uncertain which lexicon S₁/L₀ are using, and marginalizes

What This Derives

1. M-implicatures: Complex expressions → marked (low-probability) interpretations
2. Ignorance implicatures: "some or all" → speaker doesn't know which
3. Non-convex disjunctive implicatures: "one or three" ≠ "one or two"

Relationship to RSAConfig

The LUScenario type below is conceptually subsumed by RSAConfig with Latent := Lexicon. The @cite{potts-etal-2016} study demonstrates this: it uses standard RSAConfig with Latent := Lexicon (weak vs strong "some") and derives DE blocking and UE enrichment without any LU-specific infrastructure.

This file is retained for:

• The Lexicon type and Refinement infrastructure
• The LUScenario structure as a reference for the LU architecture
• The symmetry_breaking_possible conjecture (which could now be discharged using the @cite{potts-etal-2016} model as a concrete witness via RSAConfig)

structure Lexicon (Utterance World : Type) : Type

A lexicon maps each utterance to a truth function over worlds.

In @cite{bergen-levy-goodman-2016} notation: L(u, w) = 1 if w ∈ ⟦u⟧_L, else 0

For graded semantics, we allow values in [0,1].

• meaning : Utterance → World → ℚ

  The meaning function for this lexicon

def Lexicon.ofScenario {U W : Type} (_utts : List U) (_worlds : List W) (φ : U → W → ℚ) : Lexicon U W

Create a lexicon from an RSAScenario's meaning function

Equations

• Lexicon.ofScenario _utts _worlds φ = { meaning := φ }

def Lexicon.equiv {U W : Type} (L₁ L₂ : Lexicon U W) : Prop

Two lexica are equivalent if they assign the same meanings

Equations

• L₁.equiv L₂ = ∀ (u : U) (w : W), L₁.meaning u w = L₂.meaning u w

def Lexicon.refines {U W : Type} (L_refined L_base : Lexicon U W) : Prop

Check if a lexicon is a refinement of another (logically implies)

Equations

• (L_refined ≤ₗ L_base) = ∀ (u : U) (w : W), L_base.meaning u w = 0 → L_refined.meaning u w = 0

def Lexicon.«term_≤ₗ_» : Lean.TrailingParserDescr

Notation: L' ≤ₗ L means L' refines (is more specific than) L

Equations

• Lexicon.«term_≤ₗ_» = Lean.ParserDescr.trailingNode `Lexicon.«term_≤ₗ_» 50 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤ₗ ") (Lean.ParserDescr.cat `term 0))

structure LUScenario : Type 1

Lexical Uncertainty RSA Scenario.

Extends the basic RSA setup with:

• A set of possible lexica Λ
• A prior distribution over lexica

The semantic content of utterances is not fixed; rather, pragmatic inference jointly determines both the interpretation AND the lexicon.

• Utterance : Type

  Type of utterances

• World : Type

  Type of possible worlds

• baseLexicon : Lexicon self.Utterance self.World

  Base semantic lexicon (unrefined meanings)

• lexica : List (Lexicon self.Utterance self.World)

  Set of possible refined lexica

• lexPrior : Lexicon self.Utterance self.World → ℚ

  Prior over lexica (default: uniform)

• worldPrior : self.World → ℚ

  Prior over worlds

• utterances : List self.Utterance

  Enumeration of utterances

• worlds : List self.World

  Enumeration of worlds

• α : ℕ

  Rationality parameter. Higher values = more informative speaker.

• nullCost : ℚ

  Null utterance cost (high, to discourage)

• uttBEq : BEq self.Utterance
• worldBEq : BEq self.World
• worldDecEq : DecidableEq self.World

structure LexicalRefinement.Refinement (W : Type) : Type

A refinement of a truth function: a subset of worlds where it's true.

Given base meaning M : W → Bool, a valid refinement M' satisfies: ∀ w, M(w) = false → M'(w) = false

That is, M' can only narrow down the set of true worlds, not expand it.

• meaning : W → Bool

  The refined meaning as a subset indicator

def LexicalRefinement.Refinement.isValidFor {W : Type} (r : Refinement W) (base : W → Bool) : Prop

Check if one meaning refines another (is more specific).

M' refines M iff M' ⊆ M (as sets of worlds).

Equations

• r.isValidFor base = ∀ (w : W), base w = false → r.meaning w = false

def LexicalRefinement.allRefinements {W : Type} [DecidableEq W] (worlds : List W) (base : W → Bool) : List (Refinement W)

Generate all valid refinements of a Boolean meaning over finite worlds.

For a base meaning true at n worlds, there are 2ⁿ - 1 valid non-trivial refinements (excluding the empty refinement which would be contradictory).

Equations

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

inductive ObsState : Type

Observation states for ignorance implicatures.

The speaker may:

• Know all passed (∀)
• Know some-but-not-all passed (∃¬∀)
• Be ignorant (?)

• knowAll : ObsState
• knowSomeNot : ObsState
• ignorant : ObsState

instance instReprObsState : Repr ObsState

Equations

• instReprObsState = { reprPrec := instReprObsState.repr }

def instReprObsState.repr : ObsState → ℕ → Std.Format

Equations

• instReprObsState.repr ObsState.knowAll prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ObsState.knowAll")).group prec✝
• instReprObsState.repr ObsState.knowSomeNot prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ObsState.knowSomeNot")).group prec✝
• instReprObsState.repr ObsState.ignorant prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ObsState.ignorant")).group prec✝

instance instBEqObsState : BEq ObsState

Equations

• instBEqObsState = { beq := instBEqObsState.beq }

def instBEqObsState.beq : ObsState → ObsState → Bool

Equations

• instBEqObsState.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance instDecidableEqObsState : DecidableEq ObsState

Equations

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

inductive ScalarWorld : Type

World states for scalar scenarios.

• all : ScalarWorld
• someNot : ScalarWorld

def instReprScalarWorld.repr : ScalarWorld → ℕ → Std.Format

Equations

• instReprScalarWorld.repr ScalarWorld.all prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ScalarWorld.all")).group prec✝
• instReprScalarWorld.repr ScalarWorld.someNot prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ScalarWorld.someNot")).group prec✝

instance instReprScalarWorld : Repr ScalarWorld

Equations

• instReprScalarWorld = { reprPrec := instReprScalarWorld.repr }

instance instBEqScalarWorld : BEq ScalarWorld

Equations

• instBEqScalarWorld = { beq := instBEqScalarWorld.beq }

def instBEqScalarWorld.beq : ScalarWorld → ScalarWorld → Bool

Equations

• instBEqScalarWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance instDecidableEqScalarWorld : DecidableEq ScalarWorld

Equations

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

inductive SomeOrAllUtt : Type

Utterances for some-or-all ignorance implicatures.

• all_ : SomeOrAllUtt
• some_ : SomeOrAllUtt
• someOrAll : SomeOrAllUtt

instance instReprSomeOrAllUtt : Repr SomeOrAllUtt

Equations

• instReprSomeOrAllUtt = { reprPrec := instReprSomeOrAllUtt.repr }

def instReprSomeOrAllUtt.repr : SomeOrAllUtt → ℕ → Std.Format

Equations

• instReprSomeOrAllUtt.repr SomeOrAllUtt.all_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SomeOrAllUtt.all_")).group prec✝
• instReprSomeOrAllUtt.repr SomeOrAllUtt.some_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SomeOrAllUtt.some_")).group prec✝
• instReprSomeOrAllUtt.repr SomeOrAllUtt.someOrAll prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SomeOrAllUtt.someOrAll")).group prec✝

instance instBEqSomeOrAllUtt : BEq SomeOrAllUtt

Equations

• instBEqSomeOrAllUtt = { beq := instBEqSomeOrAllUtt.beq }

def instBEqSomeOrAllUtt.beq : SomeOrAllUtt → SomeOrAllUtt → Bool

Equations

• instBEqSomeOrAllUtt.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance instDecidableEqSomeOrAllUtt : DecidableEq SomeOrAllUtt

Equations

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

theorem LUTheorems.symmetry_breaking_possible : ∃ (S : LUScenario) (u₁ : S.Utterance) (u₂ : S.Utterance) (w : S.World), S.baseLexicon.meaning u₁ = S.baseLexicon.meaning u₂ ∧ True

Symmetry breaking: semantically equivalent utterances can get different interpretations.

This is the key property that enables M-implicatures.