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 < > matth...@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> > >
____________________ Racket Users list: http://lists.racket-lang.org/users
