Что такое "семантика редукции"? Пожалуйста, объясните использование PLT Redex в терминах непрофессионала.

Question

Кто-нибудь, пожалуйста, объясните использование семантики сокращения и переопределения PLT на более простом языке.

Благодарю.

Answer 1

Семантика сокращения - это метод вычисления, который включает замену выражения эквивалентным (и, мы надеемся, меньшим) выражением до тех пор, пока замена станет невозможной. Если язык полон по Тьюрингу, существуют выражения, которые никогда не прекращают замену.

Сокращение обычно обозначается стрелкой вправо, и это лучше всего объяснить на примере:

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

Это показывает стандартную семантику редукции для арифметических выражений. Выражение 15 не может быть уменьшено дальше.

Надеюсь это поможет.

Answer 2

Семантика редукции похожа (если не одинакова?) На контекстную семантику. Любое выражение можно разбить на контекст и переопределить.

Раздел 9.3 "Контекстуальная семантика" Роберта Харпера "Практические основы языков программирования" (черновой вариант PDF доступен здесь).

Пример:

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

Вы можете "вставить" редекс обратно в "дыру" контекста, чтобы получить: напечатайте 5+4. Оценка происходит в редекс. Вы разбиваете выражение на context + redex, оцениваете redex, чтобы получить новое выражение, вставляете его обратно в контекст, промываете и повторяете.

Вот немного более сложный пример, который требует знания абстрактной машины, которая оценивает лямбда-исчисление:

(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

РЕДАКТИРОВАТЬ: сложная часть распознавания, где разбить выражение на контекст и переопределить. Это требует знания операционной семантики языка (какой "фрагмент" выражения вы должны оценить далее).