DECIDABILITY AND CONFLUENCE OF BETA-ETA-TOP(LESS-THAN-OR-EQUAL-TO) REDUCTION IN F(LESS-THAN-OR-EQUAL-TO)

We contribute to the syntactic study of F less-than-or-equal-to a variant of second-order lambda-calculus F which appears as a paradigmatic kernel language for polymorphism and subtyping. The type system of F less-than-or-equal-to has a maximum type Top and bounded quantification. We endow this language with the beta-rules (for terms and types), to which we add eta-rules (for terms and types) and a rule which equates all terms of type Top. These rules are suggested by the axiomatization of cartesian closed categories. We exhibit a weakly normalizing and confluent reduction system for this theory betaeta top less-than-or-equal-to and show that it is decidable. It is also confluent, but decidability does not follow from confluence, since reduction is not effective. Our proofs rely on the confluence and decidability of a corresponding system on F1 (the extension of F with a terminal type). (C) 1994 Academic Press, Inc.