Бесплатные теоремы Рейнольдса

[Mysterious Light]

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

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.$$

[Xaositect]

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$.

[Mysterious Light]

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$.

[Xaositect]

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