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 Logic15 (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
Unification in primal algebras, their powers and their varieties
Nipkow T. (ed) Journal of the ACM 31(4): 742-776, 1984. Type: Article
Dec 1 1991
Principles of automated theorem proving
Duffy D., John Wiley & Sons, Inc., New York, NY, 1991. Type: Book (9780471927846)
Sep 1 1992
Resolution for some first-order modal systems
Cialdea M. Theoretical Computer Science 85(2): 213-229, 1991. Type: Article
Jul 1 1992

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy