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 vari ant of second-order lambda-calculus F which appears as a paradigmatic kernel language for polymorphism and subtyping. The type system of F l ess-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 axiomatizatio n of cartesian closed categories. We exhibit a weakly normalizing and confluent reduction system for this theory betaeta top less-than-or-eq ual-to and show that it is decidable. It is also confluent, but decida bility does not follow from confluence, since reduction is not effecti ve. Our proofs rely on the confluence and decidability of a correspond ing system on F1 (the extension of F with a terminal type). (C) 1994 A cademic Press, Inc.