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

That actually cuts right to the heart of one of our issues.

In our ideal semantics (e1 e2) can step to (e1' e2), (e1 e2'), or (e1'
e2'), but of course this creates many possible evaluation orders and makes
redex take a long long time.

Our quick-and-dirty version is to require synchronous steps (e1' e2'), and
then separately allow one branch to catch up if the other branch is a
value:
   (e v) -> (e' v)
   (v e) -> (v e')

So that would cover your example.  It's still parallelism, but it's an
unrealistically constrained evaluation order.

  -Ryan

On Sun, Jul 8, 2012 at 7:49 AM, Robby Findler
<robby at eecs.northwestern.edu>wrote:

> I'm not sure of another way (but there might be one I just haven't
> found), but do you want this program to reduce?
>
>   ((+ 1 2) 3)
>
> That is, a program that has a value in parallel with a computation?
>
> Robby
>
> On Sat, Jul 7, 2012 at 10:37 PM, Lindsey Kuper <lkuper at cs.indiana.edu>
> wrote:
> > On Sat, Jul 7, 2012 at 8:04 PM, Robby Findler
> > <robby at eecs.northwestern.edu> wrote:
> >> No, there is no way to do that in Redex.
> >>
> >> Are you trying to model parallelism?
> >
> > Yep.  We could have just used single-hole contexts "E ::= (E e) | (e
> > E) | ... " that allow for the two expressions in (e1 e2) to be
> > evaluated in arbitrary order, but we wanted to make parallelism
> > explicit in the model.  Using define-judgment-form, we can do
> > something along the lines of
> >
> > (define-judgment-form my-lang
> >
> >   [(small-step (e_1 e_2) (e_11 e_22))
> >    (small-step e_1 e_11)
> >    (small-step e_2 e_22)]
> >
> >   ...more rules here...
> >
> >   )
> >
> > This works, but I was wondering if there was some other trick I hadn't
> > thought of for modeling parallelism.
> >
> > Thanks,
> > Lindsey
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20120708/0c7b1a5e/attachment-0001.html>