Hostname: page-component-7c8c6479df-ph5wq Total loading time: 0 Render date: 2024-03-19T01:59:45.444Z Has data issue: false hasContentIssue false

Anti-symmetry of higher-order subtyping and equality by subtyping

Published online by Cambridge University Press:  21 February 2006

ADRIANA COMPAGNONI
Affiliation:
Stevens Institute of Technology, Castle Point on Hudson, Hoboken, NJ 07030, USA Email: abc@cs.stevens.edu
HEALFDENE GOGUEN
Affiliation:
AT&T Labs, 180 Park Ave., Florham Park, NJ 07932, USA Email: hhg@att.com

Abstract

This paper gives the first proof that the subtyping relation of a higher-order lambda calculus, ${\cal F}^{\omega}_{\leq}$, is anti-symmetric, establishing in the process that the subtyping relation is a partial order – reflexive, transitive, and anti-symmetric up to $\beta$-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, and the logical relation used to prove its equivalence with the declarative presentation of ${\cal F}^{\omega}_{\leq}$, 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 ${\cal F}^{\omega}_{\leq}$ without a relation for $\beta$-equality, which is apparently the first such, and shows its equivalence with the traditional presentation.

Type
Paper
Copyright
2006 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)