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

On Jul 11, 2012, at 3:52 PM, Ryan Newton wrote:

> 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)?


short: Redex book chapter 1

long: eval is the semantics, |--> is the machine, --> is an "algebraic" system. Both specify eval, independently. The "naive" view is that |---> "fixes" an evaluation order, and that was debunked with Plotkin's 1972 paper. In general, people are happy with a |--> specification, because a calculus is too far away from machine thinking, which is what PL people prefer. |--> does not have to be a 'sequential' [Milner 1971] transition function. 

for the mathematical spec, you don't need markings. That's just for machine processing. I have never seen it used (or would bother to use it) in a pencil-and-paper model. 

Helps? -- Matthias

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20120711/c7837d6b/attachment.html>