Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
A certified reduction strategy for homological image processing
Poza M., Domínguez C., Heras J., Rubio J.  ACM Transactions on Computational Logic 15 (3): Article No. 23, 2014. Type: Article
Date Reviewed: Nov 6 2014

True-life biomedical images, such as the synapses of neurons, are too large and onerous to process. How should the data structures of huge digital images be reliably condensed without losing their homological properties? Poza et al. propose a specialized reduction scheme for homological image processing. The unaccustomed reader of topology is encouraged to browse the imaginative algorithms used to enlighten computational topology in Computational topology [1], prior to exploring the formal mathematical validations of the algorithms for image reduction and processing in this paper.

The reputable basic perturbation lemma (BPL) is used to verify the correctness of algorithms for preserving the homological properties of digital images split into segments of small data structures. The authors present a considerably shortened formalization of the BPL. They (1) define chain complexes as families of structure-preserving maps (module morphisms) of images, (2) provide an algorithm for building the admissible discrete vector fields from the matrices of finite-type chain complexes, (3) present a vector field reduction theorem based on the BPL for computing the homology groups of much smaller finite-type chain complexes, (4) prove a generalized theorem for making use of reductions to construct the decompositions of chain complexes, and (5) show how the BPL is used to reduce the chain complexes of a digital image with the library of matrices in the SSReflect language for proving theorems in the Coq system.

The authors provide theoretical insights into proving the congruency between the homology of the chain complex of an image and the homology of its reduced chain complex. They offer insights into the creative use of the Haskell programming language for rapid prototyping of time-consuming automatic program verifications. The authors compellingly advocate the need to develop new algorithms, more effective data structures, and faster executing proof assistants for reduction in homological processing of biomedical images.

Reviewer:  Amos Olagunju Review #: CR142903 (1502-0162)
1) Edelsbrunner, H.; Harer, J. L. Computational topology: an introduction. American Mathematical Society, Providence, RI, 2010.
Bookmark and Share
  Reviewer Selected
Featured Reviewer
Mechanical Theorem Proving (F.4.1 ... )
Biology And Genetics (J.3 ... )
Formal Methods (D.2.4 ... )
Image Representation (I.4.10 )
Would you recommend this review?
Other reviews under "Mechanical Theorem Proving": Date
A theorem about computationalism and "absolute" truth
Charlesworth A.  Minds and Machines 26(3): 205-226, 2016. Type: Article
Jun 2 2017
Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
Aransay J., Divasón J.  Formal Aspects of Computing 28(6): 1005-1026, 2016. Type: Article
Mar 9 2017
Data compression for proof replay
Amjad H.  Journal of Automated Reasoning 41(3-4): 193-218, 2008. Type: Article
Aug 20 2009

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright © 2000-2021 ThinkLoud, Inc.
Terms of Use
| Privacy Policy