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
