zenna / OmegaCore.jl

1 stars 2 forks source link

Conditioning #4

Open zenna opened 4 years ago

zenna commented 4 years ago

The issues here are about conditioning and the semantics of logpdf.

Currently we have a function logpdf(x, ω), documented as "Logdensity of f on trace ω". But the semantics of which are not entirely clear.

Here's my proposal:

x(ω) = f(p1(ω), p2(ω), ..., pn(ω))

where pi is a primitive.

Caveats

There are a few questions and caveats:

  1. In open world models /control this is not entirely true that we can represent any random variable that way, the number of primitives used depends on ω

I think these can be handled by making the formulation slightly more complex. The bigger issue is whether there is a unique rendering of any random variable in this form.

Examples

x(ω) = unif1(ω) + unif2(ω) * 0

unif2 is ineffective, and could be replaced by simply 0.

Implications

So what does this mean for conditioning?

Suppose have a model like

μ = normal1(0, 1)
x = normal2(μ, 1)
μ | x == 3

What could sat(μ) evaluate to?

normal1 ↦ 3.0

The problem is that \mu does not depend on x, so in what sense should sat care about x. Well, μ | x == 3 does depend on x in a sense.

The trick is in ensuring we have all the "necessary" elements of \omega when we are doing inference.

What does that mean?

It's not:

What this all means is that sat(x) should find some \omega such that x(\omega) != bot. For metropolis hastings we need a little more right, we need a proposal distribution,

propose(\omega, x) I think that'll be fine too.

zenna commented 4 years ago

The machinery I have now uses the context system to track the logpdfs. Is this necessary? Suppose we didn't have it:

Well we still need some mechanism to get the primitives used in a random variable.

But do we need these conditional families