Еще глупый вопрос про лямбда-термы

[Sonic86]

А почему $\lambda x \ (f \ x) \neq f$?
Ведь какая разница: $(\forall t) (f \ t) = (\lambda x \ (f \ x)) \ t$, значит $\lambda x \ (f \ x) = f$.
Единственная причина, которую я нашел, это то, что один терм $f$ от $n>1$ аргументов неявно порождает $n!>1$ функций вида $\lambda x_{\pi(1)} \ ... \ \lambda x_{\pi(n)} \ (f \ x_1 \ ... \ x_n)$, где $\pi$ - перестановка, без указания порядка переменных чисто по записи терма $f$ невозможно понять, какая функция имеется ввиду.

[arseniiv]

Термы равны, если в аксиомы входит $\eta$-конверсия.

-- Вс янв 15, 2017 23:31:09 --

(Которая как раз и есть аксиома вида $\lambda v.(tv) = t$.)