Understanding lambda substitution in Redex

Question

Let us say I have the following defined in Redex:

(define-language L
    [e ::= (λ x e) (e e) x]
    [x ::= variable-not-otherwise-mentioned]
    #:binding-forms
    (λ x e #:refers-to x))

Now, I would think that the expression (λ y x) x means:

replace occurrence of y in x (inside braces in the above expression) with x (outside braces). And since there is no y in x, the answer should be just x. Then (λ y x) x y should return x y. But:

(default-language L)
(term (substitute (λ y x) x y))
'(λ y«0» y)

why does it return a function? And what does y<<0>> mean? Am I misunderstanding term (substitute ..)?

I didn't understand this result either:

(term (substitute (λ y x) x true))
'(λ y«1» true)

Could someone help me decipher this? I'm new to Racket/Redex.

Answer 1

y«0» and y«1» simply mean that while the variable is named y, its a different y than the one passed in. The #:refers-to flag is used to make forms respect capture-avoiding substitution.

In general, the idea is this, what should the result of this program be:

((lambda (x) (lambda (y) x))
 y)

Should this program evaluate to 4 or 3? If we use simple substitution, then we can say that the program reduces to:

(lambda (y) y)

Which is the identity function. This is noticeable if we, say, bound y to 5 and called the result:

(let* ([y 5]
       [f ((lambda (x) (lambda (y) x))
            y)])
  (f 6))

Here, we would expect the result to be 5, even though we are passing 6 into f. This is because the y in the result is pointing to the first y in the let*. You can see this if you mouse of y in DrRacket.

To avoid this, rather than doing a simple substitution of all xs in the expression to ys, it renames all binders going down to new names, so instead you get:

(lambda (y«0») y)

And now its clear that the two ys in this expression are different.