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

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20120709/62c2fe94/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: grammar_excerpt.pdf
Type: application/pdf
Size: 266365 bytes
Desc: not available
URL: <http://lists.racket-lang.org/users/archive/attachments/20120709/62c2fe94/attachment-0002.pdf>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: semantics_excerpt.pdf
Type: application/pdf
Size: 309360 bytes
Desc: not available
URL: <http://lists.racket-lang.org/users/archive/attachments/20120709/62c2fe94/attachment-0003.pdf>