Эта абстракция в исчислении лямбда

Eta Абстракция в исчислении лямбда означает следующее.Эта абстракция в исчислении лямбда

A function `f` can be written as `\x -> f x`

Является ли эта абстракция любого использования при уменьшении лямбда-выражений? Это лишь альтернативный способ написания определенных выражений?

источник

2016-11-15 user634615

В зависимости от вашей стратегии оценки, преобразование ета может быть полезным способом задержки оценки – naomik

Спасибо, вы можете указать мне на какую-то ссылку или пример, где есть некоторые случаи использования ЕТА абстракции. – user634615

Под строгой оценкой эта абстракция может быть использована для реализации знаменитого комбинатора Y. 'Y: = U (λh. Λf. F (λx. H h f x))' где 'U: = λf. f f' - без 'x' eta абстракции здесь, строгий оценщик перейдет в бесконечный цикл. – naomik

Уменьшение/увеличение ета является лишь следствием закона, который говорит, что с учетом

f = g

должно быть, что для любого х

f x = g x

и наоборот.

Следовательно Дано:

f x = (\y -> f y) x

мы получаем, бета уменьшая правую

f x = f x

, который должен быть истинным. Таким образом, мы можем заключить

f = \y -> f y

источник

2017-01-23 19:57:03 Ingo

Эта абстракция в исчислении лямбда

ответ

Смежные вопросы