紧类型和分裂边界
Tight Typings and Split Bounds
摘要：
多类型--又名非幂等相交类型--已被用来获得高阶程序的定量界限，由de Carvalho开创。值得注意的是，它们同时限制了评估步骤的数量和结果的大小。最近的结果表明，步骤的数量可以作为一个合理的时间复杂度的措施。然而，与此同时，这些结果表明，多类型提供了相当宽松的复杂性界限，因为结果的大小可以指数地大于步骤的数量。从这个观察开始，我们完善和推广的技术介绍Bernadet和Graham-Lengrand提供确切的界限的最大战略。我们的打字判断带有两个计数器，一个测量评估长度，另一个测量结果大小。为了强调模块化的方法，我们提供了四个评价策略的确切界限，无论是在微积分（头，最左最外，最大的评价）和线性替代演算（线性头评价）。我们的工作旨在捕捉文献中的结果，并将其扩展为新的结果。在文献方面，它通过统一的技术和基于复杂性的视角将卡瓦略和伯纳黛特与格雷厄姆-朗格朗统一起来。两个主要的新颖性是最左边的策略的精确分割界限-唯一已知的将项评估为完整的范式并提供合理的复杂性度量的策略-以及观察到隐藏在多类型背后的计算设备是远距离替换的概念，如线性替换演算所实现的。
英文摘要：
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 & Graham-Lengrand to provide exact bounds for the maximal strategy. Our typing judgements carry two 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 lambda-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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
