有人看完过《计算机程序设计艺术》的前三卷吗?


#21

说起不可变数据结构和算法,有谁说说 purely functional data structurepearly of functional algorithm design,以及其它的(比如有些书名里有persistent)的书吗?


#22

ACL2 在 certify-books 的时候 我忽略 sv 可以吗?

esim的defmodules会出错 但可以不编译 sv呢?


#23

不需要做 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 改一改。


#24

因为名字里面有 immutable 所以买来镇宅?


#25

谢谢 basic已经编译过了

文档用的是emacs-acl2.el中的acl2-doc ,还是带books的版本 单个文件80Mb的


#26

Computer-Aided Reasoning 是 A Computational Logic 的续作,后者并非是 ACL2 而是其旧版本,但大部分通用而且是 Public Domain 的,前者并非免費且定价挺高(不過 Appendices 可以免費看,是个简要使用说明,还比較有用),是不是要看就看个人意愿了。

真要說的話 ACL2 超过了 TAOCP 的內容,但我也只是指望你能过一遍,这樣的好处在于:

  1. 看到 TAOCP 中偏向数学和逻辑的部分不会立马懵逼。
  2. 不会再产生「学会这个有什麼用」的问題。能解決几亿美圓问題的工具会沒用?
  3. TAOCP 中的一些习題用 ACL2 做可以减少心智负担,也就是說你知道 ACL2 怎么工作,然後能用 ACL2 证明就代表你会做这个证明,而不用亲自去做证明,which 对习慣写代碼的人很伤。

#27

准备看啊,能借到pearls那本,打算看先看那本了,别的有空再看。


#28

道客巴巴上能一页一页的看

Case Studies 看了个开头(前四章)

应该从 An Approach 开始


#29

An Approach 中提到过 PVS 和 HOL

你有了解吗?


#30

这两个是 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 沒有太多帮助。


另外有个彩蛋

https://www.zhihu.com/question/36406987/answer/98026554


#31

高德纳 因为排版不好而开发了TeX

我是否应该先熟悉下LaTeX

套用数理逻辑导论中的一句话:

符号体系在数学中所发挥的巨大作用是大家都知道的,但很少有人追究过下列问题: 符号体系究竟起了多么巨大的作用?它起巨大作用的根源又在哪里?

看到个新闻:有人说黎曼猜想被证明了(9月24日见)。


#32

不需要。

  1. TeX 是一个偏向于美学的工具,能从中受益的基本是字体设计和排版方面的从业者。TeX 宏语言也算不上多好的编程语言,甚至可以当作编程语言设计和软件项目管理的反面教材。
  2. LaTeX 只是一个封装,就算熟练使用它也不见得需要对 TeX 有多少理解,Don Knuth 写了说明书 The TeXbook,然而同上条所说,这本书讲的完全是排版上的美学,和符号更是完全不沾边

当然,花点时间学会基本的使用还是值得的。反正就是想学就学,不需要什么理由,实际上写几份 paper 基本就熟悉了

大概知道一点,总之学界不是很看好


#33

卷4瞄了瞄,对我很有用哪。前几卷倒是没看过,典型CS的算法问题,不太能用到,貌似MIT的那本算法导论对我小白来说足够了。

现在最怕的就是Don佬的身体了,希望能起码写完5卷,最好6卷,要是完成他规划的7卷,真是造福人类啊


#34

宣称被证明了,等待大会报告后的反馈,估计就是对的也得审个至少大半年以上