Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus

Author: Giulio Guerrieri

Paper Information

Title:Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus
Authors:Giulio Guerrieri
Proceedings:ITRS Full papers
Editor: Michele Pagani
Keywords:call-by-value, lambda-calculus, non-idempotent intersection types, relational semantics, linear logic, shuffling calculus, execution time

ABSTRACT. We investigate the possibility of a semantic account of the execution time (i.e. the number of beta v-steps leading to the normal form, if any) for the shuffling calculus, an extension of Plotkin's untyped call-by-value lambda-calculus. For this purpose, we use a linear logic based denotational model that can be seen as a non-idempotent intersection type system: relational semantics. Our investigation is inspired by similar ones for linear logic proof-nets and untyped call-by-name lambda-calculus. We first prove a qualitative result: a (possibly open) term is normalizable for weak reduction (which does not reduce under abstractions) if and only if its interpretation is not empty. We then show that the size of type derivations can be used to measure the execution time. Finally, we show that, differently from the case of linear logic and call-by-name lambda-calculus, the quantitative information enclosed in type derivations does not lift to types (i.e. to the interpretation of terms). In order to get a genuine semantic measure of execution time in a call-by-value setting, we conjecture that a refinement of its syntax and operational semantics is needed.

Talk:Jul 08 12:00 (Session 38J)