I am looking for a datastructure that supports the following operations:

  1. Add a term
  2. Remove a term
  3. Return a pair of unifiable terms if one exists.

Ideally, 3 would be as close as possible to returning a pair at random rather than being biased based on e.g. the order the terms were entered.

I suspect there must be a lot of possible answers to this in the literature, so any references are appreciated, especially anything that reviews the state of the art.

I am looking for the most efficient possible (known) implementation of the above. Bonus points for supporting variations e.g. some higher-order unification

  • $\begingroup$ Maybe a variation on union-find? You'd have to be more specific about the semantics of terms and what equivalence relation they are unifiable under. $\endgroup$ Apr 8 at 5:09
  • $\begingroup$ Please clarify your specific problem or provide additional details to highlight exactly what you need. As it's currently written, it's hard to tell exactly what you're asking. $\endgroup$
    – Community Bot
    Apr 19 at 13:53


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.