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.
Document type :
Reports
Complete list of metadatas

Cited literature [2 references]  Display  Hide  Download

https://hal.inria.fr/inria-00206099
Contributor : Rapport de Recherche Inria <>
Submitted on : Monday, February 4, 2008 - 5:58:31 PM
Last modification on : Wednesday, April 17, 2019 - 12:28:06 PM
Long-term archiving on : Friday, September 24, 2010 - 11:07:46 AM

Files

RR-6441.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00206099, version 4

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⟩

Share

Metrics

Record views

321

Files downloads

321