Hi again everybody! My supervisor (Prof. Klaus Ostermann) noticed an issue with DrRacket's stepper in ISL+ (with Racket 6.2.1) and name capture. One could argue there's a straightforward name capture bug, but I think this is more confusing. For extra fun, as far as I can tell from quickly skimming, the beta rule described by HTDP/2e for ISL+ does not mention renaming (though renaming seems mentioned instead for `local`).
Concretely, consider this snippet and note the two bindings for `y`: (define y 5) (((lambda (g) (lambda (y) (g y))) (lambda (x) (+ x y))) 8) The stepper applies the beta rule to `lambda (g)` without renaming: (define y 5) ((lambda (y) ((lambda (x) (+ x y)) y)) 8) By just looking at this snippet, one would say that accidental capture occurred: the occurrence of `y` that was bound by the outer definition is now bound by the inner binding for `y`. However, the next evaluation step shows that the binding structure was not corrupted: (define y 5) ((lambda (x) (+ x y)) 8) I interpret this as "there are two distinct variables that both render to `y`", but this possibility does break lots of assumptions — and there's no way to guess the intended semantics of the second step, since no arrows are shown.* Is the intended semantics of variable names the standard one? If so, I guess the stepper should actually alpha-rename abstractions at some step, and HtDP should be adapted. Probably the alpha-renaming should be done right before the offending beta-reduction. *Which reminds me: why can't the stepper reuse the existing code for this functionality? You might need to use two separate editors, but that might be anyway an usability improvement (frankly, I didn't expect selection to work correctly in the stepper window). Cheers, Paolo -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. For more options, visit https://groups.google.com/d/optout.
