获得并行组合的有限公理化是否需要两个二元算子？
计算机科学中的逻辑
2022-03-31 v3
摘要
Bergstra 和 Klop 已证明，在扩展有二元左合并与通信合并算子的 ACP/CCS 上，互模拟具有有限等式公理化。Moller 证明了要获得 CCS 上互模拟的有限公理化，辅助算子是必需的；Aceto 等人表明当 Hennessy 合并加入该语言时这一点仍然成立。这些结果引出了一个问题：是否存在一个辅助二元算子，将其加入 CCS 可导出互模拟的有限公理化。我们在 CCS 的无递归、无重标记、无限制片段这一简化设定下致力于回答该问题。我们 formulation 了关于辅助算子的操作语义及其与并行组合关系的三个自然假设，并证明在简化设定下促成互模拟有限公理化的辅助二元算子不能满足全部三个假设。
引用
@article{arxiv.2010.01943,
title = {Are Two Binary Operators Necessary to Obtain a Finite Axiomatisation of Parallel Composition?},
author = {Luca Aceto and Valentina Castiglioni and Wan Fokkink and Anna Igolfsdottir and Bas Luttik},
journal= {arXiv preprint arXiv:2010.01943},
year = {2022}
}