函数式程序设计:等价性与价值评估

Question

我正在读一些关于SML的注释，我对作者的一个评论感到有点困惑。让e ==> v表示值的计算，e ~ e'表示e在扩展上等价于e'

作者写道：

如果是e ~ e' (都是t类型)，并且存在一个t s.t类型的SML值v。e ~ v，则有一个SML值v' (同样是t类型)，s.t。e' ==> v'和v ~ v'. 确保您注意到了这一点(并且理解为什么我们这里没有这样说，如果e ~ e'和e ~ v那么e' ==> v。

为什么不行？

Answer 1

因为这意味着两者的句法值是相同的。但外延平等与句法平等并不相同。粗略地说，这意味着程序无法区分这些值。

特别要注意的是，函数表达式本身就是值。但是，不同体的不同函数值在广义上仍然是相等的，因为它们对相同的参数计算相同的结果。微不足道的例子：

fun x => x

和

fun x => let y = x in y

是两个在语法上不同但在广义上相等的值。

Answer 2

如果以e和e'作为v和v'的值开始，那么第二个语句会说

如果v ~ v‘和v ~ v，那么v' ==> v

可以简化为

如果v ~ v'，那么v' ==> v

这与扩展性正好相反，因为你可以有。

v = fn x => x + 0
v' = fn x => x

它们不是相同的值，但在广义上是相等的。