That actually cuts right to the heart of one of our issues.<div><br></div><div>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.</div> <div><br></div><div>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: </div><div> (e v) -> (e' v)</div> <div> (v e) -> (v e')</div><div><br>So that would cover your example. It's still parallelism, but it's an unrealistically constrained evaluation order.</div><div><br></div><div> -Ryan<br><br><div class="gmail_quote"> On Sun, Jul 8, 2012 at 7:49 AM, Robby Findler <span dir="ltr"><<a href="mailto:robby@eecs.northwestern.edu" target="_blank">robby@eecs.northwestern.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> I'm not sure of another way (but there might be one I just haven't<br> found), but do you want this program to reduce?<br> <br> ((+ 1 2) 3)<br> <br> That is, a program that has a value in parallel with a computation?<br> <span class="HOEnZb"><font color="#888888"><br> Robby<br> </font></span><div class="HOEnZb"><div class="h5"><br> On Sat, Jul 7, 2012 at 10:37 PM, Lindsey Kuper <<a href="mailto:lkuper@cs.indiana.edu">lkuper@cs.indiana.edu</a>> wrote:<br> > On Sat, Jul 7, 2012 at 8:04 PM, Robby Findler<br> > <<a href="mailto:robby@eecs.northwestern.edu">robby@eecs.northwestern.edu</a>> wrote:<br> >> No, there is no way to do that in Redex.<br> >><br> >> Are you trying to model parallelism?<br> ><br> > Yep. We could have just used single-hole contexts "E ::= (E e) | (e<br> > E) | ... " that allow for the two expressions in (e1 e2) to be<br> > evaluated in arbitrary order, but we wanted to make parallelism<br> > explicit in the model. Using define-judgment-form, we can do<br> > something along the lines of<br> ><br> > (define-judgment-form my-lang<br> ><br> > [(small-step (e_1 e_2) (e_11 e_22))<br> > (small-step e_1 e_11)<br> > (small-step e_2 e_22)]<br> ><br> > ...more rules here...<br> ><br> > )<br> ><br> > This works, but I was wondering if there was some other trick I hadn't<br> > thought of for modeling parallelism.<br> ><br> > Thanks,<br> > Lindsey<br> ____________________<br> Racket Users list:<br> <a href="http://lists.racket-lang.org/users" target="_blank">http://lists.racket-lang.org/users</a><br> </div></div></blockquote></div><br></div>