时空历险记
Adventures in time and space
摘要：
本文探讨了什么是本质上是一个呼叫的PCF的价值观版本下的复杂性理论的动机类型系统。ATR的一阶规划刻画了多项式时间可计算函数，二阶规划刻画了Mehlhorn和Cook和Urquhart的2型基本可行泛函。(The ATR类型仅限于级别0、1和2。类型系统分为两部分，一部分主要限制表达式值的大小，另一部分主要限制计算表达式所需的时间。尺寸限制部分的动机是Bellantoni和Cook和Leivant的多项式时间的隐式特征。时间限制部分是Barber和Plotkin的DILL的仿射版本。为ATR构造了两种语义。第一个是对ATR的朴素指称语义的修剪。这种修剪删除了某些函数，这些函数会导致其他可行形式的递归出错。第二种语义是ATR相对于某个抽象机器的时间复杂度的模型。这个模型提供了一个设置复杂的递归所产生的ATR递归，其解决方案产生二阶多项式时间的界限。时间复杂度的语义也被证明是健全的相对于抽象机器上的解释成本。
英文摘要：
This paper investigates what is essentially a call-by-value version of PCF under a complexity-theoretically motivated type system. The programming formalism, ATR, has its first-order programs characterize the polynomial-time computable functions, and its second-order programs characterize the type-2 basic feasible functionals of Mehlhorn and of Cook and Urquhart. (The ATR-types are confined to levels 0, 1, and 2.) The type system comes in two parts, one that primarily restricts the sizes of values of expressions and a second that primarily restricts the time required to evaluate expressions. The size-restricted part is motivated by Bellantoni and Cook's and Leivant's implicit characterizations of polynomial-time. The time-restricting part is an affine version of Barber and Plotkin's DILL. Two semantics are constructed for ATR. The first is a pruning of the naive denotational semantics for ATR. This pruning removes certain functions that cause otherwise feasible forms of recursion to go wrong. The second semantics is a model for ATR's time complexity relative to a certain abstract machine. This model provides a setting for complexity recurrences arising from ATR recursions, the solutions of which yield second-order polynomial time bounds. The time-complexity semantics is also shown to be sound relative to the costs of interpretation on the abstract machine.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
