Sampling from an arbitrary sub-distribution

SPComp.sample samples uniformly from a finite nonempty type. sampleFrom d samples from an arbitrary SDistr, leaving the heap unchanged, so that non-uniform distributions — centered binomial, rejection-sampling output, biased coins, discrete Gaussians — are expressible as SPComp programs.

Main definitions

• sampleFrom d — sample from d : SDistr α, heap unchanged
• ofPMF p — the total distribution p : PMF α viewed as an SDistr α

Main results

• sampleFrom_uniform — sampleFrom (SDistr.uniform α) = SPComp.sample α, so uniform sampling is a definitional special case
• sampleFrom_eq_liftSDistr — sampleFrom and the existing liftSDistr agree
• sampleFrom_bind_apply — (sampleFrom d >>= k) h = d.bind fun a => k a h
• mass_sampleFrom, isLossless_sampleFrom_iff — mass of the computation is the mass of the distribution
• bind_const_of_mass_one, dead_sampleFrom — a lossless sample whose result is discarded is a no-op

The combinator

noncomputable def CatCrypt.NonUniform.sampleFrom {α : Type u_1} (d : Prob.SDistr α) : Core.SPComp α

Sample from an arbitrary sub-distribution, leaving the heap unchanged. The computation fails with probability d none.

Equations

• CatCrypt.NonUniform.sampleFrom d h = d.bind fun (a : α) => CatCrypt.Prob.SDistr.pure (a, h)

@[simp]

theorem CatCrypt.NonUniform.sampleFrom_apply {α : Type u_1} (d : Prob.SDistr α) (h : Core.Heap) : sampleFrom d h = d.bind fun (a : α) => Prob.SDistr.pure (a, h)

theorem CatCrypt.NonUniform.sampleFrom_uniform (α : Type u_4) [Fintype α] [Nonempty α] : sampleFrom (Prob.SDistr.uniform α) = Core.SPComp.sample α

Uniform sampling is the sampleFrom at the uniform distribution.

theorem CatCrypt.NonUniform.sampleFrom_eq_liftSDistr {α : Type} (d : Prob.SDistr α) : sampleFrom d = Core.liftSDistr d

sampleFrom agrees with the SDistr → SPComp lift already in Core.Code.

Monadic laws

theorem CatCrypt.NonUniform.sampleFrom_bind_apply {α : Type u_1} {β : Type u_2} (d : Prob.SDistr α) (k : α → Core.SPComp β) (h : Core.Heap) : (sampleFrom d).bind k h = d.bind fun (a : α) => k a h

Bind interaction: the sampled value is fed to the continuation at the unchanged heap, so the whole computation is a bind at the SDistr level.

theorem CatCrypt.NonUniform.sampleFrom_hBind_apply {α β : Type} (d : Prob.SDistr α) (k : α → Core.SPComp β) (h : Core.Heap) : (sampleFrom d >>= k) h = d.bind fun (a : α) => k a h

Operator form of sampleFrom_bind_apply.

@[simp]

theorem CatCrypt.NonUniform.sampleFrom_pure {α : Type u_1} (a : α) : sampleFrom (Prob.SDistr.pure a) = Core.SPComp.pure a

Sampling from a point mass is returning.

@[simp]

theorem CatCrypt.NonUniform.sampleFrom_fail {α : Type u_1} : sampleFrom Prob.SDistr.fail = Core.SPComp.fail

Sampling from the everywhere-failing distribution is failure.

theorem CatCrypt.NonUniform.sampleFrom_bind_sampleFrom {α : Type u_1} {β : Type u_2} (d : Prob.SDistr α) (f : α → Prob.SDistr β) : ((sampleFrom d).bind fun (a : α) => sampleFrom (f a)) = sampleFrom (d.bind f)

Two successive samples are one sample from the bound distribution.

theorem CatCrypt.NonUniform.sampleFrom_isPure {α : Type u_1} (d : Prob.SDistr α) : (sampleFrom d).IsPure

sampleFrom d does not read or write the heap.

Mass and losslessness

theorem CatCrypt.NonUniform.sampleFrom_apply_none {α : Type u_1} (d : Prob.SDistr α) (h : Core.Heap) : (sampleFrom d h) none = d none

The failure probability of sampleFrom d is the failure probability of d.

theorem CatCrypt.NonUniform.mass_sampleFrom {α : Type u_1} (d : Prob.SDistr α) (h : Core.Heap) : (sampleFrom d h).mass = d.mass

The mass of sampleFrom d is the mass of d.

theorem CatCrypt.NonUniform.isLossless_sampleFrom_iff {α : Type u_1} (d : Prob.SDistr α) : Unary.isLossless (sampleFrom d) ↔ d.mass = 1

sampleFrom d is lossless exactly when d is a total distribution.

theorem CatCrypt.NonUniform.isLossless_sampleFrom {α : Type u_1} (d : Prob.SDistr α) (hd : d.mass = 1) : Unary.isLossless (sampleFrom d)

A total distribution gives a lossless computation.

Discarding a lossless sample

theorem CatCrypt.NonUniform.bind_const_of_mass_one {α : Type u_1} {β : Type u_2} {d : Prob.SDistr α} (hd : d.mass = 1) (e : Prob.SDistr β) : (d.bind fun (x : α) => e) = e

Binding a total distribution to a constant continuation is that constant. Generalizes SDistr.uniform_bind_const from uniform to arbitrary mass-one distributions.

theorem CatCrypt.NonUniform.dead_sampleFrom {α : Type u_1} {β : Type u_2} {d : Prob.SDistr α} (hd : d.mass = 1) (k : Core.SPComp β) : ((sampleFrom d).bind fun (x : α) => k) = k

A lossless sample whose result is unused can be dropped. Generalizes dead_sample from uniform to arbitrary mass-one distributions.

Total distributions from PMF

noncomputable def CatCrypt.NonUniform.ofPMF {α : Type u_1} (p : PMF α) : Prob.SDistr α

A PMF viewed as a never-failing SDistr.

Equations

• CatCrypt.NonUniform.ofPMF p = PMF.map some p

@[simp]

theorem CatCrypt.NonUniform.ofPMF_apply_some {α : Type u_1} (p : PMF α) (a : α) : (ofPMF p) (some a) = p a

@[simp]

theorem CatCrypt.NonUniform.ofPMF_apply_none {α : Type u_1} (p : PMF α) : (ofPMF p) none = 0

@[simp]

theorem CatCrypt.NonUniform.mass_ofPMF {α : Type u_1} (p : PMF α) : (ofPMF p).mass = 1

theorem CatCrypt.NonUniform.ofPMF_uniformOfFintype (α : Type u_4) [Fintype α] [Nonempty α] : ofPMF (PMF.uniformOfFintype α) = Prob.SDistr.uniform α

SDistr.uniform is ofPMF of the uniform PMF.

theorem CatCrypt.NonUniform.isLossless_sampleFrom_ofPMF {α : Type u_1} (p : PMF α) : Unary.isLossless (sampleFrom (ofPMF p))

sampleFrom (ofPMF p) is lossless.