A Compositional Cost Model for the λ-calculus

Research output: Chapter in Book/Report/Conference proceedingChapter in a published conference proceeding

55 Downloads (Pure)

Abstract

We describe a (time) cost model for the (call-by-value) λ-calculus based on a natural presentation of its game semantics: the cost of computing a finite approximant to the denotation of a term (its evaluation tree) is the size of its smallest derivation in the semantics. This measure has an optimality property enabling compositional reasoning about cost bounds: for any term A, con C[_] and approximants a and c to the trees of A and C[A], the cost of computing c from C[A] is no more than the cost of computing a from A and c from C[a].Although the natural semantics on which it is based is nondeterministic, our cost model is reasonable: we describe a deterministic algorithm for recognizing evaluation tree approximants which satisfies it (up to a constant factor overhead) on a Random Access Machine. This requires an implementation of the λv-calculus on the RAM which is completely lazy: compositionality of costs entails that work done to evaluate any part of a term cannot be duplicated. This is achieved by a novel implementation of graph reduction for nameless explicit substitutions, to which we compile the λv-calculus via a series of linear cost reductions.

Original languageEnglish
Title of host publication2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021
PublisherIEEE
Pages1-13
Volume2021-June
ISBN (Electronic)9781665448956
ISBN (Print)9781665448956
DOIs
Publication statusPublished - 29 Jun 2021
Event36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021 -
Duration: 29 Jun 20212 Jul 2021

Publication series

NameProceedings - Symposium on Logic in Computer Science
Volume2021-June
ISSN (Print)1043-6871

Conference

Conference36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021
Period29/06/212/07/21

ASJC Scopus subject areas

  • Software
  • Mathematics(all)

Fingerprint

Dive into the research topics of 'A Compositional Cost Model for the λ-calculus'. Together they form a unique fingerprint.

Cite this