Certifying homological algorithms to study biomedical images

Resumo

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.