| Title | A Compositional Cost Model for the λ-calculus |
| Publication Type | Conference Paper |
| Year of Publication | 2021 |
| Authors | Laird, James |
| Conference Name | 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) |
| Keywords | compositionality, Computational modeling, Computer science, Games, Program processors, pubcrawl, Random access memory, Semantics, Turing machines |
| Abstract | We describe a (time) cost model for the (call-by-value) l-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 lv-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 lv-calculus via a series of linear cost reductions. |
| DOI | 10.1109/LICS52264.2021.9470567 |
| Citation Key | laird_compositional_2021 |
A Compositional Cost Model for the λ-calculus