On the Definition of the Eta-long Normal Form in Type Systems of the Cube

2023/07/03 by Dowek, Gilles, Huet, Gérard, Werner, Benjamin
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2307.00854

Abstract

The smallest transitive relation < on well-typed normal terms such that if t is a strict subterm of u then t < u and if T is the normal form of the type of t and the term t is not a sort then T < t is well-founded in the type systems of the cube. Thus every term admits a eta-long normal form.

Related

• Deciding equivalence with sums and the empty type
• A note on equivariant eta forms
• On principal types and well-foundedness of the cummulativity relation in ECC
• Some properties of β-η-normal forms in λ-K-calculus (Alcune proprietá delle forme β-η-normali nel λ-K-calcolo)
• Prenex normalization and the hierarchical classification of formulas