异步会话子类型化可判定性与不可判定性的边界

会话类型是一种行为类型，用于保证并发程序免受基本通信错误的影响。近期的工作表明，异步会话子类型化是不可判定的。然而，由于会话类型在以异步通信为常态而非例外的主流编程语言中已变得流行，检测显著的可判定子类型化关系至关重要。以往的工作考虑了极具限制性的片段，这些片段对通信缓冲区的大小施加了限制（至多为 1），或对表达多重选择的可能性进行了限制（在比较的类型之一中完全不允许使用）。在本文中，我们首次展示了一个不限制通信缓冲区且允许两个被比较类型在输入或输出上均包含多重选择的片段的可判定性，从而得出了一个从应用角度来看更具意义的片段。总体而言，我们通过考虑子类型化的多个片段来研究可判定性与不可判定性之间的边界。值得注意的是，我们表明，即使限制为不使用输出协变和输入逆变，子类型化仍然是不可判定的。