On the exp-log normal form of types - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2015

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.
Fichier principal
Vignette du fichier
explog.pdf (139.9 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-01167162 , version 1 (23-06-2015)
hal-01167162 , version 2 (17-08-2016)

Identifiants

  • HAL Id : hal-01167162 , version 1

Citer

Danko Ilik. On the exp-log normal form of types. 2015. ⟨hal-01167162v1⟩
328 Consultations
139 Téléchargements

Partager

Gmail Facebook X LinkedIn More