# 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.