通过余归纳的通用迹语义
计算机科学中的逻辑
2015-07-01 v2
摘要
迹语义已针对各种基于状态的系统进行了定义，特别是具有不同分支形式（如非确定性对概率）的系统。在本文中，我们声称识别出这些“迹语义”背后的一个潜在数学结构，即 Kleisli 范畴中的余归纳。这一主张基于我们的技术结果：在适当序增强的设定下，Kleisli 范畴中的终余代数由 Sets 范畴中的初始代数给出。此前，余代数理论主要在 Sets 中应用，其中余归纳产生了更精细的互模拟过程语义。因此，本文扩展了余代数的应用领域，提供了“通过余归纳的过程语义”这一原则的新实例。
引用
@article{arxiv.0710.2505,
title = {Generic Trace Semantics via Coinduction},
author = {Ichiro Hasuo and Bart Jacobs and Ana Sokolova},
journal= {arXiv preprint arXiv:0710.2505},
year = {2015}
}
评论
To appear in Logical Methods in Computer Science. 36 pages