Hi, 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 (http://lists.racket-lang.org/users/archive/2009-October/036237.html) 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 http://git.racket-lang.org/plt/blob/HEAD:/collects/redex/examples/define-judgment-form/sos.rkt). 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. Thanks, Lindsey ____________________ Racket Users list: http://lists.racket-lang.org/users
