Threshold Semantics Equivalences

We show that the soft meanings defined in ThresholdSemantics.lean are equal to the SDS marginals computed via SDSConstraintSystem. The gradable noun threshold pattern draws on @cite{morzycki-2009}.

theorem Semantics.Probabilistic.SDS.Marginalization.adjective_soft_meaning_uniform {E : Type} (adj : ThresholdSemantics.GradableAdjective E) (x : E) (_h_uniform : ∀ θ ∈ ThresholdInstances.thresholdRange, adj.thresholdPrior θ = 1 / 11) (_h_measure_unit : 0 ≤ adj.measure x ∧ adj.measure x ≤ 1) : adj.softMeaning x = adj.measure x

For a uniform threshold prior, the soft meaning of a gradable adjective equals the measure value.

This is because:

• softMeaning(x) = P(θ < measure(x)) for θ ~ Uniform[0,1]
• P(θ < m) = m for m ∈ [0,1]

The SDS formulation reproduces this via marginalization.

theorem Semantics.Probabilistic.SDS.Marginalization.generic_soft_truth_uniform (gen : ThresholdSemantics.GenericPredicate) (_h_uniform : ∀ θ ∈ ThresholdInstances.thresholdRange, gen.prevalencePrior θ = 1 / 11) : gen.softTruth = gen.prevalence

For a uniform prevalence prior, the soft truth of a generic equals the prevalence value.

theorem Semantics.Probabilistic.SDS.Marginalization.gradable_noun_sds_equiv {E : Type} (gn : ThresholdSemantics.GradableNounWithSize E) (x : E) : ThresholdInstances.gnHoldsSDS gn x = true ↔ gn.holds x = true

Gradable noun semantics via SDS is equivalent to the direct check.

Since gradable nouns have trivial scenario factors (no uncertainty), the SDS machinery reduces to a simple Boolean check.

Bidirectional Translation: SDS ↔ LU-RSA

We establish a formal correspondence between SDS constraint systems and Lexical Uncertainty RSA scenarios. The key insight is that both frameworks perform marginalization over latent semantic choices.

Forward Direction: SDS → LU-RSA

Given an SDS system with:

• Parameter space Θ
• selectionalFactor(θ)
• scenarioFactor(θ)

We construct an LU-RSA scenario with:

• Lexica Λ = {L_θ | θ ∈ Θ}
• Lexicon prior P(L_θ) ∝ selectionalFactor(θ) × scenarioFactor(θ)

Backward Direction: LU-RSA → SDS

Given an LU-RSA scenario with:

• Lexica Λ with prior P(L)

We construct an SDS system with:

• Parameters = Λ
• selectionalFactor(L) = 1 (trivial)
• scenarioFactor(L) = P(L)

This shows SDS generalizes LU-RSA by factoring the prior.

def Semantics.Probabilistic.SDS.Marginalization.sdsToLexiconPrior {α : Type u_1} {Θ : Type u_2} [Core.SDSConstraintSystem α Θ] (sys : α) (θ : Θ) : ℚ

The lexicon prior induced by an SDS system.

P(L_θ) ∝ selectionalFactor(θ) × scenarioFactor(θ)

This is the Product of Experts combination encoded as a single prior.

Equations

• Semantics.Probabilistic.SDS.Marginalization.sdsToLexiconPrior sys θ = Semantics.Probabilistic.SDS.Core.SDSConstraintSystem.unnormalizedPosterior sys θ

theorem Semantics.Probabilistic.SDS.Marginalization.sds_to_lursa_marginal_equiv {α : Type u_1} {Θ : Type u_2} [Core.SDSConstraintSystem α Θ] (sys : α) (pred : Θ → Bool) : Core.SDSConstraintSystem.softTruth sys pred = Core.SDSConstraintSystem.posteriorProb sys pred

Theorem: SDS marginal equals LU-RSA marginal with induced prior.

For any SDS system, the soft truth computed via SDS machinery equals the posterior probability in the induced LU-RSA scenario.

structure Semantics.Probabilistic.SDS.Marginalization.LURSAInducedSDS (U W : Type) : Type

