class Semantics.Probabilistic.SDS.Core.SDSConstraintSystem (α : Type u_1) (Θ : outParam (Type u_2)) : Type (max u_1 u_2)

A constraint system in the style of Situation Description Systems (SDS).

The core pattern: given an entity and context, we marginalize over a parameter space, combining selectional (entity-dependent) and scenario (context-dependent) factors via Product of Experts.

Type Parameters

• α: The system type (e.g., GradableAdjective E, Concept)
• Θ: The parameter space being marginalized over

Fields

• paramSupport: Finite support for marginalization
• selectionalFactor: Entity-dependent factor P(θ | entity features)
• scenarioFactor: Context-dependent factor P(θ | scenario/frame)

Key Operations

The unnormalized posterior at parameter θ is:

posterior(θ) = selectionalFactor(θ) × scenarioFactor(θ)

The normalized posterior divides by the sum over all θ in support.

• paramSupport : α → List Θ

  Support for the parameter space (for finite marginalization)

• selectionalFactor : α → Θ → ℚ

  The selectional component: entity-dependent factor

• scenarioFactor : α → Θ → ℚ

  The scenario component: context-dependent factor

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

Unnormalized posterior at a given parameter value.

This is the Product of Experts combination: posterior(θ) = selectionalFactor(θ) × scenarioFactor(θ)

Equations

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

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

Partition function (normalizing constant) for the posterior.

Z = Σ_θ selectionalFactor(θ) × scenarioFactor(θ)

Equations

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

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

Normalized posterior probability at a given parameter value.

P(θ | sys) = unnormalizedPosterior(θ) / Z

Returns 0 if Z = 0 (degenerate case).

Equations

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

def Semantics.Probabilistic.SDS.Core.SDSConstraintSystem.expectation {α : Type u_1} {Θ : Type u_2} [SDSConstraintSystem α Θ] (sys : α) (f : Θ → ℚ) : ℚ

Expected value of a function under the normalized posterior.

E[f] = Σ_θ P(θ | sys) × f(θ)

Equations

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

def Semantics.Probabilistic.SDS.Core.SDSConstraintSystem.posteriorProb {α : Type u_1} {Θ : Type u_2} [SDSConstraintSystem α Θ] (sys : α) (pred : Θ → Bool) : ℚ

Probability that a predicate holds under the posterior.

P(pred) = E[1_pred]

Equations

• Semantics.Probabilistic.SDS.Core.SDSConstraintSystem.posteriorProb sys pred = Semantics.Probabilistic.SDS.Core.SDSConstraintSystem.expectation sys fun (θ : Θ) => if pred θ = true then 1 else 0

theorem Semantics.Probabilistic.SDS.Core.SDSConstraintSystem.poe_commutative {α : Type u_1} {Θ : Type u_2} [SDSConstraintSystem α Θ] (sys : α) (θ : Θ) : selectionalFactor sys θ * scenarioFactor sys θ = scenarioFactor sys θ * selectionalFactor sys θ

Product of Experts is commutative: order of factors doesn't matter.

theorem Semantics.Probabilistic.SDS.Core.SDSConstraintSystem.poe_zero_selectional {α : Type u_1} {Θ : Type u_2} [SDSConstraintSystem α Θ] (sys : α) (θ : Θ) (h : selectionalFactor sys θ = 0) : unnormalizedPosterior sys θ = 0

Zero-absorbing: if either factor is zero, the posterior is zero.

theorem Semantics.Probabilistic.SDS.Core.SDSConstraintSystem.poe_zero_scenario {α : Type u_1} {Θ : Type u_2} [SDSConstraintSystem α Θ] (sys : α) (θ : Θ) (h : scenarioFactor sys θ = 0) : unnormalizedPosterior sys θ = 0

def Semantics.Probabilistic.SDS.Core.SDSConstraintSystem.softTruth {α : Type u_1} {Θ : Type u_2} [SDSConstraintSystem α Θ] (sys : α) (holds : Θ → Bool) : ℚ

