Scan barcode
A review by blaisepascal
The Little Prover by Carl Eastlund, Daniel P. Friedman
4.0
The Little Prover is a book on learning how to inductively prove programs correct. Like the other "Little" books by Friedman, it is written in a question/answer style, and uses a dialect of Lisp as the main computer language.
The proof technique used is basically a rewriting schema, where the idea is to "prove" a statement by applying a series of theorems and axioms which allow you to rewrite the statement, ultimately attempting to rewrite it to 't, or true. Rewriting theorems include the ability to rewrite "(if a c c)" to just "c" for any value of "a" and "c" (and the converse: rewrite "c" to "(if a c c)" for any value of "c" and "a", if that's helpful), rewrite "(equal a a)" to 't, rewrite "(if 't x y)" to "x", and so on. There are 21 rewrite rules given. Most of the book introduces these rewrite rules and gives you practice in using them.
Also discussed is a proof assistant called "J-Bob", which implements the Lisp dialect used in the book and provides an interactive tool to help write the proofs. I am not enamored by the syntax of parts of J-Bob, especially the syntax needed to give a "path" to the "focus" of a rewrite rule. For instance, to apply the "equal-same" rewrite rule to the statement "(if (if (atom b) (equal 'polar 'polar) 'f) (equal a 'bear) 't)" you'd have to specify the "path" (Q A 1), meaning the question of the first if, the answer to the second if , and the first argument to the function application, which is "(equal 'polar 'polar)". Each step in a proof uses a path based on the results of the previous step, so it is hard to read a proof in J-Bob and picture exactly how the transformations are going to understand the proof.
Of the 218 pages of the book (not counting frontmatter and backmatter, 162 are the main text, 15 are an introduction to using J-Bob, 20 are all the proofs in the book in J-Bob syntax, and 12 are the implementation of J-Bob itself. While I think the use of an interactive proof helper is useful, devoting almost 50 pages of a rather short book to the proof helper seems a bit much, especially one that is not quite as user-friendly as it could/should be.
Ignoring J-Bob, the book sometimes goes a bit fast. It may ask the question "Can we simplify this focus in this statement? (...)" with the answer "Sure, by using foo, then simplifying with bar, bat twice, and bar again. (...)". While the use of foo is perhaps easy to see (we are in the part of the book teaching about foo...), it isn't until after using foo that we would see how to apply bar, bat, and so on. Those intermediate steps are mentioned, but not shown.
I wish the "Little" books were available in an electronic format, as it would make it a lot easier to work through the book with an editor and/or lisp interpreter at hand without having to hold open the book with one hand and type with the other.
Over all, if you like the style of the other "Little" books, which I do, despite the gripes above which are frankly common to all of them, you'll probably like this one as well, and learn about inductive proving and proof assistants along the way.
The proof technique used is basically a rewriting schema, where the idea is to "prove" a statement by applying a series of theorems and axioms which allow you to rewrite the statement, ultimately attempting to rewrite it to 't, or true. Rewriting theorems include the ability to rewrite "(if a c c)" to just "c" for any value of "a" and "c" (and the converse: rewrite "c" to "(if a c c)" for any value of "c" and "a", if that's helpful), rewrite "(equal a a)" to 't, rewrite "(if 't x y)" to "x", and so on. There are 21 rewrite rules given. Most of the book introduces these rewrite rules and gives you practice in using them.
Also discussed is a proof assistant called "J-Bob", which implements the Lisp dialect used in the book and provides an interactive tool to help write the proofs. I am not enamored by the syntax of parts of J-Bob, especially the syntax needed to give a "path" to the "focus" of a rewrite rule. For instance, to apply the "equal-same" rewrite rule to the statement "(if (if (atom b) (equal 'polar 'polar) 'f) (equal a 'bear) 't)" you'd have to specify the "path" (Q A 1), meaning the question of the first if, the answer to the second if , and the first argument to the function application, which is "(equal 'polar 'polar)". Each step in a proof uses a path based on the results of the previous step, so it is hard to read a proof in J-Bob and picture exactly how the transformations are going to understand the proof.
Of the 218 pages of the book (not counting frontmatter and backmatter, 162 are the main text, 15 are an introduction to using J-Bob, 20 are all the proofs in the book in J-Bob syntax, and 12 are the implementation of J-Bob itself. While I think the use of an interactive proof helper is useful, devoting almost 50 pages of a rather short book to the proof helper seems a bit much, especially one that is not quite as user-friendly as it could/should be.
Ignoring J-Bob, the book sometimes goes a bit fast. It may ask the question "Can we simplify this focus in this statement? (...)" with the answer "Sure, by using foo, then simplifying with bar, bat twice, and bar again. (...)". While the use of foo is perhaps easy to see (we are in the part of the book teaching about foo...), it isn't until after using foo that we would see how to apply bar, bat, and so on. Those intermediate steps are mentioned, but not shown.
I wish the "Little" books were available in an electronic format, as it would make it a lot easier to work through the book with an editor and/or lisp interpreter at hand without having to hold open the book with one hand and type with the other.
Over all, if you like the style of the other "Little" books, which I do, despite the gripes above which are frankly common to all of them, you'll probably like this one as well, and learn about inductive proving and proof assistants along the way.