A certified reduction strategy for homological image processing

TL;DR

This paper presents a verified reduction strategy for digital image analysis in homological algebra, ensuring correctness through formal methods, with applications in bioinformatics where accuracy is critical.

Contribution

It introduces a certified reduction approach that preserves homological properties of images, combining computation and deduction for reliable results.

Findings

Formal verification of algorithms ensures correctness

Integration of computation and deduction improves performance

Application demonstrates high accuracy in bioinformatics

Abstract

The analysis of digital images using homological procedures is an outstanding topic in the area of Computational Algebraic Topology. In this paper, we describe a certified reduction strategy to deal with digital images, but preserving their homological properties. We stress both the advantages of our approach (mainly, the formalisation of the mathematics allowing us to verify the correctness of algorithms) and some limitations (related to the performance of the running systems inside proof assistants). The drawbacks are overcome using techniques that provide an integration of computation and deduction. Our driving application is a problem in bioinformatics, where the accuracy and reliability of computations are specially requested.