Skip to Main content Skip to Navigation
Reports

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

https://hal.inria.fr/inria-00206099
Contributor : Daniel de Carvalho <>
Submitted on : Friday, February 1, 2008 - 7:38:22 PM
Last modification on : Thursday, June 18, 2020 - 12:46:02 PM
Document(s) archivé(s) le : Thursday, September 23, 2010 - 4:16:54 PM

Files

normbysem_Rel.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00206099, version 3

Collections

PPS

Citation

Daniel de Carvalho, Michele Pagani, Lorenzo Tortora de Falco. A semantic measure of the execution time in Linear Logic. [Research Report] 2008, pp.48. ⟨inria-00206099v3⟩

Share

Metrics

Record views

8

Files downloads

65