A semantic measure of the execution time in Linear LogicReportar como inadecuado

A semantic measure of the execution time in Linear Logic - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 CALLIGRAMME - Linear logic, proof networks and categorial grammars INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications 2 PPS - Preuves, Programmes et Systèmes 3 Dipartimento di Filosofia dell-Universita Roma Tre

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.

Keywords : linear logic denotational semantics proof-nets implicit computational complexity

Autor: Daniel De Carvalho - Michele Pagani - Lorenzo Tortora de Falco -

Fuente: https://hal.archives-ouvertes.fr/


Documentos relacionados