2014 dxdy logo

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

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


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


В этом разделе нельзя создавать новые темы.

Если Вы хотите задать новый вопрос, то не дописывайте его в существующую тему, а создайте новую в корневом разделе "Помогите решить/разобраться (М)".

Если Вы зададите новый вопрос в существующей теме, то в случае нарушения оформления или других правил форума Ваше сообщение и все ответы на него могут быть удалены без предупреждения.

Не ищите на этом форуме халяву, правила запрещают участникам публиковать готовые решения стандартных учебных задач. Автор вопроса обязан привести свои попытки решения и указать конкретные затруднения.

Обязательно просмотрите тему Правила данного раздела, иначе Ваша тема может быть удалена или перемещена в Карантин, а Вы так и не узнаете, почему.



Начать новую тему Ответить на тему
 
 Бесплатные теоремы Рейнольдса
Сообщение11.09.2013, 02:22 
Аватара пользователя


29/05/11
227
Красноармейск, Донецкая обл.

(Литература)

Wadler, Philip. "Theorems for free!." Proceedings of the fourth international conference on Functional programming languages and computer architecture. ACM, 1989

Прочитал статью и возникли вопросы.

Прежде всего, параметрическая $\lambda$ в смысле Рейнольдса (или Жирара-Рейнольдса?) — это тоже самое, что $\lambda2$ в $\lambda$-кубе Барендрегта? То есть это такая же по-максимуму явная система типов, допускающая всяческую абстракцию терма по типу, и слабую (я не ошибся в названии? имел в виду наличие квантора только снаружи) вроде $\forall X.X\to X$, и сильную вроде $\forall Y. (\forall X.X)\to Y$ (квантор появился внутри)?

Рассмотрим несколько простых типов.
$i: \forall X. X\to X$ — это тип Истины. Типичный пример тому — идентичность $\Lambda X.\lambda x:X. x$.
Утверждаем, что $(i,i)\in \forall\mathscr{X. X\to X}$, где вместо типа — неформальное отношение между типами. Для любого отношения $\mathscr{A}: A_1\Leftrightarrow A_2$ тогда $(i_{A_1},i_{A_2})\in \mathscr{A\to A}$.$$(\forall \mathscr{A}: A_1\Leftrightarrow A_2) \; (\forall x_1: A_1) (\forall x_2: A_2) \;\; (x_1,x_2)\in\mathscr{A} \Rightarrow (i_{A_1}(x_1),i_{A_2}(x_2))\in \mathscr{A}.$$
В частном случае, когда отношение является функцией, получается$$(\forall a: A_1\to A_2) \;(\forall x: A_1)\;\; i_{A_2}(x_2) = a(i_{A_1}(x_1)).$$
Итак, получили бесплатную теорему $$i_A \circ a = a\circ i_B, \;\forall a: A\to B$$
Можно ли из этой теоремы заключить, что в адекватной $\lambda$-системе ничего, кроме идентичности, удовлетворять этой теореме не может?

Ещё: проекция $X\times Y\to Y$ или K-комбинатор $X\to Y\to X$, абстрагированные по $X,Y$.
Применяя ту же схему, получим (в инфиксной форме записаны отношения, индексы типов опущены)
\begin{multiline*}
(\forall\mathscr{A}:A_1\Leftrightarrow A_2) (\forall\mathscr{B}:B_1\Leftrightarrow B_2) \;
(\forall x_1: A_1) (\forall x_2: A_2) \; x_1\mathscr{A}x_2 \;\Rightarrow \\
\Rightarrow \Bigl( (\forall y_1: B_1) (\forall y_2: B_2) \; y_1\mathscr{B}y_2 \;\Rightarrow \;
Kx_1y_1 \mathscr{A} Kx_2y_2 \Bigr).
\end{multiline*}

Для функций: $$ (\forall a) (\forall b) (\forall x) (\forall y) \; K (ax) (by) = a (Kxy).$$Это бесплатная теорема для K-комбинатора и по совместительству для двух проекций.
Достаточно ли этого, чтобы считать $K$ независимым от $y$? Интуитивно мне кажется, что стоит опираться на частный случай $a=I$, в котором теорема принимает вид $Kxy = Kx(by), \;\forall x,y,b$, но я не знаю, как это лучше обыграть, чтоб было по-формальнее.

Эти вопросы были навеяны красивыми манипуляциями в статье над функциями reverse, map и fold. В частности, там показано, что $m: \forall X.\forall Y. (X\to Y)\to X^\ast \to Y^\ast$ обязательно представима в виде композиции map и переупорядочивания: $$m(f) = f^\ast \circ m(I) = m(I) \circ f^\ast.$$

 Профиль  
                  
 
 Re: Бесплатные теоремы Рейнольдса
Сообщение11.09.2013, 06:44 
Заслуженный участник
Аватара пользователя


06/10/08
6422
Mysterious Light в сообщении #762695 писал(а):
Прежде всего, параметрическая $\lambda$ в смысле Рейнольдса (или Жирара-Рейнольдса?) — это тоже самое, что $\lambda2$ в $\lambda$-кубе Барендрегта?
Да. В "Theorems for free" она описывается в 4 разделе.

Mysterious Light в сообщении #762695 писал(а):
Итак, получили бесплатную теорему $$i_A \circ a = a\circ i_B, \;\forall a: A\to B$$
Можно ли из этой теоремы заключить, что в адекватной $\lambda$-системе ничего, кроме идентичности, удовлетворять этой теореме не может?
У Вас индексы $A$ и $B$ перепутаны.
С помощью этого соотношения можно просто доказать, что $i_A x = x$, взяв в качестве $a$ функцию $K_{A,A}x\colon A\to A$. Тогда $i_A x = i_A (K_{A,A} x z) = K_{A,A} x (i_A z) = x$.

