Mengapa Grafik Refleksif untuk Parametrisitas?

Melihat model polimorfisme parametrik, saya ingin tahu mengapa kategori grafik refleksif digunakan?

Secara khusus, mengapa mereka tidak memasukkan komposisi relasional? Dalam melihat model, mereka semua tampaknya mendukung gagasan alami komposisi relasional:

$$x(R;S)z \iff \exists y. xRy \wedge y S z$$

Sebagian besar makalah baru-baru ini yang menggunakan grafik refleksif tampaknya menerima begitu saja, dan satu-satunya makalah yang lebih tua yang dapat saya temukan yang membahasnya adalah "Relational Parametricity dan Variabel Lokal" oleh O'Hearn dan Tennent yang mengatakan:

Salah satu alasan untuk tidak memerlukan kompabilitas adalah bahwa, seperti diketahui, komposisi tidak dipertahankan oleh hubungan logis pada tipe yang lebih tinggi.

Dan saya tidak begitu yakin apa artinya ini, jadi pertanyaan pertama saya adalah apa yang dimaksud dengan ini dan semoga referensi yang lebih baik tentang pertanyaan ini.

Apa yang saya pikirkan artinya adalah bahwa misalnya eksponensial tidak selalu mempertahankan komposisi relasional pada hidung. Secara khusus kami tidak dapat menampilkan . Ini berarti bahwa eksponensial tidak meluas ke functor pada kategori hubungan.$(R;R') \to (S;S') \equiv ((R \to S);(R' \to S'))$

Namun, sementara saya tidak dapat menunjukkan kesetaraan antara hubungan di atas, saya pasti dapat membuktikan penyertaan , kan?$((R \to S);(R' \to S')) \subset ((R;R') \to (S;S'))$

Mengingat , maka ada dari tipe yang sesuai dengan , jadi diberikan sebuah , saya dapat menunjukkan . Bukankah ini berarti bahwa eksponensial tidak memberi saya longgar functor , yang tampaknya seperti properti yang buruk untuk membuang? Jadi pertanyaan kedua saya adalah apakah ada contoh di mana inklusi ke arah ini tidak dapat dibuktikan?$f((R \to S);(R' \to S')) h$$g$$f(R\to S)g(R'\to S')h$$xRyR'z$$f(x) S g(y) S' h(z)$

Pada bulan-bulan sejak saya mengajukan pertanyaan ini, saya pikir saya telah menemukan jawaban yang masuk akal.

Seringkali, jenis hubungan yang dipertimbangkan tidak menulis. Misalnya, jika gagasan Anda tentang relasi antara CPO adalah rantai subset lengkap dari, maka hubungan antara naturals yang dipesan ditambah infinity dan CPO datar naturals diberikan oleh tahan dan tidak ada yang lain , maka dapat diterima, seperti halnya sebaliknya, tetapi gabungan tidak lengkap rantai, karena untuk setiap alam, tetapi kami tidak punya$R : D \to E$$\omega$$\omega$$|D|\times |E|$$R : \omega + 1 \to \mathbb{N}$$\omega+1$$\mathbb{N}$$R(n,n)$$R$$R;R^T : \omega+1 \to \omega + 1$$n R;R^T n$$\omega R; R^T \omega$ .