On this page:
3.1 Reduction TLDR
3.2 Small-step Reduction
3.3 Evaluation and Normalization
3.4 Testing Reduction Relations
3.5 Caveat:   Compatible Closure of Mutually Defined Relations
8.3.0.10

3 Reduction and Evaluation in Redex

After specifying my language syntax, I define reduction, normalization, and evaluation. Once I define the reduction relation, Redex gives me a nondeterministic interpreter. Redex makes this extremely easy. I can give the small-step reductions, and Redex will compute for me the compatible closure automatically, giving me a normalization relation. If I need a specific reduction strategy, I can define the evaluation contexts manually and have Redex compute the context closure of a relation. For data like numbers, I don’t need to resort to inductive encoding; I can easily escape into Racket to compute.

After defining a reduction relation, Redex can do the following for me:
  • apply one step of a reduction relation

  • apply a reduction relation until a normal form

  • apply a reduction relation until some condition

  • compute closures of a reduction relation

3.1 Reduction TLDR

In short, I define the small-step reductions using reduction-relation. I usually define the full reduction using compatible-closure, which in 1 line of code extends the small-step relation to apply under any context. When I need a specific reduction strategy, I manually define evaluation contexts as syntax, as in the previous section, and use context-closure. For querying Redex reduction relations, I use apply-reduction-relation to apply a reduction relation a single step, and apply-reduction-relation* to reduce an expression to the normal form of the given reduction relation. Since apply-reduction-relation* is a Racket function, I usually define metafunctions using define-metafunction to easily call the reduction and normalization relations from Redex. For testing reduction relations, I use test-->, test-->>, and test-->>∃.

There is one common pitfall I run into: full reduction for mutually defined syntax. If expressions and values are mutually defined, for example, then compatible-closure will not compute the correct relation. In this case, we must manually give the mutually defined contexts for which we context-closure should compute the closure of a relation. Thankfully, Redex exposes the function compatible-closure-context for computing common contexts. In most cases I encounter, Redex can easily compute the various mutual contexts with a couple of calls to compatible-closure-context, and then give me the full reduction relation using context-closure.

3.2 Small-step Reduction

In Redex, reduction relations are defined using reduction-relation. It requires a language identifier and a sequence of rewrite rules. The form also supports a lot of optional and additional features, most of which I never use. I will commonly use #:domain and #:codomain to catch bugs, including some pitfalls mentioned in the last section.

Below, I define the small-step reduction for BoxyL.

Example:
> (define ->
    (reduction-relation
     BoxyL
     #:domain e
     #:codomain e
     (--> ((λ (x : A) e_1) e_2) (substitute e_1 x e_2)
         "β→")
     (--> (car (cons e_1 e_2)) e_1
         "β×₁")
     (--> (cdr (cons e_1 e_2)) e_2
         "β×₂")
     (--> (+ v_1 v_2) ,(+ (term v_1) (term v_2))
         "plus")
     (--> (let ((box x) (box e_1)) e_2) (substitute e_2 x e_1)
         "β□")))

Unlike define-language, reduction-relation creates a Racket value. This means we need to bind it to an identifier using Racket’s define. It also means we have to be in Racket-land when using the reduction relation.

To run the reduction, I use apply-reduction-relation to take a single step, and apply-reduction-relation* to run all possible reductions.

Examples:
> (apply-reduction-relation -> (term (car (cons 1 2))))

'(1)

> (apply-reduction-relation* -> (term (car (cons (+ 1 2) 2))))

'(3)

Like redex-match, both of these return a set of results, since Redex allows the reduction relation to be non-deterministic.

We can use apply-reduction-relation* to stop when an arbitrary condition holds of the term being reduced. For example, we can stop when we try to reduce (+ 1 2).

Example:
> (apply-reduction-relation* -> (term (car (cons (+ 1 2) 2)))
    #:stop-when (lambda (term)
                  (redex-match? BoxyL (+ 1 2) term)))

'((+ 1 2))

3.3 Evaluation and Normalization

To define full reduction, we can easily get the compatible closure of the relation with respect to a nonterminal. Redex will lift the small-step relation to apply any reduction anywhere in any subexpression of the nonterminal. It’s one line of code.

Examples:
> (define ->* (compatible-closure -> BoxyL e))
> (apply-reduction-relation* -> (term (λ (x : Nat) (car (cons (+ 1 2) 2)))))

'((λ (x : Nat) (car (cons (+ 1 2) 2))))

> (apply-reduction-relation* ->* (term (λ (x : Nat) (car (cons (+ 1 2) 2)))))

'((λ (x : Nat) 3))

This lifts -> to apply under any context generated from the nonterminal e. Now we can easily compute normal form of a term.

To define the call-by-value left-to-right semantics, we can reuse the evaluation contexts defined earlier, and ask Redex to compute the closure of the relation with respect to that context via context-closure.

Examples:
> (define ->cbv (context-closure -> BoxyEvalL E))
> (apply-reduction-relation ->cbv (term (λ (x : Nat) (car (cons (+ 1 2) 2)))))

'()

> (apply-reduction-relation* ->cbv (term (λ (x : Nat) (car (cons (+ 1 2) 2)))))

'((λ (x : Nat) (car (cons (+ 1 2) 2))))

When I have a deterministic semantics, I define metafunctions that let me use a reduction relation under term. This helps me easily use reduction relations in Redex-land rather than Racket-land, and reduces boilerplate.

Examples:
> (define-metafunction BoxyL
    boxy-eval : e -> v
    [(boxy-eval e)
     ,(car (apply-reduction-relation* ->cbv (term e)))])
> (define-metafunction BoxyL
    normalize : e -> e
    [(normalize e)
     ,(car (apply-reduction-relation* ->* (term e)))])
