Почему рефлексивные графы для параметричности?

11

Глядя на модели параметрического полиморфизма, мне интересно, почему используются рефлексивные категории графов ?

В частности, почему они не включают реляционную композицию? При взгляде на модели все они, кажется, поддерживают естественное понятие реляционной композиции:

x(R;S)zy.xRyySz

В последних работах, в которых используются рефлексивные графы, кажется, что это само собой разумеющееся, и единственная старая статья, которую я смог найти, которая обсуждала это, была «Реляционная параметрическость и локальные переменные» О'Хирна и Теннента, которые говорят:

Одна из причин, по которой не требуется составляемость, состоит в том, что, как хорошо известно, композиция не сохраняется логическими отношениями на более высоких типах.

И я не совсем уверен, что это значит, поэтому мой первый вопрос заключается в том, что подразумевается под этим, и, надеюсь, лучше справиться с этим вопросом.

Я думаю, это означает, что, например, экспонента не обязательно сохраняет реляционную композицию на носу. В частности, мы не можем показать . Это означает, что экспонента не распространяется на функтор в категории отношений.(R;R)(S;S)((RS);(RS))

((RS);(RS))((R;R)(S;S))

f((RS);(RS))hgf(RS)g(RS)hxRyRzf(x)Sg(y)Sh(z)

Макс Новый
источник

Ответы:

1

Через несколько месяцев после того, как я задал этот вопрос, я думаю, что нашел разумный ответ.

R:DEωω|D|×|E|R:ω+1Nω+1NR(n,n)RR;RT:ω+1ω+1nR;RTnωR;RTω

Макс Новый
источник