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.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 Core.ProductOfExperts

The SDSConstraintSystem typeclass is conceptually equivalent to Core.ProductOfExperts.FactoredDist, but with key differences:

1. Typeclass vs Structure: SDS uses a typeclass for instance inference, allowing automatic derivation of operations for any type that provides the selectional/scenario factors.

2. Universe Polymorphism: SDS is fully universe-polymorphic (Type*), while FactoredDist uses Type.

3. Instance Pattern: SDS supports instantiation at different entity types (e.g., SDSConstraintSystem (AdjWithEntity E) ℚ for any E).

For types where both apply, the underlying computation is identical:

• unnormalizedPosterior = FactoredDist.unnormScores
• normalizedPosterior = FactoredDist.combine
• hasConflict uses the same argmax-based detection

See Core.ProductOfExperts for the standalone PoE combinators.

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
• hasUniformScenario: Check for degenerate/trivial scenario factors

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)

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