Why Reflexive Graphs for Parametricity?

Question

Looking at models of parametric polymorphism, I am curious why are reflexive graph categories are used?

In particular, why do they not include relational composition? In looking at the models, they all seem to support a natural notion of relational composition:

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

Most recent papers that use reflexive graphs seem to take this for granted, and the only older paper I could find that discussed it was "Relational Parametricity and Local Variables" by O'Hearn and Tennent who say:

One reason for not requiring composability is that, as is well known, composition is not preserved by logical relations at higher types.

And I'm not quite sure what this means, so my first question is what is meant by this and hopefully a better reference on this question.

What I think this means is that for instance the exponential doesn't necessarily preserve relational composition on the nose. In particular we can't show $(R;R') \to (S;S') \equiv ((R \to S);(R' \to S'))$. This means that the exponential doesn't extend to a functor on a category of relations.

However, while I can't show the equivalence between the above relations, I can certainly prove an inclusion $((R \to S);(R' \to S')) \subset ((R;R') \to (S;S'))$, right?

Given $f((R \to S);(R' \to S')) h$, then there exists a $g$ of appropriate type with $f(R\to S)g(R'\to S')h$, so given an $xRyR'z$, I can show $f(x) S g(y) S' h(z)$. Doesn't this means that the exponential does give me a lax functor, which seems like a bad property to throw away? So my second question is are there examples where the inclusion in this direction is not provable, either?

Answer 1

In the months since I asked this question, I think I have found a sensible answer.

Often, the type of relations considered do not compose. For instance, if your notion of a relation $R : D \to E$ between $\omega$CPOs is an $\omega$-chain complete subset of $|D|\times |E|$, then the relation $R : \omega + 1 \to \mathbb{N}$ between the ordered naturals plus infinity $\omega+1$ and the flat CPO of naturals $\mathbb{N}$ given by $R(n,n)$ holds and nothing else, then $R$ is admissible, as is its converse, but the composite $R;R^T : \omega+1 \to \omega + 1$ is not chain-complete, since $n R;R^T n$ for every natural, but we don't have $\omega R; R^T \omega$.