高阶语言中应用双模拟同余性的范畴框架
计算机科学中的逻辑
2023-06-22 v5
摘要
应用双模拟是 call-by-name λ-演算中观测等价性的余归纳刻画,由 Abramsky (1990) 引入。Howe (1996) 给出了其为一同余的直接证明,并将该结果推广到所有符合适当格式的语言。我们提出一个用于指定操作语义的范畴框架,在其中我们证明(应用双模拟的抽象类比)自动为一同余。示例实例包括 call-by-name、call-by-value 以及 call-by-name 非确定性 -演算中的标准应用双模拟,更一般地,包括所有符合 Howe 格式变体的语言。
引用
@article{arxiv.2103.16833,
title = {A categorical framework for congruence of applicative bisimilarity in higher-order languages},
author = {Tom Hirschowitz and Ambroise Lafont},
journal= {arXiv preprint arXiv:2103.16833},
year = {2023}
}