On principal types and well-foundedness of the cummulativity relation in ECC

TL;DR

This paper investigates the well-foundedness of the cumulativity relation in the Extended Calculus of Constructions (ECC), showing it holds under certain restrictions and providing an independent proof of principal types.

Contribution

It establishes conditions under which the cumulativity relation in ECC is well-founded and offers an independent proof of principal types, avoiding circular reasoning.

Findings

Cumulativity is well-founded for types in valid contexts.

Cumulativity is well-founded for terms with normal forms.

Provides an independent proof of principal types in ECC.

Abstract

When we investigate a type system, it is helpful if we can establish the well-foundedness of types or terms with respect to a certain hierarchy, and the Extended Calculus of Constructions (called $ECC$, defined and studied comprehensively in [Luo,1994]) is no exception. However, under a very natural hierarchy relation (called the cumulativity relation in [Luo,1994]), the well-foundedness of the hierarchy does not hold generally. In this article,we show that the cumulativity relation is well-founded if it is restricted to one of the following two natural families of terms: \begin{enumerate} \item types in a valid context \item terms having normal forms \end{enumerate} Also, we give an independent proof of the existence of principal types in $ECC$ since it is used in the proof of well-foundedness of cumulativity relation in a valid context although it is often proved by utilizing the well-foundedness of the hierarchy, which would make our argument circular if adopted.