异步会话子类型的不可判定性

会话类型用于描述分布式系统中的通信协议，并且如同类型理论中通常的那样，会话子类型刻画了通信进程的可替换性。我们研究了异步通信系统中会话类型子类型的（不）可判定性。我们首先设计了一个核心的不可判定子类型关系，该关系通过对类型结构施加限制而得到。然后，作为这一初始不可判定性结果的推论，我们证明（与文献中所述或所推测的不同）迄今为止为会话类型定义的三种异步子类型概念都是不可判定的。即，我们考虑了 Mostrous 和 Yoshida 针对二元会话的异步会话子类型，Chen 等人基于每条发出的消息最终都会被消费的假设针对二元会话的关系，以及 Mostrous 等人针对多方会话类型的关系。最后，通过证明核心子类型关系的两个片段是可判定的，我们表明对类型结构的进一步限制可使我们的核心子类型关系变得可判定。