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

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