Compare model to implementation in Redex

Question

I'm working on building a model in Redex of a type system that also has a canonical implementation. I would like to use redex-check to fuzz test my model against the actual implementation.

The implementation (with an adapter) can take my abstract syntax, so what I need is a way of passing the term generated by the fuzzer to the implementation. Is there a way to do this?

Answer 1

As it turns out redex-check, when combined with apply-reduction-relation* handles this directly if you can either give redex terms to your actual implementation, or convert them to fit with your implementation. Your code will look something like this:

(redex-check λv e
             (equal? (implementation (convert (term e)))
                     (first (apply-reduction-relation* red (term e)))))

Where implementation is your implementation, red is the reduction relation your model uses, and convert converts the term into something your implementation can handle. Also λv is your language and e is the term in your language you want it to test.

The first is simply because apply-reduction-relation* returns a list of all possible reductions. If your model is deterministic, this should be a list of length one. (Which you can check by using the following reduction relation instead:

(redex-check λv e
             (let ([result (apply-reduction-relation* red (term e))])
               (and (= (length result) 1)
                    (equal? (implementation (convert (term e)))
                            (first result)))))

You can see another example of how to use redex-check on the tutorial on the redex home page.