The Probability Monad

@cite{lassiter-goodman-2017}

We define P α abstractly as a structure with pure and bind operations satisfying the monad laws. This allows us to reason about probabilistic programs without committing to a specific representation (PMF, measure, etc.).

In Grove & White notation:

• ⌜v⌝ is pure v (trivial distribution at v)
• x ← m; k is bind m (λ x => k)

class Semantics.Dynamic.Probabilistic.ProbMonad (P : Type → Type) : Type 1

Abstract probability monad interface.

A probability monad provides:

• pure: Lift a value to a trivial distribution
• bind: Sequence probabilistic computations
• Monad laws as equalities

This is the semantic interface; implementations may use PMFs, measures, etc.

Note: We use Type instead of Type* to avoid universe issues. For semantic work, this is typically sufficient.

• pure {α : Type} : α → P α

  Trivial distribution concentrated at a value

• bind {α β : Type} : P α → (α → P β) → P β

  Sequence: sample from m, then continue with k

• pure_bind {α β : Type} (v : α) (k : α → P β) : bind (pure v) k = k v

  Left identity: pure v >>= k = k v

• bind_pure {α : Type} (m : P α) : bind m pure = m

  Right identity: m >>= pure = m

• bind_assoc {α β γ : Type} (m : P α) (n : α → P β) (o : β → P γ) : bind (bind m n) o = bind m fun (x : α) => bind (n x) o

  Associativity: (m >>= n) >>= o = m >>= (λx. n x >>= o)

def Semantics.Dynamic.Probabilistic.ProbMonad.map {P : Type → Type} [ProbMonad P] {α β : Type} (f : α → β) (m : P α) : P β

Map a function over a distribution

Equations

• Semantics.Dynamic.Probabilistic.ProbMonad.map f m = Semantics.Dynamic.Probabilistic.ProbMonad.bind m fun (x : α) => Semantics.Dynamic.Probabilistic.ProbMonad.pure (f x)

def Semantics.Dynamic.Probabilistic.ProbMonad.seq {P : Type → Type} [ProbMonad P] {α β : Type} (m : P α) (n : P β) : P β

Sequence two distributions, ignoring the first result

Equations

• Semantics.Dynamic.Probabilistic.ProbMonad.seq m n = Semantics.Dynamic.Probabilistic.ProbMonad.bind m fun (x : α) => n

theorem Semantics.Dynamic.Probabilistic.ProbMonad.map_id {P : Type → Type} [ProbMonad P] {α : Type} (m : P α) : map id m = m

Map preserves identity

theorem Semantics.Dynamic.Probabilistic.ProbMonad.map_comp {P : Type → Type} [ProbMonad P] {α β γ : Type} (f : α → β) (g : β → γ) (m : P α) : map g (map f m) = map (g ∘ f) m

Map composes

Parameterized State Monad

In Grove & White's parameterized state monad, the state type can change during computation. This models how discourse updates can modify the structure of the context (e.g., pushing questions onto the QUD stack).

P^σ_σ' α = σ → P(α × σ')

The parameters σ and σ' are the input and output state types.

def Semantics.Dynamic.Probabilistic.PState (P : Type → Type) (σ σ' α : Type) : Type

Parameterized probabilistic state monad.

Maps input state σ to a distribution over (value, output state) pairs. The output state type σ' can differ from σ, allowing type-changing updates.

This is Grove & White's P^σ_σ' α.

Equations

• Semantics.Dynamic.Probabilistic.PState P σ σ' α = (σ → P (α × σ'))

def Semantics.Dynamic.Probabilistic.PState.pure {P : Type → Type} [ProbMonad P] {σ α : Type} (v : α) : PState P σ σ α

Return for the parameterized state monad.

Returns the value paired with the unchanged state. Grove & White: ⌜v⌝^σ = λs. ⌜(v, s)⌝

Equations

• Semantics.Dynamic.Probabilistic.PState.pure v s = Semantics.Dynamic.Probabilistic.ProbMonad.pure (v, s)

