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

• Type: Journal
• Year: 2011
• Where: TCS
• Authors: Daniel de Carvalho, Michele Pagani, Lorenzo Tortora de Falco
• Keywords: Cut Elimination, Cut Free Nets, Semantics, TCS 2011, Theoretical Computer Science