On Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time

TL;DR

This paper introduces a quasilinear time algorithm for equivalence checking in orthocomplemented bisemilattices, a substructure of boolean algebra, utilizing a combination of tree isomorphism techniques and term rewriting.

Contribution

It presents the first efficient algorithm for the word problem in orthocomplemented bisemilattices, proving termination and confluence of the rewriting system used.

Findings

Algorithm operates in quasilinear time.

Rewriting system is proven terminating and confluent.

Implementation in Scala demonstrates practical applicability.

Abstract

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.