A semantic measure of the execution time in Linear Logic

Abstract : We give a semantic account of the execution time (i.e. the number of cut-elimination steps leading to the normal form) of an untyped MELL (proof-)net. We first prove that: 1) a net is head-normalizable (i.e. normalizable at depth 0) if and only if its interpretation in the multiset based relational semantics is not empty and 2) a net is normalizable if and only if its exhaustive interpretation (a suitable restriction of its interpretation) is not empty. We then define a size on every experiment of a net, and we precisely relate the number of cut-elimination steps of every stratified reduction sequence to the size of a particular experiment. Finally, we give a semantic measure of execution time: we prove that we can compute the number of cut-elimination steps leading to a cut free normal form of the net obtained by connecting two cut free nets by means of a cut link, from the interpretations of the two cut free nets. These results are inspired by similar ones obtained by the first author for the (untyped) lambda-calculus.
Type de document :
Rapport
[Research Report] RR-6441, INRIA. 2008, pp.48
Liste complète des métadonnées

Littérature citée [2 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00206099
Contributeur : Rapport de Recherche Inria <>
Soumis le : lundi 4 février 2008 - 17:58:31
Dernière modification le : jeudi 15 novembre 2018 - 20:26:59
Document(s) archivé(s) le : vendredi 24 septembre 2010 - 11:07:46

Fichiers

RR-6441.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00206099, version 4

Collections

Citation

Daniel De Carvalho, Michele Pagani, Lorenzo Tortora de Falco. A semantic measure of the execution time in Linear Logic. [Research Report] RR-6441, INRIA. 2008, pp.48. 〈inria-00206099v4〉

Partager

Métriques

Consultations de la notice

228

Téléchargements de fichiers

192