Certifying homological algorithms to study biomedical images

• Autores: María Poza López de Echazarreta
• Directores de la Tesis: César Domínguez (dir. tes.) , Julio Rubio García (dir. tes.)
• Lectura: En la Universidad de La Rioja ( España ) en 2013
• Idioma: inglés
• Número de páginas: 261
• Tribunal Calificador de la Tesis: Eladio Domínguez Murillo (presid.) , María Vico Pascual Martínez-Losa (secret.) , Ángel Ramón Francés Román (voc.) , Yves Bertot (voc.) , José Luis Ruiz Reina (voc.)
• Enlaces
  • Tesis en acceso abierto en: Dialnet
• Resumen
  • español

    En esta tesis se aborda el problema de la verificación de programas para el procesamiento homológico de imágenes biomédicas. Concretamente, se formalizan en la herramienta de demostración Coq/SSReflect algoritmos para el cálculo de grupos de homología, lo que produce programas ejecutables que son correctos por construcción. Como una tarea necesaria se formalizan partes de matemáticas relacionadas con la Topología Algebraica.

    La idea central en la tesis es que se puede formalizar en teoría de tipos constructiva (y, por tanto, se pueden obtener programas correctos) todo el proceso que lleva de una imagen digital al cálculo homológico que permite interpretar topológicamente la imagen de partida. Cuando este esquema general se aplica a imágenes biomédicas, aparece el problema de que su enorme talla impide que los programas correctos sean aplicados sobre ellas. Por ello, se hace necesario utilizar (y formalizar) técnicas de homología efectiva que permiten reducir el tamaño de las estructuras de datos, preservando la información homológica.

    Tras un primer capítulo de preliminares (con una introducción de las matemáticas a formalizar y de Coq/SSReflect, así como la metodología utilizada), en el capítulo 2 se formaliza un algoritmo de Romero-Sergeraert para la construcción de campos admisibles de vectores discretos asociados a matrices que provienen de imágenes digitales.

    En los capítulos 3 y 4 se formalizan en Coq las matemáticas necesarias para demostrar la corrección de un algoritmo que produce la reducción asociada a un campo de vectores discretos. En particular, hemos formalizado una versión del Lema Básico de Perturbación para complejos de cadenas finitamente generados; este "lema" es un resultado central en el Álgebra Homológica Computacional.

    El capítulo 5 versa sobre el cálculo verificado de la homología y el capítulo 6 está dedicado a los aspectos experimentales de nuestra investigación: se recogen distintos experimentos con baterías de ejemplos, se compara el rendimiento de los programas producidos a lo largo de la tesis y, finalmente, se consigue calcular de modo certificado la homología de una imagen biomédica real, siendo necesario para ello (debido a problemas de eficiencia) utilizar programas Haskell como oráculos.

    La tesis termina con un capítulo de conclusiones y trabajo futuro.

  • English

    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.