Why do I need evaluation contexts in Redex?

Question

It's perfectly possible to write the evaluation rules for my language without using evaluation contexts. My semantics are entirely call by value and do not permit the term to be stepped forwards inside of lambdas. Despite this, all the resources I've seen use reduction contexts in some way. Is there a good reason to use contexts that I am missing?

Answer 1

Short answer: You don't, but its much easier with them.

Long answer: Pretty much everything you would use an evaluation context for, you can do yourself with a different reduction rule in your reduction relation, it just becomes much more obnoxious, especially as you model anything but the smallest of languages.

Let's say you want to model the call by value lambda calculus. The language for it (without evaluation contexts) would be:

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

(here, the last two lines are used to take advantage of Redex's capture avoiding substitution.

Now, lets try making the semantics for this language without using evaluation contexts. There are two places we can expand sub-expressions, the operator and the operand of function application. So, including that with normal beta-reduction gives us:

(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))))

This isn't too bad, but remember that we have to add an additional rule for every place that a sub-expression can be evaluated. So let would need its own rule, if would need its own rule, etc. And remember that this is on top of the rules for each of these forms.

A much easier way to do this is just with evaluation contexts, which allows us to specify which expressions have sub-expressions that can take a step, and what order they should happen in. So let's try rewriting our Lv language with evaluation contexts:

(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))

It's three lines longer now, but this tells redex that we'll be evaluating our expressions in an evaluation context, E, and when its done evaluating the expression, place it into the context (where hole is the top-level context so to speak). Thus, we can reduce our reduction relation down to just one rule, beta reduction:

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

Here we use in-hole to say that we are in a hole that follows E as shown above. This follows call by value semantics because holes can only appear from left to right in applications.

You can imagine that if you had a much larger calculi with many sub-expressions that this would save you from writing a very large amount of reduction rules.

So, to recap, you don't need to, it just makes your model much much shorter.