Tight typings and split bounds, fully developed

Multi types – aka non-idempotent intersection types – have been used. to obtain quantitative bounds on higher-order programs, as pioneered by de Carvalho. Notably, they bound at the same time the number of evaluation steps and the size of the result. Recent results show that the number of steps can...

Full description

Saved in:
Bibliographic Details
Published in:Journal of functional programming 2020, Vol.30, Article e14
Main Authors: ACCATTOLI, BENIAMINO, GRAHAM-LENGRAND, STÉPHANE, KESNER, DELIA
Format: Article
Language:English
Subjects:
Calculus
Canonical forms
Complexity
Computer Science
Consumer goods
Evaluation
Logic in Computer Science
Modularity
Substitutes
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Multi types – aka non-idempotent intersection types – have been used. to obtain quantitative bounds on higher-order programs, as pioneered by de Carvalho. Notably, they bound at the same time the number of evaluation steps and the size of the result. Recent results show that the number of steps can be taken as a reasonable time complexity measure. At the same time, however, these results suggest that multi types provide quite lax complexity bounds, because the size of the result can be exponentially bigger than the number of steps. Starting from this observation, we refine and generalise a technique introduced by Bernadet and Graham-Lengrand to provide exact bounds. Our typing judgements carry counters, one measuring evaluation lengths and the other measuring result sizes. In order to emphasise the modularity of the approach, we provide exact bounds for four evaluation strategies, both in the λ -calculus (head, leftmost-outermost, and maximal evaluation) and in the linear substitution calculus (linear head evaluation). Our work aims at both capturing the results in the literature and extending them with new outcomes. Concerning the literature, it unifies de Carvalho and Bernadet & Graham-Lengrand via a uniform technique and a complexity-based perspective. The two main novelties are exact split bounds for the leftmost strategy – the only known strategy that evaluates terms to full normal forms and provides a reasonable complexity measure – and the observation that the computing device hidden behind multi types is the notion of substitution at a distance, as implemented by the linear substitution calculus.
ISSN:0956-7968
1469-7653
DOI:10.1017/S095679682000012X