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 <rrnew...@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 <ro...@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 <lku...@cs.indiana.edu> >> wrote: >> > On Sat, Jul 7, 2012 at 8:04 PM, Robby Findler >> > <ro...@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 > > ____________________ Racket Users list: http://lists.racket-lang.org/users
