# Unification --- removing equations and updating the solution

This question is concerned with the first order unification. Suppose I have a set $D$ of equations and a solution to these equations. Let this solution be a set $S$ of substitutions. Now, suppose I remove some equations from $D$. Is there an algorithm that just uses these removed equations and quickly updates $D$, or the unification needs to be done from scratch?

(In my application, I tend to have a lot of equations, so that is why I am interested in a solution that does not recompute everything.)

If all you have is the solution to these equations (the most general unifier for $D$), I don't know of any good algorithm for your problem that will be better than "compute the answer from scratch" in general.

However, if you are willing to save some extra information on the side while you are solving $D$, then yes there are methods to do what you want -- with some caveats. In particular, you can use a persistent union-find data structure to help. Normally, we'd use union-find for unification (to compute the solution, i.e., the most general unifier). Here the idea is to instead use a persistent union-find data structure. This provides the ability to "roll back" some of the union operations and then go forward from there.

See the following research paper:

A persistent union-find data structure. Sylvain Conchon, Jean-Christophe Filliâtre. ACM SIGPLAN Workshop on ML, 2007. See also https://www.lri.fr/~filliatr/puf/ .

Caveats: Their data structure is only semi-persistent, i.e., only partially persistent. This means you can roll back to an earlier version of the data structure and make modifications from there, but you can't do any more than that.

One consequence is that the efficiency of the above approach will depend upon the order in which you process the equations. If you want to remove a few equations that were processed near the end and then compute the new solution, this will be very efficient (with the above data structure). But if you want to remove an equation that was processed near the beginning and then compute the new solution, this will be relatively slow. In other words, suppose your equations are $D=\{D_1,\dots,D_n\}$ and you compute the solution (most general unifier) by processing the equations in the order $D_1,D_2,\dots,D_n$ (to process an equation you call the Union operation on the union-find data structure). Now suppose you want to remove equation $D_i$. With the above partially persistent union-find data structure, you can do this by rolling back the state of the union-find data structure to its state after processing $D_1,\dots,D_{i-1}$, then processing equations $D_{i+1},\dots,D_n$ starting from there. If $i$ is close to $n$, this will be efficient (it will take $n-i$ Union operations), but if $i$ is small, it won't be much better than just starting from scratch.

In principle if we had a confluently persistent union-find data structure we could remove this limitation. However, I don't personally know of any efficient confluently persistent union-find data structure. I'm not sure whether such a thing has been studied in the literature or not; this answer seems to suggest it was an open problem, at least as of 2010. (Here is a survey on confluent persistence.)