Soft truth value: probability that a threshold-based predicate holds.

For threshold semantics, this computes: E[1_{measure(x) ≥ θ}] under the posterior over θ

This is the key connection: threshold uncertainty yields soft/graded meanings.

Equations

• Semantics.Probabilistic.SDS.Core.SDSConstraintSystem.softTruth sys holds = Semantics.Probabilistic.SDS.Core.SDSConstraintSystem.posteriorProb sys holds

def Semantics.Probabilistic.SDS.Core.SDSConstraintSystem.marginal {α : Type u_1} {Θ : Type u_2} [SDSConstraintSystem α Θ] (sys : α) (project : Θ → ℚ) : ℚ

Marginal over parameter space.

Returns the distribution over some property computed from θ. For SDS, this is how soft meanings emerge from Boolean semantics + uncertainty.

Equations

• Semantics.Probabilistic.SDS.Core.SDSConstraintSystem.marginal sys project = Semantics.Probabilistic.SDS.Core.SDSConstraintSystem.expectation sys project

def Semantics.Probabilistic.SDS.Core.listArgmax {α : Type u_1} (xs : List α) (f : α → ℚ) : Option α

Find the element with maximum value according to a scoring function.

Equations

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

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

Detect when selectional and scenario factors disagree.

A conflict occurs when the argmax of each factor differs. This is useful for predicting ambiguity, puns, and zeugma.

Equations

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

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

Get the degree of conflict between factors.

Measures how different the expert preferences are.

Equations

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

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

Posterior uncertainty as Gini impurity: 1 - Σ_θ P(θ)².

For a two-concept system, ranges from 0 (one concept has probability 1) to 0.5 (uniform 50/50). For a k-concept uniform distribution, equals (k-1)/k. Captures "how spread out is the posterior" without requiring real-valued logarithms.

Equations

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

def Semantics.Probabilistic.SDS.Core.isTied {α : Type u_1} {Θ : Type u_2} [SDSConstraintSystem α Θ] (sys : α) (θ₁ θ₂ : Θ) (tolerance : ℚ := 1 / 10) : Bool

Two parameter values are tied under the posterior if their normalized posteriors are within tolerance of each other (default 1/10).

Equations

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

theorem Semantics.Probabilistic.SDS.Core.hasConflict_iff_different_argmax {α : Type u_1} {Θ : Type u_2} [SDSConstraintSystem α Θ] [BEq Θ] (sys : α) : hasConflict sys = true ↔ ∃ (θ₁ : Θ), ∃ (θ₂ : Θ), listArgmax (SDSConstraintSystem.paramSupport sys) (SDSConstraintSystem.selectionalFactor sys) = some θ₁ ∧ listArgmax (SDSConstraintSystem.paramSupport sys) (SDSConstraintSystem.scenarioFactor sys) = some θ₂ ∧ (θ₁ != θ₂) = true

Substrate property: hasConflict is true exactly when the selectional and scenario factors have different argmax elements (and both argmaxes exist).

