Sharing is optimal

AbstractOne of the most popular abstract domains used for the analysis of logic programs is the domain Sharing which expresses the fact that computed substitutions bind variables to terms containing common variables. Despite the fact that this domain is widely used and studied, it is not yet known whether its abstract operations are complete or at least optimal. We solve this open question showing that the operations of lub and projection of Sharing are complete (and thus optimal), whereas that of unification is optimal, but not complete