24
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

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

      Preprint

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          We investigate the possibility of a semantic account of the execution time (i.e. the number of beta-steps leading to the normal form, if any) for the shuffling calculus, an extension of Plotkin's 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). 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.

          Related collections

          Most cited references36

          • Record: found
          • Abstract: not found
          • Book: not found

          States, Effects, and Operations Fundamental Notions of Quantum Theory

            Bookmark
            • Record: found
            • Abstract: not found
            • Article: not found

            An extension of the basic functionality theory for the $\lambda$-calculus.

              Bookmark
              • Record: found
              • Abstract: not found
              • Article: not found

              A new type assignment for λ-terms

                Bookmark

                Author and article information

                Journal
                22 April 2019
                Article
                10.4204/EPTCS.293.5
                1904.10800
                6d14c926-3799-46e3-8d34-982c2271bbad

                http://arxiv.org/licenses/nonexclusive-distrib/1.0/

                History
                Custom metadata
                EPTCS 293, 2019, pp. 57-72
                In Proceedings DCM 2018 and ITRS 2018 , arXiv:1904.09561. arXiv admin note: substantial text overlap with arXiv:1812.10799
                cs.LO cs.DM cs.PL
                EPTCS

                Theoretical computer science,Programming languages,Discrete mathematics & Graph theory

                Comments

                Comment on this article

                scite_
                0
                0
                0
                0
                Smart Citations
                0
                0
                0
                0
                Citing PublicationsSupportingMentioningContrasting
                View Citations

                See how this article has been cited at scite.ai

                scite shows how a scientific paper has been cited by providing the context of the citation, a classification describing whether it supports, mentions, or contrasts the cited claim, and a label indicating in which section the citation was made.

                Similar content360

                Most referenced authors955