Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 20 Oct 1994 16:12:32 +0100 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA19601; Thu, 20 Oct 1994 09:06:43 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA19597; Thu, 20 Oct 1994 09:06:35 -0600 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Thu, 20 Oct 1994 15:58:20 +0100 To: info-hol@leopard.cs.byu.edu Subject: Re: probability theory in HOL In-Reply-To: Your message of "Thu, 13 Oct 94 12:31:42 PDT." <9410131931.AA20051@elvis.ds.boeing.com> Date: Thu, 20 Oct 94 15:58:08 +0100 From: John Harrison Message-Id: <"swan.cl.cam.:025130:941020145840"@cl.cam.ac.uk> David Fura writes: | Has anybody implemented probability theory in HOL or another | prover, or know about somebody who has? | | I'm interested in representing probabilistic measures such as | 'reliablity' and have a simple embedding that seems adequate | for this. It's not very elegant though and I'd be open to | suggestions for improvement. This topic may be of interest | to others as well? I'd never thought of doing probability theory in HOL -- looks an interesting project. I have only the vaguest ideas of how probability theory is done these days. Does one still start with Kolmogorov's axioms? But I get the impression that measure theory is an important tool in certain areas. I might be able to help you with that, since I have a modest theory of gauge integration. The gauge integral of the indicator (characteristic) function of a set gives the set's Lebesgue measure. It may take a bit of work to prove the measure-theoretic facts you want, but probability measures should be a bit easier to formalize since you don't have to worry about infinity all the time. Anyway, I'm glad to see that the number of "reals" library users has reached double figures (in binary). John.