Why Reflexive Graphs for Parametricity? 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?
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$.