对数线性时间上正交可补双半格的等价性检验
On Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time
摘要：
我们提出了一个拟线性时间算法来解决自然代数结构上的字问题，我们称之为正补二半格，布尔代数的一个子理论。我们使用作为一个基地的变化Hopcroft，Ullman和Aho算法的树同构，我们结合一个长期重写系统，以决定两个条款的等价。我们证明了重写系统是可终止的和汇合的，因此存在一个范式，我们的算法是计算它。我们还讨论了应用程序，并提出了一个有效的实现在Scala中。
英文摘要：
We present a quasilinear time algorithm to decide the word problem on a natural algebraic structures we call orthocomplemented bisemilattices, a subtheory of boolean algebra. We use as a base a variation of Hopcroft, Ullman and Aho algorithm for tree isomorphism which we combine with a term rewriting system to decide equivalence of two terms. We prove that the rewriting system is terminating and confluent and hence the existence of a normal form, and that our algorithm is computing it. We also discuss applications and present an effective implementation in Scala.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
