Email Gateway (Aug 23 2022 at 08:19): Email Gateway (Aug 23 2022 at 08:19):From: Jose Manuel Rodriguez Caballero <jose.manuel.rodriguez.caballero@ut.ee>
Dear Isabelle users,
Next week I will be in a course of probabilistic programming [2]. I think that it will be a great learning experience to combine this theory with practice in Isabelle. So, I would like to ask how could probabilistic programming be done in Isabelle? Is there any tutorial?
My guess is that I need to use ML and a random number generator, but maybe there is an easier way (without ML). I know the book [1], which is an introduction to ML, but I have not started using ML in a systematic way yet.
Sincerely yours,
José M.
Reference:
[1] Paulson, Lawrence C. ML for the Working Programmer. Cambridge University Press, 1996.
URL = https://www.cl.cam.ac.uk/~lp15/MLbook/
[2] Joost-Pieter Katoen, Foundations of probabilistic programming
URL = http://cs.ioc.ee/ewscs/2020/index.php?page=katoen
Email Gateway (Aug 23 2022 at 08:19):From: Manuel Eberl <eberlm@in.tum.de>
It's not quite clear to me what you want to achieve. Isabelle is not a
programming language as such, but a logical system (okay, the code
generator sort of allows you to you use it in a similar fashion as a
programming language).
You can write down probabilistic algorithms in Isabelle using the Giry
Monad, either on measure spaces or on "Probability Mass Functions"
(PMFs). The latter is more restricted (it only supports distributions
with discrete support), but much more pleasant to use since you don't
have to worry about measurability.
There is currently no way to execute such algorithms in the way you
think (e.g. sampling a single random result from them) or to obtain
executable code for them. Doing this would probably require some
extension to the code generator (similarly to Imperative HOL). We
thought about this occasionally in the past, but nobody did it yet. Any
such implementation would, however, necessarily be somewhat unfaithful
in the sense that when you reason about these things in Isabelle, you
assume a perfectly random distribution, whereas translating the
algorithms to a real programming language with some pseudo-random number
generator will never be able to provide that. Therefore, some properties
that you proved abstractly might not hold anymore.
What you can, however, do in most cases is to execute the algorithm to
obtain the entire probability distribution of results. This also allows
you to compute expectation, standard deviation etc. Of course, this is
usually much more expensive than sampling a single result, but it can
still be useful for experiments, and it means that QuickCheck works and
you can sometimes get counterexamples.
I don't think there are any tutorials, but there are a number of AFP
entries with relatively simple, self-contained examples:
https://www.isa-afp.org/entries/Fisher_Yates.html
https://www.isa-afp.org/entries/Quick_Sort_Cost.html
https://www.isa-afp.org/entries/Random_BSTs.html
https://www.isa-afp.org/entries/Randomised_BSTs.html
https://www.isa-afp.org/entries/Treaps.html
https://www.isa-afp.org/entries/Skip_Lists.html
And there is Andreas Lochbihler's very advanced AFP entry on CryptHOL,
which uses probabilistic reasoning in Isabelle to prove properties of
cryptographic systems:
https://www.isa-afp.org/entries/CryptHOL.html
All of these do /not/ use an actual deeply-embedded programming language
with a formal semantics, but rather they directly describe these
algorithms as probability distributions in the logic and reason about
them mathematically (as opposed to a program logic whose correctness was
proven seperately).
There is also one with a deeply-embedded probabilistic programming
language, which is the more usual approach when working on paper:
https://www.isa-afp.org/entries/pGCL.html
Related publications:
Verified Analysis of Random Binary Tree Structures (Eberl et al.), DOI:
10.1007/s10817-020-09545-0 (open access)
Formalizing Constructive Cryptography using CryptHOL (Lochbihler et
al.), DOI: 10.1109/CSF.2019.00018 (preprint at
http://www.andreas-lochbihler.de/pub/lochbihler2019csf.pdf )
Cheers,
Manuel
Last updated: Nov 21 2024 at 12:39 UTC