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

This looks like a fairly conventional form of parallel evaluation with some form of attempt at 'free deterministic update'. 

If I were to model this kind of thing, I am sure I'd use a multi-hole reduction semantics to represent non-coordinated parallelism. Too bad Redex can't model this, but it doesn't mean you can't formulate it as a plain old reduction semantics. 

Whether you "believe" it to be deterministic is pretty irrelevant. If you want it to be deterministic, you construct it that way, and with multi-hole "standard" reductions it is quite easy (near trivial) to show this -- assuming you get your effects right.

Enough said, good luck -- Matthias





On Jul 9, 2012, at 3:11 PM, Ryan Newton wrote:

> Hi all,
> 
> Thanks for all the advice.
> 
> Just to be clear about the context.  This is a parallel language that we developed on paper which we strongly believed was deterministic.  We wrote the paper proof and also, on the side, wanted to make a redex model to check ourselves.
> 
> We felt it was necessary to include simultaneous steps (Matthias's [A] scenario) to model real parallel machines and force us to deal with potentially incompatible simultaneous updates to the store.  
> 
> Lindsey had a slightly awkward time shoehorning things into redex, and the resulting model runs pretty slowly.  BUT, these are just nits and possible areas for improvement.  Redex was still enormously helpful and fulfilled its purpose.  There wasn't any existential crisis here.
> 
>   -Ryan
> 
> P.S.  It would be simpler to just share the paper rather than describing the problems out of context.  However, I don't want to send the draft out quite yet, because it needs a few more tweaks to have all the refactorings pushed through and achieve internal consistency.  But I'm attached the reduction rules and grammar, FYI.
> 
> On Mon, Jul 9, 2012 at 12:34 PM, Matthias Felleisen <matthias at ccs.neu.edu> wrote:
> 
> On Jul 9, 2012, at 6:29 AM, Lindsey Kuper wrote:
> 
> > I had been assuming that "one-step" meant "small-step", but
> > now I think that by "one-step" David means a relation that doesn't
> > reduce redexes in parallel.  So, in fact, ours *is* multi-step because
> > it *does* reduce in parallel.
> 
> 
> Lindsey and Ryan, I have had no time until now to catch up with this thread (argh). And I have my own POPL deadline, so here are some general remarks:
> 
> 1. The parallel reduction trick that David pointed out goes back to the early 1970s. Tait appears to be the source. See Barendregt.
> 
> 2. 'small step' is NOT 'one-step' and 'one-step' is not 'notion of reduction'. See Redex, chapter 1 for definitions. They are the same ones as Barendregt uses and the informed PL community has used when publishing semantics papers in this style. I dislike 'small step'  A LOT but if you want a relationship |---> (standard reduction) is what most publishing PLists would call a 'small step' semantics.
> 
> 3. Also Redex, chapter 1 suggests that 'eval' is the actual semantics and |---> or -->> are two distinct ways of specifying it. Since eval is the key, this also eliminates any worries about reflexive rules -- as long as you think of eval as the mathematical semantics and the arrow relations as just one possible mechanism to define it.
> 
> 4. The reduction relations (-->> or standard) become important only if you wish to make some claim about the intension of the semantics, i.e., how it relates to actual machine steps. You don't have to. Plotkin 74, for example, shows that it is perfectly okay to show two different unrelated ways of defining eval (secd and a recursive interpreter) and to prove them equivalent -- brute force in his case.  You do that because you might be able to use one definitional mechanism to show one thing (type soundness) and with another one you can show something else (cost of execution). I have done it many times.
> 
> 5. The confusion between reduction relations and parallel execution is about 40 years old (perhaps a bit less). Indeed, the confusion between reduction relations in LC and plain execution is that old -- see so-called "optimal reduction sequences", which a well-trained  computer scientist (===/== mathematician masquerading as a PL person) will quickly recognize that it is nonsense. Fortunately we have had a proof for 10 years that this horse is dead.
> 
> ;; ---
> 
> May I propose a re-thinking of your approach that may benefit us Redex designers?
> 
> -- figure out what your real goal is; it cannot be to develop a semantics of some hypothetical PL (see above, especially 4)
> -- develop a paper and pencil model of a semantics that helps you prove this goal/theorem
> -- if it happens to be a reduction semantics (I am of course convinced that 90% of all goals can be reached via reduction semantics),
>         allow one of two things to happen:
>   [A] you need to model 'simultaneous' steps meaning you need multi-hole
>   [B] you don't need truly simultaneous steps but you allow some non-determinism in |--->
> 
> For [A], Redex is ill-suited. The define-judgment form isn't remotely as helpful for semantics as is the core redex language.
> 
> For [B], Redex is your friend.
> 
> See my paper with Cormac in the mid 90s on modeling futures with reduction systems, for one approach to parallelism. We did intend to tackle an FP language with set! at the time, but the analysis didn't work out so we abandoned this direction.
> 
> In short, decouple what you want to accomplish from the tool that might look like it could help.
> 
> 
> -- Matthias
> 
> 
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users
> 
> <grammar_excerpt.pdf><semantics_excerpt.pdf>