Towards a semantic measure of the execution time in call-by-value lambda-calculus

Research output: Contribution to journalConference article

Abstract

We investigate the possibility of a semantic account of the execution time (i.e. the number of βv-steps leading to the normal form, if any) for the shuffling calculus, an extension of Plotkin’s call-by-value λ-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 λ-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 λ-calculus, the quantitative information enclosed in type derivations does not lift to types (i.e. to the interpretation of terms). To get a truly semantic measure of execution time in a call-by-value setting, we conjecture that a refinement of its syntax and operational semantics is needed.

Original languageEnglish
Pages (from-to)57-72
Number of pages16
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
Volume293
DOIs
Publication statusPublished - 2019
Event12th Workshop on Developments in Computational Models, DCM 2018 and 9th Workshop on Intersection Types and Related Systems, ITRS 2018 - Oxford, UK United Kingdom
Duration: 8 Jul 20188 Jul 2018

ASJC Scopus subject areas

  • Software

Cite this

@article{7f0b7cbc87d142448a96bbfcac8d438e,
title = "Towards a semantic measure of the execution time in call-by-value lambda-calculus",
abstract = "We investigate the possibility of a semantic account of the execution time (i.e. the number of βv-steps leading to the normal form, if any) for the shuffling calculus, an extension of Plotkin’s call-by-value λ-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 λ-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 λ-calculus, the quantitative information enclosed in type derivations does not lift to types (i.e. to the interpretation of terms). To get a truly semantic measure of execution time in a call-by-value setting, we conjecture that a refinement of its syntax and operational semantics is needed.",
author = "Giulio Guerrieri",
year = "2019",
doi = "10.4204/EPTCS.293.5",
language = "English",
volume = "293",
pages = "57--72",
journal = "Electronic Proceedings in Theoretical Computer Science",
issn = "2075-2180",
publisher = "Open Publishing Association",

}

TY - JOUR

T1 - Towards a semantic measure of the execution time in call-by-value lambda-calculus

AU - Guerrieri, Giulio

PY - 2019

Y1 - 2019

N2 - We investigate the possibility of a semantic account of the execution time (i.e. the number of βv-steps leading to the normal form, if any) for the shuffling calculus, an extension of Plotkin’s call-by-value λ-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 λ-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 λ-calculus, the quantitative information enclosed in type derivations does not lift to types (i.e. to the interpretation of terms). To get a truly semantic measure of execution time in a call-by-value setting, we conjecture that a refinement of its syntax and operational semantics is needed.

AB - We investigate the possibility of a semantic account of the execution time (i.e. the number of βv-steps leading to the normal form, if any) for the shuffling calculus, an extension of Plotkin’s call-by-value λ-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 λ-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 λ-calculus, the quantitative information enclosed in type derivations does not lift to types (i.e. to the interpretation of terms). To get a truly semantic measure of execution time in a call-by-value setting, we conjecture that a refinement of its syntax and operational semantics is needed.

UR - http://www.scopus.com/inward/record.url?scp=85066074836&partnerID=8YFLogxK

U2 - 10.4204/EPTCS.293.5

DO - 10.4204/EPTCS.293.5

M3 - Conference article

VL - 293

SP - 57

EP - 72

JO - Electronic Proceedings in Theoretical Computer Science

JF - Electronic Proceedings in Theoretical Computer Science

SN - 2075-2180

ER -