Comparing Cubes

We study the cube of type assignment systems, as introduced in [13], and confront it with Barendregt's typed -cube [4]. The first is obtained from the latter through applying a natural type erasing function E to derivation rules, that erases type information from terms. In particular, we address the question whether a judgement, derivable in a type assignment system, is always an erasure of a derivable judgement in a corresponding typed system; we show that this property holds only for the systems without polymorphism. The type assignment systems we consider satisfy the properties `subject reduction' and `strong normalization'. Moreover, we define a new type assignment cube that is isomorphic to the typed one.

• Type: Conference
• Year: 1994
• Where: LFCS
• Authors: Steffen van Bakel, Luigi Liquori, Simona Ronchi Della Rocca, Pawel Urzyczyn
• Keywords: Artificial Intelligence, LFCS 1994, Type Assignment, Type Assignment Systems, Type Erasing Function