2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




 
 Еще глупый вопрос про лямбда-термы
Сообщение15.01.2017, 21:10 
А почему $\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$ невозможно понять, какая функция имеется ввиду.

 
 
 
 Re: Еще глупый вопрос про лямбда-термы
Сообщение15.01.2017, 21:21 
Термы равны, если в аксиомы входит $\eta$-конверсия.

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

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

 
 
 [ Сообщений: 2 ] 


Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group