2014 dxdy logo

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

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


Правила форума


Посмотреть правила форума



Начать новую тему Ответить на тему
 
 Еще глупый вопрос про лямбда-термы
Сообщение15.01.2017, 21:10 
Заслуженный участник


08/04/08
8505
А почему $\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 
Заслуженный участник
Аватара пользователя


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

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

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

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 2 ] 

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group