Но тут проблема в том, что, формально говоря, элементами типов являются не функции, а термы, и чисто теоретически может быть ситуация (в $\lambda2$ такого, если я правильно помню, не бывает), когда два терма всегда отображают одни и те же элементы в одни и те же, но при этом не равны с точки зрения $\beta$-эквивалентности. Я не уверен, что "бесплатные теоремы" что-то говорят о синтаксической эквивалентности.

Mysterious Light в сообщении #762695 писал(а):
Для функций: $$ (\forall a) (\forall b) (\forall x) (\forall y) \; K (ax) (by) = a (Kxy).$$Это бесплатная теорема для K-комбинатора и по совместительству для двух проекций.
Достаточно ли этого, чтобы считать $K$ независимым от $y$? Интуитивно мне кажется, что стоит опираться на частный случай $a=I$, в котором теорема принимает вид $Kxy = Kx(by), \;\forall x,y,b$, но я не знаю, как это лучше обыграть, чтоб было по-формальнее.
Тут надо сначала формально написать, что именно значит независимость, а потом опять же подобрать нужную функцию $b$.

 Профиль  
                  
 
 Re: Бесплатные теоремы Рейнольдса
Сообщение11.09.2013, 11:36 
Аватара пользователя


29/05/11
227
Красноармейск, Донецкая обл.
Xaositect в сообщении #762713 писал(а):
Mysterious Light в сообщении #762695 писал(а):
Итак, получили бесплатную теорему $$i_A \circ a = a\circ i_B, \;\forall a: A\to B$$
Можно ли из этой теоремы заключить, что в адекватной $\lambda$-системе ничего, кроме идентичности, удовлетворять этой теореме не может?
У Вас индексы $A$ и $B$ перепутаны.
С помощью этого соотношения можно просто доказать, что $i_A x = x$, взяв в качестве $a$ функцию $K_{A,A}x\colon A\to A$. Тогда $i_A x = i_A (K_{A,A} x z) = K_{A,A} x (i_A z) = x$.

Это очень красивый ход. Спасибо.

Xaositect в сообщении #762713 писал(а):
Но тут проблема в том, что, формально говоря, элементами типов являются не функции, а термы, и чисто теоретически может быть ситуация (в $\lambda2$ такого, если я правильно помню, не бывает), когда два терма всегда отображают одни и те же элементы в одни и те же, но при этом не равны с точки зрения $\beta$-эквивалентности. Я не уверен, что "бесплатные теоремы" что-то говорят о синтаксической эквивалентности.

Я вовсе не разбираюсь в таких тонкостях, но могу предположить, что за счёт введения сразу $\eta$-редукции и доказательства теоремы путём перенесения $\lambda$-суждений $\bar{X},\bar{x}\vdash t:T$ на множественные суждения $\bar{X},\bar{x} \vDash t:T$ в значении $(\forall \bar{A},\bar{a}) \;[t]\bar A\bar a\in \mathbb{D}_}{[T]\bar A}$, то два эквивалентных терма совпадают в лямбде, потому что есть $\eta$, и в множествах, потому что там эквивалентные множества (и отношения, и функции) всегда равны.

Ещё объясните, пожалуйста, феноменологически один момент, который мне встечался много где, когда модели к лямбде начинают строиться.
В этой статье $\lambda$-терму сопоставляется $[t] = \phi(\ldots)$ для абстракций и $[t]=\psi(\ldots)$ для применения, причём $\phi\circ\psi=id$. Это условие говорит о том, что $[D_A\to D_B]\equiv \mathfrak{Hom} D_A D_B$ является ретракцией $D_{A\to B}$. Почему именно ректракцией, а не биекцией? Я так понимаю, что это условие позволяет сохранить $\beta$-редукцию: $$[(\lambda x. t)u] = \phi(\psi(\lambda a. [t]_{x:=a}))[u] = [t]_{x:=u}.$$Здесь одна из $\lambda$ — теоретико-множественная абстракция, поэтому второе равенство доказуемо в ТМ.
Но ведь эти функции вполне допускают ситуацию, что найдётся представление терма $[t]\in\mathbb{D}_{A\to B}$ такое, что $\psi(\phi([t]))\neq [t]$. И этого я не понимаю.

Xaositect в сообщении #762713 писал(а):
Mysterious Light в сообщении #762695 писал(а):
Для функций: $$ (\forall a) (\forall b) (\forall x) (\forall y) \; K (ax) (by) = a (Kxy).$$Это бесплатная теорема для K-комбинатора и по совместительству для двух проекций.
Достаточно ли этого, чтобы считать $K$ независимым от $y$? Интуитивно мне кажется, что стоит опираться на частный случай $a=I$, в котором теорема принимает вид $Kxy = Kx(by), \;\forall x,y,b$, но я не знаю, как это лучше обыграть, чтоб было по-формальнее.
Тут надо сначала формально написать, что именно значит независимость, а потом опять же подобрать нужную функцию $b$.
Независимость означает, что не может быть никакого $\lambda$-терма с таким типом, кроме $\lambda xy.x$.
Я это попытаюсь доказать в качестве домашнего упражнения примерно тем же способом, как Вы рассуждали для $i$.

 Профиль  
                  
 
 Re: Бесплатные теоремы Рейнольдса
Сообщение12.09.2013, 09:53 
Заслуженный участник
Аватара пользователя


06/10/08
6422
Я, честно говоря, практически ничего не знаю о теории моделей $\lambda$-исчисления, мне всегда хватало синтаксического рассмотрения.
Если будет время на следующей неделе, попробую посмотреть что-нибудь по этому вопросу.

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

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



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

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


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

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