NoisyLex — Noisy lexical semantics bundle

[DHG+20] [WD21] [SW23]

A NoisyLex U W packages the per-(token, world) lex function shared by RSA models with continuous / Product-of-Experts semantics. From the bundle we derive:

• prefixMeaning — PoE composition over a list of tokens (delegates to RSA.prefixMeaning) Studies build their sequential chains from lex and prefixMeaning (No-Brevity β = 1 for [SW23]; rpow + cost-atom for [WD21]).

This is the structure-shaped alternative to the typeclass roadmap that previously lived in Channel.lean. There is no canonical noisy semantics per (U, W) pair — every paper picks its own reliability parameters — so each study constructs an explicit NoisyLex value and calls a builder, mirroring how mathlib's PMF / Kernel are bundled structures rather than typeclass-driven.

Scope

The builders here all use PoE prefix-product L0 semantics — the meaning at a prefix is the product of per-word lex values. Studies that use extension-averaging L0 instead (e.g. [WD21]'s continuousMeaning averages PoE over scene-filtered completions) need their own bespoke chains; the bundle's lex and prefixMeaning are still useful as building blocks (see WaldonDegen2021.uttContinuousQ_eq_prefixMeaning).

A complementary bundle for extension-counting (Boolean truth, not graded) semantics ([CGGP19]) lives in Incremental.lean as IncrementalSemantics.

structure RSA.NoisyLex (U W : Type) : Type

Bundle of noisy lexical semantics: a per-(token, world) ℚ-valued score that is non-negative everywhere. The lex field is the "Product of Experts" per-word factor underlying [DHG+20], [WD21], and [SW23].

Currently ℚ-valued for computable studies. PMF / ℝ generalization is future work tracked in MEMORY.md (RSA → mathlib-PMF migration).

• lex : U → W → ℚ

  Per-(token, world) noisy meaning value.

• lex_nonneg (u : U) (w : W) : 0 ≤ self.lex u w

  Noisy meaning is non-negative.

def RSA.NoisyLex.prefixMeaning {U W : Type} (s : NoisyLex U W) (pfx : List U) (w : W) : ℚ

The PoE prefix meaning derived from the lex function — multiplicative composition over a list of tokens. Delegates to RSA.prefixMeaning.

Equations

• s.prefixMeaning pfx w = RSA.prefixMeaning s.lex pfx w

theorem RSA.NoisyLex.prefixMeaning_nonneg {U W : Type} (s : NoisyLex U W) (pfx : List U) (w : W) : 0 ≤ s.prefixMeaning pfx w

theorem RSA.NoisyLex.prefixMeaning_perm {U W : Type} (s : NoisyLex U W) {pfx pfx' : List U} (h : pfx.Perm pfx') (w : W) : s.prefixMeaning pfx w = s.prefixMeaning pfx' w

def RSA.NoisyLex.ofChannel {U W : Type} (applies : U → W → Bool) (rPlus rMinus : ℚ) (h0 : 0 ≤ rMinus) (h1 : rMinus ≤ rPlus) : NoisyLex U W

Standard noisy-lex construction: pick a "true" reliability r⁺ and a noise floor r⁻ (typically 1 - r⁺), and let lex u w = r⁺ when applies u w and r⁻ otherwise. This is the [DHG+20] Bernoulli-channel form: lex = noiseChannel r⁺ r⁻ (applies? 1 0).

Equations

• RSA.NoisyLex.ofChannel applies rPlus rMinus h0 h1 = { lex := fun (u : U) (w : W) => if applies u w = true then rPlus else rMinus, lex_nonneg := ⋯ }

theorem RSA.NoisyLex.ofChannel_lex_eq_noiseChannel {U W : Type} (applies : U → W → Bool) (rPlus rMinus : ℚ) (h0 : 0 ≤ rMinus) (h1 : rMinus ≤ rPlus) (u : U) (w : W) : (ofChannel applies rPlus rMinus h0 h1).lex u w = Noise.noiseChannel rPlus rMinus (if applies u w = true then 1 else 0)

The ofChannel lex agrees with RSA.Noise.noiseChannel.