structure Semantics.Montague.BayesianSemantics.ThresholdPred (E : Type u_1) (Θ : Type u_2) [Fintype Θ] [Preorder Θ] : Type (max u_1 u_2)

A threshold predicate: "x has property P iff measure(x) > θ"

This models gradable adjectives like "tall", "expensive", etc.

• measure : E → Θ

  The measure function (e.g., height, price)

• thresholdPrior : Core.FinitePMF Θ

  Prior over thresholds

def Semantics.Montague.BayesianSemantics.ThresholdPred.toParamPred {E : Type u_1} {Θ : Type u_2} [Fintype Θ] [Preorder Θ] [DecidableRel fun (x1 x2 : Θ) => x1 < x2] (pred : ThresholdPred E Θ) : Probabilistic.ParamPred.ParamPred E Θ

Convert to a parameterized predicate

Equations

• pred.toParamPred = { semantics := fun (θ : Θ) (x : E) => decide (pred.measure x > θ), prior := pred.thresholdPrior }

def Semantics.Montague.BayesianSemantics.ThresholdPred.gradedTruth {E : Type u_1} {Θ : Type u_2} [Fintype Θ] [Preorder Θ] [DecidableRel fun (x1 x2 : Θ) => x1 < x2] (pred : ThresholdPred E Θ) (x : E) : ℚ

Graded truth for threshold predicates

Equations

• pred.gradedTruth x = pred.toParamPred.gradedTruth x

theorem Semantics.Montague.BayesianSemantics.ThresholdPred.gradedTruth_eq_prob {E : Type u_1} {Θ : Type u_2} [Fintype Θ] [DecidableEq Θ] [Preorder Θ] [DecidableRel fun (x1 x2 : Θ) => x1 < x2] (pred : ThresholdPred E Θ) (x : E) : pred.gradedTruth x = pred.thresholdPrior.prob fun (θ : Θ) => decide (pred.measure x > θ)

Graded truth equals probability that measure > threshold.

For "tall(John)": P(height(John) > θ) under the threshold prior.

structure Semantics.Montague.BayesianSemantics.FeaturePred (E : Type u_1) (n : ℕ) : Type (max u_1 (u_2 + 1))

A feature-based predicate where entities are characterized by features and the predicate is a linear classifier.

Entity satisfaction: bias + Σᵢ weight_i · feature_i(x) > 0

This models the Bernardy et al. approach where predicates are hyperplanes.

• features : E → Fin n → ℚ

  Extract feature vector from entity

• params : Type u_2

  Predicate parameters: bias and weights

• paramsFintype : Fintype self.params

  Fintype instance for params

• paramsDecEq : DecidableEq self.params
• bias : self.params → ℚ

  Bias for each parameter setting

• weights : self.params → Fin n → ℚ

  Weights for each parameter setting

• prior : Core.FinitePMF self.params

  Prior over parameters

def Semantics.Montague.BayesianSemantics.FeaturePred.dotProduct {n : ℕ} (w f : Fin n → ℚ) : ℚ

Dot product of weight vector and feature vector

Equations

• Semantics.Montague.BayesianSemantics.FeaturePred.dotProduct w f = ∑ i : Fin n, w i * f i

def Semantics.Montague.BayesianSemantics.FeaturePred.satisfies {E : Type u_1} {n : ℕ} (pred : FeaturePred E n) (p : pred.params) (x : E) : Bool

Boolean semantics for a specific parameter setting

Equations

• pred.satisfies p x = decide (pred.bias p + Semantics.Montague.BayesianSemantics.FeaturePred.dotProduct (pred.weights p) (pred.features x) > 0)

def Semantics.Montague.BayesianSemantics.FeaturePred.toParamPred {E : Type u_1} {n : ℕ} (pred : FeaturePred E n) : Probabilistic.ParamPred.ParamPred E pred.params

Convert to parameterized predicate

Equations

• pred.toParamPred = { semantics := pred.satisfies, prior := pred.prior }

def Semantics.Montague.BayesianSemantics.FeaturePred.gradedTruth {E : Type u_1} {n : ℕ} (pred : FeaturePred E n) (x : E) : ℚ

Graded truth emerges from parameter uncertainty

Equations

• pred.gradedTruth x = pred.toParamPred.gradedTruth x

Compositional Structure

@cite{bernardy-blanck-chatzikyriakidis-lappin-2018}

Two Strategies

1. Marginalize early (GradedProposition.lean):

   • Convert to graded values immediately
   • Compose using probabilistic operations (×, +−pq)
   • Algebraic structure (De Morgan, etc.)

2. Marginalize late (this module):

   • Keep Boolean semantics during composition
   • Parameter uncertainty tracked but not resolved
   • Graded values emerge only when needed

3. Probability monad (Grove's PDS):

   • Standard compositional semantics
   • Probability as monadic effect
   • Compiles to probabilistic programs

Strategy #3 is most principled but requires more infrastructure. This module implements #2 as an intermediate step.