Зачем мне нужны контексты оценки в Redex?

Question

Вполне возможно написать правила оценки для моего языка без использования контекстов оценки. Моя семантика полностью основана на значении и не позволяет продвигать термин внутри лямбд. Несмотря на это, все ресурсы, которые я видел, так или иначе используют контексты сокращения. Есть ли веская причина использовать контексты, которые мне не хватает?

Answer 1

Короткий ответ: нет, но с ними намного проще.

Длинный ответ: Практически во всем, для чего вы будете использовать контекст оценки, вы можете сами сделать с помощью другого правила сокращения в отношении сокращения, оно становится гораздо более неприятным, особенно если вы моделируете что-либо, кроме самых маленьких языков.

Допустим, вы хотите смоделировать вызов по лямбда-исчислению значения. Язык для него (без контекстов оценки) будет:

(define-language Lv
  (v (λ (x) e))
  (e v
     (e e))
  (x variable-not-otherwise-mentioned)
  #:binding-forms
  (λ (x) e #:refers-to x))

(здесь последние две строки используются для того, чтобы воспользоваться преимуществом захвата Redex и избежать подмены.

Теперь давайте попробуем создать семантику для этого языка без использования оценочных контекстов. Мы можем расширить подвыражения в двух местах: оператор и операнд приложения-функции. Итак, в том числе и с нормальным бета-сокращением мы получаем

(define red
  (reduction-relation
   Lv
   (--> (e_1 e_2)
        (v_1 e_2)
        (where v_1 ,(first (apply-reduction-relation red (term e_1)))))
   (--> (v_1 e_2)
        (v_1 v_2)
        (where v_2 ,(first (apply-reduction-relation red (term e_2)))))
   (--> ((λ (x) e) e_2)
        (substitute e x e_2))))

Это не так уж плохо, но помните, что мы должны добавить дополнительное правило для каждого места, которое может быть оценено подвыражением. Так что пусть понадобится свое собственное правило, если понадобится собственное правило и т. Д. И помните, что это на вершине правил для каждой из этих форм.

Гораздо проще сделать это с помощью контекстов оценки, которые позволяют нам указать, какие выражения имеют подвыражения, которые могут сделать шаг, и в каком порядке они должны произойти. Поэтому давайте попробуем переписать наш Lv язык с оценочными контекстами:

(define-language Lv2
  (v (λ (x) e))
  (e v
     (e e))
  (x variable-not-otherwise-mentioned)
  (E hole
     (E e)
     (v E))
  #:binding-forms
  (λ (x) e #:refers-to x))

Теперь это на три строки длиннее, но это говорит redex, что мы будем оценивать наши выражения в контексте оценки, E и когда он завершит оценку выражения, поместите его в контекст (где hole это контекст верхнего уровня, так сказать). Таким образом, мы можем сократить наше отношение сокращения до одного правила - уменьшение бета:

(define red2
  (reduction-relation
   Lv2
   (--> (in-hole E ((λ (x) e) e_2))
        (in-hole E (substitute e x e_2)))))

Здесь мы используем in-hole сказать, что мы в дыре, которая следует E как показано выше. Это следует за семантикой вызова по значению, потому что дыры могут появляться только слева направо в приложениях.

Вы можете вообразить, что если бы у вас было гораздо большее исчисление со многими подвыражениями, это избавило бы вас от написания очень большого количества правил сокращения.

Итак, резюмируя, вам не нужно, это просто делает вашу модель намного короче.