Lexical uncertainty: the Lexicon type

The shared Lexicon type for lexical-uncertainty RSA models: models marginalize over a latent lexicon (Latent := YourLexiconType; see [PLLF16] and [PL15]). Consumed by Syntax/ConstructionGrammar/GrammarDist.lean (grammars as distributions over lexica) and Studies/Clark1983.lean.

structure RSA.Lexicon (Utterance World : Type) : Type

A lexicon maps each utterance to a graded truth function over worlds — [BLG16]'s L(u, w), with values in [0,1] to allow graded semantics.

• meaning : Utterance → World → ℚ

  The meaning function for this lexicon

def RSA.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 RSA.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 RSA.Lexicon.«term_≤ₗ_» : Lean.TrailingParserDescr

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

Equations

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