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

From: Ryan Newton (rrnewton at gmail.com)
Date: Wed Jul 11 15:52:40 EDT 2012

Thanks, we ended up removing most of our section on Redex until we can
explore these issues.  Lindsey wasn't comfortable having slightly different
semantics in the Redex define-judgment-form
no ERefl) than reported in the paper.

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

... 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.

Yes, most of our design effort was precisely in "getting the effects
right".  We did find several ways to design state observation mechanisms
with bugs ;-).

> but it doesn't mean you can't formulate it as a plain old reduction
> semantics.

So would this mean using a marking approach like David's example?  Or
simply pick an evaluation order, but provide a mechanism to proceed if the
desired redex is stuck (e.g. a blocked 'get' waiting for communication)?


P.S. FYI the paper draft is up:

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>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20120711/e4fdfae5/attachment.html>

Posted on the users mailing list.