什么是"减少语义"？请解释PLT Redex在外行术语中的使用

Question

有人请用简单的语言解释缩减语义和PLT Redex的用法.

谢谢.

Answer 1

缩减语义是一种计算技术,它涉及用等效(并且希望更小)表达式替换表达式,直到不再可能替换为止.如果语言是图灵完备的,那么表达式永远不会停止替换.

减少通常用右箭头表示,最好通过示例解释:

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

这显示了算术表达式的标准缩减语义.表达式15不能再进一步减少.

希望这可以帮助.

Answer 2

约简语义与上下文语义类似(如果不相同？).任何表达式都可以分解为上下文和redex.

Robert Harper的编程语言实践基础(这里提供的草案PDF )第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"粘贴"到上下文的"洞"中以获得:print 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

编辑:棘手的部分是识别将表达式分解为上下文和重新索引的位置.它需要了解语言的操作语义(下一步需要评估的表达式的"片段").