NoisyLex — Noisy lexical semantics bundle

@cite{degen-etal-2020} @cite{waldon-degen-2021} @cite{schlotterbeck-wang-2023}

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)
• toRSAConfig — one-shot RSAConfig: meaning is lex directly
• toRSAConfigSeq scene — sequential RSAConfig with α=1, no cost (S&W's β=1 default)
• toRSAConfigSeqWithUtility scene α α_pos cost — sequential with rpow + exp(-α·cost) speaker (W&D-flavored speaker, PoE-prefix L0)

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. @cite{waldon-degen-2021}'s continuousMeaning averages PoE over scene-filtered completions) need their own bespoke RSAConfig.mk; 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 (@cite{cohn-gordon-goodman-potts-2019}) 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 @cite{degen-etal-2020}, @cite{waldon-degen-2021}, and @cite{schlotterbeck-wang-2023}.

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 @cite{degen-etal-2020} 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.

noncomputable def RSA.NoisyLex.toRSAConfig {U W : Type} [Fintype U] [Fintype W] (s : NoisyLex U W) : RSAConfig U W

One-shot RSAConfig from a NoisyLex bundle. Meaning is just the lex function; Ctx = Unit, α = 1, no cost, uniform priors.

Equations

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

@[simp]

theorem RSA.NoisyLex.toRSAConfig_meaning {U W : Type} [Fintype U] [Fintype W] (s : NoisyLex U W) (ctx l : Unit) (u : U) (w : W) : s.toRSAConfig.meaning ctx l u w = ↑(s.lex u w)

@[simp]

theorem RSA.NoisyLex.toRSAConfig_α {U W : Type} [Fintype U] [Fintype W] (s : NoisyLex U W) : s.toRSAConfig.α = 1

noncomputable def RSA.NoisyLex.toRSAConfigSeq {U W : Type} [Fintype U] [Fintype W] (s : NoisyLex U W) (scene : W → Bool := fun (x : W) => true) : RSAConfig U W

Sequential RSAConfig from a NoisyLex bundle, optionally scene-restricted. Meaning is the PoE product over ctx ++ [u]; off-scene worlds get 0. Default scene is the full domain. α = 1, no cost (the @cite{schlotterbeck-wang-2023} "S1^inc with β = 1" configuration).

Equations

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

@[simp]

theorem RSA.NoisyLex.toRSAConfigSeq_meaning {U W : Type} [Fintype U] [Fintype W] (s : NoisyLex U W) (scene : W → Bool) (ctx : List U) (l : Unit) (u : U) (w : W) : (s.toRSAConfigSeq scene).meaning ctx l u w = if scene w = true then ↑(s.prefixMeaning (ctx ++ [u]) w) else 0

@[simp]

theorem RSA.NoisyLex.toRSAConfigSeq_α {U W : Type} [Fintype U] [Fintype W] (s : NoisyLex U W) (scene : W → Bool) : (s.toRSAConfigSeq scene).α = 1

@[simp]

theorem RSA.NoisyLex.toRSAConfigSeq_transition {U W : Type} [Fintype U] [Fintype W] (s : NoisyLex U W) (scene : W → Bool) (ctx : List U) (u : U) : (s.toRSAConfigSeq scene).transition ctx u = ctx ++ [u]

@[simp]

theorem RSA.NoisyLex.toRSAConfigSeq_initial {U W : Type} [Fintype U] [Fintype W] (s : NoisyLex U W) (scene : W → Bool) : (s.toRSAConfigSeq scene).initial = []

theorem RSA.NoisyLex.toRSAConfigSeq_meaning_perm {U W : Type} [Fintype U] [Fintype W] (s : NoisyLex U W) (scene : W → Bool) {ctx₁ ctx₂ : List U} {u₁ u₂ : U} (h : (ctx₁ ++ [u₁]).Perm (ctx₂ ++ [u₂])) (w : W) (l : Unit) : (s.toRSAConfigSeq scene).meaning ctx₁ l u₁ w = (s.toRSAConfigSeq scene).meaning ctx₂ l u₂ w

Headline order-independence at the bundle level. The meaning of a sequential noisy-RSA config depends on (ctx, u) only through the multiset ctx ++ [u]. Inherits from RSA.prefixMeaning_perm.

noncomputable def RSA.NoisyLex.toRSAConfigSeqWithUtility {U W : Type} [Fintype U] [Fintype W] (s : NoisyLex U W) (scene : W → Bool := fun (x : W) => true) (α : ℝ) (α_pos : 0 < α) (cost : U → ℝ := fun (x : U) => 0) : RSAConfig U W

Sequential RSAConfig with rpow + exp(-α·cost) speaker (the W&D-style soft-rational speaker), but PoE-prefix L0 meaning. For studies that want α ≠ 1 or non-zero per-word cost while still using PoE semantics.

Equations

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

@[simp]

theorem RSA.NoisyLex.toRSAConfigSeqWithUtility_meaning {U W : Type} [Fintype U] [Fintype W] (s : NoisyLex U W) (scene : W → Bool) (α : ℝ) (α_pos : 0 < α) (cost : U → ℝ) (ctx : List U) (l : Unit) (u : U) (w : W) : (s.toRSAConfigSeqWithUtility scene α α_pos cost).meaning ctx l u w = if scene w = true then ↑(s.prefixMeaning (ctx ++ [u]) w) else 0

@[simp]

theorem RSA.NoisyLex.toRSAConfigSeqWithUtility_α {U W : Type} [Fintype U] [Fintype W] (s : NoisyLex U W) (scene : W → Bool) (α : ℝ) (α_pos : 0 < α) (cost : U → ℝ) : (s.toRSAConfigSeqWithUtility scene α α_pos cost).α = α