Re: [isabelle] Theorem-proving for a Bayesian model compiler
On Mar 16, 2011, at 4:14 AM, Johannes Hölzl wrote:
Am Dienstag, den 15.03.2011, 09:11 -0600 schrieb Kevin Van Horn:
... I'm writing a Bayesian model compiler, something that will
specification of a joint probability distribution plus indication of
what variables are observed into Markov chain Monte Carlo code for
estimating the parameters. ... it appears that I'll need some sort
of theorem proving...
Which mathematical background theories do you need? We have measure /
probability theory but no theorems about MCMC.
In addition to measure / probability theory, I'll need some linear
algebra (matrix/vector multiplication, inverse, determinants) and
standard probability density functions (gamma, normal, multivariate
normal, etc.). A lot of what I'll be doing looks a lot more like
computer algebra (transforming a function into an equivalent function,
where equivalent means the same up to a constant of proportionality,
and deriving gradients of multivariate functions), along with
establishing some upper bounds and proving some arithmetic results on
I don't expect to be proving anything very deep. Mostly, I'm looking
to automate (at least partially) a process that is currently done by
doing the math by hand following some pretty standard patterns; I need
to be able to automate new patterns as they arise; and I need to be
highly confident that the results are correct.
A introduction on how to write tactics is found in the Isabelle
Great! This seems to have a lot of the missing pieces I couldn't find
in the tutorial and reference manual.
This archive was generated by a fusion of
Pipermail (Mailman edition) and