[TYPES] a counterexample to Plotkin and Abadi's characterization of equivalence at existential type?

[Derek Dreyer]

I have what appears to be a counterexample to the characterization of
equivalence at existential type in Plotkin and Abadi's logic for
parametric polymorphism, and I'm wondering what's going on.  Here is a
link to their TLCA'93 paper from Gordon's web page:

http://homepages.inf.ed.ac.uk/gdp/publications/Par_Poly.pdf

In short, Theorem 7 in their paper says that two terms of existential
type are equal *if and only if* there exists a "simulation relation"
between their internal representations of the abstract type such that
the operations are logically related at the appropriate type
(interpreting the abstract type using the chosen simulation relation).
 The "if" direction is fine: that's just the well-known principle of
"representation independence".  It's the "only if" direction that I'm
confused about.

In particular, it seems to me that, using the "only if" direction of
Theorem 7, I can derive a contradiction in the logic, so I'm trying to
figure out where/if I screwed up.

The issue is the following: There is an example given in Pitts'
chapter in Pierce's ATTAPL book, namely Sumii's variation on Example
7.7.4 discussed in Remark 7.7.7.  (I will reproduce it below.)  The
entire point of the example, which in Sumii's variation applies to
pure System F, is that it shows a case where two existential packages
are contextually equivalent despite the fact that there is no
simulation relation between their type representations that would make
a simulation argument (i.e. representation independence proof) go
through.  Pitts proves that there is no simulation proof, and he also
sketches the proof of contextual equivalence of the packages through
brute-force means.

Now, by itself, Pitts' result is not in contradiction to Theorem 7
from the Plotkin-Abadi logic (PAL) paper, since PAL does not talk
about contextual equivalence: it talks about its own primitive notion
of equality.  So one might write off this example as a quirk of
contextual equivalence which is not relevant to the better-behaved PAL
equality.

However, in March 2008, I worked out (and privately circulated) a
*much* simpler proof of the contextual equivalence in question, which
is not brute force: rather, it relies on a simple transitive
combination of two simulation subproofs (see below).  Now it seems to
me that there should be no problem expressing my simulation proofs in
PAL, and therefore constructing a proof of equivalence of the
existential packages in the example (by transitivity of PAL's
equality), despite the fact that there is provably no direct
simulation argument that shows them equivalent.  So, unless I'm
confused (which I probably am), this would seem to contradict the
"only if" direction of Theorem 7.

One basic problem I have is that I do not understand the proof of the
"only if" direction of Theorem 7 in PAL -- it is not presented in the
paper (which merely suggests that it follows from the "parametricity
schema"), and I have not yet found a worked-out proof of it in any
follow-on paper either.  If someone can point me to such a proof, that
would be most helpful.  If not, how would one prove it?
Alternatively, have I gone wrong somewhere in my argument that it is
false?

The details of the "counterexample" are given below.

Thanks and best regards,
Derek

-------

First, here are the details of Pitts' example (the Sumii variation):

Q = Exists X. (X -> Bool) -> Bool
Void = Forall X. X
H1 = \f:Void->Bool. False
P1 = pack [Void,H1] as Q
H2 = \f:Bool->Bool. (f True) and not (f False)
P2 = pack [Bool,H2] as Q

We want to prove that P1 is equivalent to P2.  Intuitively, they are
equivalent because the only possible function that could be passed in
as the instantiation of f is the constant function returning True or
False.  In either case, both H1(f) and H2(f) will return False.

A direct simulation proof does not exist.  To see this, suppose one
did exist: it would involve a simulation relation between Void and
Bool, together with a proof that H1 and H2 are related at "(E -> Bool)
-> Bool".

1. Void is an empty type, so the only possible simulation relation
between Void and Bool is the empty relation E.

2. Given E as the necessary choice of simulation relation, we can
choose f1 to be any function of type Void -> Bool and we can choose f2
to be the identity function at Bool -> Bool.  Since E is empty, it is
trivial to show that f1 and f2 are logically related at "E -> Bool".
However, H1(f1) returns False, while H2(f2) returns True, in which
case they are not logically related at Bool.  So H1 and H2 are *not*
logically related at "(E -> Bool) -> Bool".  Contradiction.

OK, now I will prove that P1 and P2 are in fact equivalent by giving a
*pair* of simulation proofs demonstrating that each of them is
equivalent to P3, defined as follows:

H3 = \f:Bool->Bool. (f True) and not (f True)
P3 = pack [Bool,H3] as Q

To prove P1 equivalent to P3 by simulation argument:

1. We choose the simulation relation to be the empty relation E
between Void and Bool (that's all we can choose).

2. Let f1 and f3 be functions of type Void -> Bool and Bool -> Bool
related at "E -> Bool".  We must show H1(f1) and H3(f3) are related at
Bool.  Clearly, H1(f1) = False, so we must show H3(f3) = False.  We
know that (f3 True) has type Bool, so it either equals True or False
(the logical relations lemma tells us that, if nothing else).  In
either case, H3(f3) = False, so we are done.

To prove P3 equivalent to P2 by simulation argument:

1. We choose the simulation relation to be the full relation R between
Bool and Bool.  Choosing R = {(True,True),(True,False)} would also
work.

2. Let f3 and f2 be functions, both of type Bool -> Bool, related at
"R -> Bool".  We must show H3(f3) and H2(f2) related at Bool, i.e.
that H3(f3) = H2(f2).  Since (True,True) and (True,False) are both in
R, we have from the relatedness of f3 and f2 that (f3 True) = (f2
True) and (f3 True) = (f2 False).  Hence, (f2 True) = (f3 True) = (f2
False), and so H3(f3) = H2(f2) = False.

Thus, P1 = P3 = P2, which implies P1 = P2 by transitivity, but there
is no direct simulation proof of P1 = P2, which seems to contradict
the "only if" direction of Theorem 7.