Optimal multi-binding unification for sharing and linearity analysis

TL;DR

This paper proves that the optimal abstract operator for single-binding unification in the domain inp, used for sharing and linearity analysis in logic programs, remains optimal when applied repeatedly for multi-binding unification.

Contribution

The paper provides a formal proof that the optimality of the unification operator extends from single-binding to multi-binding scenarios in the inp domain.

Findings

The unification operator is proven to be optimal for multi-binding unification.

The domain inp effectively combines sharing and linearity information.

The proof confirms the theoretical soundness of using the operator repeatedly.

Abstract

In the analysis of logic programs, abstract domains for detecting sharing properties are widely used. Recently the new domain $\Linp$ has been introduced to generalize both sharing and linearity information. This domain is endowed with an optimal abstract operator for single-binding unification. The authors claim that the repeated application of this operator is also optimal for multi-binding unification. This is the proof of such a claim.