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

[Uday S Reddy]

Derek Dreyer writes:

> So how do you show this?  How do you *prove* that simulation is the
> only way to prove that two terms of existential type are equal?  I
> don't see how it follows from Theorem 7.

It doesn't follow from Theorem 7.  It can't.  Notice that Theorem 7 is a
theorem *within* PAL.  (It is really like a derived proof rule.)  The
property you want is a metatheorem *about* PAL.  It says that the only
proofs of equality within PAL will be transitive compositions of simulation
proofs.

I don't expect that proving that formally will be easy.  It will have to be
some kind of a proof reduction argument, along the lines of "if there is a
proof of u = v then there is a proof of u = v of this particular form...".
It might have to run through all the axioms and proof rules of PAL and argue
that nothing else is possible.

However, intuitively it is easy to see (I hope) that the only way to prove
the equality of terms of existential types is via Theorem 7, and it allows
you to prove it using simulation relations.  So, in a finite proof, you can
only have a finite number of such simulation relation steps.

> > That is indeed right.  For closed types, the "only if" direction is trivial.
> > However, for open types, it is not.  You would notice in Theorem 7 the
> > additional condition that x and y have to be related by A[S,rho].  That
> > plays a significant role.
> 
> This is fascinating, but I still don't understand concretely what one
> can "do" with the "only if" direction in the case of open types.

My point was this: In Theorem 7, you find \vecB and \vecC as free type
variables.  That means that A[X, \vecB] and A[Y, \vecC] are different types,
and you can't pick x and y to be the same as you did in the closed types
case.  So, the "only if" part of the general statement of Theorem 7 is not
trivial in general, but it becomes trivial for the closed types case.

As to what you can "do" with the "only if" direction, I don't know.  I was
assuming that you had some application in mind since you raised this.  The
"only if" directions are essentially stating completeness of the respective
proof rules.  So, they could presumably be used to *disprove* that two terms
are related by showing that all possible ways proving them related are
exhausted.

Cheers,
Uday