RSA Prior Combinators

Reusable combinators for constructing priors over product spaces and uniform distributions. These are common building blocks for RSA models where the world space is a product (e.g., State × Goal in @cite{kao-etal-2014-hyperbole}).

def RSA.Priors.jointPrior {A : Type u_1} {B : Type u_2} (marginal : A → ℝ) (conditional : A → B → ℝ) : A × B → ℝ

Joint prior: P(a,b) = marginal(a) * conditional(a, b).

Equations

• RSA.Priors.jointPrior marginal conditional (a, b) = marginal a * conditional a b

theorem RSA.Priors.jointPrior_nonneg {A : Type u_1} {B : Type u_2} {marginal : A → ℝ} {conditional : A → B → ℝ} (hm : ∀ (a : A), 0 ≤ marginal a) (hc : ∀ (a : A) (b : B), 0 ≤ conditional a b) (p : A × B) : 0 ≤ jointPrior marginal conditional p

def RSA.Priors.uniformPrior {A : Type u_1} : A → ℝ

Uniform prior: weight 1 everywhere.

Equations

• RSA.Priors.uniformPrior x✝ = 1

theorem RSA.Priors.uniformPrior_nonneg {A : Type u_1} (a : A) : 0 ≤ uniformPrior a