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 familiar beta-rules (for terms and types), to which we add extensionality rules: the eta-rules (for terms and types), and a rule (top) which equates all terms of type Top. These rules are suggested by the axiomatization of cartesian closed categories. We show that this theory beta-eta-top less-than-or-equal-to is decidable, by exhibiting an effectively weakly normalizing and confluent rewriting system for it. Our proof of confluence relies on the confluence of a corresponding system on F1 (the extension of F with a terminal type), and follows a general pattern that we investigate for itself in a separate paper.

Subtyping + extensionality: Confluence of beta-eta top in Fsub, extended abstract

GHELLI, GIORGIO
1991

Abstract

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 familiar beta-rules (for terms and types), to which we add extensionality rules: the eta-rules (for terms and types), and a rule (top) which equates all terms of type Top. These rules are suggested by the axiomatization of cartesian closed categories. We show that this theory beta-eta-top less-than-or-equal-to is decidable, by exhibiting an effectively weakly normalizing and confluent rewriting system for it. Our proof of confluence relies on the confluence of a corresponding system on F1 (the extension of F with a terminal type), and follows a general pattern that we investigate for itself in a separate paper.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11568/18631
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? 4
social impact