> (term (boxy-eval (λ (x : Nat) (car (cons (+ 1 2) 2)))))

'(λ (x : Nat) (car (cons (+ 1 2) 2)))

> (term (normalize (λ (x : Nat) (car (cons (+ 1 2) 2)))))

'(λ (x : Nat) 3)

3.4 Testing Reduction Relations

Redex provides a handful of test functions for reduction relations. I use test--> to test single steps of reduction.

Examples:
> (test--> -> (term (+ 1 2)) (term 3))
> (test--> -> #:equiv alpha-equivalent?
           (term ((λ (x : Nat) (λ (y : Nat) y)) 1))
           (term (λ (z : Nat) z)))
> (test-results)

Both tests passed.

This takes the name of the relation, followed by an optional equivalence predicate, and two terms. It checks that the first term steps in one step of the relation to the second.

I use test-->> to test arbitrary number of steps of reduction, which has essentially the same interface.

Examples:
> (test-->> ->* #:equiv alpha-equivalent?
            (term (λ (x : Nat) (car (cons (+ 1 2) 2))))
            (term (λ (z : Nat) 3)))
> (test-results)

One test passed.

I use test-->>∃ (or test-->>E) to test that there exists a way to reduce a term to another term.

Examples:
> (test-->>∃ ->*
            (term (λ (x : Nat) (car (cons (+ 1 2) 2))))
            (term (λ (x : Nat) (car (cons 3 2)))))
> (test-->>∃ #:steps 1 ->*
           (term (λ (x : Nat) (car (cons (+ 1 2) 2))))
           (term (λ (x : Nat) (car (cons 3 2)))))
> (test-->>∃ #:steps 1 ->*
             (term (λ (x : Nat) (car (cons (+ 1 2) 2))))
             (term (λ (x : Nat) 3)))

FAILED :90.0

term (λ (x : Nat) 3) not reachable from (λ (x : Nat) (car (cons (+ 1 2) 2))) (within 1 steps)

> (test-->>∃ #:steps 2 ->*
             (term (λ (x : Nat) (car (cons (+ 1 2) 2))))
             (lambda (x)
               (alpha-equivalent? x (term (λ (z : Nat) 3)))))
> (test-results)

1 test failed (out of 4 total).

Unlike the other test functions, test-->>∃ does not take an #:equiv optional argument, and doesn’t obey default-equiv. Instead, the second term can be either a value or a predicate.

This may change soon because I’m about to file a pull request.

3.5 Caveat: Compatible Closure of Mutually Defined Relations

The compatible-closure functions doesn’t work when we have expressions whose syntax is mutually defined, since compatible-closure requires a single nonterminal. Consider the call-by-push-value language definition given below. In this language, values and expressions are mutually defined, and have explicit injection terms between each.

Examples:
> (require redex/reduction-semantics)
> (define-language cbpvL
    (e ::= (λ (x) e) (e v) (force v) (return v))
    (v ::= (thunk e) () x)
    (x ::= variable-not-otherwise-mentioned)
  
    #:binding-forms
    (λ (x) e #:refers-to x))
> (define ->
    (reduction-relation
     cbpvL
     (--> (force (thunk e)) e
          "force")
     (--> ((λ (x) e) v) (substitute e x v)
          "β")))
> (apply-reduction-relation* -> (term (force (thunk (return x)))))

'((return x))

Trying to use compatible-closure here will not give us full reduction. Worse, it won’t result in an error; instead, it will compute unexpected results. Some terms will compute properly, while others won’t.

Examples:
> (define wrong->* (compatible-closure -> cbpvL e))
> (define wrong^->* (compatible-closure -> cbpvL v))
>
> (apply-reduction-relation* wrong->*
    (term (λ (x) (return (thunk (λ (x) (force (thunk (return x)))))))))

'((λ (x) (return (thunk (λ (x) (return x))))))

> (apply-reduction-relation* wrong^->*
    (term (λ (x) (return (thunk (λ (x) (force (thunk (return x)))))))))

'((λ (x) (return (thunk (λ (x) (force (thunk (return x))))))))

>
> (apply-reduction-relation* wrong->*
    (term (thunk (λ (x) (return (thunk (λ (x) (force (thunk (return x))))))))))

'((thunk (λ (x) (return (thunk (λ (x) (force (thunk (return x)))))))))

> (apply-reduction-relation* wrong^->*
    (term (thunk (λ (x) (return (thunk (λ (x) (force (thunk (return x))))))))))

'((thunk (λ (x) (return (thunk (λ (x) (force (thunk (return x)))))))))

The problem is that compatible-closure is automatically computing a context. However, its default mode of computing the context does not work for mutually defined nonterminals.

To properly define the full reduction relation for this language, we need to use context-closure and manually give the mutually defined contexts All compatible-closure does is compute the obvious context of a given nonterminal and call context-closure.

We can define the contexts manually, but this is extremely tedious. Thankfully, Redex exposes some internals of compatible-closure, as compatible-closure-context, to let us compute the context we want.

Examples:
> (define-extended-language cbpvCtxtL cbpvL
    (C ::= (compatible-closure-context v #:wrt e)
       (compatible-closure-context e)
       (compatible-closure-context e #:wrt v)))
> (define ->* (context-closure -> cbpvCtxtL C))
> (apply-reduction-relation* ->*
    (term (thunk (λ (x) (return (thunk (λ (x) (force (thunk (return x))))))))))

'((thunk (λ (x) (return (thunk (λ (x) (return x)))))))

> (apply-reduction-relation* ->*
    (term (λ (x) (return (thunk (λ (x) (force (thunk (return x)))))))))

'((λ (x) (return (thunk (λ (x) (return x))))))

Syntax in RedexJudgments in Redex