前情提要:/t/430679。
自从上次以来,修复了一些 bug 并重构了代码,为实现 规范顺序归约、记忆化懒惰求值 做准备。实现了 η-变换和 β-归约,并完成了一个简单的 interactive interpreter。实现这个版本的 β-规约的方法论是三步,每一步都很自然:
- 在做 β-归约时,把所有要替换的绑定变量替换为被替换的东西,并且共享对象引用(这样下次 β-归约这个被替换对象的时候,就可以一下子归约很多地方,提高效率);
- 在 β-归约 (λx. M) N 的时候,语法树里面的 M 需要被 深复制 才能替换 x 为 N,这是因为前面一个方法导致的(或是因为一些子项来自常数表导致的)共享对象会导致 M 可能和 N 共享一些引用,如果不深复制(比如,原地修改),可能会意外改变 N 里面的东西,更惨的是可能改变这个子项之外的东西;
- 要确保一次 β-归约被最佳利用,需要在 (λx. M) N 被归约后把所有 (λx. M) N 的引用都替换为归约结果。
还可以从这个 GitHub 仓库 访问代码,现已按 MIT License 提供授权。