轻量化全局类型

全局会话类型可防止参与者等待永远不会到来的消息。某些交互仅仅是为了通知接收者某条消息将永远不会到达或会话已终止。通过将大型全局类型分解为多个轻量级全局类型，可以避免此类冗余交互。轻量化全局类型为我们提供了更清晰的全局类型，保留了所有必要的通信。本文提出了一种框架，能够轻松地将全局类型分解为轻量级全局类型，在去除冗余交互的同时保留原始类型的交互序列。