Лямбда: конверсия эта, расширение, уточнение сокращения - PullRequest
Новая
       12

Лямбда: конверсия эта, расширение, уточнение сокращения

1 голос
/ 06 мая 2019

В моем понимании Eta-преобразование выглядит следующим образом:

Как Eta-сокращение 

(lambda (x) (M x)) -> M
  • , когда M не содержит x free;

Итак, 

(lambda (x) ((lambda (y) (y y)) x)) -> 
                       (lambda (y) (y y))

Решение вопроса:

Как Эта-расширение 

M -> (lambda (x) (M x))

(lambda (y) (y y)) -> 
         (lambda (x) ((lambda (y) (y y)) x))

1 Ответ

1 голос
/ 10 мая 2019

Eta-расширение для функций, которые принимают 1 аргумент, преобразует любое выражение, которое производит такую ​​функцию, и создает выражение, которое оборачивает ее в лямбду, которая оценивает это выражение только при вызове функции.

Допустим, выражение E создает функцию с 1 аргументом: 

E

Это eta-расширение - лямбда, которая принимает аргумент и делегирует E

(lambda (x) (E x))

Где вы используете новую переменную x, которая не является свободной в E. Это похоже на определение (f x) как (g x), поэтому эта новая функция должна вести себя эквивалентно E.

Например, если E является переменной, такой как y, расширение eta может превратить y в (lambda (x) (y x)). Однако, если E включает переменную x, вам придется сгенерировать другую переменную вместо x, поэтому расширение eta x может привести к (lambda (x2) (x x2)).

Основное различие между E и расширенной версией (lambda (x) (E x)) заключается в том, когда E оценивается. Только с E выражение E вычисляется один раз, прямо тогда. Однако с помощью eta-extension (lambda (x) (E x)) оценка E откладывается до времени, когда функция вызывается впервые, а E переоценивается каждый раз, когда вызывается функция. На языке с побочными эффектами вы можете продемонстрировать это с помощью оператора print как части E.

Пусть E будет: 

(begin (displayln "E") f)

Тогда расширение eta E равно: 

(lambda (x) ((begin (displayln "E") f) x))

Если вы определили g как E, тогда вы получите отображение при оценке этого определения. 

> (define g (begin (displayln "E") f))
E

И когда вы звоните g, ему не нужно снова его оценивать, поэтому он не печатает больше E s 

> (g 1)
> (g 2)

Однако, если вы определите g как eta-расширение, вы не получите этого дисплея. 

> (define g (lambda (x) ((begin (displayln "E") f) x)))

Вместо этого, когда вы вызываете g с аргументами (g 1) (g 2) (g 3), он выводит E для каждого из них 

> (g 1)
E
> (g 2)
E
> (g 3)
E

Как это относится к вашим примерам:

Ваш первый пример преобразования eta-Reduction (lambda (x) (M x)) в M, где x не является свободным в M. Eta-расширение противоположно, поэтому оно преобразует M в (lambda (x) (M x)), где вы должны выбрать x, который не является бесплатным в M.

Ваш второй пример преобразования eta-сокращения (lambda (x) ((lambda (y) (y y)) x)) в (lambda (y) (y y)). Опять же, eta-расширение противоположно, поэтому, если ему дано (lambda (y) (y y)), оно даст (lambda (x) ((lambda (y) (y y)) x)).

Ваш третий пример отличается. Вы пытаетесь eta-expand (lambda (y) (y y)), который согласно второму примеру должен выдать (lambda (x) ((lambda (y) (y y)) x)). Однако ваш пример говорит о другом: 

(lambda (y) (y y))
-> (lambda (x y) (y y x))

Где это должно быть 

(lambda (y) (y y))
-> (lambda (x) ((lambda (y) (y y)) x))
...