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

<p>Often, the type of relations considered do <em>not</em> 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$.</p>

CC BY-SA 3.0
2017-07-28T19:05:35.907Z
2017-07-28T19:05:35.907Z
Max New
<p>Looking at models of parametric polymorphism, I am curious why are
<em>reflexive graph</em> categories are used?</p>

<p>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:</p>

<p>$$ x(R;S)z \iff \exists y. xRy \wedge y S z$$</p>

<p>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:</p>

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

<p>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.</p>

<p>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.</p>

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

<p>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 <a href="https://ncatlab.org/nlab/show/lax+functor" rel="noreferrer"><em>lax</em> functor</a>,
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?</p>

CC BY-SA 4.0
2023-01-06T10:21:08.487Z
Relational composition does not seem to be useful for proving the parametricity theorem or for reasoning about parametricity properties. This is precisely because the relational composition is not compatible with the exponential. You are right about the *inclusion* property but it is not enough. The proof of the parametricity theorem requires handling the exponential types as one of the inductive cases.
winitzki
<ct.category-theory><parametricity><logical-relations>
Why Reflexive Graphs for Parametricity?
Max New
# Why Reflexive Graphs for Parametricity?

(Asked by: username_0 on 2017-02-28)

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](https://ncatlab.org/nlab/show/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?

**Tags:** ct.category-theory, parametricity, logical-relations

> **Comments:**
> **username_1**: Relational composition does not seem to be useful for proving the parametricity theorem or for reasoning about parametricity properties. This is precisely because the relational composition is not compatible with the exponential. You are right about the *inclusion* property but it is not enough. The proof of the parametricity theorem requires handling the exponential types as one of the inductive cases.  

---

## 1 answers

### Answer by username_0 on 2017-07-28. Score: 2 | Accepted answer

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


---

