A Computer Verified Theory of Compact Sets
Logic in Computer Science
2010-08-04 v1
Abstract
Compact sets in constructive mathematics capture our intuition of what computable subsets of the plane (or any other complete metric space) ought to be. A good representation of compact sets provides an efficient means of creating and displaying images with a computer. In this paper, I build upon existing work about complete metric spaces to define compact sets as the completion of the space of finite sets under the Hausdorff metric. This definition allowed me to quickly develop a computer verified theory of compact sets. I applied this theory to compute provably correct plots of uniformly continuous functions.
Keywords
Cite
@article{arxiv.0806.3209,
title = {A Computer Verified Theory of Compact Sets},
author = {Russell O'Connor},
journal= {arXiv preprint arXiv:0806.3209},
year = {2010}
}
Comments
This paper is to be part of the proceedings of the Symbolic Computation in Software Science Austrian-Japanese Workshop (SCSS 2008)