The Little Prover
- External Link:
- Amazon: The Little Prover (Amazon)
- Rank: ★★★★
- Hard: ★★
- Tag: J-Bob, lisp, axiom, theorem, claim, total function, recursion, induction
- Reviews:
这是一本期待已久的『小人书』，
前几本都在讲具体的语言，Lisp, Scheme，
而这一本很不相同，在讲Prover。
在看这本书之前，根本不知道Prover是什么，
满满的都是神秘，茫然不知所措，
其他方面，仅知道有Coq这种Proof assistant。
于是，很期待这本书，
如果读完以后就能变成了大牛多好，
然而，这一定是不可能的。
本书从一开始就埋下了伏笔，
作者说书末尾有一个神奇的J-Bob工具，
可以用来自动证明定理。
好吧，为了能达到这一步，
还是硬着头皮看下去吧。
一问一答式的风格，确实很新颖，
但是也比较啰嗦。
让读者在自问自答中，
提取出作者想要表达什么，
像解谜一样，私以为特别费力。。。
本书讲了，什么是公理，什么是定理，
什么是total function，什么是function的measure，
什么是induction，以及三种induction，
List induction, Star induction, Defun induction
剩下的大部分篇幅，
都在推导。。。
本书涉及到的数学概念很少，
适合任何年龄阶段阅读品评，
其中，Recursion是一个很核心的概念，
值得慢慢琢磨。
书末尾的J-Bob出现后，
文风忽然犀利了，
剧情忽然明朗了，
音乐忽然摇滚了。
可以使用J-Bob在人肉指定推导步骤的情况下，
自动得到结论，
这想必就是辅助证明吧。
但即使这样，J-Bob仍然是一个很别致的『小玩意』，
要能支持已经证明过的定理，
支持指定当前focus的推导位置，
支持指定induction的方式。
作者在附录B把全书用J-Bob证了一遍，
畅快淋漓。
J-Bob有CL和Scheme实现，
书中还提到了ACL2，据说是一个更牛的Prover，
只需要指定公理和定理，不用指定步骤都行。
How amazing!