关于Supercompliation里的一些名词解释 & 勘误

[Javran]

由于讨论的时候大家普遍觉得这篇里用的一些名词不是很常规(或许是因为70s名词还不是很统一?),所以开个issue稍微汇总一下上次讨论之后的共识.或许不是很准确,大家补充就是了.

此外原文里有几个小错误顺便也放在这里了

• configuration 是包含自由变量的表达式
• closed expression 相对的,不包含自由变量(原文中提到的"without any variables"应该指的是"without any free variables")
• substitution 是在表达式中把左手边的变量替换为右手边的表达式,原文里那个 e/{v1 := e, ..., vn := en} 应该是 e/{v1 := e1, ..., vn := en} 注意这个替换应该是同时发生的否则紧接着的那个exercise就无解了
• program 是一系列的函数定义.见 Figure1: SLL abstract syntax

一个具体的例子见Figure5: An example of a task evaluation.最上方深色的框里,(even(sqr(S(x)))是一个configuration(因为其中的x是自由变量),prog1是一个program,其中包含了Figure2: prog1: Working with Peano number的一系列定义, 下面的x := Z()理解成substitution (所以大概就是我们现在说的environment).

Figure 5里在接下来的s0,s1,...,s7中,所有带下划线的地方都是redex,大概就是可以使用Figure 3中规则的位置.

另外,Figure 2的第二行应该是add(S(x),y) = S(add(x,y)).

[Javran]

过期话题关闭