Convert an LU-RSA lexicon to an SDS parameter.

Each lexicon L becomes a parameter in the SDS parameter space.

• lexica : List (Lexicon U W)

  The lexica as parameters

• lexPrior : Lexicon U W → ℚ

  Prior over lexica

instance Semantics.Probabilistic.SDS.Marginalization.instSDSConstraintSystemLURSAInducedSDSLexicon {U W : Type} : Core.SDSConstraintSystem (LURSAInducedSDS U W) (Lexicon U W)

LU-RSA scenarios induce SDS systems with trivial selectional factors.

When we view LU-RSA through the SDS lens:

• Parameters = lexica
• selectionalFactor = 1 (trivial/uniform)
• scenarioFactor = P(L) (the lexicon prior)

This shows that LU-RSA is a special case of SDS where the selectional factor is uninformative.

Equations

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

theorem Semantics.Probabilistic.SDS.Marginalization.lursa_trivial_selectional {U W : Type} (ind : LURSAInducedSDS U W) (L : Lexicon U W) : Core.SDSConstraintSystem.selectionalFactor ind L = 1

LU-RSA has trivial selectional factors when viewed as Semantics.Probabilistic.SDS.

theorem Semantics.Probabilistic.SDS.Marginalization.lursa_to_sds_exists (S : LUScenario) : ∃ (sds : LURSAInducedSDS S.Utterance S.World), sds.lexica = S.lexica ∧ sds.lexPrior = S.lexPrior

Theorem: Every LU-RSA scenario can be represented as an SDS system.

Given an LU-RSA scenario with lexicon prior P(L), we construct an SDS system where scenarioFactor = P(L) and selectionalFactor = 1.

theorem Semantics.Probabilistic.SDS.Marginalization.sds_trivial_selectional_reduces {U W : Type} (ind : LURSAInducedSDS U W) (L : Lexicon U W) : Core.SDSConstraintSystem.unnormalizedPosterior ind L = ind.lexPrior L

SDS with trivial selectional factors is equivalent to unfactored prior.

When selectionalFactor(θ) = 1 for all θ, the SDS posterior reduces to just the scenario factor (normalized).

SDS Extends LU-RSA with Factored Priors

The core difference between SDS and LU-RSA:

LU-RSA: P(L) is a single, opaque prior distribution

SDS: P(θ) = selectionalFactor(θ) × scenarioFactor(θ) is factored

This factorization provides:

1. Interpretability: We can see why a parameter is preferred
2. Modularity: Factors can be learned/specified independently
3. Conflict detection: When factors disagree, we can detect ambiguity
4. Compositionality: Selectional factors can come from compositional semantics

Examples

"The astronomer married the star"

SDS factorization:

• selectional(CELEBRITY) = 0.9 (MARRY wants human)
• selectional(CELESTIAL) = 0.1
• scenario(CELEBRITY) = 0.1 (ASTRONOMY frame)
• scenario(CELESTIAL) = 0.9

Product: P(CELEBRITY) ∝ 0.09, P(CELESTIAL) ∝ 0.09 → TIE → pun!

Plain LU-RSA would need to stipulate P(L_celebrity) = P(L_celestial) without explaining why.

def Semantics.Probabilistic.SDS.Marginalization.sdsConflictImpliesAmbiguity {α : Type u_1} {Θ : Type u_2} [Core.SDSConstraintSystem α Θ] [BEq Θ] (sys : α) : Bool

SDS can detect conflicts that LU-RSA cannot.

A conflict occurs when selectional and scenario factors prefer different values. This predicts puns, zeugma, and pragmatic ambiguity.

Equations

• Semantics.Probabilistic.SDS.Marginalization.sdsConflictImpliesAmbiguity sys = Semantics.Probabilistic.SDS.Core.hasConflict sys

Formal Bidirectional Translation Theorems

We prove that SDS and LU-RSA are intertranslatable, establishing a formal correspondence between the frameworks.

structure Semantics.Probabilistic.SDS.Marginalization.SDSPackage : Type 1

Structure representing an SDS system packaged for translation to LU-RSA.

