Certifying homological algorithms to study biomedical images

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.

Grantor dc:publisher

Universidad de La Rioja (España)

Year dc:date

2013

Author dc:creator

• Poza López de Echazarreta, María

Contributors dc:contributor

• Domínguez Pérez, César (Universidad de La Rioja)
• Rubio García, Julio (Universidad de La Rioja)

• Interactive theorem provers
• Homological processing
• Biomedical images
• Formalization of mathematics
• Asistentes para la demostración
• Procesamiento homológico
• Formalización de matemáticas
• Imágenes biomédicas

Statement dc:rights

• LICENCIA DE USO: Los documentos a texto completo incluidos en Dialnet son de acceso libre y propiedad de sus autores y/o editores. Por tanto, cualquier acto de reproducción, distribución, comunicación pública y/o transformación total o parcial requiere el consentimiento expreso y escrito de aquéllos. Cualquier enlace al texto completo de estos documentos deberá hacerse a través de la URL oficial de éstos en Dialnet. Más información: https://dialnet.unirioja.es/info/derechosOAI | INTELLECTUAL PROPERTY RIGHTS STATEMENT: Full text documents hosted by Dialnet are protected by copyright and/or related rights. This digital object is accessible without charge, but its use is subject to the licensing conditions set by its authors or editors. Unless expressly stated otherwise in the licensing conditions, you are free to linking, browsing, printing and making a copy for your own personal purposes. All other acts of reproduction and communication to the public are subject to the licensing conditions expressed by editors and authors and require consent from them. Any link to this document should be made using its official URL in Dialnet. More info: https://dialnet.unirioja.es/info/derechosOAI

Language dc:language

eng

Repository record dc:identifier

https://dialnet.unirioja.es/servlet/oaites?codigo=37842

OAI identifier oai:identifier

oai:dialnet.unirioja.es:TES0000004255