On principal types and well-foundedness of the cummulativity relation in ECC
| Autor: | Ken, Eitetsu, Natori, Masaki, Tojo, Kenji, Watanabe, Kazuki |
|---|---|
| Rok vydání: | 2020 |
| Předmět: | |
| Druh dokumentu: | Working Paper |
| Popis: | 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. Comment: 14 pages, no figures, the title changed, the historical remarks modified, the results unchanged, the e-mail addresses added |
| Databáze: | arXiv |
| Externí odkaz: |
|