关于SP-范畴的字问题与双向通信的性质
计算机科学中的逻辑
2009-04-10 v1 范畴论
逻辑
摘要
具有自由积与余积（和）的范畴（即SP-范畴）的字问题，直接与确定某些过程等价性的问题相关。事实上，这些范畴中的态射可直接解释为通过双向信道通信的过程。SP-范畴的态射也可被视为一种具有博弈论解释的简单逻辑的证明论。该逻辑的消割过程仅能确定在某种置换转换下的相等性。由于这些置换转换下的等价类是有限的，因此容易看出，无割项（即使存在加法单位元）之间的相等性是可判定的。遗憾的是，这并不能产生一个易处理的判定算法，因为这些等价类可能包含指数多个项。然而，这些自由范畴（以及双向通信）相当特殊的性质，使得我们可以设计一个易处理的相等性算法。我们证明，在限制于无割项 s,t : X --> A 的情况下，判定过程在 |X||A|（定义域与余定义域类型大小的乘积）的多项式时间内运行。
引用
@article{arxiv.0904.1529,
title = {On the word problem for SP-categories, and the properties of two-way communication},
author = {Luigi Santocanale and Robin Cockett},
journal= {arXiv preprint arXiv:0904.1529},
year = {2009}
}