无限会话类型的不同层次
The Different Shades of Infinite Session Types
摘要：
许多类型系统包含无限类型。在会话类型系统中，这是本文的重点，无限类型是很重要的，因为它们允许通信协议的规范，是无限的时间。通常无限会话类型作为简单的有限状态表达式$\mathsf{rec}\, X.T$或通过非参数方程定义$X\doteq T$引入。或者，某些依赖于标签或值的会话类型系统超越了简单的递归类型。然而，撇开依赖类型不谈，无限会话类型的世界要丰富得多，从各种形式的参数方程定义，一直到共归纳定义空间中的任意无限类型。我们研究无限会话类型跨越灰色阴影的光谱的方式，一般无限类型的明亮的光。我们确定了四个点上的频谱，其特征在于不同风格的方程定义，并表明，他们形成了一个严格的层次结构，通过建立双向对应类的自动机：有限状态，1-计数器，下推和2-计数器。这使我们能够建立可判定性和不可判定性的结果的问题的类型形成，类型等价和对偶的每一类类型。我们还考虑了上下文无关会话类型（并将其扩展到高阶）和嵌套会话类型的先前工作，并将它们定位在我们的无限类型谱中。
英文摘要：
Many type systems include infinite types. In session type systems, which are the focus of this paper, infinite types are important because they allow the specification of communication protocols that are unbounded in time. Usually infinite session types are introduced as simple finite-state expressions $\mathsf{rec}\, X.T$ or by non-parametric equational definitions $X\doteq T$. Alternatively, some systems of label- or value-dependent session types go beyond simple recursive types. However, leaving dependent types aside, there is a much richer world of infinite session types, ranging through various forms of parametric equational definitions, all the way to arbitrary infinite types in a coinductively defined space. We study infinite session types across a spectrum of shades of grey on the way to the bright light of general infinite types. We identify four points on the spectrum, characterised by different styles of equational definitions, and show that they form a strict hierarchy by establishing bidirectional correspondences with classes of automata: finite-state, 1-counter, pushdown and 2-counter. This allows us to establish decidability and undecidability results for the problems of type formation, type equivalence and duality in each class of types. We also consider previous work on context-free session types (and extend it to higher-order) and nested session types, and locate them on our spectrum of infinite types.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