def Semantics.Dynamic.Probabilistic.PState.bind {P : Type → Type} [ProbMonad P] {σ σ' σ'' α β : Type} (m : PState P σ σ' α) (k : α → PState P σ' σ'' β) : PState P σ σ'' β

Bind for the parameterized state monad.

Sequences stateful-probabilistic computations, threading state through. Grove & White: do { x ← m; k x } = λs. (x, s') ← m(s); k(x)(s')

Equations

• m.bind k s = Semantics.Dynamic.Probabilistic.ProbMonad.bind (m s) fun (x : α × σ') => match x with | (x, s') => k x s'

def Semantics.Dynamic.Probabilistic.PState.view {P : Type → Type} [ProbMonad P] {σ α : Type} (proj : σ → α) : PState P σ σ α

View (get) a component of the state.

Returns the value of applying proj to the current state, without modification.

Equations

• Semantics.Dynamic.Probabilistic.PState.view proj s = Semantics.Dynamic.Probabilistic.ProbMonad.pure (proj s, s)

def Semantics.Dynamic.Probabilistic.PState.set {P : Type → Type} [ProbMonad P] {σ σ' : Type} (upd : σ → σ') : PState P σ σ' Unit

Set (put) a component of the state.

Returns the new state created by upd, with a trivial value.

Equations

• Semantics.Dynamic.Probabilistic.PState.set upd s = Semantics.Dynamic.Probabilistic.ProbMonad.pure ((), upd s)

def Semantics.Dynamic.Probabilistic.PState.modify {P : Type → Type} [ProbMonad P] {σ : Type} (f : σ → σ) : PState P σ σ Unit

Modify the state in place.

Equations

• Semantics.Dynamic.Probabilistic.PState.modify f s = Semantics.Dynamic.Probabilistic.ProbMonad.pure ((), f s)

theorem Semantics.Dynamic.Probabilistic.PState.pure_bind {P : Type → Type} [ProbMonad P] {σ σ' α β : Type} (v : α) (k : α → PState P σ σ' β) : (pure v).bind k = k v

Left identity for PState: pure v >>= k = k v

theorem Semantics.Dynamic.Probabilistic.PState.bind_pure {P : Type → Type} [ProbMonad P] {σ σ' α : Type} (m : PState P σ σ' α) : m.bind pure = m

Right identity for PState: m >>= pure = m

theorem Semantics.Dynamic.Probabilistic.PState.bind_assoc {P : Type → Type} [ProbMonad P] {σ σ' σ'' σ''' α β γ : Type} (m : PState P σ σ' α) (n : α → PState P σ' σ'' β) (o : β → PState P σ'' σ''' γ) : (m.bind n).bind o = m.bind fun (x : α) => (n x).bind o

Associativity for PState.

Conditioning

Grove & White's observe operation conditions a distribution on a boolean.

observe : Bool → P Unit
observe true continues; observe false blocks

This is the mechanism for assertion: update the CG by observing the asserted proposition is true.

class Semantics.Dynamic.Probabilistic.CondProbMonad (P : Type → Type) extends Semantics.Dynamic.Probabilistic.ProbMonad P : Type 1

Extended probability monad with conditioning.

Adds observe for conditioning on boolean observations.

• pure {α : Type} : α → P α
• bind {α β : Type} : P α → (α → P β) → P β
• pure_bind {α β : Type} (v : α) (k : α → P β) : bind (pure v) k = k v
• bind_pure {α : Type} (m : P α) : bind m pure = m
• bind_assoc {α β γ : Type} (m : P α) (n : α → P β) (o : β → P γ) : bind (bind m n) o = bind m fun (x : α) => bind (n x) o
• fail {α : Type} : P α

  The zero distribution (blocks all continuations)

• observe : Bool → P Unit

  Condition on a boolean: continue if true, block if false

• observe_true : observe true = ProbMonad.pure ()

  Observing true is a no-op

• observe_false_bind {α : Type} (k : Unit → P α) : ProbMonad.bind (observe false) k = fail

  Observing false blocks all continuations

• fail_bind {α β : Type} (k : α → P β) : ProbMonad.bind fail k = fail

  fail is a left zero for bind

theorem Semantics.Dynamic.Probabilistic.CondProbMonad.observe_true_pure {P : Type → Type} [CondProbMonad P] : (ProbMonad.bind (observe true) fun (x : Unit) => ProbMonad.pure ()) = observe true

Observe filters: observe true then return is identity

theorem Semantics.Dynamic.Probabilistic.CondProbMonad.observe_false_pure {P : Type → Type} [CondProbMonad P] : (ProbMonad.bind (observe false) fun (x : Unit) => ProbMonad.pure ()) = fail

Observe false blocks: any continuation after observe false gives fail

Choice Operations

RSA's S1 isn't just conditioning - it's choosing an utterance weighted by utility. This requires a choose operation in addition to observe.

choose : (α → ℚ) → P α -- sample from weighted distribution

The relationship:

• observe b filters: keeps current path if b, blocks otherwise
• choose w samples: draws from distribution proportional to weights w

class Semantics.Dynamic.Probabilistic.ChoiceProbMonad (P : Type → Type) extends Semantics.Dynamic.Probabilistic.CondProbMonad P : Type 1

Probability monad with choice (for speaker models).

Adds choose for sampling from weighted distributions. This is what S1's softmax requires.

• pure {α : Type} : α → P α
• bind {α β : Type} : P α → (α → P β) → P β
• pure_bind {α β : Type} (v : α) (k : α → P β) : bind (pure v) k = k v
• bind_pure {α : Type} (m : P α) : bind m pure = m
• bind_assoc {α β γ : Type} (m : P α) (n : α → P β) (o : β → P γ) : bind (bind m n) o = bind m fun (x : α) => bind (n x) o
• fail {α : Type} : P α
• observe : Bool → P Unit
• observe_true : observe true = ProbMonad.pure ()
• observe_false_bind {α : Type} (k : Unit → P α) : ProbMonad.bind (observe false) k = fail
• fail_bind {α β : Type} (k : α → P β) : ProbMonad.bind fail k = fail
• choose {α : Type} [Fintype α] : (α → ℚ) → P α

  Sample from a weighted distribution over a finite type

• choose_uniform {α : Type} [Fintype α] [Nonempty α] : (choose fun (x : α) => 1) = choose fun (x : α) => 1

  choose with uniform weights is like a uniform prior

• choose_observe {α : Type} [Fintype α] (w : α → ℚ) (p : α → Bool) : (ProbMonad.bind (choose w) fun (a : α) => ProbMonad.bind (CondProbMonad.observe (p a)) fun (x : Unit) => ProbMonad.pure a) = choose fun (a : α) => w a * if p a = true then 1 else 0

  choose then observe is like weighted observe

def Semantics.Dynamic.Probabilistic.ChoiceProbMonad.softmaxChoice {P : Type → Type} [ChoiceProbMonad P] {α : Type} [Fintype α] (utility : α → ℚ) (temperature : ℚ) : P α

Softmax choice: choose with exp-scaled weights.

This is S1's decision rule: P(u) ∝ exp(α · utility(u))

Note: We use ℚ so can't compute exp directly. In practice, implementations use Float or work with log-probabilities. This definition is for the interface.

Equations

• Semantics.Dynamic.Probabilistic.ChoiceProbMonad.softmaxChoice utility temperature = Semantics.Dynamic.Probabilistic.ChoiceProbMonad.choose utility

Threshold Semantics

Threshold semantics + threshold uncertainty produces graded truth values. This is a special case of the PDS framework.

For a gradable adjective like "tall":

• measure : Entity → ℝ gives heights
• threshold : θ is the standard of comparison
• ⟦tall⟧_θ(x) = measure(x) > θ is Boolean

With uncertainty over θ:

• ⟦tall⟧(x) = E_θ[⟦tall⟧_θ(x)] = P(measure(x) > θ)

This probability is the graded truth value.

def Semantics.Dynamic.Probabilistic.thresholdSem {ε : Type} (measure : ε → ℚ) (threshold : ℚ) (x : ε) : Bool

Threshold semantics: entity satisfies predicate if measure exceeds threshold.

Equations

• Semantics.Dynamic.Probabilistic.thresholdSem measure threshold x = decide (measure x > threshold)

def Semantics.Dynamic.Probabilistic.gradedFromThreshold {ε Θ : Type} [Fintype Θ] [DecidableEq Θ] (measure : ε → ℚ) (thresholds prior : Θ → ℚ) (x : ε) : ℚ

Graded truth from threshold uncertainty.

Given a prior over thresholds, the graded truth is the probability that the entity's measure exceeds the threshold.

Equations

• Semantics.Dynamic.Probabilistic.gradedFromThreshold measure thresholds prior x = ∑ θ : Θ, prior θ * if measure x > thresholds θ then 1 else 0

theorem Semantics.Dynamic.Probabilistic.graded_eq_bool_of_point_mass {ε Θ : Type} [Fintype Θ] [DecidableEq Θ] (measure : ε → ℚ) (thresholds : Θ → ℚ) (θ₀ : Θ) (x : ε) : have pointMass := fun (θ : Θ) => if θ = θ₀ then 1 else 0; gradedFromThreshold measure thresholds pointMass x = if measure x > thresholds θ₀ then 1 else 0

For a point-mass prior (no uncertainty), graded truth reduces to Boolean.

This shows that graded semantics reduces to Boolean semantics when there's no parameter uncertainty.

Connection to RSA

Grove & White's framework connects to RSA as follows:

1. Literal meaning φ: a function ι → Bool (proposition)
2. Common ground: a distribution P ι over indices
3. Assertion: observe(φ(i)) for i ← cg
4. Probability computation: Pr[φ] = E_i[1_{φ(i)}]

RSA's graded φ emerges from:

• Boolean φ_θ indexed by parameters θ
• A prior distribution over θ
• Marginalization: φ(x) = E_θ[φ_θ(x)]

This is exactly Lassiter & Goodman's "threshold + uncertainty = graded".

def Semantics.Dynamic.Probabilistic.probProp {ι : Type} [Fintype ι] (mass : ι → ℚ) (φ : BProp ι) : ℚ

Probability of a proposition in a finite distribution.

This is Pr[φ] = E_i[1_{φ(i)}] in Grove & White notation. For finite distributions, this is the sum of masses where φ holds.

Equations

• Semantics.Dynamic.Probabilistic.probProp mass φ = ∑ i : ι, mass i * if φ i = true then 1 else 0

theorem Semantics.Dynamic.Probabilistic.probProp_true {ι : Type} [Fintype ι] (mass : ι → ℚ) : (probProp mass fun (x : ι) => true) = Finset.univ.sum mass

Probability of a true proposition is the total mass (1 for normalized distributions).

theorem Semantics.Dynamic.Probabilistic.probProp_false {ι : Type} [Fintype ι] (mass : ι → ℚ) : (probProp mass fun (x : ι) => false) = 0

Probability of a false proposition is 0.