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

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
implementation<https://github.com/lkuper/lambdapar-redex/blob/16e95cda63642e3af6296dcf6f9bbedfaaf2722e/lambdapar.rkt>(i.e.
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)?

 -Ryan

P.S. FYI the paper draft is up:
   http://www.cs.indiana.edu/~rrnewton/papers/2012-lambdapar-draft.pdf


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>