Symbolic evaluation with PLT Redex

PLT Redex is a great tool for testing and debugging a small-step operational semantics (particularly a reduction semantics using Felleisen-style evaluation contexts). I've just learned it's also useful for doing symbolic evaluation, where a program term may contain symbolic placeholders for some of its subterms. This is important when doing proofs, where you want to know how a fragment of a program is going to reduce for an entire class of terms.

For example, in a simulation proof I'm writing, I want to reason about how a program fragment would reduce in any initial continuation K0. So I extended the grammar of continuations to include the form

K ::= ... | (sym variable)

i.e., an s-expression containing the symbol 'sym followed by any variable. Then I could represent the abstract continuation K0 as '(sym K0). That's all it took, and Redex happily reduced my program.

Of course, once the reduction sequence gets to the point where it's returning a value to the continuation K0, it gets stuck, because there are no reduction rules that operate on these symbolic terms. But that's fine, because I'll never need to do such concrete reasoning about abstract terms.