Abstract
Inter alia, Lebesgue-style integration plays a major role in advanced probability. We formalize a significant part of its theory in Higher Order Logic using Isabelle/Isar. This involves concepts of elementary measure theory, real-valued random variables as Borel-measurable functions, and a stepwise inductive definition of the integral itself. Building on previous work about formal verification of probabilistic algorithms, we exhibit an example application in this domain; another primitive for randomized functional programming is developed to this end.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bauer, H.: Maß- und Integrationstheorie. de Gruyter (1990)
Billingsley, P.: Probability and Measure, 2nd edn. John Wiley, Chichester (1986)
Endou, N., Wasaki, K., Shidama, Y.: Definitions and basic properties of measurable functions. Journal of Formalized Mathematics 12 (2000), Available on the web as http://mizar.uwb.edu.pl/JFM/Vol12/mesfunc1.html
Endou, N., Wasaki, K., Shidama, Y.: The measurability of extended real valued functions. Journal of Formalized Mathematics 12 (2000), Available on the web as http://mizar.uwb.edu.pl/JFM/Vol12/mesfunc2.html
Fleuriot, J.D., Paulson, L.C.: Mechanizing nonstandard real analysis. LMS Journal of Computation and Mathematics 3, 140–190 (2000)
Harrison, J.: Theorem Proving with the Real Numbers. Springer, Heidelberg (1996)
Hurd, J.: Formal Verification of Probabilistic Algorithms. PhD thesis, University of Cambridge (2002)
Motwani, R., Raghavan, P.: Randomized Algorithms. Cambridge University Press, Cambridge (1997)
Nipkow, T.: Order-sorted polymorphism in isabelle. In: Huet, G., Plotkin, G. (eds.) Logical Environments, pp. 164–188. Cambridge University Press, Cambridge (1993)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle’s logics: HOL (2002), Unpublished. Available on the web as http://isabelle.in.tum.de/doc/logics-HOL.pdf
Paulson, L.C.: Isabelle: The next 700 theorem provers. In: Odifreddi, P. (ed.) Logic and Computer Science, pp. 361–386. Academic Press, London (1990)
Paulson, L.C.: Isabelle: A generic theorem prover. LNCS, vol. 828, pp. xvii + 321. Springer, Heidelberg (1994)
Skalberg, S.: Import tool, Available on the web as http://www.mangust.dk/skalberg/isabelle.php
Wenzel, M.: Isabelle/Isar — a versatile environment for human-readable formal proof documents. PhD thesis, Technische Universität München (2002)
Wenzel, M.: Using axiomatic type classes in Isabelle (2002) (unpublished), Available on the web as http://isabelle.in.tum.de/dist/Isabelle2002/doc/axclass.pdf
Williams, D.: Probability with Martingales. Cambridge University Press, Cambridge (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Richter, S. (2004). Formalizing Integration Theory with an Application to Probabilistic Algorithms. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2004. Lecture Notes in Computer Science, vol 3223. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30142-4_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-30142-4_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23017-5
Online ISBN: 978-3-540-30142-4
eBook Packages: Springer Book Archive