A Compositional Cost Model for the Lambda-calculus

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

53 Downloads (Pure)


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, context 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 publicationProceedings of Logic in Computer Science, 2021
ISBN (Print)9781665448956
Publication statusE-pub ahead of print - 29 Jun 2021
Event36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021 -
Duration: 29 Jun 20212 Jul 2021


Conference36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021


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

Cite this