Re: [isabelle] Theorem-proving for a Bayesian model compiler



Am Dienstag, den 15.03.2011, 09:11 -0600 schrieb Kevin Van Horn:
> I'm trying to figure out if Isabelle is the right theorem prover /  
> proof assistant for my needs, or if I should use something else. 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.  There are existing software packages that  
> do something similar -- WinBUGS/OpenBUGS, JAGS, and hbc -- but they  
> all have limitations that are unacceptable for my purposes, and it  
> appears that I'll need some sort of theorem proving to overcome those  
> limitations.

Which mathematical background theories do you need? We have measure /
probability theory but no theorems about MCMC.

> Here are the features I'm looking for:
> 
> * Interactive theorem proving (Isabelle seems to do this very well).

> * Ability to write new proof tactics.

I only developed two small tactics in Isabelle, so I'm not very
experienced. But I think it is very easy to do in the interactive mode
in ProofGeneral. Open a new theory and write 

  theory test imports Main begin

  ML {*
    fun .....
  *}

  theorem "..."
    apply (tactic {* ML code *})
  
This is a very nice playground for ideas, later you can of course move
your code to its own ML-file.

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

For further information take a look at the reference manuals
http://isabelle.in.tum.de/documentation.html


> * Ability to do derivational proofs where I know the form of what I  
> want to prove but don't know exactly what I'm proving until I reach  
> the end.  For example, I'm doing a chain of A1 = A2 = ... An, and only  
> when I reach an An that has the form I want do I know I'm done and  
> know that A1 = An is what I'm proving.  Likewise, I might be trying to  
> find a usable upper bound: B1 <= B2 <= ... Bn.

> * Ability to call the theorem prover as a software module in a larger  
> system (no user interaction). This would be for tasks simple enough to  
> fully automate with appropriate tactics, or to spit out subgoals for  
> which the user will need to provide proofs in harder cases.

Some proof methods in Isabelle work in this way. The most often used
proof method (simp) works in this way. The user states a goal, applies
the simplifier and gets back the simplified goal where he can apply
further tactics. (This should also answer the previous question.)

> How does Isabelle rate on these?  Would a different theorem prover /  
> proof assistant better fill these requirements?
> 
> (BTW I'm also looking at  HOL Light and HOL 4, which appear have the  
> last three features above, but my impression is that Isabelle is  
> easier to use for interactive proof and that the finished proofs are  
> easier to read.)

I have no experiences with HOL Light or HOL 4. When you write your
proofs in Isar (Isabelle's proof language) they are more readable.
However I assume the OCaml / ML internals of HOL Light / HOL 4 are
easier to understand.

Greetings,
  Johannes







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