[Prev][Next][Index][Thread]
Anti-Symmetry of Higher-Order Subtyping
Hello,
We would like to announce the availability of our new paper, featuring
the first proof of Anti-Symmetry of Higher-Order Subtyping, at:
http://www.dcs.ed.ac.uk/home/hhg/anti-sym.dvi.gz
or
http://guinness.cs.stevens-tech.edu/~abc/anti-sym.ps.gz
We mean by anti-symmetry:
A < B and B < A implies A =beta B (< means less or equal)
The benefits of having proved anti-symmetry can be found in the paper.
The main obstacle to showing anti-symmetry was to prove that:
G |- G(X)(A1,...,Am) < X(A1,...,Am) : K
is not derivable for any G, X, and A1 to Am (where G(X) is the bound
of X in the context G, and < means less or equal). Our previously
developed typed operational semantics for subtyping was crucial in
finding a proof of the non-derivability of that judgement.
This has been an intriguing open problem for a long time. On the one
hand, we knew that G(X)(A1,...,Am) was an upper bound of
X(A1,...,Am), but we didn't know how to prove that the opposite was
not derivable.
Moreover, because the X may appear among the Ai's, the arguments to
show that G(X) cannot be less than or equal to X would not apply in
general. In particular, consider the case m = 2, A1 = X, and G(X) =
/\Y<B. YY. Then X X A2 and (/\Y<B. YY)X A2 are beta-equal.
So the proof that
G|- G(X)(A1,...,Am) < X(A1,...,Am) : K is not derivable needs
to rely on the kinding system, because in the pseudo-types it is not
even true.
Best wishes,
Adriana Compagnoni and Healfdene Goguen