On abstract unification for variable aliasing

  We face the problem of devising optimal unification operators for
  domains of abstract substitutions. In particular, we are interested
  in abstract domains for sharing and linerity properties, which are
  widely used in logic program analysis. We propose a new (infinite)
  domain ShLin^? which can be thought of as a general framework from
  which other domains can be easily derived by abstraction. The
  advantage is that abstract unification in ShLin^? is simple and
  elegant, and it is based on a new concept of sharing graph
  which plays the same role of alternating paths for pair sharing
  analysis. We also provide an alternative, purely algebraic
  description of sharing graphs.  Starting from the results for
  ShLin^?, we derive optimal abstract operators for two well-known
  domains which combine sharing and linearity: a domain proposed by Andy   King and the classic Sharing X Lin.