Idempotent Joins
Closed this issue · 0 comments
svenkeidel commented
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.