Email Gateway (Sep 11 2023 at 12:56): Email Gateway (Sep 11 2023 at 12:56):From: Gergely Buday <cl-isabelle-users@lists.cam.ac.uk>
Hi there,
I have not found a formalisation of finite distributions. The Probability
directory contains a deep development using measure spaces but I'm not sure
if I should build a finite distribution modelling on that.
And in general, when should I build on existing libraries and when should I
better build something from scratch?
Email Gateway (Sep 11 2023 at 13:24):From: Manuel Eberl <manuel@pruvisto.org>
There's a lot about finite (or rather countable-support) distributions
under the name of "Probability Mass Functions" (PMFs). Just look at a
few AFP entries that use them, e.g. the ones in the "Randomizsed
Algorithms" category:
https://www.isa-afp.org/topics/computer-science/algorithms/randomized/
Feel free to ask on the mailing list or me privately if you have any
specific questions about it.
And in general, when should I build on existing libraries and when
should I better build something from scratch?
As a general rule I'd say if there is an existing library, try to use
that. Only build something from scratch if there is nothing in the
library or the thing in the library is really unsuitable for what you
are doing. Even in that case it is a good idea to make a "compatibility
layer" between your new thing and the old thing in the library to allow
transferring results between the two.
Cheers,
Manuel
Last updated: Jan 04 2025 at 20:18 UTC