Порядочность бета-редукции

[deniok]

(1) Является ли отношение многошаговой бета-редукции на термах бестипового лямбда-исчисления отношением порядка? Докажите или приведите контрпример.

(2) Верен ли ваш ответ для просто типизированной лямбды?

Comments

Re: Вопрос по ЛИ

[deniok]

Ваш контрпример x(\у.уу)(\у.уу) не работает, потому что аппликация ассоциативна влево, и читается он так (x(\у.уу))(\у.уу).

Конструкция x M_1 ... M_k называется головной нормальной формой. Это не обычная нормальная форма (в Mi могут быть редексы), но тем не менее в некотором смысле содержательный результат вычислений. При дальнейших вычислениях структура терма в виде переменной x примененной к k аргументам уже не изменится. Более того, редукция в одном Mi совершенно никак не зависит от и не влияет на другой Mj.

Re: Вопрос по ЛИ

[andrey83]

спасибо большое!