论混合选择会话的表达能力（技术报告）
计算机科学中的逻辑
2022-08-16 v1
摘要
会话类型为结构化交互提供了灵活的编程风格，并用于保证分布式进程安全且一致的组成。传统会话类型仅包含单向输入（外部）与输出（内部）守护选择。这阻碍了会话进程探索pi演算的全部表达能力，其中已证明混合选择比（非混合）守护选择更具表达力。为解决此问题，Casal、Mordido与Vasconcelos近期提出了带混合选择的二元会话类型（CMV+）。本文给出了关于CMV+的一个令人惊讶且不巧的结果：尽管包含了带混合选择的 unrestricted 通道，CMV+的混合选择实为分离而非混合。我们使用两种方法（以领导者选举问题或同步模式作为区分特征）证明了这一负面结果，表明不存在从pi演算到CMV+且保持分布的良好编码。随后我们解决了其关于从CMV+到CMV（无混合选择）编码的开放问题，证明了其可靠性，从而该编码在耦合相似意义下是良好的。本技术报告扩展了发表于EXPRESS/SOS'22研讨会的论文。
引用
@article{arxiv.2208.07041,
title = {On the Expressiveness of Mixed Choice Sessions (Technical Report)},
author = {Kirstin Peters and Nobuko Yoshida},
journal= {arXiv preprint arXiv:2208.07041},
year = {2022}
}
备注
This technical report extends a paper presented at the workshop EXPRESS/SOS'22