AI 中文总结
该研究将热带半环作为分级系数类型化的分级空间，构建含递归与多态类型的分级类型系统及新型交集类型系统，保证程序高效性且可类型性为Π₀²性质，实现递归论最优。
AI 中文摘要
我们证明，自然数上的热带半环作为分级系数类型化的分级空间时，可精准模拟时间流逝，同时保证良型程序的高效性。当将等级a赋予函数参数时，该参数并非必须立即可用，而是会在a个时间步后可用。我们通过两个形式系统研究这一思路：首先引入具备递归类型与多态类型的分级类型系统，证明在该场景下，对递归类型施加自然限制即可保证高效性，同时仍允许定义流及其上的递归程序；特别地，我们证明Nakano的后续模态可直接嵌入该系统。随后，我们证明热带分级自然催生了一种新型交集类型，其中原本由类型集或多重集承担的角色，现由“时间化集”承担——即函数为每个类型A分配对应项以类型A可用的最早时间（以等级表示）。对于所得系统，我们不仅证明其可保证高效性，还证明其具有特征性：可类型化项恰好是那些具有遗传头范式的项。值得注意的是，该系统在递归论意义上是最优的，即可类型性可直接被证明为算术分层中的Π₀²性质。
英文摘要
We show that the tropical semiring over the natural numbers, when used as the grading space in graded coeffect typing, faithfully models the passage of time while simultaneously guaranteeing productivity of well-typed programs. A grade a, when assigned to a function parameter, indicates that the parameter is not necessarily available immediately, but will become available after a time steps. We investigate this idea through two formal systems. We first introduce a graded type system featuring recursive and polymorphic types, and show that, in this setting, a natural restriction on recursive types is sufficient to guarantee productivity, while still allowing the definition of streams and recursive programs on them. In particular, we prove that Nakano's later modality can be embedded directly into our system. We then show that tropical grading naturally suggests a novel form of intersection typing, in which the role traditionally played by sets or multisets of types is instead taken by "timed" sets, i.e., functions assigning to each type A the earliest time, represented as a grade, from which the underlying term is available with type A. For the resulting system, we prove not only that productivity is guaranteed, but that it is also characterized: the typable terms are exactly those with hereditarily head normal forms. Remarkably, the system is recursion-theoretically optimal, i.e., typability can be directly proved to be a $Π_0^2$ property in the arithmetical hierarchy.
