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...
Guardado en:
Autor principal: | |
---|---|
Otros Autores: | |
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 |