Download PDFOpen PDF in browserTowards a Semantic Measure of the Execution Time in CallbyValue lambdaCalculusEasyChair Preprint no. 33432 pages•Date: July 9, 2018AbstractWe investigate the possibility of a semantic account of the execution time (i.e. the number of beta vsteps leading to the normal form, if any) for the shuffling calculus, an extension of Plotkin's untyped callbyvalue lambdacalculus. For this purpose, we use a linear logic based denotational model that can be seen as a nonidempotent intersection type system: relational semantics. Our investigation is inspired by similar ones for linear logic proofnets and untyped callbyname lambdacalculus. 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 callbyname lambdacalculus, 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 callbyvalue setting, we conjecture that a refinement of its syntax and operational semantics is needed. Keyphrases: callbyvalue, denotational model, execution time, lambda calculus, linear logic, nonidempotent intersection types, quantitative subject reduction, relational semantics, Shuffling Calculus, Size invariance, Type derivation
