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

Posted 2023-02-24

【中文标题】什么是“减少语义”？请通俗地解释一下PLT Redex的使用

【英文标题】：What are "reduction semantics"? Please explain the use of PLT Redex in layman's term

【发布时间】：2010-11-14 08:40:09

【问题描述】：

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

谢谢。

【参考方案1】：

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

Robert Harper 的 Practical Foundations for Programming Languages（PDF 草案可用here）第 9.3 节上下文语义很好地解释了它们。

一个例子：

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。它需要了解语言的操作语义（接下来您需要评估表达式的哪个“部分”）。

【参考方案2】：

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

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

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

这显示了算术表达式的标准归约语义。表达式15 不能再减少了。

希望这会有所帮助。

【讨论】：

另见 redex 网站 (redex.plt-scheme.org) 和最近出版的书（“Semantics Engineering with PLT Redex”）。

@Norman：归约和评估的替代模型一样吗？