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

Are there places where one side might do some effect that should be
visible by the other one? If so, then I guess that you must have some
way to identify those points so you make sure you cover all of the
possible interleavings?

I ask because it occurs to me that you could have an explicit token
that says whose turn it is an then use that to remove states from the
model. Whatever technique you're using to handle the above should also
be able to be adapted to this kind of explicit token thing. (Also, the
"token" could be something like "first one in a sequence" reduces and
then you could have a non-deterministic step that would pick the guy
that gets to go next. This would reduce the irrelevant interleaving,
possibly.)

Also, I'm kind of sad but not surprised to hear that Redex's
performance is what motivates all this. If you'd like, please pass
along some program (and instructions for running it that makes it do
something slow) and I'll have a look to see if there is something
stupid going on and there is some straightforward improvement to Redex
that'd help out.

Robby

On Sun, Jul 8, 2012 at 10:38 AM, Ryan Newton <rrnewton at gmail.com> wrote:
> 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
>
>