Certifying homological algorithms to study biomedical images

Abstract

In this thesis, we deal with the verification of homological programs which analyze biomedical images. Concretely, some algorithms to compute homology groups have been formalized using the Coq interactive theorem prover and its SSReflect library, producing executable programs which are correct by construction. To this aim, it has been necessary the formalization of some mathematical results related to Algebraic Topology. We can formalize in constructive type theory (obtaining correct programs) the process which allows us to analyze images through homological computations - this is the central idea of the thesis. When we want to apply this process to biomedical images, the problem of the big size of those images arises. Then, it is necessary to use (and formalize) effective homological tools to reduce the size of the data structures preserving the homological information - in our case, we have used the Romero-Sergeraert algorithm. The first chapter introduces some instrumental notions for the rest of the thesis: the mathematics to formalize, Coq/SSReflect and the methodology that we have used. In Chapter 2, we present the formalization of the Romero-Sergeraert's algorithm - this algorithm builds an admissible discrete vector field associated with matrices. Chapters 3 and 4 are devoted to the Coq formalization of the necessary mathematics to reduce the size of data structures preserving the homological properties. In particular, we have formalized in Coq a version of the Basic Perturbation Lemma for finitely generated chain complexes. This is an important lemma in Computational Homological Algebra. Chapter 5 deals with certified computation of the homology given a pair of matrices. Chapter 6 is devoted to experimental aspects of our research. This chapter includes different experiments with batteries of examples, comparison of timing costs of the programs implemented along the thesis, and the way of computing, in a certified way, the homology of a real biomedical image - in this computation, Haskell programs are used as oracles due to efficiency problems within Coq. The thesis ends up with a chapter of conclusions and further work, and the bibliography.