[4/3] 我觉得硬件加速定理证明过程首先要解决的是如何让 CPU 把逻辑表达式当作基本数据类型来对待并在此基础上做符号计算，但这不就是之前 Lisp 机所做的事情吗？（可能也包括所谓第五代计算机——针对 Prolog 优化）所以其实定理证明器所需的硬件指令完全可以在 Lisp 机开发者制定的复杂指令集上再加几条就够了。前人留下的那些电路图已没有实际意义，重要的是指令集和相关的数据格式。我可以从 OpenSPARC 开始研究，只要我能彻底搞清楚一个现成的多核多线程 CPU 的全部细节，就可以对其指令集加以扩展，让它支持符号计算、类型检查和硬件 GC，到时候 Lisp/Prolog/SML/HOL 的硬件加速问题就直接一锅端了。（至于祖国的 RISC-V 社区，只能先对不起了，你们的指令集太乱了……）


https://postimg.cc/gallery/8G3KVSb

https://i.postimg.cc/gJRccpb2/72fd082bgy1huncktwdozj21kw23w1gr.jpg

https://i.postimg.cc/6qf9Rh3s/72fd082bgy1huncphwt13j21kw23we84.jpg

https://i.postimg.cc/D0Tv8N7d/72fd082bgy1huncpjwd6uj21kw23wu0z.jpg