组成重写理论的基本原理
摘要:组合范畴重写理论的基础理论被提出,基于一系列类似纤维化的属性,这些属性共同导致并且内在地构造了在并发性和结合性等定理的证明中使用的大量引理集合。结果给出了这些定理的高度通用的证明。值得注意的是,并发性定理的证明仅需几行,而结合性定理的证明虽然稍长,但如果以基本引理直接书写将会过长以至于难以阅读。实质上,我们的框架通过展示潜在的模块化性,提高了这些证明的可读性和理解效果。通过一个经过筛选的已知实例列表,结论部分详细讨论了图转换的双向排挤和半双向排挤语义在何种条件下是组合的。
作者:Nicolas Behr (Universit''e Paris Cit''e, CNRS, IRIF), Russ Harmer (Univ. Lyon, EnsL, UCBL, CNRS, LIP, France), Jean Krivine (Universit''e Paris Cit''e, CNRS, IRIF)
论文ID:2204.07175
分类:Logic in Computer Science
分类简称:cs.LO
提交时间:2023-07-17