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

Thanks for the example!


>    Masako Takahashi "Parallel Reductions in λ-Calculus", Information
>    and Computation 118(1), 1995.

(A lovely paper that is not so easy to find in PDF.)
>

Ah, good to see you cite that paper.  We've been using it as one of our
references, and did manage to find a PDF for it somewhere.  We indeed are
using a similar multistep relation.

This marking trick is a neat thing to add to the redex toolbelt, and it
looks like we could adapt it to CBV just by tweaking the mark function.
 However, it evaluates the maximum number of possible redexes in each step,
which is fine if you already know you've got Church-Rosser.  But there's a
bit of a circularity here and what we really want is a redex model that we
can use in two different modes for two different purposes:

   - Full mode - explore all (or many) thread interleavings, to help us
   convince ourselves that CR does hold for our language.  FYI our language is
   parallel CBV with no reduction under lambdas and it does have limited
   effects.
   - Quick mode - explore many fewer (or one) thread interleaving just to
   get to the answer quickly.

What Lindsey's done currently is to come up with a semantics using *
define-judgment-form* for which we can swap out a couple rules to switch
between these two modes -- well, at least between all-interleavings and our
specific lockstep-interleaving (it would be nice to explore random orders,
as suggested in Robby's message).

Cheers,
   -Ryan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20120708/6b60f771/attachment.html>