基于上下文无关字符串图族的等式推理
计算机科学中的逻辑
2015-10-14 v2 形式语言与自动机理论
范畴论
摘要
字符串图为以图形方式表达相互作用过程网络提供了一种直观的语言。一种称为字符串图的离散表示允许通过双推出重写进行机械化等式推理。然而，人们通常希望表达的不仅仅是单个方程，而是任意大小图表之间的整个方程族。为此，我们定义了一类称为 B-ESG 文法的上下文无关文法，它们适用于定义整个字符串图族，关键是定义字符串图重写规则。我们证明了这些文法的语言成员资格问题和匹配枚举问题是可判定的，因此存在一种根据 B-ESG 重写模式重写字符串图的算法。我们还表明，可以通过提供一种通过字符串图重写转换文法的简单方法，并证明诱导的 B-ESG 重写模式的可容许性，从而在文法层面进行推理。
引用
@article{arxiv.1504.02716,
title = {Equational reasoning with context-free families of string diagrams},
author = {Aleks Kissinger and Vladimir Zamdzhiev},
journal= {arXiv preprint arXiv:1504.02716},
year = {2015}
}
备注
International Conference on Graph Transformation, ICGT 2015. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-21145-9_9