一句话：通过带计数器的多重类型系统，为多种求值策略给出精确的求值步数与结果规模界。
多重类型（即非幂等交集类型）已被用于高阶程序的定量分析，能够同时约束求值步数与结果规模，但已有结果给出的界较宽松：结果规模可能比步数指数级大。本文精炼并推广 Bernadet 与 Graham-Lengrand 的技术，在类型判断中引入两个计数器，分别测度求值长度与结果规模，从而为 λ-演算的 head、leftmost-outermost、maximal 求值以及线性替换演算的 linear head 求值给出精确界。工作统一了 de Carvalho 与 Bernadet–Graham-Lengrand 的结果，并从复杂度视角加以扩展。主要新意包括：为 leftmost 策略给出精确分裂界，这是已知唯一能求值到完整正规形并提供合理复杂度度量的策略；以及揭示多重类型背后的计算装置是线性替换演算中实现的“远距离替换”。
Abstract 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.
@article{AccattoliGK20,
title = {Tight typings and split bounds, fully developed},
author = {BENIAMINO ACCATTOLI and STÉPHANE GRAHAM-LENGRAND and DELIA KESNER},
journal = {Journal of Functional Programming},
volume = {30},
year = {2020},
doi = {10.1017/s095679682000012x}
}