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

From: Ryan Newton (rrnewton at gmail.com)
Date: Mon Jul 9 15:11:04 EDT 2012

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.


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>

Posted on the users mailing list.