说起不可变数据结构和算法，有谁说说 purely functional data structure 和 pearly of functional algorithm design，以及其它的(比如有些书名里有persistent)的书吗？
ACL2 在 certify-books 的时候 我忽略 sv 可以吗？
esim的defmodules会出错 但可以不编译 sv呢？
不需要做 certify books。文档也说明了可能有些 book 需要额外的依赖才能证明。而且基本学习和使用并不需要 book。
如果要做，文档只推荐做 basic build。这个我试过不需要额外依赖就能过。
http://www.cs.utexas.edu/users/moore/acl2/current/combined-manual/?topic=ACL2____BOOKS-CERTIFICATION
这个文档是可以在官网下载线下看的。不过里面用了 google font 服务导致在国内会加载很慢，自己看 index.html 改一改。
因为名字里面有 immutable 所以买来镇宅？
1 个赞
谢谢 basic已经编译过了
文档用的是emacs-acl2.el中的acl2-doc ,还是带books的版本 单个文件80Mb的
Computer-Aided Reasoning 是 A Computational Logic 的续作，后者并非是 ACL2 而是其旧版本，但大部分通用而且是 Public Domain 的，前者并非免費且定价挺高(不過 Appendices 可以免費看，是个简要使用说明，还比較有用)，是不是要看就看个人意愿了。
真要說的話 ACL2 超过了 TAOCP 的內容，但我也只是指望你能过一遍，这樣的好处在于：
- 看到 TAOCP 中偏向数学和逻辑的部分不会立马懵逼。
- 不会再产生「学会这个有什麼用」的问題。能解決几亿美圓问題的工具会沒用？
- TAOCP 中的一些习題用 ACL2 做可以减少心智负担，也就是說你知道 ACL2 怎么工作，然後能用 ACL2 证明就代表你会做这个证明，而不用亲自去做证明，which 对习慣写代碼的人很伤。
1 个赞
准备看啊，能借到pearls那本，打算看先看那本了，别的有空再看。
道客巴巴上能一页一页的看
Case Studies 看了个开头（前四章）
应该从 An Approach 开始
An Approach 中提到过 PVS 和 HOL
你有了解吗？
这两个是 Higher Order Logic，ACL2 是 first class logic。Higher Order Logic 通常涉及 type theory，建议深入学习 Haskell 或 Standard ML 或 Ocaml 中一個再去了解。Knuth 的书并沒有涉及 Higher Order Logic，而且使用 high order logic 的 proof assistant 自动化程度并不高，总之对于看 TAOCP 沒有太多帮助。
另外有个彩蛋
1 个赞
高德纳 因为排版不好而开发了TeX
我是否应该先熟悉下LaTeX
套用数理逻辑导论中的一句话：
符号体系在数学中所发挥的巨大作用是大家都知道的，但很少有人追究过下列问题： 符号体系究竟起了多么巨大的作用？它起巨大作用的根源又在哪里？
看到个新闻：有人说黎曼猜想被证明了（9月24日见）。
不需要。
- TeX 是一个偏向于美学的工具，能从中受益的基本是字体设计和排版方面的从业者。TeX 宏语言也算不上多好的编程语言，甚至可以当作编程语言设计和软件项目管理的反面教材。
- LaTeX 只是一个封装，就算熟练使用它也不见得需要对 TeX 有多少理解，Don Knuth 写了说明书 The TeXbook，然而同上条所说，这本书讲的完全是排版上的美学，和符号更是完全不沾边
当然，花点时间学会基本的使用还是值得的。反正就是想学就学，不需要什么理由，实际上写几份 paper 基本就熟悉了
大概知道一点，总之学界不是很看好
卷4瞄了瞄，对我很有用哪。前几卷倒是没看过，典型CS的算法问题，不太能用到，貌似MIT的那本算法导论对我小白来说足够了。
现在最怕的就是Don佬的身体了，希望能起码写完5卷，最好6卷，要是完成他规划的7卷，真是造福人类啊
宣称被证明了，等待大会报告后的反馈，估计就是对的也得审个至少大半年以上