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 turn a
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 array indices.

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
Cookbook:
http://www4.in.tum.de/~urbanc/cgi-bin/repos.cgi/isabelle-cookbook/raw-file/tip/progtutorial.pdf

Great! This seems to have a lot of the missing pieces I couldn't find in the tutorial and reference manual.

-- Kevin






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.