Sciweavers

Share
TCS
2011

A semantic measure of the execution time in linear logic

8 years 5 months ago
A semantic measure of the execution time in linear logic
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 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 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. Key words: Linear Logic, Denotational Semantics, Computational complexity
Daniel de Carvalho, Michele Pagani, Lorenzo Tortor
Added 15 May 2011
Updated 15 May 2011
Type Journal
Year 2011
Where TCS
Authors Daniel de Carvalho, Michele Pagani, Lorenzo Tortora de Falco
Comments (0)
books