Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Synthesis of list algorithms by mechanical proving
Drămnesc I., Jebelean T. Journal of Symbolic Computation69 (C):61-92,2015.Type:Article
Date Reviewed: Jan 11 2016

Program synthesis via extraction of programs from constructive proofs is now very well established, with a large literature base. There are still quite a few hurdles to overcome, but the meta-theory has been in place for quite some time now.

It is thus disappointing that the authors of the paper seem to ignore almost all of it. Looking at their references, one is at once struck by how old most of them are; this is not necessarily bad--the pioneers deserve continued recognition. But this research area is currently extremely active, so it is baffling to find no reference to it at all. Especially since there really is a lot of relevant work around; various items done with Coq [1], Isabelle [2], or ACL2 [3] come immediately to mind. Every proof strategy that I looked up was known or a special case of a strategy in Visser’s 2005 survey [4]. Automating such proofs is now considered feasible; see Claesen and colleagues [5] for just one example.

Digging a little deeper, it is surprising that there are also no real references for the theory of lists; in particular, Bird’s classic paper [6] (cited 524 times, thus rather well known) is apparently unknown to the authors. It should also be noted that the authors reference 11 of their own papers, five of which are actually technical reports.

Fundamentally, this work is very ad hoc and ignores most of the current research on the topic. It is also made extra hard to read by using non-standard notation throughout.

Reviewer:  Jacques Carette Review #: CR144090 (1604-0269)
1) Tesson, J.; Hashimoto, H.; Hu, Z.; Loulergue, F.; Takeichi, M. Program calculation in Coq. In Proc. of the Int. Conf. on Algebraic Methodology and Software Technology. Johnson, M., Pavlovic, D., Eds. Springer-Verlag, 2010, 163–179.
2) Basin, D. A. Logic framework for logic programs. In Proc. of the 4th Int. Workshops on Logic Programming Synthesis and Transformation. Springer-Verlag, 1994, 1–16.
3) Bevier, B. Source code for ACL2. Computational Logic, Inc. Austin, TX, 1997. https://github.com/acl2/acl2/blob/master/books/data-structures/list-defuns.lisp.
4) Visser, E. A survey of strategies in rule-based program transformation systems. Journal of Symbolic Computation 40, 1(2005), 831–873.
5) Claesen, K.; Johansson, M.; Rosen, D.; Smallbone, N. Automating inductive proofs using theory exploration. In Automated Deduction - CADE-24. Springer, 2013, 392–406.
6) Bird, R. Introduction to the theory of lists. Univ. Oxford Computing Lab, Oxford, UK, 1986.
Bookmark and Share
  Featured Reviewer  
 
Algorithms (I.1.2 )
 
 
Mechanical Theorem Proving (F.4.1 ... )
 
Would you recommend this review?
yes
no
Other reviews under "Algorithms": Date
Standard bases and some computations in rings of power series
Becker T. Journal of Symbolic Computation 10(2): 165-178, 1990. Type: Article
Dec 1 1992
Real zeroes of polynomials
Collins G. (ed), Loos R., Springer-Verlag New York, Inc., New York, NY, 1983. Type: Book (9780387817767)
Jun 1 1985
Fast parallel absolute irreducibility testing
Kaltofen E. (ed) Journal of Symbolic Computation 1(1): 57-68, 1985. Type: Article
Apr 1 1989
more...

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