functional-programming - 什么是“减少语义”？请通俗地解释一下PLT Redex的使用

Question

有人请用更简单的语言解释归约语义和 PLT Redex 的用法。

谢谢。

Answer 1

约简语义是一种计算技术，它涉及用等价的（并且希望更小的）表达式替换表达式，直到无法再替换为止。如果一种语言是图灵完备的，那么有些表达式永远不会停止替换。

减少通常用右箭头表示，最好用例子来解释：

(3 + 7) + 5   -->  10 + 5  -->  15

这显示了算术表达式的标准归约语义。表达式15不能进一步简化。

希望这可以帮助。

Answer 2

约简语义与上下文语义相似（如果不相同？）。任何表达式都可以分解为上下文并重新定义。

Robert Harper 的 Practical Foundations for Programming Languages（此处提供 PDF 草案）第 9.3 节 Contextual Semantics 很好地解释了它们。

一个例子：

print 5+4
**context: print [],  redex: 5+4
**evaluate redex: 9
**plug back into context

print 9
**context: [], redex: print 9
**evaluate redex: nil  ==> 9
**plug back into context

nil

您可以将 redex '粘'回上下文的'洞'中以获得：打印 5+4。评估发生在 redex。您将表达式分解为上下文 + redex，评估 redex 以获得新的表达式，将其插入上下文中，冲洗并重复。

这是一个稍微复杂一点的例子，它需要了解计算 lambda 演算的抽象机器：

(lambda x.x+1) 5
**context: [] 5, redex: (lambda x.x+1)
**evaluate redex: <(lambda x.x+1), {environment}> <- create a closure
**plug back into context

<(lambda x.x+1), {}> 5
**context: [], redex: <(lambda x.x+1), {}> 5
**evaluate redex: x+1 where x:=5
**plug back into context

x+1 where x:=5
**context: []+1, redex: x
**evaluate redex: 5 (since x:=5 in our environment)
*plug back into context

5+1...
6

编辑：棘手的部分是识别在哪里将表达式分解为上下文和 redex。它需要了解语言的操作语义（接下来需要评估的表达式的“部分”）。