On the exp-log normal form of types
Résumé
We present a type pseudo-normal form that any type built from arrows, products and sums can be isomorphically mapped to and that systematically minimizes the number of premises of sum type used. Inspired from a representation of exponential polynomials, the normal form presents an extension of the notion of disjunctive normal form that handles arrows. We also show how to apply it for simplifying the axioms of the theory of βη-equality of terms of the lambda calculus with sums.
Origine : Fichiers produits par l'(les) auteur(s)