Бета-редукция некоторой лямбды

У меня есть следующее лямбда-исчисление, и я хочу знать, как его бета-сокращение.

Лямбда это:

λxy.xy

Я предполагаю, что бета-редукция невозможна, потому что замены нет, а x привязан к телу.

Верно ли мое предположение?


lambda lambda-calculus
person softshipper    schedule 26.01.2017    source источник
comment
да. Здесь можно только уменьшить эту.   -  person Alec    schedule 26.01.2017
comment
что такое эта редукция?   -  person softshipper    schedule 26.01.2017
comment
Похоже, он более известен как eta conversion.   -  person Alec    schedule 26.01.2017
comment
Является ли x выражением? Как я могу описать x ?   -  person softshipper    schedule 26.01.2017
comment
Иногда в лямбда-исчислении вы работаете только с бета-правилом, иногда вы добавляете еще и правило редукции эта. Если вас интересует только бета, ваш срок уже максимально сокращен — он находится в бета-нормальной форме.   -  person chi    schedule 26.01.2017

Ответы (1)


arrow_upward
4
arrow_downward

Вы не можете применить бета-редукции (что, вероятно, то, что вы ищете). Бета-редукция может применяться только к функциональным приложениям (да и то не во всех случаях).

Вы можете применить эта-преобразование, которое преобразует x.fx в f, если x не встречается свободно в f. Затем вы можете преобразовать свое выражение:

xy.xy = x.y.xy x.x (= I).

person Community    schedule 26.01.2017
comment
извините, я не могу следить за вами. Что означает эта конверсия? Не могли бы вы показать мне очень простой пример? Что означает (= я)? - person softshipper; 27.01.2017
comment
Преобразование @zero_coding Eta просто означает, что если какая-то абстракция применяет константное выражение f только к своему аргументу x (т. е. \x.fx, если f не содержит x), то эта абстракция эквивалентна самой f. Абстракция только блокирует f/forward x, поэтому ее можно удалить. - person ; 27.01.2017