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 racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
