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
