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 co...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Poza López de Echazarreta, María
Otros Autores: Domínguez Pérez, César (Universidad de La Rioja)
Formato: text (thesis)
Lenguaje:eng
Publicado: Universidad de La Rioja (España) 2013
Materias:
Acceso en línea:https://dialnet.unirioja.es/servlet/oaites?codigo=37842
Etiquetas: Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
id oai-TES0000004255
record_format dspace
institution DialNet
collection DialNet
language eng
topic Interactive theorem provers
Homological processing
Biomedical images
Formalization of mathematics
Asistentes para la demostración
Procesamiento homológico
Imágenes biomédicas
Formalización de matemáticas
spellingShingle Interactive theorem provers
Homological processing
Biomedical images
Formalization of mathematics
Asistentes para la demostración
Procesamiento homológico
Imágenes biomédicas
Formalización de matemáticas
Poza López de Echazarreta, María
Certifying homological algorithms to study biomedical images
description 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.
author2 Domínguez Pérez, César (Universidad de La Rioja)
author_facet Domínguez Pérez, César (Universidad de La Rioja)
Poza López de Echazarreta, María
format text (thesis)
author Poza López de Echazarreta, María
author_sort Poza López de Echazarreta, María
title Certifying homological algorithms to study biomedical images
title_short Certifying homological algorithms to study biomedical images
title_full Certifying homological algorithms to study biomedical images
title_fullStr Certifying homological algorithms to study biomedical images
title_full_unstemmed Certifying homological algorithms to study biomedical images
title_sort certifying homological algorithms to study biomedical images
publisher Universidad de La Rioja (España)
publishDate 2013
url https://dialnet.unirioja.es/servlet/oaites?codigo=37842
work_keys_str_mv AT pozalopezdeechazarretamaria certifyinghomologicalalgorithmstostudybiomedicalimages
_version_ 1718346605198835712
spelling oai-TES00000042552019-06-09Certifying homological algorithms to study biomedical imagesPoza López de Echazarreta, MaríaInteractive theorem proversHomological processingBiomedical imagesFormalization of mathematicsAsistentes para la demostraciónProcesamiento homológicoImágenes biomédicasFormalización de matemáticasEn 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.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.Universidad de La Rioja (España)Domínguez Pérez, César (Universidad de La Rioja)Rubio García, Julio (Universidad de La Rioja)2013text (thesis)application/pdfhttps://dialnet.unirioja.es/servlet/oaites?codigo=37842engLICENCIA 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