Понимание лямбда-замены в Redex

Question

Допустим, в Redex определено следующее:

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

Теперь я думаю, что выражение (λ y x) x означает:

заменить вхождение y в x (внутри скобок в вышеприведенном выражении) с x (вне скобок). И поскольку в x нет y, ответ должен быть просто x. Тогда (λ y x) x y должен вернуть x y. Но:

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

почему он возвращает функцию? А что значит y<<0>>? Я неправильно понимаю term (substitute ..)?

Я тоже не понял этого результата:

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

Может ли кто-нибудь помочь мне расшифровать это? Я новичок в Racket / Redex.

Answer 1

y«0» и y«1» просто означают, что хотя переменная имеет имя y, она отличается от y, чем передаваемая. Флаг #:refers-to используется для того, чтобы формы учитывали подстановку, избегающую захвата.

В общем, идея такова, каким должен быть результат этой программы:

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

Должна ли эта программа оценивать 4 или 3? Если мы используем простую подстановку, то можем сказать, что программа сокращается до:

(lambda (y) y)

Что является функцией тождества. Это заметно, если мы, скажем, привязали y к 5 и назвали результат:

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

Здесь мы ожидаем, что результат будет 5, даже если мы передаем 6 в f. Это потому, что y в результате указывает на первое y в let*. Вы можете увидеть это, если вы щелкнете мышью по y в DrRacket.

Чтобы избежать этого, вместо простой замены всех x с в выражении на y с, он переименовывает все связующие вплоть до новых имен, поэтому вместо этого вы получите:

(lambda (y«0») y)

И теперь ясно, что два y в этом выражении различны.