2014 dxdy logo

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

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


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


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



Начать новую тему Ответить на тему
 
 Доказательство законов классов типов на бесконечных типах
Сообщение12.04.2017, 02:25 


05/09/12
2587
Здравствуйте. Давно я сюда ничего не писал, но вот недавно возникла ситуация, и я решил попросить помощи.
Фабула: есть классический функциональный тип Список:
Код:
data List a = Nil | Cons a (List a)

для него требуется доказать выполнение второго закона класса типов Функтор:
Код:
fmap f (fmap g l) = fmap (f . g) l

то есть композиция функторного преобразования равна функторному преобразованию по композиции составляющих. На одной площадке было написано простейшее индуктивное доказательство в духе Tapl и Бенджамина Пирса: доказываем для базы индукции Nil, доказываем индукционный переход. Но Пирса можно понять - у него все выкладки базируются на языке со строгой семантикой и все типы конечны, мы не встретим там бесконечных списков, значит наивная индукция работает. Но подобное доказательство было приведено относительно Хаскеля, где присутствуют бесконечные списки. Это вызвало мое подозрение, т.к. по такой же логике можно доказать утверждение "бесконечных списков не существует", что противоречит истине. Мне были даны ссылки на Википедию "Трансфинитная индукция", но детально затруднились показать, как мы вводим отношение порядка на множестве списков для удовлетворения условиям этой индукции.

Собственно, вопрос: как доказать? В процессе обсуждения были высказаны предположения, что даже само определение равенства термов, не имеющих нормальной формы, может вызвать затруднения. Но в этом вопросе у меня есть некий оптимизм - мы можем попытаться ввести понятие равенства термов не приводя их к нормальным формам, а пытаясь привести оба терма (через частичные применения альфа/бета/эта редукции) к таким термам, которые равны (не являясь нормальными формами) - этакое экстенсиальное равенство. А поскольку в реальности мы можем ограничиться только конечными термам и (возможно, не имеющими нормальной формы), то на исходном множестве конечных термов можно считать отношение равенства определенным. Вопрос про применение индукции на таких бесконечных коиндуктивных типах, ну и, возможно, определение равенства на них.

 Профиль  
                  
 
 Re: Доказательство законов классов типов на бесконечных типах
Сообщение12.04.2017, 10:52 
Заслуженный участник
Аватара пользователя


28/07/09
1178
Может просто сравнить оба (бесконечных) списка поэлементно?

 Профиль  
                  
 
 Re: Доказательство законов классов типов на бесконечных типах
Сообщение12.04.2017, 11:22 
Заслуженный участник


16/02/13
4105
Владивосток
Если вы используете в запуске программы 1000 первых элементов списка, то вам, в общем-то, всё равно, сколько в нём — 1001 элемент, 10000, или бесконечность. Может, отсюда плясать?

 Профиль  
                  
 
 Re: Доказательство законов классов типов на бесконечных типах
Сообщение12.04.2017, 12:06 
Заслуженный участник
Аватара пользователя


06/10/08
6422
M. P. Fiore "A Coinduction Principle for Recursive Data Types Based on Bisimulation"
Вкратце: Бисимуляция для коиндукцивных списков - это такое отношение $R$, что $R([], [])$ и $R(x, y) \Rightarrow \operatorname{head}(x) = \operatorname{head}(y) \& R(\operatorname{tail}(x), \operatorname{tail}(y))$. Из бисимуляции следует равенство, потому что коиндуктивный тип - это терминальная коалгебра.

 Профиль  
                  
 
 Re: Доказательство законов классов типов на бесконечных типах
Сообщение12.04.2017, 14:05 


05/09/12
2587
Xaositect, спасибо, похоже это именно то, что надо. На досуге попробую детальнее разобраться.

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

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



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

Сейчас этот форум просматривают: YandexBot [bot]


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

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