9.9

TAPL 读后感 2

CIS 5000: Software Foundations

不难注意到，本书是宾大 CIS 5000 的补充教材，而今年 Fall 2025 正是由作者 Benjamin C. Pierce亲自授课，可以在课程官网上获取两本主要教材：Software Foundations series 的卷 1 和卷 2（同样是有名的一套书）

diagram chase

这是一个布尔系统的三条求值规则：

if true then t_{2} else t_{3} \to t_{2} (E-IfTrue)

if false then t_{2} else t_{3} \to t_{3} (E-IfFalse)

\frac{t_{1} \to t_{1}^{'}}{if t_{1} then t_{2} else t_{3} \to if t_{1}^{'} then t_{2} else t_{3}} (E-If)

如果再加上下面这条规则，那么单步求值结果不唯一：

\frac{t_{2} \to t_{2}^{'}}{if t_{1} then t_{2} else t_{3} \to if t_{1} then t_{2}^{'} else t_{3}} (E-FUNNY2)

可以看出，这只是改变的求值的可选顺序，求值仍然是可终止的，且结果唯一。那么，如何证明这一点？

书中的习题解答用 “diagram chase” 技术给出了证明，非常优雅。

超燃配环境 - OCaml

本书使用的语言是 OCaml

在 OCaml for Windows - Installation下载 Graphic Installer 并运行，会获得一个 OCaml bash，此时在 bash 里执行 ocaml 命令就能解释和编译文件了，但是作为 VSCode 爱好者，继续配置 VSCode！

安装 OCaml Platform 扩展
在 OCaml bash 执行命令 opam install ocaml-lsp-server ocamlformat
通过在 OCaml bash 内输入文件路径来启动 VSCode，由于挂载和空格转义，路径形式为 bash /cygdrive/c/Users/.../Microsoft\ VS\ Code/Code.exe

现在，可以在 VSCode 里使用语法提示功能，并且可以使用软件内终端进行解释和编译！

创建文件 hello.ml，输入 print_endline "Hello, world!"，使用 ocaml hello.ml 即可在终端中输出 Hello, world!

既然已经有了 opam，不妨顺手把 Coq 给装了，参考知乎文章编译原理：Coq安装与配置(vscode），作者是 SJTU IEEE CS $\to$ CMU MSML，现居匹兹堡，太成功了！！！（令我想到一位故人）

结果找不到头文件 gmp.h，出了问题，一看官网，写了这么一段话：

depext-cygwinports unfortunately became increasingly useless, as the main maintainer of the corresponding packages stopped his activities more than a year ago. Hopefully someone else will develop a suitable alternative; many packages rely on current third-party libraries like gmp.

好吧，不是我的问题，是停止维护的问题。于是放弃在 OCaml for Windows 里装 Coq 了，换成 WSL！

既然用了 WSL，那么之前基于 Windows 装的东西就全没用了。先试着直接在一个已经装的 Debian 里安装，结果折腾了半天，网络问题都解决不了，我猜这是因为它是 CSAPP 课程特供版，做了某些手脚，于是新装了一个 Ubuntu，光速解决问题，配好了 OCaml 和 Coq，拿下！什么 Mingw-w64，Cygwin，OCaml for Windows，鬼才用！WSL 是世界上最伟大的发明！

MISC

在西区教育超市购置了一个 22.5W 充电头和一根三头充电线，现在可以在宿舍同时为两个设备充电。由于现在有了 Micro USB 充电口，可以为入耳式蓝牙耳机充电，用于室外活动，防止佩戴头戴式耳机自动变成嘉豪。可惜的是，今天整个晚上都在配环境，被 OCaml for Windows 玩来玩去，没时间出去夜骑和跑步了。