Anti-Symmetry of Higher-Order Subtyping
We would like to announce the availability of our new paper, featuring
the first proof of Anti-Symmetry of Higher-Order Subtyping, at:
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
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
Adriana Compagnoni and Healfdene Goguen