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.

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.

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.

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

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.

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.

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.

3.4 Testing Reduction Relations

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.

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.

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.

← Syntax in RedexJudgments in Redex →