中文

中心子幺半群与计算概念:可靠性、完备性与内语言

计算机科学中的逻辑 2025-10-31 v3 编程语言 范畴论

摘要

范畴论中的幺半群是可用于为编程语言中的计算效应建模的代数结构。我们展示了“中心”概念,更一般地“中心性”(即一个效应与所有其他效应可对易的性质),如何为作用于对称幺半范畴上的强幺半群所表述。我们确定了刻画强幺半群中心存在的三个等价条件(其中部分将其与 Power 和 Robinson 的预幺半中心相联系),并表明许多著名自然出现的范畴上的每个强幺半群确实都容许一个中心,从而说明这一新概念无处不在。更一般地,我们研究中心子幺半群,它们必然是可交换的,正如强幺半群的中心一样。我们通过表述配备中心子幺半群的 lambda 演算等式理论给出计算解释,描述这些理论的范畴模型,并证明我们语义的可靠性、完备性与内语言结果。

关键词

引用

@article{arxiv.2207.09190,
  title  = {Central Submonads and Notions of Computation: Soundness, Completeness and Internal Languages},
  author = {TItouan Carette and Louis Lemonnier and Vladimir Zamdzhiev},
  journal= {arXiv preprint arXiv:2207.09190},
  year   = {2025}
}

备注

Journal version of the conference paper accepted to LICS'23