A semantic measure of the execution time in linear logic

作者：de Carvalho D^*; Pagani M; de Falco L Tortora

来源：Theoretical Computer Science, 2011, 412(20): 1884-1902.

DOI：10.1016/j.tcs.2010.12.017

• Linear logic
• Denotational semantics
• Computational complexity

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.

• 出版日期2011-4-29