## 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 language | English |
---|---|

Title of host publication | 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021 |

Publisher | IEEE |

Pages | 1-13 |

Volume | 2021-June |

ISBN (Electronic) | 9781665448956 |

ISBN (Print) | 9781665448956 |

DOIs | |

Publication status | Published - 29 Jun 2021 |

Event | 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021 - Duration: 29 Jun 2021 → 2 Jul 2021 |

### Publication series

Name | Proceedings - Symposium on Logic in Computer Science |
---|---|

Volume | 2021-June |

ISSN (Print) | 1043-6871 |

### Conference

Conference | 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021 |
---|---|

Period | 29/06/21 → 2/07/21 |

### Bibliographical note

Publisher Copyright:© 2021 IEEE.

## ASJC Scopus subject areas

- Software
- General Mathematics