[racket] Does Redex have support for multi-hole evaluation contexts?

From: Lindsey Kuper (lkuper at cs.indiana.edu)
Date: Sat Jul 7 22:29:49 EDT 2012


I have a Redex model for a language witih an explicitly parallel
reduction semantics, where an application (e1 e2) can step to (e1'
e2') -- that is, where both the operator and the operand can step at
once.  Because we wanted to explicitly model this parallel reduction,
we first thought of using multi-hole evaluation contexts, but a
mailing list thread that I found from 2009
indicated that Redex didn't support those (in fact, that person was
trying to solve a similar problem).

So, instead, we use an inference-rule-based semantics (defined using
`define-judgment-form`, with the reduction relation defined as a thin
wrapper around `judgment-holds`, something like in
 This has been working fine, but I'm curious if it's still necessary
to do it that way, or if Redex now supports multi-hole contexts -- or
if there is yet another way to do explicit parallel reductions that
I've not yet considered.


Posted on the users mailing list.