Почему мы останавливаемся после достижения этого срока? Лямбда-исчисление

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

(\a.\b.(\x.a b x)(\y. b y x) a) (\f. f f)g

и нормальная форма этого

    g g (\y. g y x)(\f. f f)

У меня тоже такое получилось но потом продолжил и не понимаю почему это последний срок. я продолжил с

g g g (\f. f f) x

а потом

g g g x x

Но, видимо, я зашел слишком далеко, ты знаешь, почему ты должен остановиться раньше?

lambda reduction lambda-calculus

Peter111 02.04.2017 источник

arrow_upward
4
arrow_downward

Дело не в том, чтобы остановиться раньше. Вы неправильно интерпретируете синтаксис лямбда-исчисления.

По соглашению, когда мы пишем A B C, мы имеем в виду (A B) C, а не A (B C); то есть приложение функции остается ассоциативным.

Поэтому

g g (\y. g y x)(\f. f f)

разбирает как

((g g) (\y. (g y) x)) (\f. f f)

В частности, (g g) применяется к (\y. g y x), тогда как (\y. g y x) не применяется к (\f. f f).

melpomene 02.04.2017