Idempotent Joins

[svenkeidel]

The Problem

Currently, values are still joined, even if the values are identical. For example, let G be a regular tree grammar, then G ⊔ G still joins the grammar by computing G ∪ G. This is very expensive, because G ∪ G doubles the size of the grammars. We could improve this by checking if G == G it is save to return G in G ⊔ G, however this equality check is also expensive.

What would we like to be able to do

Ideally, we would like to know that G has not be touched and that G ⊔ G = G without even comparing the grammars for equality.

Possible Solutions

One possible solution is to attach to every value a unique identity, e.g., a unique number and whenever two values have the same identity, then these have to be equal.