Binary decision diagrams by shared rewriting

In this paper we propose a uniform description of basic BDD theory and algorithms by means of term rewriting. Since a BDD is a DAG instead of a tree we need a notion of shared rewriting and develop appropriate theory. A rewriting system is presented by which canonical forms can be obtained. Various reduction strategies give rise to different algorithms. A layerwise strategy is proposed having the same time complexity as the traditional apply- algorithm, and the lazy strategy is studied, which resembles the existing up-one-algorithm. We show that these algorithms have incomparable performance.