Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
The little prover
Friedman D., Eastlund C., The MIT Press, Cambridge, MA, 2015. 248 pp. Type: Book (978-0-262527-95-8)
Date Reviewed: Dec 9 2015

The goal of this book is to teach readers how to prove that recursive Lisp programs are correct. The method used is based on principles from mathematical logic; it involves identifying basic axioms, theorems, and rules of text transformation, and expressing those axioms, theorems, and rules in Lisp notation. Using induction, the axioms and rules are then used to prove that the theorems--which are really Lisp programs--return the value of true.

The strategy is to present material leading up to three kinds of induction: list induction, star induction, and defun induction. List induction deals with a list in a natural order: first element first, and each subsequent element in turn until the end of the list. Star induction follows a similar order, but in this case any element of the list can itself be a list. List induction and star induction are given as Lisp procedures on page 125. Defun induction, a more general form of induction, is given a rather lengthy, precise mathematical definition on page 124, where the reader is told that list induction and star induction are each based on defun induction. On page 136, the reader is told to go back through chapter 9, “Changing the Rules,” if necessary, since “defun induction can take time.” Indeed. The entire book, in fact, merits very careful reading and rereading, perhaps more than once.

­The little prover is written in a style similar to two other well-known books, The little Lisper [1] and The little Schemer [2]. Information is presented in small chunks in two columns that mimic a dialog where the voice in one column asks questions or presents information that needs elucidation, and the voice in the other column replies with explanations or suggestions. This Socratic method, meant to convey knowledge in a gentle, friendly manner, is very effective in The little Lisper and The little Schemer, which teach the reader how to write recursive programs. The subject matter of The little prover, however, is much more intellectually demanding, and the Socratic method is not quite as effective here.

Although only 229 pages long, The little prover is a challenging book. The whimsical chapter titles (“Old Games, New Rules”; “Even Older Games”; “What’s in a Name?”; “Part of This Total Breakfast”; “Think It Over, and Over, and Over”; “Think It Through”; “Oh My, Stars!”; “Learning the Rules”; “Changing the Rules”; and “The Stars are Aligned”) convey little information about their contents.

On the other hand, the entire book consists of a guided tour of examples and detailed explanations. To draw attention to specific sections of code, the authors use three colors. Sample code is given in blue, with selected sections in blue or red. A section of code that is about to be transformed by a rule (here called “the focus”) is given in black, and sections of code that need to be highlighted or identified in the accompanying discussion (inductive premises, for example) are given in red. The use of multiple colors is extremely effective.

And now we come to the second element of The little prover: J-Bob. J-Bob is a simple proof assistant defined in the same language as the theorems proved in the book. The code for J-Bob is given in the book and can, of course, be downloaded (http://the-little-prover.org). Appendix A, “Recess,” explains what J-Bob is by experimenting with it. Appendix B, “The Proof of the Pudding,” lists J-Bob code for all examples and proofs in the book. Appendix C, “The Little Assistant,” gives the code for J-Bob in ACL2 and in Scheme. (I ran examples in DrRacket using the Dracula package.) The authors “encourage the reader to implement J-Bob and its language in any language of choice.”

The book can be read and understood without using J-Bob at all, but the authors strongly encourage the reader to use it. I got a great deal more from the text itself than from running J-Bob.

The book concludes with Appendix D, “Restless for More?” a brief but excellent set of recommendations for further study. Finally, the index is indispensable.

The authors are correct in claiming that acquaintance with The little Lisper or The little Schemer is not essential, since The little prover contains the relevant information. However, prior experience with recursive programming is invaluable. I would consider it a prerequisite.

This book is best approached in class under the guidance of an instructor who can shed light on questions or difficulties. The reader who tackles this book for self-instruction can expect to put out considerable effort.

More reviews about this item: Amazon, Goodreads

Reviewer:  Edgar R. Chavez Review #: CR144006 (1602-0104)
1) Friedman, D. P.; Felleisen, M. The little Lisper (3rd ed.). Pearson, Upper Saddle River, NJ, 1989.
2) Friedman, D. P.; Felleisen, M. The little Schemer (4th ed.). MIT Press, Cambridge, MA, 1995.
Bookmark and Share
  Reviewer Selected
Featured Reviewer
 
 
Deduction And Theorem Proving (I.2.3 )
 
 
Complexity Of Proof Procedures (F.2.2 ... )
 
 
Mechanical Theorem Proving (F.4.1 ... )
 
 
Mathematical Logic (F.4.1 )
 
 
Nonnumerical Algorithms And Problems (F.2.2 )
 
Would you recommend this review?
yes
no
Other reviews under "Deduction And Theorem Proving": Date
Noninteractive zero-knowledge
Blum M., De Santis A., Micali S., Persiano G. SIAM Journal on Computing 20(6): 1084-1118, 1991. Type: Article
Jan 1 1993
Cut elimination and automatic proof procedures
Zhang W. Theoretical Computer Science 91(2): 265-284, 1991. Type: Article
Apr 1 1993
A non-reified temporal logic
Bacchus F., Tenenberg J., Koomen J. Artificial Intelligence 52(1): 87-108, 1991. Type: Article
Oct 1 1992
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