Lexical Uncertainty: Core Types

The Lexicon type used by lexical uncertainty models in RSA.

For RSA models with lexical uncertainty, use a latent-lexicon chain with Latent := YourLexiconType (see [PLLF16] and [PL15] for examples). This file provides the shared Lexicon type used by:

• GrammarDist.lean (Construction Grammar as distribution over lexica)
• SDS/Marginalization.lean (SDS ↔ LU-RSA bidirectional translation)

structure Lexicon (Utterance World : Type) : Type

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

In [BLG16] 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.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))