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

From: Lindsey Kuper (lkuper at cs.indiana.edu)
Date: Mon Jul 9 16:13:27 EDT 2012

On Mon, Jul 9, 2012 at 12:11 PM, Ryan Newton <rrnewton at gmail.com> wrote:
> We felt it was necessary to include simultaneous steps (Matthias's [A]
> scenario) to model real parallel machines and force us to deal with
> potentially incompatible simultaneous updates to the store.
> Lindsey had a slightly awkward time shoehorning things into redex, and the
> resulting model runs pretty slowly.  BUT, these are just nits and possible
> areas for improvement.  Redex was still enormously helpful and fulfilled its
> purpose.  There wasn't any existential crisis here.

Yep.  Although, as Matthias pointed out, Redex is ill-suited for
modeling simultaneous steps, it has *still* been quite helpful in
clarifying our thinking and exposing bugs, even though we weren't able
to take advantage of most of what it has to offer.  Having said that,
there must be semantics engineering tools that are better suited for
modeling truly simultaneous reductions (the K system comes to mind as
a possibility, although I haven't tried it yet).  But the
lightweight-ness of Redex is pretty hard to beat.  (It's also
enormously fun.)


Posted on the users mailing list.