SDSMeasureSystem Design

@cite{lassiter-goodman-2017}

A measure-theoretic SDS constraint system would be the continuous analogue of SDSConstraintSystem, where:

• The parameter space Θ has a measurable structure
• Factors are measurable functions
• Marginalization uses integration instead of summation

Planned Type Parameters

• α: The system type
• Θ: The parameter space (must be a MeasurableSpace)

Key Differences from Discrete SDS

Discrete SDS	Measure SDS
List Θ support	MeasurableSpace Θ
foldl (+)	∫ dμ
ℚ values	ℝ≥0∞ or ℝ values
Exact computation	May need numerical methods

Planned Interface

class SDSMeasureSystem (α : Type*) (Θ : Type*) [MeasurableSpace Θ] where
  selectionalDensity : α → Θ → ℝ≥0∞
  scenarioDensity : α → Θ → ℝ≥0∞
  baseMeasure : α → Measure Θ
  selectional_measurable : ∀ sys, Measurable (selectionalDensity sys)
  scenario_measurable : ∀ sys, Measurable (scenarioDensity sys)

Embedding Discrete into Continuous

Any discrete SDSConstraintSystem can be viewed as an SDSMeasureSystem where the base measure is a sum of Dirac deltas:

μ_discrete = Σ_{θ ∈ support} δ_θ

This makes the integral reduce to a sum:

∫ f dμ_discrete = Σ_{θ ∈ support} f(θ)

Planned Theorems

/-- Embed a discrete SDS into the measure-theoretic framework -/
noncomputable def discreteToMeasure [SDSConstraintSystem α Θ] (sys : α) : Measure Θ

/-- For discrete systems, integration equals summation -/
theorem discrete_integral_eq_sum [SDSConstraintSystem α Θ] (sys : α) (f : Θ → ℚ) :
    ∫ f dμ = (paramSupport sys).sum f

Continuous Gradable Adjectives

For gradable adjectives with continuous threshold semantics:

• Parameter space: Θ = [0, 1] ⊂ ℝ (unit interval)
• Base measure: Lebesgue measure (or a prior density)
• Selectional: 1_{measure(x) ≥ θ} (indicator function)
• Scenario: P(θ | context) (threshold prior density)

The soft meaning becomes:

⟦tall⟧(x) = ∫₀¹ 1_{height(x) ≥ θ} · p(θ) dθ
          = ∫₀^{height(x)} p(θ) dθ
          = P(θ < height(x))

For uniform prior p(θ) = 1, this gives ⟦tall⟧(x) = height(x).

Result

With uniform threshold prior:

• softMeaning(x) = measure(x)

This elegantly derives graded meanings from Boolean semantics + uncertainty.

structure Semantics.Probabilistic.SDS.MeasureTheory.ContinuousAdjective (E : Type u_1) : Type u_1

Continuous gradable adjective with real-valued measure and threshold. (Simplified placeholder - full version would use Mathlib measures)

• name : String

  Name of the adjective

• measure : E → ℚ

  Measure function mapping entities to [0,1]

• thresholdPrior : ℚ → ℚ

  Threshold prior (discretized for now)

• measure_unit (x : E) : 0 ≤ self.measure x ∧ self.measure x ≤ 1

  Measure is in [0,1]

def Semantics.Probabilistic.SDS.MeasureTheory.ContinuousAdjective.softMeaning {E : Type u_1} (adj : ContinuousAdjective E) (x : E) : ℚ

Soft meaning via marginalization (discrete approximation).

For uniform prior, this equals the measure value.

Equations

• adj.softMeaning x = adj.measure x

Bridge to Mathlib's PMF

For finite/countable parameter spaces, we can use Mathlib's PMF type which provides:

• Guaranteed sum-to-one property
• Expectation and variance
• Conditioning operations

The discrete SDSConstraintSystem can produce a PMF via normalization.

Planned Interface

/-- Convert discrete SDS posterior to Mathlib PMF -/
noncomputable def discreteToPMF [SDSConstraintSystem α Θ] [Fintype Θ]
    (sys : α) (hZ : partitionFunction sys ≠ 0) : PMF Θ

/-- PMF expectation equals SDS expectation -/
theorem pmf_expect_eq_sds [SDSConstraintSystem α Θ]
    (sys : α) (f : Θ → ℚ) :
    (discreteToPMF sys hZ).expectation f = SDSConstraintSystem.expectation sys f

Information-Theoretic Extensions

With measure-theoretic foundations, we can define:

Entropy of SDS Posterior

H[P] = -∫ p(θ) log p(θ) dθ

KL Divergence between Factors

D_KL(selectional || scenario) = ∫ sel(θ) log(sel(θ)/scen(θ)) dθ

Mutual Information

I(X; Θ) for entity X and parameter Θ

These connect to:

• Zaslavsky et al. rate-distortion analysis
• Information-theoretic pragmatics
• Efficient communication theories

See RSA.Extensions.InformationTheory for discrete versions.

Summary: Measure-Theoretic SDS

What This Module Will Provide (When Implemented)

1. SDSMeasureSystem: Continuous analogue of SDSConstraintSystem
2. Integration-based marginalization: Replace sums with integrals
3. Embedding theorem: Discrete SDS embeds into continuous
4. Continuous threshold semantics: Real-valued thresholds with densities

Planned Key Types

Type	Purpose
SDSMeasureSystem α Θ	Continuous SDS with measures
ContinuousAdjective E	Gradable adj with real threshold
posteriorMeasure	Normalized posterior as a measure

Required Mathlib Dependencies

• MeasureTheory.Measure.ProbabilityMeasure
• Probability.ProbabilityMassFunction.Basic
• MeasureTheory.Integral.Bochner

Implementation Status

This is a placeholder module. Full implementation requires:

1. Careful handling of measurability conditions
2. Integrability proofs for densities
3. Numerical integration for computation
4. Connection to existing RSA measure-theoretic work

Future Directions

1. Implement continuous threshold semantics fully
2. Add entropy/KL divergence for SDS
3. Connect to rate-distortion framework
4. Numerical computation via Mathlib's analysis