def Semantics.Probabilistic.SDS.ThresholdInstances.thresholdRange : List ℚ

Discretized threshold range: [0, 1/10, 2/10,..., 1]

This provides finite support for marginalization over threshold values.

Equations

• Semantics.Probabilistic.SDS.ThresholdInstances.thresholdRange = [0, 1 / 10, 2 / 10, 3 / 10, 4 / 10, 5 / 10, 6 / 10, 7 / 10, 8 / 10, 9 / 10, 1]

Gradable Adjectives as SDS

@cite{lassiter-goodman-2017} @cite{tessler-goodman-2019}

For a gradable adjective like "tall":

• Param: threshold values θ ∈ [0,1]
• Selectional: indicator 1_{measure(x) ≥ θ} (which thresholds x satisfies)
• Scenario: P(θ) the threshold prior from context

The soft meaning E[1_{height(x) ≥ θ}] emerges from marginalization.

structure Semantics.Probabilistic.SDS.ThresholdInstances.AdjWithEntity (E : Type) : Type

Entity-instantiated gradable adjective for Semantics.Probabilistic.SDS.

We curry the entity into the system so that selectional factors can depend on it.

• adj : ThresholdSemantics.GradableAdjective E

  The underlying adjective

• entity : E

  The entity being predicated of

instance Semantics.Probabilistic.SDS.ThresholdInstances.instSDSConstraintSystemAdjWithEntityRat {E : Type} : Core.SDSConstraintSystem (AdjWithEntity E) ℚ

Equations

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

def Semantics.Probabilistic.SDS.ThresholdInstances.adjToSDS {E : Type} (adj : ThresholdSemantics.GradableAdjective E) (x : E) : AdjWithEntity E

Create an SDS system from an adjective and entity

Equations

• Semantics.Probabilistic.SDS.ThresholdInstances.adjToSDS adj x = { adj := adj, entity := x }

Generics as SDS

For a generic like "Birds fly":

• Param: threshold values θ ∈ [0,1] over prevalence
• Selectional: indicator 1_{prevalence ≥ θ} (which thresholds the prevalence satisfies)
• Scenario: P(θ) the threshold prior (varies by property type)

The soft truth emerges from marginalizing over the uncertain threshold.

instance Semantics.Probabilistic.SDS.ThresholdInstances.instSDSConstraintSystemGenericPredicateRat : Core.SDSConstraintSystem ThresholdSemantics.GenericPredicate ℚ

Equations

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

Gradable Nouns as SDS (Degenerate Case)

For a gradable noun like "big idiot":

• Param: threshold values (but only one is active)
• Selectional: delta function at the compositionally-determined threshold
• Scenario: trivial (constant 1) - no contextual uncertainty

This is a degenerate SDS where there's no marginalization - the threshold is fixed by the size adjective's scale structure.

instance Semantics.Probabilistic.SDS.ThresholdInstances.instSDSConstraintSystemGradableNounWithSizeRat {E : Type} : Core.SDSConstraintSystem (ThresholdSemantics.GradableNounWithSize E) ℚ

Equations

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

theorem Semantics.Probabilistic.SDS.ThresholdInstances.gradable_noun_uniform_scenario {E : Type} (gn : ThresholdSemantics.GradableNounWithSize E) : Core.hasUniformScenario gn = true

Gradable nouns have trivial (uniform) scenario factors. This captures the key difference from adjectives/generics.

def Semantics.Probabilistic.SDS.ThresholdInstances.adjSoftMeaningSDS {E : Type} (adj : ThresholdSemantics.GradableAdjective E) (x : E) : ℚ

Compute soft meaning for an adjective via SDS marginalization.

This shows the SDS machinery reproduces the expected soft meaning.

Equations

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

def Semantics.Probabilistic.SDS.ThresholdInstances.genericSoftTruthSDS (gen : ThresholdSemantics.GenericPredicate) : ℚ

Compute soft truth for a generic via SDS marginalization.

Equations

• Semantics.Probabilistic.SDS.ThresholdInstances.genericSoftTruthSDS gen = Semantics.Probabilistic.SDS.Core.SDSConstraintSystem.softTruth gen fun (θ : ℚ) => decide (gen.prevalence ≥ θ)

def Semantics.Probabilistic.SDS.ThresholdInstances.gnHoldsSDS {E : Type} (gn : ThresholdSemantics.GradableNounWithSize E) (x : E) : Bool

Compute holds for a gradable noun via Semantics.Probabilistic.SDS.

Since the scenario is trivial and support is a single point, this reduces to a simple Boolean check.

Equations

• Semantics.Probabilistic.SDS.ThresholdInstances.gnHoldsSDS gn x = decide (gn.nounMeasure x ≥ max gn.sizeThreshold gn.nounStandard)

The Bigness Generalization

@cite{morzycki-2009} shows why "big idiot" works but "small idiot" doesn't. This follows from scale structure:

• Positive adjectives (big): min{d : big(d)} = θ_big > 0 (substantive)
• Negative adjectives (small): min{d : small(d)} = d₀ = 0 (vacuous)

In SDS terms:

• Positive → selectional factor is substantive (threshold > 0)
• Negative → selectional factor is vacuous (threshold = 0, always satisfied)

def Semantics.Probabilistic.SDS.ThresholdInstances.isPositiveSizeAdj (adjName : String) : Bool

Positive size adjective has positive threshold

Equations

• Semantics.Probabilistic.SDS.ThresholdInstances.isPositiveSizeAdj adjName = decide (adjName ∈ ["big", "huge", "enormous", "large", "gigantic"])

def Semantics.Probabilistic.SDS.ThresholdInstances.isNegativeSizeAdj (adjName : String) : Bool

Negative size adjective has zero threshold (vacuous)

Equations

• Semantics.Probabilistic.SDS.ThresholdInstances.isNegativeSizeAdj adjName = decide (adjName ∈ ["small", "tiny", "minuscule", "little"])

theorem Semantics.Probabilistic.SDS.ThresholdInstances.positive_adj_substantive_threshold {E : Type} (gn : ThresholdSemantics.GradableNounWithSize E) (_hpos : isPositiveSizeAdj gn.sizeAdj = true) (hthresh : gn.sizeThreshold > 0) : max gn.sizeThreshold gn.nounStandard > 0

For positive size adjectives, the SDS threshold is substantive (> 0).

Summary

This module establishes:

Instances

1. AdjWithEntity E is an SDSConstraintSystem _ ℚ
2. GenericPredicate is an SDSConstraintSystem _ ℚ
3. GradableNounWithSize E is an SDSConstraintSystem _ ℚ

Key Operations

• adjToSDS: Convert adjective + entity to SDS system
• adjSoftMeaningSDS: Compute soft meaning via SDS marginalization
• genericSoftTruthSDS: Compute generic soft truth via SDS
• gnHoldsSDS: Compute gradable noun truth via SDS

Theorems

• threshold_domains_are_sds: All three domains are SDS instances
• gradable_noun_uniform_scenario: Gradable nouns have trivial scenario factors

Design Decision: Entity Currying

For gradable adjectives, we curry the entity into an AdjWithEntity structure. This allows the selectional factor to depend on entity features (measure value).

Alternative: Have selectionalFactor : α → Entity → Θ → ℚ We chose currying to keep the typeclass simpler.