函数式编程：值的等价和评估答案

【问题标题】：Functional Programming: Equivalence and Evaluation to a Value函数式编程：值的等价和评估
【发布时间】：2016-11-04 16:27:55
【问题描述】：

我正在阅读一些关于 SML 的笔记，对作者的其中一个评论感到有些困惑。让e ==> v 表示对一个值的评估，e ~ e' 表示e 扩展等价于e'

作者写道：

如果e ~ e'（均为t 类型）并且存在v 类型为t 的SML 值。 e ~ v，然后有一个 SML 值 v'（同样是 t 类型），s.t. e' ==> v' 和 v ~ v'。

确保您注意到这一点（并理解我们为什么不在这里说如果e ~ e' 和e ~ v 然后e' ==> v。

为什么不呢？

【问题讨论】：

鉴于==> 的定义方式，您对fn x => 0 与fn x => (0 + 0) 有何看法？
@gallais 我想说他们总是评估相同的值，所以他们在扩展上是等价的
SML 在 lambda 抽象下会减少吗？如果我没记错的话，这两个函数已经是 values 并且它们不再减少了。但它们确实是等价的，因为它们在外延上是相等的。

标签： functional-programming sml

【解决方案1】：

因为这意味着两者都减少到相同的 syntactic 值。但外延相等与句法相等不同。这大致意味着，程序无法区分这些值。

请特别注意，函数表达式本身就是值。但是具有不同主体的不同函数值仍然可能在扩展上相等，因为它们在应用于相同参数时计算相同的结果。简单的例子：

fun x => x

和

fun x => let y = x in y

是两个语法不同但外延相等的值。

【讨论】：

【解决方案2】：

如果您以 e 和 e' 开头，已经是值 v 和 v'，那么第二个语句会说

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

可以简化为

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

这与扩展性完全相反，因为您可以拥有例如

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

它们的值不同，但外延相等。

【讨论】：