Ваш контрпример x(\у.уу)(\у.уу) не работает, потому что аппликация ассоциативна влево, и читается он так (x(\у.уу))(\у.уу).
Конструкция x M_1 ... M_k называется головной нормальной формой. Это не обычная нормальная форма (в Mi могут быть редексы), но тем не менее в некотором смысле содержательный результат вычислений. При дальнейших вычислениях структура терма в виде переменной x примененной к k аргументам уже не изменится. Более того, редукция в одном Mi совершенно никак не зависит от и не влияет на другой Mj.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Re: Вопрос по ЛИ
Date: 2018-02-24 06:24 am (UTC)Конструкция x M_1 ... M_k называется головной нормальной формой. Это не обычная нормальная форма (в Mi могут быть редексы), но тем не менее в некотором смысле содержательный результат вычислений. При дальнейших вычислениях структура терма в виде переменной x примененной к k аргументам уже не изменится. Более того, редукция в одном Mi совершенно никак не зависит от и не влияет на другой Mj.