• System : Type

  System type

• Param : Type

  Parameter type

• inst : Core.SDSConstraintSystem self.System self.Param

  The SDS instance

• sys : self.System

  A concrete system value

structure Semantics.Probabilistic.SDS.Marginalization.LURSAPackage : Type 1

Structure representing an LU-RSA scenario packaged for translation to Semantics.Probabilistic.SDS.

• U : Type

  Utterance type

• W : Type

  World type

• lexica : List (Lexicon self.U self.W)

  Lexica

• prior : Lexicon self.U self.W → ℚ

  Prior

def Semantics.Probabilistic.SDS.Marginalization.sdsToLURSA (pkg : SDSPackage) [DecidableEq pkg.Param] : LURSAPackage

Forward translation: SDS → LU-RSA

Every SDS system induces an equivalent LU-RSA structure where the lexicon prior encodes the Product of Experts combination.

Note: This requires DecidableEq on the parameter type for the indicator function in the lexicon meaning.

Equations

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

def Semantics.Probabilistic.SDS.Marginalization.lursaToSDS (pkg : LURSAPackage) : SDSPackage

Backward translation: LU-RSA → SDS

Every LU-RSA scenario is an SDS system with trivial selectional factors.

Equations

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

theorem Semantics.Probabilistic.SDS.Marginalization.lursa_sds_roundtrip_prior (pkg : LURSAPackage) (L : Lexicon pkg.U pkg.W) : let sds := lursaToSDS pkg; Core.SDSConstraintSystem.unnormalizedPosterior sds.sys L = pkg.prior L

Round-trip property: LU-RSA → SDS → LU-RSA preserves the prior structure.

When we translate an LU-RSA scenario to SDS and back, the lexicon prior is preserved (up to the trivial selectional factor).

Scale Structure from SDS Perspective

The Bigness Generalization follows from SDS structure:

Positive adjectives (big)

• min{d : big(d)} = θ_big > 0
• SDS selectional factor is substantive: 1_{measure ≥ θ_big} for positive θ

Negative adjectives (small)

• min{d : small(d)} = d₀ = 0 (scale minimum)
• SDS selectional factor is vacuous: 1_{measure ≥ 0} = 1 always!

This is why "small idiot" doesn't work: the selectional constraint is always satisfied, providing no information.

theorem Semantics.Probabilistic.SDS.Marginalization.positive_scale_substantive (θ : ℚ) (hθ : θ > 0) : ∃ (x : ℚ), ¬x ≥ θ

For positive adjectives, the minimum threshold is positive. This yields a substantive selectional constraint.

theorem Semantics.Probabilistic.SDS.Marginalization.negative_scale_vacuous (x : ℚ) : 0 ≤ x → x ≥ 0

For negative adjectives, the minimum threshold is 0. This yields a vacuous selectional constraint (always satisfied).

Summary: SDS ↔ LU-RSA Correspondence

Bidirectional Translation

1. SDS → LU-RSA (sdsToLURSA): Every SDS system induces an LU-RSA scenario where the lexicon prior is the Product of Experts of selectional × scenario.

2. LU-RSA → SDS (lursaToSDS): Every LU-RSA scenario is an SDS system where selectionalFactor = 1 (trivial) and scenarioFactor = P(L).

Theorems

• sds_to_lursa_marginal_equiv: SDS soft truth = SDS posterior probability
• lursa_to_sds_exists: Every LU-RSA scenario is representable as SDS
• lursa_trivial_selectional: LU-RSA has trivial selectional factors
• sds_trivial_selectional_reduces: Trivial selectional → unfactored prior
• lursa_sds_roundtrip_prior: Round-trip preserves prior structure

What SDS Adds

SDS extends LU-RSA with factored priors:

• P(θ) = selectional(θ) × scenario(θ)
• Enables conflict detection
• Provides interpretability
• Supports compositional derivation of selectional factors

Connection to Other Modules

• BayesianSemantics.ParamPred: SDS is ParamPred with factored priors
• ThresholdSemantics: All three domains are SDS instances
• SDSandRSA: This module extends that correspondence formally