Conditioning by Lazy Partial Evaluation

Chung-chieh Shan
Indiana University

29 April 2015

  1. Measures
    • defined mathematically
    • expressed as programs
  2. Conditioning
    • defined mathematically
    • implemented as program transformation

Measurable spaces

A type is a measurable space:
a set equipped with a notion of what’s measurable.

α×β Product spaces
α+β Sum spaces
Space of measures (so monad)

A term denotes
an element of a measurable function from a product space to
a measurable space.

Measures

Each measure μ : Mα corresponds to its “volume” functional

μ* : (α → [0,∞]) → [0,∞]

(Calculus integration vs Lebesgue integration.)

Notation λ* for naming a measure by its volume functional (uniquely).

uniform 0 1             =  λ*c. ∫01 c(x) dx
return 3                =  λ*c. c(3)
μ >>= κ                 =  λ*c. μ*λx. (κx)*c

uniform 0 1 >>= λx.
uniform 0 1 >>= λy.
return (x-y,x)          =  λ*c. ∫0101 c(x-y,x) dy dx

lebesgue                =  λ*c. ∫-∞ c(x) dx
factor r                =  λ*c. r × c()

lebesgue >>= λx.
factor (f(x)) >>= λ().
return x                =  λ*c. ∫-∞ f(x) × c(x) dx

Density

Definition of density:

τ = μ >>= λt.
    factor (f(t)) >>= λ().
    return t
  = λ*c. μ*λt. f(t) × c(t)

Example (change integration bound):

μ = lebesgue
τ = uniform 0 1

f(t) | 0 < t < 1 = 1
     | otherwise = 0

Example (change integration variable):

μ = lebesgue
τ = uniform 0 1 >>= λx.
    return (-log x)

f(t) | 0 < exp (-t) < 1 = factor (exp (-t))
     | otherwise        = mzero

Disintegration

Generalize density to definition of disintegration:

τ = μ >>= λt.
    κt >>= λu.
    return (t,u)
  = λ*c. μ*λt. (κt)*λu. c(t,u)

Example (change integration variable):

μ = lebesgue
τ = uniform 0 1 >>= λx.
    uniform 0 1 >>= λy.
    return (x-y,x)

κt | t ≤-1     = mzero
   | t < 0     = factor (t + 1) >>= λ().
                 uniform 0 (t + 1)
   | t < 1     = factor (1 - t) >>= λ().
                 uniform t 1
   | otherwise = mzero

Conditioning = disintegration + normalization
Type: M(α,β) → α → Mβ
κ defined up to almost-sure equivalence

Implementation: Lazy partial evaluation

 fwdExec : N(Mα) →(Nα → Heap → N(Mγ)) → Heap → N(Mγ)
[fwdEval : T  α  →(Nα → Heap → N(Mγ)) → Heap → N(Mγ)]
[bwdExec : N(MR) → NR →(Heap → N(Mγ)) → Heap → N(Mγ)]
 bwdEval : T  R  → NR →(Heap → N(Mγ)) → Heap → N(Mγ)

 bwdEval (x-y) t
         (λh'. do {h'; return x})
         (x ← uniform 0 1; y ← uniform 0 1)
 = fwdExec (uniform 0 1)
           (λn h. bwdEval y (n-t)
                          (λh'. do {h'; return x})
                          (h; let x=n; y ← uniform 0 1))
           ([])
 = do {n ← uniform 0 1;
       bwdEval y (n-t)
               (λh'. do {h'; return x})
               (let x=n; y ← uniform 0 1)}
 = do {n ← uniform 0 1;
       factor (if 0<n-t<1 then 1 else 0);
       let x=n;
       let y=n-t;
       return x}

Borel’s paradox

Example (change integration variable):

μ = lebesgue
τ = uniform 0 1 >>= λx.
    uniform 0 1 >>= λy.
    return (x/y,x)

κt | t < 0     = mzero
   | t < 1     = uniform 0 t >>= λx.
                 factor (x/t) >>= λ().
                 return x
   | otherwise = factor (1/2/t/t) >>= λ().
                 beta 2 1 >>= λx.
                 return x