The Little Prover - 图1

    关键字:J-Bob, lisp, axiom, theorem, claim, total function, recursion, induction

    推荐:★★★★
    难度:★★

    豆瓣链接:https://book.douban.com/subject/26429992/


    这是一本期待已久的『小人书』,
    前几本都在讲具体的语言,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!