Anti-Symmetry of Higher-Order Subtyping

This paper gives the first proof that the subtyping relation of a higherorder lambda calculus, Fω ≤, is anti-symmetric, establishing in the process that the subtyping relation is a partial order—reflexive, transitive, and anti-symmetric up to β-equality. While a subtyping relation is reflexive and transitive by definition, anti-symmetry is a derived property. The result, which may seem obvious to the non-expert, is technically challenging, and had been an open problem for almost a decade. In this context, typed operational semantics for subtyping offers a powerful new technology to solve the problem: of particular importance is our extended rule for the well-formedness of types with head variables. The paper also gives a presentation of Fω ≤ without a relation for β-equality, apparently the first such, and shows its equivalence with the traditional presentation.

• Type: Conference
• Year: 1999
• Where: CSL
• Authors: Adriana B. Compagnoni, Healfdene Goguen
• Keywords: Automated Reasoning, CSL 1999, Partial Order—reflexive, Subtyping, first Proof