Distributions

Distributions.ae — linear batch samplers (issue #441 follow-up). Each producer draws a batch from a linear ``Rng`` (``libraries/Random.ae``), returning an opaque ``SampleDraw`` paired with the successor generator. Project the array through the distribution-specific ``*_value`` function (where the quantile-bound refinements live), then bind ``sample_next`` to continue the chain. Batch draws never use ``numpy.random`` or other global RNG state. Refinement-language predicates (fracBelow, fracAbove, sampleMean, ...) and their monotonicity axioms (widenBelow, widenAbove, ...) live in Statistics. Opaque batch draw: a sample array paired with the successor generator.
Imports
open Array; open Math; open Random; open Statistics;
Table of Contents

Types

SampleDraw

(type) linear
Opaque batch draw: a sample array paired with the successor generator.
linear type SampleDraw

Functions

sample_next

def sample_next (1 d : SampleDraw) : Rng

normal_sample

def normal_sample (1 g : Rng) (mu : Float) (sigma : Float | sigma > 0.0) (n : Int | n > 0) : SampleDraw

normal_value

def normal_value (mu : Float) (sigma : Float | sigma > 0.0) (borrow d : SampleDraw) : { xs : (Array Float) | Array.size xs > 0 && fracBelow xs (mu + 2.33 * sigma) ≥ 0.99 && fracBelow xs (mu + 1.645 * sigma) ≥ 0.95 && fracBelow xs (mu + 1.282 * sigma) ≥ 0.9 && fracBelow xs mu ≥ 0.5 && fracAbove xs (mu - 1.282 * sigma) ≥ 0.9 && fracAbove xs (mu - 1.645 * sigma) ≥ 0.95 && fracAbove xs (mu - 2.33 * sigma) ≥ 0.99 }

standard_normal_sample

def standard_normal_sample (1 g : Rng) (n : Int | n > 0) : SampleDraw

standard_normal_value

def standard_normal_value (borrow d : SampleDraw) : { xs : (Array Float) | Array.size xs > 0 && fracBelow xs 2.33 ≥ 0.99 && fracBelow xs 1.645 ≥ 0.95 && fracBelow xs 1.282 ≥ 0.9 && fracBelow xs 0.0 ≥ 0.5 && fracAbove xs 0.0 ≥ 0.5 && fracAbove xs (0.0 - 1.282) ≥ 0.9 && fracAbove xs (0.0 - 2.33) ≥ 0.99 }

uniform_sample

def uniform_sample (1 g : Rng) (a : Float) (b : Float | b > a) (n : Int | n > 0) : SampleDraw

uniform_value

def uniform_value (a : Float) (b : Float | b > a) (borrow d : SampleDraw) : { xs : (Array Float) | Array.size xs > 0 && fracAbove xs a ≥ 1.0 && fracBelow xs b ≥ 1.0 && fracBelow xs (a + 0.99 * (b - a)) ≥ 0.99 && fracBelow xs (a + 0.95 * (b - a)) ≥ 0.95 && fracBelow xs (a + 0.5 * (b - a)) ≥ 0.5 && fracBelow xs (a + 0.1 * (b - a)) ≥ 0.1 }

exponential_sample

def exponential_sample (1 g : Rng) (lam : Float | lam > 0.0) (n : Int | n > 0) : SampleDraw

exponential_value

def exponential_value (lam : Float | lam > 0.0) (borrow d : SampleDraw) : { xs : (Array Float) | Array.size xs > 0 && fracAbove xs 0.0 ≥ 1.0 && fracBelow xs (4.6052 / lam) ≥ 0.99 && fracBelow xs (2.9957 / lam) ≥ 0.95 && fracBelow xs (2.3026 / lam) ≥ 0.9 && fracBelow xs (0.6931 / lam) ≥ 0.5 }

beta_sample

def beta_sample (1 g : Rng) (alpha : Float | alpha > 0.0) (beta : Float | beta > 0.0) (n : Int | n > 0) : SampleDraw

beta_value

def beta_value (alpha : Float | alpha > 0.0) (beta : Float | beta > 0.0) (borrow d : SampleDraw) : { xs : (Array Float) | Array.size xs > 0 && fracAbove xs 0.0 ≥ 1.0 && fracBelow xs 1.0 ≥ 1.0 && sampleMean xs = alpha / (alpha + beta) }

gamma_sample

def gamma_sample (1 g : Rng) (k : Float | k > 0.0) (theta : Float | theta > 0.0) (n : Int | n > 0) : SampleDraw

gamma_value

def gamma_value (k : Float | k > 0.0) (theta : Float | theta > 0.0) (borrow d : SampleDraw) : { xs : (Array Float) | Array.size xs > 0 && fracAbove xs 0.0 ≥ 1.0 && sampleMean xs = k * theta && sampleVar xs = k * (theta * theta) }

chi_squared_sample

def chi_squared_sample (1 g : Rng) (k : Int | k > 0) (n : Int | n > 0) : SampleDraw

chi_squared_value

def chi_squared_value (borrow d : SampleDraw) : {xs : (Array Float) | Array.size xs > 0 && fracAbove xs 0.0 ≥ 1.0}

bernoulli_sample

def bernoulli_sample (1 g : Rng) (p : Float | p ≥ 0.0 && p ≤ 1.0) (n : Int | n > 0) : SampleDraw

bernoulli_value

def bernoulli_value (p : Float | p ≥ 0.0 && p ≤ 1.0) (borrow d : SampleDraw) : { xs : (Array Float) | Array.size xs > 0 && fracBelow xs 0.5 ≥ 1.0 - p && fracAbove xs 0.5 ≥ p && fracBelow xs 1.5 ≥ 1.0 && fracAbove xs (0.0 - 0.5) ≥ 1.0 }

binomial_sample

def binomial_sample (1 g : Rng) (trials : Int | trials > 0) (p : Float | p ≥ 0.0 && p ≤ 1.0) (n : Int | n > 0) : SampleDraw

binomial_value

def binomial_value (borrow d : SampleDraw) : {xs : (Array Float) | Array.size xs > 0 && fracAbove xs (0.0 - 0.5) ≥ 1.0}

poisson_sample

def poisson_sample (1 g : Rng) (lam : Float | lam > 0.0) (n : Int | n > 0) : SampleDraw

poisson_value

def poisson_value (lam : Float | lam > 0.0) (borrow d : SampleDraw) : {xs : (Array Float) | Array.size xs > 0 && fracAbove xs (0.0 - 0.5) ≥ 1.0 && sampleMean xs = lam}

discard_sample

End ownership after the last sample read.
def discard_sample (1 d : SampleDraw) : Unit