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.
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.