This is the formal content of "selectional and scenario disagree on which parameter to prefer." Polymorphic over any SDSConstraintSystem; the DisambiguationScenario case (the paper's bat/star/port examples) is the intended consumer.

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

A degenerate SDS where the scenario factor is uniform (no context dependence).

This captures cases like gradable nouns where the threshold is compositionally determined rather than contextually inferred.

Equations

• Semantics.Probabilistic.SDS.Core.trivialScenario sys θ = decide (Semantics.Probabilistic.SDS.Core.SDSConstraintSystem.scenarioFactor sys θ = 1)

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

Check if all scenario factors are trivial (constant 1).

Equations

• Semantics.Probabilistic.SDS.Core.hasUniformScenario sys = (Semantics.Probabilistic.SDS.Core.SDSConstraintSystem.paramSupport sys).all (Semantics.Probabilistic.SDS.Core.trivialScenario sys)

Relationship to PMF.productOfExperts

The SDSConstraintSystem typeclass implements the SDS-specific selectional × scenario product factorization, with unnormalizedPosterior giving the multiplicative joint score and normalizedPosterior doing the explicit ℚ-valued normalization. For the canonical mathlib mechanism (PMF-typed, ENNReal-valued, with measure-theoretic foundation), see Mathlib.Probability.ProbabilityMassFunction.Constructions (PMF.normalize) and Core/Probability/Posterior.lean (PMF.productOfExperts, PMF.posterior). The SDS typeclass favors decidable ℚ computation for study-file replications; PMF is canonical for general probability work.

Summary

This module provides:

Core Typeclass

• SDSConstraintSystem α Θ: Any domain with factored constraints over parameters

Operations

• unnormalizedPosterior: Product of Experts combination
• normalizedPosterior: Normalized distribution over parameters
• expectation: Expected value under posterior
• softTruth: Soft meaning via marginalization

Utilities

• hasConflict: Detect when factors disagree (predicts ambiguity)
• conflictDegree: Quantify disagreement between factors
• posteriorUncertainty: Gini impurity of the posterior
• isTied: Two parameter values tied within a tolerance
• hasUniformScenario: Check for degenerate/trivial scenario factors

Substrate theorems

• hasConflict_iff_different_argmax: hasConflict is true iff selectional/scenario argmaxes differ

Insight

SDS unifies many linguistic phenomena under a common computational pattern:

• Gradable adjectives (threshold uncertainty)
• Generics (prevalence threshold uncertainty)
• Concept disambiguation (concept uncertainty)
• Lexical uncertainty RSA (lexicon uncertainty)

All share: Boolean semantics + parameter uncertainty = soft/graded meanings

structure Semantics.Probabilistic.SDS.Core.DisambiguationScenario (C : Type) : Type

A disambiguation scenario with selectional and scenario constraints.

This is the standard SDS setup from @cite{erk-herbelot-2024}: an ambiguous word in context, with a selectional factor (from the governing predicate) and a scenario factor (from the activated frame/script).

• word : String

  Name of the ambiguous word

• context : String

  Context sentence

• selectional : C → ℚ

  Selectional constraint (from predicate)

• scenario : C → ℚ

  Scenario constraint (from frame/context words)

• concepts : List C

  Support (list of concepts)

@[implicit_reducible]

instance Semantics.Probabilistic.SDS.Core.instSDSConstraintSystemDisambiguationScenario {C : Type} : SDSConstraintSystem (DisambiguationScenario C) C

Equations

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

structure Semantics.Probabilistic.SDS.Core.ConceptFeature (Concept : Type u_1) (Feature : Type u_2) : Type (max u_1 u_2)

Concept-associated features, following @cite{mcrae-etal-2005}.

Each concept has features with associated probabilities. For example, BAT-ANIMAL has features like flies (prob 1.0), is_black (prob 0.75). These features can be projected back into DRS conditions after disambiguation.

• featureProb : Concept → Feature → ℚ

  P(feature | concept) — probability of feature given concept

def Semantics.Probabilistic.SDS.Core.ConceptFeature.projectFeature {α : Type u_1} {Concept : Type u_2} {Feature : Type u_3} [SDSConstraintSystem α Concept] (cf : ConceptFeature Concept Feature) (sys : α) (f : Feature) : ℚ

Project a feature through the posterior over concepts.

Given a posterior distribution over concepts and concept-feature associations, compute the posterior probability of a feature:

P(feature | context) = Σ_c P(feature | c) × P(c | context)

This is the mechanism by which disambiguation affects truth conditions: features inferred from the winning concept become DRS conditions.

Equations

• cf.projectFeature sys f = Semantics.Probabilistic.SDS.Core.SDSConstraintSystem.expectation sys fun (c : Concept) => cf.featureProb c f